Theorem eqappendlem ≪ | index | src | ≫ 

theorem eqappendlem {a: nat} (l1 l2 r1 r2: nat):
  $ len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 ->
    E. a (l1 = r1 ++ a /\ r2 = a ++ l2) $;
StepHypRefExpression
1 eqidd 
a = take r2 (len l1 - len r1) -> l1 = l1
2 eqidd 
a = take r2 (len l1 - len r1) -> r1 = r1
3 id 
a = take r2 (len l1 - len r1) -> a = take r2 (len l1 - len r1)
4 2, 3 appendeqd 
a = take r2 (len l1 - len r1) -> r1 ++ a = r1 ++ take r2 (len l1 - len r1)
5 1, 4 eqeqd 
a = take r2 (len l1 - len r1) -> (l1 = r1 ++ a <-> l1 = r1 ++ take r2 (len l1 - len r1))
6 eqidd 
a = take r2 (len l1 - len r1) -> r2 = r2
7 eqidd 
a = take r2 (len l1 - len r1) -> l2 = l2
8 3, 7 appendeqd 
a = take r2 (len l1 - len r1) -> a ++ l2 = take r2 (len l1 - len r1) ++ l2
9 6, 8 eqeqd 
a = take r2 (len l1 - len r1) -> (r2 = a ++ l2 <-> r2 = take r2 (len l1 - len r1) ++ l2)
10 5, 9 aneqd 
a = take r2 (len l1 - len r1) -> (l1 = r1 ++ a /\ r2 = a ++ l2 <-> l1 = r1 ++ take r2 (len l1 - len r1) /\ r2 = take r2 (len l1 - len r1) ++ l2)
11 10 iexe 
l1 = r1 ++ take r2 (len l1 - len r1) /\ r2 = take r2 (len l1 - len r1) ++ l2 -> E. a (l1 = r1 ++ a /\ r2 = a ++ l2)
12 appendinj1 
len l1 = len (r1 ++ take r2 (len l1 - len r1)) ->
  (l1 ++ l2 = (r1 ++ take r2 (len l1 - len r1)) ++ drop r2 (len l1 - len r1) <-> l1 = r1 ++ take r2 (len l1 - len r1) /\ l2 = drop r2 (len l1 - len r1))
13 appendlen 
len (r1 ++ take r2 (len l1 - len r1)) = len r1 + len (take r2 (len l1 - len r1))
14 takelen 
len (take r2 (len l1 - len r1)) = min (len r2) (len l1 - len r1)
15 eqmin2 
len l1 - len r1 <= len r2 -> min (len r2) (len l1 - len r1) = len l1 - len r1
16 lesubadd2 
len l1 - len r1 <= len r2 <-> len l1 <= len r1 + len r2
17 leaddid1 
len l1 <= len l1 + len l2
18 appendlen 
len (l1 ++ l2) = len l1 + len l2
19 appendlen 
len (r1 ++ r2) = len r1 + len r2
20 anr 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> l1 ++ l2 = r1 ++ r2
21 20 leneqd 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> len (l1 ++ l2) = len (r1 ++ r2)
22 18, 19, 21 eqtr3g 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> len l1 + len l2 = len r1 + len r2
23 22 leeq2d 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> (len l1 <= len l1 + len l2 <-> len l1 <= len r1 + len r2)
24 17, 23 mpbii 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> len l1 <= len r1 + len r2
25 16, 24 sylibr 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> len l1 - len r1 <= len r2
26 15, 25 syl 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> min (len r2) (len l1 - len r1) = len l1 - len r1
27 14, 26 syl5eq 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> len (take r2 (len l1 - len r1)) = len l1 - len r1
28 27 addeq2d 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> len r1 + len (take r2 (len l1 - len r1)) = len r1 + (len l1 - len r1)
29 pncan3 
len r1 <= len l1 -> len r1 + (len l1 - len r1) = len l1
30 29 anwl 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> len r1 + (len l1 - len r1) = len l1
31 28, 30 eqtrd 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> len r1 + len (take r2 (len l1 - len r1)) = len l1
32 31 eqcomd 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> len l1 = len r1 + len (take r2 (len l1 - len r1))
33 13, 32 syl6eqr 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> len l1 = len (r1 ++ take r2 (len l1 - len r1))
34 12, 33 syl 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 ->
  (l1 ++ l2 = (r1 ++ take r2 (len l1 - len r1)) ++ drop r2 (len l1 - len r1) <-> l1 = r1 ++ take r2 (len l1 - len r1) /\ l2 = drop r2 (len l1 - len r1))
35 appendass 
(r1 ++ take r2 (len l1 - len r1)) ++ drop r2 (len l1 - len r1) = r1 ++ take r2 (len l1 - len r1) ++ drop r2 (len l1 - len r1)
36 appendeq2 
take r2 (len l1 - len r1) ++ drop r2 (len l1 - len r1) = r2 -> r1 ++ take r2 (len l1 - len r1) ++ drop r2 (len l1 - len r1) = r1 ++ r2
37 takedrop 
take r2 (len l1 - len r1) ++ drop r2 (len l1 - len r1) = r2
38 36, 37 ax_mp 
r1 ++ take r2 (len l1 - len r1) ++ drop r2 (len l1 - len r1) = r1 ++ r2
39 38, 20 syl6eqr 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> l1 ++ l2 = r1 ++ take r2 (len l1 - len r1) ++ drop r2 (len l1 - len r1)
40 35, 39 syl6eqr 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> l1 ++ l2 = (r1 ++ take r2 (len l1 - len r1)) ++ drop r2 (len l1 - len r1)
41 34, 40 mpbid 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> l1 = r1 ++ take r2 (len l1 - len r1) /\ l2 = drop r2 (len l1 - len r1)
42 41 anld 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> l1 = r1 ++ take r2 (len l1 - len r1)
43 41 anrd 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> l2 = drop r2 (len l1 - len r1)
44 43 appendeq2d 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> take r2 (len l1 - len r1) ++ l2 = take r2 (len l1 - len r1) ++ drop r2 (len l1 - len r1)
45 37, 44 syl6eq 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> take r2 (len l1 - len r1) ++ l2 = r2
46 45 eqcomd 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> r2 = take r2 (len l1 - len r1) ++ l2
47 42, 46 iand 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> l1 = r1 ++ take r2 (len l1 - len r1) /\ r2 = take r2 (len l1 - len r1) ++ l2
48 11, 47 syl 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> E. a (l1 = r1 ++ a /\ r2 = a ++ l2)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)