Theorem sublistAt_append ≪ | index | src | ≫ 

theorem sublistAt_append (l l1 l2 n: nat):
  $ sublistAt n l (l1 ++ l2) <->
    sublistAt n l l1 /\ sublistAt (n + len l1) l l2 $;
StepHypRefExpression
1 bitr4 
(E. b (l = a ++ (l1 ++ l2) ++ b /\ len a = n) <-> E. b (E. b2 (l = a ++ l1 ++ b2 /\ len a = n) /\ E. a1 (l = a1 ++ l2 ++ b /\ len a1 = n + len l1))) ->
  (E. b2 (l = a ++ l1 ++ b2 /\ len a = n) /\ sublistAt (n + len l1) l l2 <->
    E. b (E. b2 (l = a ++ l1 ++ b2 /\ len a = n) /\ E. a1 (l = a1 ++ l2 ++ b /\ len a1 = n + len l1))) ->
  (E. b (l = a ++ (l1 ++ l2) ++ b /\ len a = n) <-> E. b2 (l = a ++ l1 ++ b2 /\ len a = n) /\ sublistAt (n + len l1) l l2)
2 bitr2 
(E. b (E. b2 (l = a ++ l1 ++ b2 /\ len a = n) /\ E. a1 (l = a1 ++ l2 ++ b /\ len a1 = n + len l1)) <->
    E. b (E. b2 l = a ++ l1 ++ b2 /\ E. a1 (l = a1 ++ l2 ++ b /\ len a1 = n + len l1)) /\ len a = n) ->
  (E. b (E. b2 l = a ++ l1 ++ b2 /\ E. a1 (l = a1 ++ l2 ++ b /\ len a1 = n + len l1)) /\ len a = n <-> E. b (l = a ++ (l1 ++ l2) ++ b /\ len a = n)) ->
  (E. b (l = a ++ (l1 ++ l2) ++ b /\ len a = n) <-> E. b (E. b2 (l = a ++ l1 ++ b2 /\ len a = n) /\ E. a1 (l = a1 ++ l2 ++ b /\ len a1 = n + len l1)))
3 exan2 
E. b2 (l = a ++ l1 ++ b2 /\ len a = n) <-> E. b2 l = a ++ l1 ++ b2 /\ len a = n
4 3 bian21i 
E. b2 (l = a ++ l1 ++ b2 /\ len a = n) /\ E. a1 (l = a1 ++ l2 ++ b /\ len a1 = n + len l1) <->
  E. b2 l = a ++ l1 ++ b2 /\ E. a1 (l = a1 ++ l2 ++ b /\ len a1 = n + len l1) /\ len a = n
5 4 bian2exi 
E. b (E. b2 (l = a ++ l1 ++ b2 /\ len a = n) /\ E. a1 (l = a1 ++ l2 ++ b /\ len a1 = n + len l1)) <->
  E. b (E. b2 l = a ++ l1 ++ b2 /\ E. a1 (l = a1 ++ l2 ++ b /\ len a1 = n + len l1)) /\ len a = n
6 2, 5 ax_mp 
(E. b (E. b2 l = a ++ l1 ++ b2 /\ E. a1 (l = a1 ++ l2 ++ b /\ len a1 = n + len l1)) /\ len a = n <-> E. b (l = a ++ (l1 ++ l2) ++ b /\ len a = n)) ->
  (E. b (l = a ++ (l1 ++ l2) ++ b /\ len a = n) <-> E. b (E. b2 (l = a ++ l1 ++ b2 /\ len a = n) /\ E. a1 (l = a1 ++ l2 ++ b /\ len a1 = n + len l1)))
7 appendass 
(l1 ++ l2) ++ b = l1 ++ l2 ++ b
8 appendeq2 
b2 = l2 ++ b -> l1 ++ b2 = l1 ++ l2 ++ b
9 7, 8 syl6eqr 
b2 = l2 ++ b -> l1 ++ b2 = (l1 ++ l2) ++ b
10 9 appendeq2d 
b2 = l2 ++ b -> a ++ l1 ++ b2 = a ++ (l1 ++ l2) ++ b
11 10 eqeq2d 
b2 = l2 ++ b -> (l = a ++ l1 ++ b2 <-> l = a ++ (l1 ++ l2) ++ b)
12 11 exeqe 
E. b2 (b2 = l2 ++ b /\ l = a ++ l1 ++ b2) <-> l = a ++ (l1 ++ l2) ++ b
13 exan2 
E. b2 (l = a ++ l1 ++ b2 /\ E. a1 (l = a1 ++ l2 ++ b /\ len a1 = n + len l1)) <-> E. b2 l = a ++ l1 ++ b2 /\ E. a1 (l = a1 ++ l2 ++ b /\ len a1 = n + len l1)
14 ancomb 
l = a ++ l1 ++ b2 /\ b2 = l2 ++ b <-> b2 = l2 ++ b /\ l = a ++ l1 ++ b2
15 addcan1 
len a + len l1 = n + len l1 <-> len a = n
16 appendlen 
len (a ++ l1) = len a + len l1
17 leneq 
a1 = a ++ l1 -> len a1 = len (a ++ l1)
18 16, 17 syl6eq 
a1 = a ++ l1 -> len a1 = len a + len l1
19 18 eqeq1d 
a1 = a ++ l1 -> (len a1 = n + len l1 <-> len a + len l1 = n + len l1)
20 15, 19 syl6bb 
a1 = a ++ l1 -> (len a1 = n + len l1 <-> len a = n)
21 20 aneq2d 
a1 = a ++ l1 -> (b2 = l2 ++ b /\ len a1 = n + len l1 <-> b2 = l2 ++ b /\ len a = n)
22 21 exeqe 
E. a1 (a1 = a ++ l1 /\ (b2 = l2 ++ b /\ len a1 = n + len l1)) <-> b2 = l2 ++ b /\ len a = n
23 eqcomb 
a ++ l1 = a1 <-> a1 = a ++ l1
24 23 aneq1i 
a ++ l1 = a1 /\ (b2 = l2 ++ b /\ len a1 = n + len l1) <-> a1 = a ++ l1 /\ (b2 = l2 ++ b /\ len a1 = n + len l1)
25 appendass 
(a ++ l1) ++ b2 = a ++ l1 ++ b2
26 anlr 
len a = n /\ l = a ++ l1 ++ b2 /\ len a1 = n + len l1 -> l = a ++ l1 ++ b2
27 25, 26 syl6eqr 
len a = n /\ l = a ++ l1 ++ b2 /\ len a1 = n + len l1 -> l = (a ++ l1) ++ b2
28 27 eqeq1d 
len a = n /\ l = a ++ l1 ++ b2 /\ len a1 = n + len l1 -> (l = a1 ++ l2 ++ b <-> (a ++ l1) ++ b2 = a1 ++ l2 ++ b)
29 appendinj1 
len (a ++ l1) = len a1 -> ((a ++ l1) ++ b2 = a1 ++ l2 ++ b <-> a ++ l1 = a1 /\ b2 = l2 ++ b)
30 anll 
len a = n /\ l = a ++ l1 ++ b2 /\ len a1 = n + len l1 -> len a = n
31 30 addeq1d 
len a = n /\ l = a ++ l1 ++ b2 /\ len a1 = n + len l1 -> len a + len l1 = n + len l1
32 anr 
len a = n /\ l = a ++ l1 ++ b2 /\ len a1 = n + len l1 -> len a1 = n + len l1
33 31, 32 eqtr4d 
len a = n /\ l = a ++ l1 ++ b2 /\ len a1 = n + len l1 -> len a + len l1 = len a1
34 16, 33 syl5eq 
len a = n /\ l = a ++ l1 ++ b2 /\ len a1 = n + len l1 -> len (a ++ l1) = len a1
35 29, 34 syl 
len a = n /\ l = a ++ l1 ++ b2 /\ len a1 = n + len l1 -> ((a ++ l1) ++ b2 = a1 ++ l2 ++ b <-> a ++ l1 = a1 /\ b2 = l2 ++ b)
36 28, 35 bitrd 
len a = n /\ l = a ++ l1 ++ b2 /\ len a1 = n + len l1 -> (l = a1 ++ l2 ++ b <-> a ++ l1 = a1 /\ b2 = l2 ++ b)
37 36 bian11da 
len a = n /\ l = a ++ l1 ++ b2 -> (l = a1 ++ l2 ++ b /\ len a1 = n + len l1 <-> a ++ l1 = a1 /\ (b2 = l2 ++ b /\ len a1 = n + len l1))
38 24, 37 syl6bb 
len a = n /\ l = a ++ l1 ++ b2 -> (l = a1 ++ l2 ++ b /\ len a1 = n + len l1 <-> a1 = a ++ l1 /\ (b2 = l2 ++ b /\ len a1 = n + len l1))
39 38 exeqd 
len a = n /\ l = a ++ l1 ++ b2 -> (E. a1 (l = a1 ++ l2 ++ b /\ len a1 = n + len l1) <-> E. a1 (a1 = a ++ l1 /\ (b2 = l2 ++ b /\ len a1 = n + len l1)))
40 22, 39 syl6bb 
len a = n /\ l = a ++ l1 ++ b2 -> (E. a1 (l = a1 ++ l2 ++ b /\ len a1 = n + len l1) <-> b2 = l2 ++ b /\ len a = n)
41 bian2 
len a = n -> (b2 = l2 ++ b /\ len a = n <-> b2 = l2 ++ b)
42 41 anwl 
len a = n /\ l = a ++ l1 ++ b2 -> (b2 = l2 ++ b /\ len a = n <-> b2 = l2 ++ b)
43 40, 42 bitrd 
len a = n /\ l = a ++ l1 ++ b2 -> (E. a1 (l = a1 ++ l2 ++ b /\ len a1 = n + len l1) <-> b2 = l2 ++ b)
44 43 aneq2da 
len a = n -> (l = a ++ l1 ++ b2 /\ E. a1 (l = a1 ++ l2 ++ b /\ len a1 = n + len l1) <-> l = a ++ l1 ++ b2 /\ b2 = l2 ++ b)
45 14, 44 syl6bb 
len a = n -> (l = a ++ l1 ++ b2 /\ E. a1 (l = a1 ++ l2 ++ b /\ len a1 = n + len l1) <-> b2 = l2 ++ b /\ l = a ++ l1 ++ b2)
46 45 exeqd 
len a = n -> (E. b2 (l = a ++ l1 ++ b2 /\ E. a1 (l = a1 ++ l2 ++ b /\ len a1 = n + len l1)) <-> E. b2 (b2 = l2 ++ b /\ l = a ++ l1 ++ b2))
47 13, 46 syl5bbr 
len a = n -> (E. b2 l = a ++ l1 ++ b2 /\ E. a1 (l = a1 ++ l2 ++ b /\ len a1 = n + len l1) <-> E. b2 (b2 = l2 ++ b /\ l = a ++ l1 ++ b2))
48 12, 47 syl6bb 
len a = n -> (E. b2 l = a ++ l1 ++ b2 /\ E. a1 (l = a1 ++ l2 ++ b /\ len a1 = n + len l1) <-> l = a ++ (l1 ++ l2) ++ b)
49 48 exeqd 
len a = n -> (E. b (E. b2 l = a ++ l1 ++ b2 /\ E. a1 (l = a1 ++ l2 ++ b /\ len a1 = n + len l1)) <-> E. b l = a ++ (l1 ++ l2) ++ b)
50 49 biexan1a 
E. b (E. b2 l = a ++ l1 ++ b2 /\ E. a1 (l = a1 ++ l2 ++ b /\ len a1 = n + len l1)) /\ len a = n <-> E. b (l = a ++ (l1 ++ l2) ++ b /\ len a = n)
51 6, 50 ax_mp 
E. b (l = a ++ (l1 ++ l2) ++ b /\ len a = n) <-> E. b (E. b2 (l = a ++ l1 ++ b2 /\ len a = n) /\ E. a1 (l = a1 ++ l2 ++ b /\ len a1 = n + len l1))
52 1, 51 ax_mp 
(E. b2 (l = a ++ l1 ++ b2 /\ len a = n) /\ sublistAt (n + len l1) l l2 <->
    E. b (E. b2 (l = a ++ l1 ++ b2 /\ len a = n) /\ E. a1 (l = a1 ++ l2 ++ b /\ len a1 = n + len l1))) ->
  (E. b (l = a ++ (l1 ++ l2) ++ b /\ len a = n) <-> E. b2 (l = a ++ l1 ++ b2 /\ len a = n) /\ sublistAt (n + len l1) l l2)
53 excomb 
E. a1 E. b (l = a1 ++ l2 ++ b /\ len a1 = n + len l1) <-> E. b E. a1 (l = a1 ++ l2 ++ b /\ len a1 = n + len l1)
54 53 conv sublistAt 
sublistAt (n + len l1) l l2 <-> E. b E. a1 (l = a1 ++ l2 ++ b /\ len a1 = n + len l1)
55 54 biexan2i 
E. b2 (l = a ++ l1 ++ b2 /\ len a = n) /\ sublistAt (n + len l1) l l2 <->
  E. b (E. b2 (l = a ++ l1 ++ b2 /\ len a = n) /\ E. a1 (l = a1 ++ l2 ++ b /\ len a1 = n + len l1))
56 52, 55 ax_mp 
E. b (l = a ++ (l1 ++ l2) ++ b /\ len a = n) <-> E. b2 (l = a ++ l1 ++ b2 /\ len a = n) /\ sublistAt (n + len l1) l l2
57 56 bian2exi 
E. a E. b (l = a ++ (l1 ++ l2) ++ b /\ len a = n) <-> E. a E. b2 (l = a ++ l1 ++ b2 /\ len a = n) /\ sublistAt (n + len l1) l l2
58 57 conv sublistAt 
sublistAt n l (l1 ++ l2) <-> sublistAt n l l1 /\ sublistAt (n + len l1) l 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)