Theorem nthext ≪ | index | src | ≫ 

theorem nthext (l1 l2: nat) {n: nat}: $ l1 = l2 <-> A. n nth n l1 = nth n l2 $;
StepHypRefExpression
1 ntheq2 
l1 = l2 -> nth n l1 = nth n l2
2 1 iald 
l1 = l2 -> A. n nth n l1 = nth n l2
3 eqallt1 
len l1 = len l2 <-> A. n (n < len l1 <-> n < len l2)
4 nthne0 
nth n l1 != 0 <-> n < len l1
5 nthne0 
nth n l2 != 0 <-> n < len l2
6 neeq1 
nth n l1 = nth n l2 -> (nth n l1 != 0 <-> nth n l2 != 0)
7 4, 5, 6 bitr3g 
nth n l1 = nth n l2 -> (n < len l1 <-> n < len l2)
8 7 alimi 
A. n nth n l1 = nth n l2 -> A. n (n < len l1 <-> n < len l2)
9 3, 8 sylibr 
A. n nth n l1 = nth n l2 -> len l1 = len l2
10 eqidd 
A. n nth n l1 = nth n l2 -> len l2 = len l2
11 ntheq1 
n = a1 -> nth n l1 = nth a1 l1
12 ntheq1 
n = a1 -> nth n l2 = nth a1 l2
13 11, 12 eqeqd 
n = a1 -> (nth n l1 = nth n l2 <-> nth a1 l1 = nth a1 l2)
14 13 eale 
A. n nth n l1 = nth n l2 -> nth a1 l1 = nth a1 l2
15 14 anwl 
A. n nth n l1 = nth n l2 /\ a1 < len l2 -> nth a1 l1 = nth a1 l2
16 9, 10, 15 nthext2d 
A. n nth n l1 = nth n l2 -> l1 = l2
17 2, 16 ibii 
l1 = l2 <-> A. n nth n l1 = nth n 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)