Theorem zipnth ≪ | index | src | ≫ 

theorem zipnth (G: wff) (a b i l1 l2: nat):
  $ G -> nth i l1 = suc a $ >
  $ G -> nth i l2 = suc b $ >
  $ G -> nth i (zip l1 l2) = suc (a, b) $;
StepHypRefExpression
1 nthlfn 
i < min (len l1) (len l2) -> nth i (lfn (\ x, nth x l1 - 1, nth x l2 - 1) (min (len l1) (len l2))) = suc ((\ x, nth x l1 - 1, nth x l2 - 1) @ i)
2 1 conv zip 
i < min (len l1) (len l2) -> nth i (zip l1 l2) = suc ((\ x, nth x l1 - 1, nth x l2 - 1) @ i)
3 ltmin 
i < min (len l1) (len l2) <-> i < len l1 /\ i < len l2
4 nthne0 
nth i l1 != 0 <-> i < len l1
5 sucne0 
nth i l1 = suc a -> nth i l1 != 0
6 hyp h1 
G -> nth i l1 = suc a
7 5, 6 syl 
G -> nth i l1 != 0
8 4, 7 sylib 
G -> i < len l1
9 nthne0 
nth i l2 != 0 <-> i < len l2
10 sucne0 
nth i l2 = suc b -> nth i l2 != 0
11 hyp h2 
G -> nth i l2 = suc b
12 10, 11 syl 
G -> nth i l2 != 0
13 9, 12 sylib 
G -> i < len l2
14 8, 13 iand 
G -> i < len l1 /\ i < len l2
15 3, 14 sylibr 
G -> i < min (len l1) (len l2)
16 2, 15 syl 
G -> nth i (zip l1 l2) = suc ((\ x, nth x l1 - 1, nth x l2 - 1) @ i)
17 sucsub1 
suc a - 1 = a
18 anr 
G /\ x = i -> x = i
19 18 ntheq1d 
G /\ x = i -> nth x l1 = nth i l1
20 6 anwl 
G /\ x = i -> nth i l1 = suc a
21 19, 20 eqtrd 
G /\ x = i -> nth x l1 = suc a
22 21 subeq1d 
G /\ x = i -> nth x l1 - 1 = suc a - 1
23 17, 22 syl6eq 
G /\ x = i -> nth x l1 - 1 = a
24 sucsub1 
suc b - 1 = b
25 18 ntheq1d 
G /\ x = i -> nth x l2 = nth i l2
26 11 anwl 
G /\ x = i -> nth i l2 = suc b
27 25, 26 eqtrd 
G /\ x = i -> nth x l2 = suc b
28 27 subeq1d 
G /\ x = i -> nth x l2 - 1 = suc b - 1
29 24, 28 syl6eq 
G /\ x = i -> nth x l2 - 1 = b
30 23, 29 preqd 
G /\ x = i -> nth x l1 - 1, nth x l2 - 1 = a, b
31 30 applamed 
G -> (\ x, nth x l1 - 1, nth x l2 - 1) @ i = a, b
32 31 suceqd 
G -> suc ((\ x, nth x l1 - 1, nth x l2 - 1) @ i) = suc (a, b)
33 16, 32 eqtrd 
G -> nth i (zip l1 l2) = suc (a, b)

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)