Theorem takenth ≪ | index | src | ≫ 

theorem takenth (i l n: nat): $ i < n -> nth i (take l n) = nth i l $;
StepHypRefExpression
1 leorlt 
len l <= i \/ i < len l
2 ntheq0 
nth i (take l n) = 0 <-> len (take l n) <= i
3 letr 
len (take l n) <= len l -> len l <= i -> len (take l n) <= i
4 leeq1 
len (take l n) = min (len l) n -> (len (take l n) <= len l <-> min (len l) n <= len l)
5 takelen 
len (take l n) = min (len l) n
6 4, 5 ax_mp 
len (take l n) <= len l <-> min (len l) n <= len l
7 minle1 
min (len l) n <= len l
8 6, 7 mpbir 
len (take l n) <= len l
9 3, 8 ax_mp 
len l <= i -> len (take l n) <= i
10 9 anwr 
i < n /\ len l <= i -> len (take l n) <= i
11 2, 10 sylibr 
i < n /\ len l <= i -> nth i (take l n) = 0
12 ntheq0 
nth i l = 0 <-> len l <= i
13 anr 
i < n /\ len l <= i -> len l <= i
14 12, 13 sylibr 
i < n /\ len l <= i -> nth i l = 0
15 11, 14 eqtr4d 
i < n /\ len l <= i -> nth i (take l n) = nth i l
16 ancom 
i < n /\ i < len l -> i < len l /\ i < n
17 ltmin 
i < min (len l) n <-> i < len l /\ i < n
18 nthlfn 
i < min (len l) n -> nth i (lfn (\ x, nth x l - 1) (min (len l) n)) = suc ((\ x, nth x l - 1) @ i)
19 18 conv take 
i < min (len l) n -> nth i (take l n) = suc ((\ x, nth x l - 1) @ i)
20 17, 19 sylbir 
i < len l /\ i < n -> nth i (take l n) = suc ((\ x, nth x l - 1) @ i)
21 16, 20 rsyl 
i < n /\ i < len l -> nth i (take l n) = suc ((\ x, nth x l - 1) @ i)
22 anr 
i < n /\ i < len l /\ x = i -> x = i
23 22 ntheq1d 
i < n /\ i < len l /\ x = i -> nth x l = nth i l
24 23 subeq1d 
i < n /\ i < len l /\ x = i -> nth x l - 1 = nth i l - 1
25 24 applamed 
i < n /\ i < len l -> (\ x, nth x l - 1) @ i = nth i l - 1
26 25 suceqd 
i < n /\ i < len l -> suc ((\ x, nth x l - 1) @ i) = suc (nth i l - 1)
27 sub1can 
nth i l != 0 -> suc (nth i l - 1) = nth i l
28 nthne0 
nth i l != 0 <-> i < len l
29 anr 
i < n /\ i < len l -> i < len l
30 28, 29 sylibr 
i < n /\ i < len l -> nth i l != 0
31 27, 30 syl 
i < n /\ i < len l -> suc (nth i l - 1) = nth i l
32 26, 31 eqtrd 
i < n /\ i < len l -> suc ((\ x, nth x l - 1) @ i) = nth i l
33 21, 32 eqtrd 
i < n /\ i < len l -> nth i (take l n) = nth i l
34 15, 33 eorda 
i < n -> len l <= i \/ i < len l -> nth i (take l n) = nth i l
35 1, 34 mpi 
i < n -> nth i (take l n) = nth i 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)