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 eqidd 
m = n -> suc (min (len l1) (len l2)) = suc (min (len l1) (len l2))
23 21, 22 lteqd 
m = n -> (m < suc (min (len l1) (len l2)) <-> n < suc (min (len l1) (len l2)))
24 eqidd 
m = n -> zip (a : l1) (b : l2) = zip (a : l1) (b : l2)
25 21, 24 ntheqd 
m = n -> nth m (zip (a : l1) (b : l2)) = nth n (zip (a : l1) (b : l2))
26 eqidd 
m = n -> (a, b) : zip l1 l2 = (a, b) : zip l1 l2
27 21, 26 ntheqd 
m = n -> nth m ((a, b) : zip l1 l2) = nth n ((a, b) : zip l1 l2)
28 25, 27 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))
29 23, 28 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))
30 id 
m = 0 -> m = 0
31 eqidd 
m = 0 -> suc (min (len l1) (len l2)) = suc (min (len l1) (len l2))
32 30, 31 lteqd 
m = 0 -> (m < suc (min (len l1) (len l2)) <-> 0 < suc (min (len l1) (len l2)))
33 eqidd 
m = 0 -> zip (a : l1) (b : l2) = zip (a : l1) (b : l2)
34 30, 33 ntheqd 
m = 0 -> nth m (zip (a : l1) (b : l2)) = nth 0 (zip (a : l1) (b : l2))
35 eqidd 
m = 0 -> (a, b) : zip l1 l2 = (a, b) : zip l1 l2
36 30, 35 ntheqd 
m = 0 -> nth m ((a, b) : zip l1 l2) = nth 0 ((a, b) : zip l1 l2)
37 34, 36 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))
38 32, 37 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))
39 id 
m = suc n -> m = suc n
40 eqidd 
m = suc n -> suc (min (len l1) (len l2)) = suc (min (len l1) (len l2))
41 39, 40 lteqd 
m = suc n -> (m < suc (min (len l1) (len l2)) <-> suc n < suc (min (len l1) (len l2)))
42 eqidd 
m = suc n -> zip (a : l1) (b : l2) = zip (a : l1) (b : l2)
43 39, 42 ntheqd 
m = suc n -> nth m (zip (a : l1) (b : l2)) = nth (suc n) (zip (a : l1) (b : l2))
44 eqidd 
m = suc n -> (a, b) : zip l1 l2 = (a, b) : zip l1 l2
45 39, 44 ntheqd 
m = suc n -> nth m ((a, b) : zip l1 l2) = nth (suc n) ((a, b) : zip l1 l2)
46 43, 45 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))
47 41, 46 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))
48 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)
49 nthZ 
nth 0 (a : l1) = suc a
50 49 a1i 
T. -> nth 0 (a : l1) = suc a
51 nthZ 
nth 0 (b : l2) = suc b
52 51 a1i 
T. -> nth 0 (b : l2) = suc b
53 50, 52 zipnth 
T. -> nth 0 (zip (a : l1) (b : l2)) = suc (a, b)
54 53 trud 
nth 0 (zip (a : l1) (b : l2)) = suc (a, b)
55 48, 54 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)
56 nthZ 
nth 0 ((a, b) : zip l1 l2) = suc (a, b)
57 55, 56 ax_mp 
nth 0 (zip (a : l1) (b : l2)) = nth 0 ((a, b) : zip l1 l2)
58 57 a1i 
0 < suc (min (len l1) (len l2)) -> nth 0 (zip (a : l1) (b : l2)) = nth 0 ((a, b) : zip l1 l2)
59 ltsuc 
n < min (len l1) (len l2) <-> suc n < suc (min (len l1) (len l2))
60 nthS 
nth (suc n) ((a, b) : zip l1 l2) = nth n (zip l1 l2)
61 ltmin 
n < min (len l1) (len l2) <-> n < len l1 /\ n < len l2
62 nthS 
nth (suc n) (a : l1) = nth n l1
63 sub1can 
nth n l1 != 0 -> suc (nth n l1 - 1) = nth n l1
64 nthne0 
nth n l1 != 0 <-> n < len l1
65 anl 
n < len l1 /\ n < len l2 -> n < len l1
66 64, 65 sylibr 
n < len l1 /\ n < len l2 -> nth n l1 != 0
67 63, 66 syl 
n < len l1 /\ n < len l2 -> suc (nth n l1 - 1) = nth n l1
68 67 eqcomd 
n < len l1 /\ n < len l2 -> nth n l1 = suc (nth n l1 - 1)
69 62, 68 syl5eq 
n < len l1 /\ n < len l2 -> nth (suc n) (a : l1) = suc (nth n l1 - 1)
70 nthS 
nth (suc n) (b : l2) = nth n l2
71 sub1can 
nth n l2 != 0 -> suc (nth n l2 - 1) = nth n l2
72 nthne0 
nth n l2 != 0 <-> n < len l2
73 anr 
n < len l1 /\ n < len l2 -> n < len l2
74 72, 73 sylibr 
n < len l1 /\ n < len l2 -> nth n l2 != 0
75 71, 74 syl 
n < len l1 /\ n < len l2 -> suc (nth n l2 - 1) = nth n l2
76 75 eqcomd 
n < len l1 /\ n < len l2 -> nth n l2 = suc (nth n l2 - 1)
77 70, 76 syl5eq 
n < len l1 /\ n < len l2 -> nth (suc n) (b : l2) = suc (nth n l2 - 1)
78 69, 77 zipnth 
n < len l1 /\ n < len l2 -> nth (suc n) (zip (a : l1) (b : l2)) = suc (nth n l1 - 1, nth n l2 - 1)
79 68, 76 zipnth 
n < len l1 /\ n < len l2 -> nth n (zip l1 l2) = suc (nth n l1 - 1, nth n l2 - 1)
80 78, 79 eqtr4d 
n < len l1 /\ n < len l2 -> nth (suc n) (zip (a : l1) (b : l2)) = nth n (zip l1 l2)
81 61, 80 sylbi 
n < min (len l1) (len l2) -> nth (suc n) (zip (a : l1) (b : l2)) = nth n (zip l1 l2)
82 60, 81 syl6eqr 
n < min (len l1) (len l2) -> nth (suc n) (zip (a : l1) (b : l2)) = nth (suc n) ((a, b) : zip l1 l2)
83 59, 82 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)
84 83 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)
85 29, 38, 29, 47, 58, 84 ind 
n < suc (min (len l1) (len l2)) -> nth n (zip (a : l1) (b : l2)) = nth n ((a, b) : zip l1 l2)
86 13, 20, 85 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)