Theorem takeappend1 ≪ | index | src | ≫ 

theorem takeappend1 (l1 l2 n: nat):
  $ n <= len l1 -> take (l1 ++ l2) n = take l1 n $;
StepHypRefExpression
1 takelen 
len (take (l1 ++ l2) n) = min (len (l1 ++ l2)) n
2 eqmin2 
n <= len (l1 ++ l2) -> min (len (l1 ++ l2)) n = n
3 leeq2 
len (l1 ++ l2) = len l1 + len l2 -> (len l1 <= len (l1 ++ l2) <-> len l1 <= len l1 + len l2)
4 appendlen 
len (l1 ++ l2) = len l1 + len l2
5 3, 4 ax_mp 
len l1 <= len (l1 ++ l2) <-> len l1 <= len l1 + len l2
6 leaddid1 
len l1 <= len l1 + len l2
7 5, 6 mpbir 
len l1 <= len (l1 ++ l2)
8 letr 
n <= len l1 -> len l1 <= len (l1 ++ l2) -> n <= len (l1 ++ l2)
9 7, 8 mpi 
n <= len l1 -> n <= len (l1 ++ l2)
10 2, 9 syl 
n <= len l1 -> min (len (l1 ++ l2)) n = n
11 1, 10 syl5eq 
n <= len l1 -> len (take (l1 ++ l2) n) = n
12 takelen 
len (take l1 n) = min (len l1) n
13 eqmin2 
n <= len l1 -> min (len l1) n = n
14 12, 13 syl5eq 
n <= len l1 -> len (take l1 n) = n
15 takenth 
a1 < n -> nth a1 (take (l1 ++ l2) n) = nth a1 (l1 ++ l2)
16 15 anwr 
n <= len l1 /\ a1 < n -> nth a1 (take (l1 ++ l2) n) = nth a1 (l1 ++ l2)
17 takenth 
a1 < n -> nth a1 (take l1 n) = nth a1 l1
18 17 anwr 
n <= len l1 /\ a1 < n -> nth a1 (take l1 n) = nth a1 l1
19 appendnth1 
a1 < len l1 -> nth a1 (l1 ++ l2) = nth a1 l1
20 ltletr 
a1 < n -> n <= len l1 -> a1 < len l1
21 20 impcom 
n <= len l1 /\ a1 < n -> a1 < len l1
22 19, 21 syl 
n <= len l1 /\ a1 < n -> nth a1 (l1 ++ l2) = nth a1 l1
23 18, 22 eqtr4d 
n <= len l1 /\ a1 < n -> nth a1 (take l1 n) = nth a1 (l1 ++ l2)
24 16, 23 eqtr4d 
n <= len l1 /\ a1 < n -> nth a1 (take (l1 ++ l2) n) = nth a1 (take l1 n)
25 11, 14, 24 nthext2d 
n <= len l1 -> take (l1 ++ l2) n = take l1 n

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)