Theorem nthS ≪ | index | src | ≫ 

pub theorem nthS (n a l: nat): $ nth (suc n) (a : l) = nth n l $;
StepHypRefExpression
1 bitr4 
(n < len l <-> suc n < suc (len l)) -> (suc n < len (a : l) <-> suc n < suc (len l)) -> (n < len l <-> suc n < len (a : l))
2 ltsuc 
n < len l <-> suc n < suc (len l)
3 1, 2 ax_mp 
(suc n < len (a : l) <-> suc n < suc (len l)) -> (n < len l <-> suc n < len (a : l))
4 lteq2 
len (a : l) = suc (len l) -> (suc n < len (a : l) <-> suc n < suc (len l))
5 lenS 
len (a : l) = suc (len l)
6 4, 5 ax_mp 
suc n < len (a : l) <-> suc n < suc (len l)
7 3, 6 ax_mp 
n < len l <-> suc n < len (a : l)
8 ifpos 
suc n < len (a : l) -> if (suc n < len (a : l)) (suc (listfn (a : l) @ suc n)) 0 = suc (listfn (a : l) @ suc n)
9 8 conv nth 
suc n < len (a : l) -> nth (suc n) (a : l) = suc (listfn (a : l) @ suc n)
10 7, 9 sylbi 
n < len l -> nth (suc n) (a : l) = suc (listfn (a : l) @ suc n)
11 suceq 
listfn (a : l) @ suc n = listfn l @ n -> suc (listfn (a : l) @ suc n) = suc (listfn l @ n)
12 listfnSS 
listfn (a : l) @ suc n = listfn l @ n
13 11, 12 ax_mp 
suc (listfn (a : l) @ suc n) = suc (listfn l @ n)
14 ifpos 
n < len l -> if (n < len l) (suc (listfn l @ n)) 0 = suc (listfn l @ n)
15 14 conv nth 
n < len l -> nth n l = suc (listfn l @ n)
16 13, 15 syl6eqr 
n < len l -> nth n l = suc (listfn (a : l) @ suc n)
17 10, 16 eqtr4d 
n < len l -> nth (suc n) (a : l) = nth n l
18 noteq 
(n < len l <-> suc n < len (a : l)) -> (~n < len l <-> ~suc n < len (a : l))
19 18, 7 ax_mp 
~n < len l <-> ~suc n < len (a : l)
20 ifneg 
~suc n < len (a : l) -> if (suc n < len (a : l)) (suc (listfn (a : l) @ suc n)) 0 = 0
21 20 conv nth 
~suc n < len (a : l) -> nth (suc n) (a : l) = 0
22 19, 21 sylbi 
~n < len l -> nth (suc n) (a : l) = 0
23 ifneg 
~n < len l -> if (n < len l) (suc (listfn l @ n)) 0 = 0
24 23 conv nth 
~n < len l -> nth n l = 0
25 22, 24 eqtr4d 
~n < len l -> nth (suc n) (a : l) = nth n l
26 17, 25 cases 
nth (suc n) (a : l) = nth n l

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)