Theorem zipS ≪ | index | src | ≫ 

theorem zipS (a b l1 l2: nat): $ zip (a : l1) (b : l2) = (a, b) : zip l1 l2 $;
StepHypRefExpression
1 eqtr 
len (zip (a : l1) (b : l2)) = min (len (a : l1)) (len (b : l2)) ->
  min (len (a : l1)) (len (b : l2)) = suc (min (len l1) (len l2)) ->
  len (zip (a : l1) (b : l2)) = suc (min (len l1) (len l2))
2 ziplen 
len (zip (a : l1) (b : l2)) = min (len (a : l1)) (len (b : l2))
3 1, 2 ax_mp 
min (len (a : l1)) (len (b : l2)) = suc (min (len l1) (len l2)) -> len (zip (a : l1) (b : l2)) = suc (min (len l1) (len l2))
4 eqtr4 
min (len (a : l1)) (len (b : l2)) = min (suc (len l1)) (suc (len l2)) ->
  suc (min (len l1) (len l2)) = min (suc (len l1)) (suc (len l2)) ->
  min (len (a : l1)) (len (b : l2)) = suc (min (len l1) (len l2))
5 mineq 
len (a : l1) = suc (len l1) -> len (b : l2) = suc (len l2) -> min (len (a : l1)) (len (b : l2)) = min (suc (len l1)) (suc (len l2))
6 lenS 
len (a : l1) = suc (len l1)
7 5, 6 ax_mp 
len (b : l2) = suc (len l2) -> min (len (a : l1)) (len (b : l2)) = min (suc (len l1)) (suc (len l2))
8 lenS 
len (b : l2) = suc (len l2)
9 7, 8 ax_mp 
min (len (a : l1)) (len (b : l2)) = min (suc (len l1)) (suc (len l2))
10 4, 9 ax_mp 
suc (min (len l1) (len l2)) = min (suc (len l1)) (suc (len l2)) -> min (len (a : l1)) (len (b : l2)) = suc (min (len l1) (len l2))
11 minS 
suc (min (len l1) (len l2)) = min (suc (len l1)) (suc (len l2))
12 10, 11 ax_mp 
min (len (a : l1)) (len (b : l2)) = suc (min (len l1) (len l2))
13 3, 12 ax_mp 
len (zip (a : l1) (b : l2)) = suc (min (len l1) (len l2))
14 eqtr 
len ((a, b) : zip l1 l2) = suc (len (zip l1 l2)) ->
  suc (len (zip l1 l2)) = suc (min (len l1) (len l2)) ->
  len ((a, b) : zip l1 l2) = suc (min (len l1) (len l2))
15 lenS 
len ((a, b) : zip l1 l2) = suc (len (zip l1 l2))
16 14, 15 ax_mp 
suc (len (zip l1 l2)) = suc (min (len l1) (len l2)) -> len ((a, b) : zip l1 l2) = suc (min (len l1) (len l2))
17 suceq 
len (zip l1 l2) = min (len l1) (len l2) -> suc (len (zip l1 l2)) = suc (min (len l1) (len l2))
18 ziplen 
len (zip l1 l2) = min (len l1) (len l2)
19 17, 18 ax_mp 
suc (len (zip l1 l2)) = suc (min (len l1) (len l2))
20 16, 19 ax_mp 
len ((a, b) : zip l1 l2) = suc (min (len l1) (len l2))
21 id 
m = n -> m = n
22 21 lteq1d 
m = n -> (m < suc (min (len l1) (len l2)) <-> n < suc (min (len l1) (len l2)))
23 21 ntheq1d 
m = n -> nth m (zip (a : l1) (b : l2)) = nth n (zip (a : l1) (b : l2))
24 21 ntheq1d 
m = n -> nth m ((a, b) : zip l1 l2) = nth n ((a, b) : zip l1 l2)
25 23, 24 eqeqd 
m = n -> (nth m (zip (a : l1) (b : l2)) = nth m ((a, b) : zip l1 l2) <-> nth n (zip (a : l1) (b : l2)) = nth n ((a, b) : zip l1 l2))
26 22, 25 imeqd 
m = n ->
  (m < suc (min (len l1) (len l2)) -> nth m (zip (a : l1) (b : l2)) = nth m ((a, b) : zip l1 l2) <->
    n < suc (min (len l1) (len l2)) -> nth n (zip (a : l1) (b : l2)) = nth n ((a, b) : zip l1 l2))
27 id 
m = 0 -> m = 0
28 27 lteq1d 
m = 0 -> (m < suc (min (len l1) (len l2)) <-> 0 < suc (min (len l1) (len l2)))
29 27 ntheq1d 
m = 0 -> nth m (zip (a : l1) (b : l2)) = nth 0 (zip (a : l1) (b : l2))
30 27 ntheq1d 
m = 0 -> nth m ((a, b) : zip l1 l2) = nth 0 ((a, b) : zip l1 l2)
31 29, 30 eqeqd 
m = 0 -> (nth m (zip (a : l1) (b : l2)) = nth m ((a, b) : zip l1 l2) <-> nth 0 (zip (a : l1) (b : l2)) = nth 0 ((a, b) : zip l1 l2))
32 28, 31 imeqd 
m = 0 ->
  (m < suc (min (len l1) (len l2)) -> nth m (zip (a : l1) (b : l2)) = nth m ((a, b) : zip l1 l2) <->
    0 < suc (min (len l1) (len l2)) -> nth 0 (zip (a : l1) (b : l2)) = nth 0 ((a, b) : zip l1 l2))
33 id 
m = suc n -> m = suc n
34 33 lteq1d 
m = suc n -> (m < suc (min (len l1) (len l2)) <-> suc n < suc (min (len l1) (len l2)))
35 33 ntheq1d 
m = suc n -> nth m (zip (a : l1) (b : l2)) = nth (suc n) (zip (a : l1) (b : l2))
36 33 ntheq1d 
m = suc n -> nth m ((a, b) : zip l1 l2) = nth (suc n) ((a, b) : zip l1 l2)
37 35, 36 eqeqd 
m = suc n -> (nth m (zip (a : l1) (b : l2)) = nth m ((a, b) : zip l1 l2) <-> nth (suc n) (zip (a : l1) (b : l2)) = nth (suc n) ((a, b) : zip l1 l2))
38 34, 37 imeqd 
m = suc n ->
  (m < suc (min (len l1) (len l2)) -> nth m (zip (a : l1) (b : l2)) = nth m ((a, b) : zip l1 l2) <->
    suc n < suc (min (len l1) (len l2)) -> nth (suc n) (zip (a : l1) (b : l2)) = nth (suc n) ((a, b) : zip l1 l2))
39 eqtr4 
nth 0 (zip (a : l1) (b : l2)) = suc (a, b) -> nth 0 ((a, b) : zip l1 l2) = suc (a, b) -> nth 0 (zip (a : l1) (b : l2)) = nth 0 ((a, b) : zip l1 l2)
40 nthZ 
nth 0 (a : l1) = suc a
41 40 a1i 
T. -> nth 0 (a : l1) = suc a
42 nthZ 
nth 0 (b : l2) = suc b
43 42 a1i 
T. -> nth 0 (b : l2) = suc b
44 41, 43 zipnth 
T. -> nth 0 (zip (a : l1) (b : l2)) = suc (a, b)
45 44 trud 
nth 0 (zip (a : l1) (b : l2)) = suc (a, b)
46 39, 45 ax_mp 
nth 0 ((a, b) : zip l1 l2) = suc (a, b) -> nth 0 (zip (a : l1) (b : l2)) = nth 0 ((a, b) : zip l1 l2)
47 nthZ 
nth 0 ((a, b) : zip l1 l2) = suc (a, b)
48 46, 47 ax_mp 
nth 0 (zip (a : l1) (b : l2)) = nth 0 ((a, b) : zip l1 l2)
49 48 a1i 
0 < suc (min (len l1) (len l2)) -> nth 0 (zip (a : l1) (b : l2)) = nth 0 ((a, b) : zip l1 l2)
50 ltsuc 
n < min (len l1) (len l2) <-> suc n < suc (min (len l1) (len l2))
51 nthS 
nth (suc n) ((a, b) : zip l1 l2) = nth n (zip l1 l2)
52 ltmin 
n < min (len l1) (len l2) <-> n < len l1 /\ n < len l2
53 nthS 
nth (suc n) (a : l1) = nth n l1
54 sub1can 
nth n l1 != 0 -> suc (nth n l1 - 1) = nth n l1
55 nthne0 
nth n l1 != 0 <-> n < len l1
56 anl 
n < len l1 /\ n < len l2 -> n < len l1
57 55, 56 sylibr 
n < len l1 /\ n < len l2 -> nth n l1 != 0
58 54, 57 syl 
n < len l1 /\ n < len l2 -> suc (nth n l1 - 1) = nth n l1
59 58 eqcomd 
n < len l1 /\ n < len l2 -> nth n l1 = suc (nth n l1 - 1)
60 53, 59 syl5eq 
n < len l1 /\ n < len l2 -> nth (suc n) (a : l1) = suc (nth n l1 - 1)
61 nthS 
nth (suc n) (b : l2) = nth n l2
62 sub1can 
nth n l2 != 0 -> suc (nth n l2 - 1) = nth n l2
63 nthne0 
nth n l2 != 0 <-> n < len l2
64 anr 
n < len l1 /\ n < len l2 -> n < len l2
65 63, 64 sylibr 
n < len l1 /\ n < len l2 -> nth n l2 != 0
66 62, 65 syl 
n < len l1 /\ n < len l2 -> suc (nth n l2 - 1) = nth n l2
67 66 eqcomd 
n < len l1 /\ n < len l2 -> nth n l2 = suc (nth n l2 - 1)
68 61, 67 syl5eq 
n < len l1 /\ n < len l2 -> nth (suc n) (b : l2) = suc (nth n l2 - 1)
69 60, 68 zipnth 
n < len l1 /\ n < len l2 -> nth (suc n) (zip (a : l1) (b : l2)) = suc (nth n l1 - 1, nth n l2 - 1)
70 59, 67 zipnth 
n < len l1 /\ n < len l2 -> nth n (zip l1 l2) = suc (nth n l1 - 1, nth n l2 - 1)
71 69, 70 eqtr4d 
n < len l1 /\ n < len l2 -> nth (suc n) (zip (a : l1) (b : l2)) = nth n (zip l1 l2)
72 52, 71 sylbi 
n < min (len l1) (len l2) -> nth (suc n) (zip (a : l1) (b : l2)) = nth n (zip l1 l2)
73 51, 72 syl6eqr 
n < min (len l1) (len l2) -> nth (suc n) (zip (a : l1) (b : l2)) = nth (suc n) ((a, b) : zip l1 l2)
74 50, 73 sylbir 
suc n < suc (min (len l1) (len l2)) -> nth (suc n) (zip (a : l1) (b : l2)) = nth (suc n) ((a, b) : zip l1 l2)
75 74 a1i 
(n < suc (min (len l1) (len l2)) -> nth n (zip (a : l1) (b : l2)) = nth n ((a, b) : zip l1 l2)) ->
  suc n < suc (min (len l1) (len l2)) ->
  nth (suc n) (zip (a : l1) (b : l2)) = nth (suc n) ((a, b) : zip l1 l2)
76 26, 32, 26, 38, 49, 75 ind 
n < suc (min (len l1) (len l2)) -> nth n (zip (a : l1) (b : l2)) = nth n ((a, b) : zip l1 l2)
77 13, 20, 76 nthext2 
zip (a : l1) (b : l2) = (a, b) : zip l1 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)