Theorem dropnth ≪ | index | src | ≫ 

theorem dropnth (i l n: nat): $ nth i (drop l n) = nth (i + n) l $;
StepHypRefExpression
1 eor 
(len l <= i + n -> nth i (drop l n) = nth (i + n) l) ->
  (i + n < len l -> nth i (drop l n) = nth (i + n) l) ->
  len l <= i + n \/ i + n < len l ->
  nth i (drop l n) = nth (i + n) l
2 ntheq0 
nth i (drop l n) = 0 <-> len (drop l n) <= i
3 leeq1 
len (drop l n) = len l - n -> (len (drop l n) <= i <-> len l - n <= i)
4 droplen 
len (drop l n) = len l - n
5 3, 4 ax_mp 
len (drop l n) <= i <-> len l - n <= i
6 lesubadd 
len l - n <= i <-> len l <= i + n
7 6 bi2i 
len l <= i + n -> len l - n <= i
8 5, 7 sylibr 
len l <= i + n -> len (drop l n) <= i
9 2, 8 sylibr 
len l <= i + n -> nth i (drop l n) = 0
10 ntheq0 
nth (i + n) l = 0 <-> len l <= i + n
11 10 bi2i 
len l <= i + n -> nth (i + n) l = 0
12 9, 11 eqtr4d 
len l <= i + n -> nth i (drop l n) = nth (i + n) l
13 1, 12 ax_mp 
(i + n < len l -> nth i (drop l n) = nth (i + n) l) -> len l <= i + n \/ i + n < len l -> nth i (drop l n) = nth (i + n) l
14 ltaddsub 
i + n < len l <-> i < len l - n
15 nthlfn 
i < len l - n -> nth i (lfn (\ x, nth (x + n) l - 1) (len l - n)) = suc ((\ x, nth (x + n) l - 1) @ i)
16 15 conv drop 
i < len l - n -> nth i (drop l n) = suc ((\ x, nth (x + n) l - 1) @ i)
17 14, 16 sylbi 
i + n < len l -> nth i (drop l n) = suc ((\ x, nth (x + n) l - 1) @ i)
18 anr 
i + n < len l /\ x = i -> x = i
19 18 addeq1d 
i + n < len l /\ x = i -> x + n = i + n
20 19 ntheq1d 
i + n < len l /\ x = i -> nth (x + n) l = nth (i + n) l
21 20 subeq1d 
i + n < len l /\ x = i -> nth (x + n) l - 1 = nth (i + n) l - 1
22 21 applamed 
i + n < len l -> (\ x, nth (x + n) l - 1) @ i = nth (i + n) l - 1
23 22 suceqd 
i + n < len l -> suc ((\ x, nth (x + n) l - 1) @ i) = suc (nth (i + n) l - 1)
24 nthne0 
nth (i + n) l != 0 <-> i + n < len l
25 sub1can 
nth (i + n) l != 0 -> suc (nth (i + n) l - 1) = nth (i + n) l
26 24, 25 sylbir 
i + n < len l -> suc (nth (i + n) l - 1) = nth (i + n) l
27 23, 26 eqtrd 
i + n < len l -> suc ((\ x, nth (x + n) l - 1) @ i) = nth (i + n) l
28 17, 27 eqtrd 
i + n < len l -> nth i (drop l n) = nth (i + n) l
29 13, 28 ax_mp 
len l <= i + n \/ i + n < len l -> nth i (drop l n) = nth (i + n) l
30 leorlt 
len l <= i + n \/ i + n < len l
31 29, 30 ax_mp 
nth i (drop l n) = nth (i + 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)