Theorem nthext2d ≪ | index | src | ≫ 

theorem nthext2d (G: wff) (l1 l2 n: nat) {i: nat}:
  $ G -> len l1 = n $ >
  $ G -> len l2 = n $ >
  $ G /\ i < n -> nth i l1 = nth i l2 $ >
  $ G -> l1 = l2 $;
StepHypRefExpression
1 lfnnth 
lfn (\ i, nth i l1 - 1) (len l1) = l1
2 lfnnth 
lfn (\ i, nth i l2 - 1) (len l2) = l2
3 hyp h3 
G /\ i < n -> nth i l1 = nth i l2
4 nthne0 
nth i l1 != 0 <-> i < len l1
5 4 conv ne 
~nth i l1 = 0 <-> i < len l1
6 hyp h1 
G -> len l1 = n
7 6 lteq2d 
G -> (i < len l1 <-> i < n)
8 7 bi1d 
G -> i < len l1 -> i < n
9 5, 8 syl5bi 
G -> ~nth i l1 = 0 -> i < n
10 9 con1d 
G -> ~i < n -> nth i l1 = 0
11 10 imp 
G /\ ~i < n -> nth i l1 = 0
12 nthne0 
nth i l2 != 0 <-> i < len l2
13 12 conv ne 
~nth i l2 = 0 <-> i < len l2
14 hyp h2 
G -> len l2 = n
15 14 lteq2d 
G -> (i < len l2 <-> i < n)
16 15 bi1d 
G -> i < len l2 -> i < n
17 13, 16 syl5bi 
G -> ~nth i l2 = 0 -> i < n
18 17 con1d 
G -> ~i < n -> nth i l2 = 0
19 18 imp 
G /\ ~i < n -> nth i l2 = 0
20 11, 19 eqtr4d 
G /\ ~i < n -> nth i l1 = nth i l2
21 3, 20 casesda 
G -> nth i l1 = nth i l2
22 21 subeq1d 
G -> nth i l1 - 1 = nth i l2 - 1
23 22 lameqd 
G -> \ i, nth i l1 - 1 == \ i, nth i l2 - 1
24 6, 14 eqtr4d 
G -> len l1 = len l2
25 23, 24 lfneqd 
G -> lfn (\ i, nth i l1 - 1) (len l1) = lfn (\ i, nth i l2 - 1) (len l2)
26 1, 2, 25 eqtr3g 
G -> 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)