Theorem takedrop ≪ | index | src | ≫ 

theorem takedrop (l n: nat): $ take l n ++ drop l n = l $;
StepHypRefExpression
1 eqtr 
len (take l n ++ drop l n) = len (take l n) + len (drop l n) -> len (take l n) + len (drop l n) = len l -> len (take l n ++ drop l n) = len l
2 appendlen 
len (take l n ++ drop l n) = len (take l n) + len (drop l n)
3 1, 2 ax_mp 
len (take l n) + len (drop l n) = len l -> len (take l n ++ drop l n) = len l
4 eqtr 
len (take l n) + len (drop l n) = min (len l) n + (len l - n) -> min (len l) n + (len l - n) = len l -> len (take l n) + len (drop l n) = len l
5 addeq 
len (take l n) = min (len l) n -> len (drop l n) = len l - n -> len (take l n) + len (drop l n) = min (len l) n + (len l - n)
6 takelen 
len (take l n) = min (len l) n
7 5, 6 ax_mp 
len (drop l n) = len l - n -> len (take l n) + len (drop l n) = min (len l) n + (len l - n)
8 droplen 
len (drop l n) = len l - n
9 7, 8 ax_mp 
len (take l n) + len (drop l n) = min (len l) n + (len l - n)
10 4, 9 ax_mp 
min (len l) n + (len l - n) = len l -> len (take l n) + len (drop l n) = len l
11 minaddsub 
min (len l) n + (len l - n) = len l
12 10, 11 ax_mp 
len (take l n) + len (drop l n) = len l
13 3, 12 ax_mp 
len (take l n ++ drop l n) = len l
14 eqid 
len l = len l
15 ltorle 
i < n \/ n <= i
16 bitr 
(i < len (take l n) <-> i < min (len l) n) -> (i < min (len l) n <-> i < len l /\ i < n) -> (i < len (take l n) <-> i < len l /\ i < n)
17 lteq2 
len (take l n) = min (len l) n -> (i < len (take l n) <-> i < min (len l) n)
18 17, 6 ax_mp 
i < len (take l n) <-> i < min (len l) n
19 16, 18 ax_mp 
(i < min (len l) n <-> i < len l /\ i < n) -> (i < len (take l n) <-> i < len l /\ i < n)
20 ltmin 
i < min (len l) n <-> i < len l /\ i < n
21 19, 20 ax_mp 
i < len (take l n) <-> i < len l /\ i < n
22 appendnth1 
i < len (take l n) -> nth i (take l n ++ drop l n) = nth i (take l n)
23 21, 22 sylbir 
i < len l /\ i < n -> nth i (take l n ++ drop l n) = nth i (take l n)
24 takenth 
i < n -> nth i (take l n) = nth i l
25 24 anwr 
i < len l /\ i < n -> nth i (take l n) = nth i l
26 23, 25 eqtrd 
i < len l /\ i < n -> nth i (take l n ++ drop l n) = nth i l
27 appendnth2 
len (take l n) <= i -> nth i (take l n ++ drop l n) = nth (i - len (take l n)) (drop l n)
28 letr 
len (take l n) <= n -> n <= i -> len (take l n) <= i
29 leeq1 
len (take l n) = min (len l) n -> (len (take l n) <= n <-> min (len l) n <= n)
30 29, 6 ax_mp 
len (take l n) <= n <-> min (len l) n <= n
31 minle2 
min (len l) n <= n
32 30, 31 mpbir 
len (take l n) <= n
33 28, 32 ax_mp 
n <= i -> len (take l n) <= i
34 33 anwr 
i < len l /\ n <= i -> len (take l n) <= i
35 27, 34 syl 
i < len l /\ n <= i -> nth i (take l n ++ drop l n) = nth (i - len (take l n)) (drop l n)
36 dropnth 
nth (i - len (take l n)) (drop l n) = nth (i - len (take l n) + n) l
37 eqmin2 
n <= len l -> min (len l) n = n
38 anr 
i < len l /\ n <= i -> n <= i
39 ltle 
i < len l -> i <= len l
40 39 anwl 
i < len l /\ n <= i -> i <= len l
41 38, 40 letrd 
i < len l /\ n <= i -> n <= len l
42 37, 41 syl 
i < len l /\ n <= i -> min (len l) n = n
43 6, 42 syl5eq 
i < len l /\ n <= i -> len (take l n) = n
44 43 subeq2d 
i < len l /\ n <= i -> i - len (take l n) = i - n
45 44 addeq1d 
i < len l /\ n <= i -> i - len (take l n) + n = i - n + n
46 npcan 
n <= i -> i - n + n = i
47 46 anwr 
i < len l /\ n <= i -> i - n + n = i
48 45, 47 eqtrd 
i < len l /\ n <= i -> i - len (take l n) + n = i
49 48 ntheq1d 
i < len l /\ n <= i -> nth (i - len (take l n) + n) l = nth i l
50 36, 49 syl5eq 
i < len l /\ n <= i -> nth (i - len (take l n)) (drop l n) = nth i l
51 35, 50 eqtrd 
i < len l /\ n <= i -> nth i (take l n ++ drop l n) = nth i l
52 26, 51 eorda 
i < len l -> i < n \/ n <= i -> nth i (take l n ++ drop l n) = nth i l
53 15, 52 mpi 
i < len l -> nth i (take l n ++ drop l n) = nth i l
54 13, 14, 53 nthext2 
take l n ++ drop l 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)