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 id 
a = take r2 (len l1 - len r1) -> a = take r2 (len l1 - len r1)
2 1 appendeq2d 
a = take r2 (len l1 - len r1) -> r1 ++ a = r1 ++ take r2 (len l1 - len r1)
3 2 eqeq2d 
a = take r2 (len l1 - len r1) -> (l1 = r1 ++ a <-> l1 = r1 ++ take r2 (len l1 - len r1))
4 1 appendeq1d 
a = take r2 (len l1 - len r1) -> a ++ l2 = take r2 (len l1 - len r1) ++ l2
5 4 eqeq2d 
a = take r2 (len l1 - len r1) -> (r2 = a ++ l2 <-> r2 = take r2 (len l1 - len r1) ++ l2)
6 3, 5 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)
7 6 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)
8 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))
9 appendlen 
len (r1 ++ take r2 (len l1 - len r1)) = len r1 + len (take r2 (len l1 - len r1))
10 takelen 
len (take r2 (len l1 - len r1)) = min (len r2) (len l1 - len r1)
11 eqmin2 
len l1 - len r1 <= len r2 -> min (len r2) (len l1 - len r1) = len l1 - len r1
12 lesubadd2 
len l1 - len r1 <= len r2 <-> len l1 <= len r1 + len r2
13 leaddid1 
len l1 <= len l1 + len l2
14 appendlen 
len (l1 ++ l2) = len l1 + len l2
15 appendlen 
len (r1 ++ r2) = len r1 + len r2
16 anr 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> l1 ++ l2 = r1 ++ r2
17 16 leneqd 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> len (l1 ++ l2) = len (r1 ++ r2)
18 14, 15, 17 eqtr3g 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> len l1 + len l2 = len r1 + len r2
19 18 leeq2d 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> (len l1 <= len l1 + len l2 <-> len l1 <= len r1 + len r2)
20 13, 19 mpbii 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> len l1 <= len r1 + len r2
21 12, 20 sylibr 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> len l1 - len r1 <= len r2
22 11, 21 syl 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> min (len r2) (len l1 - len r1) = len l1 - len r1
23 10, 22 syl5eq 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> len (take r2 (len l1 - len r1)) = len l1 - len r1
24 23 addeq2d 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> len r1 + len (take r2 (len l1 - len r1)) = len r1 + (len l1 - len r1)
25 pncan3 
len r1 <= len l1 -> len r1 + (len l1 - len r1) = len l1
26 25 anwl 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> len r1 + (len l1 - len r1) = len l1
27 24, 26 eqtrd 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> len r1 + len (take r2 (len l1 - len r1)) = len l1
28 27 eqcomd 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> len l1 = len r1 + len (take r2 (len l1 - len r1))
29 9, 28 syl6eqr 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> len l1 = len (r1 ++ take r2 (len l1 - len r1))
30 8, 29 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))
31 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)
32 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
33 takedrop 
take r2 (len l1 - len r1) ++ drop r2 (len l1 - len r1) = r2
34 32, 33 ax_mp 
r1 ++ take r2 (len l1 - len r1) ++ drop r2 (len l1 - len r1) = r1 ++ r2
35 34, 16 syl6eqr 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> l1 ++ l2 = r1 ++ take r2 (len l1 - len r1) ++ drop r2 (len l1 - len r1)
36 31, 35 syl6eqr 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> l1 ++ l2 = (r1 ++ take r2 (len l1 - len r1)) ++ drop r2 (len l1 - len r1)
37 30, 36 mpbid 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> l1 = r1 ++ take r2 (len l1 - len r1) /\ l2 = drop r2 (len l1 - len r1)
38 37 anld 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> l1 = r1 ++ take r2 (len l1 - len r1)
39 37 anrd 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> l2 = drop r2 (len l1 - len r1)
40 39 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)
41 33, 40 syl6eq 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> take r2 (len l1 - len r1) ++ l2 = r2
42 41 eqcomd 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> r2 = take r2 (len l1 - len r1) ++ l2
43 38, 42 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
44 7, 43 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)