Theorem takeArray ≪ | index | src | ≫ 

theorem takeArray (A: set) (l m n: nat):
  $ m <= n /\ l e. Array A n -> take l m e. Array A m $;
StepHypRefExpression
1 elArray 
take l m e. Array A m <-> take l m e. List A /\ len (take l m) = m
2 appendT 
take l m ++ drop l m e. List A <-> take l m e. List A /\ drop l m e. List A
3 eleq1 
take l m ++ drop l m = l -> (take l m ++ drop l m e. List A <-> l e. List A)
4 takedrop 
take l m ++ drop l m = l
5 3, 4 ax_mp 
take l m ++ drop l m e. List A <-> l e. List A
6 elArrayList 
l e. Array A n -> l e. List A
7 6 anwr 
m <= n /\ l e. Array A n -> l e. List A
8 5, 7 sylibr 
m <= n /\ l e. Array A n -> take l m ++ drop l m e. List A
9 2, 8 sylib 
m <= n /\ l e. Array A n -> take l m e. List A /\ drop l m e. List A
10 9 anld 
m <= n /\ l e. Array A n -> take l m e. List A
11 takelen 
len (take l m) = min (len l) m
12 eqmin2 
m <= len l -> min (len l) m = m
13 elArraylen 
l e. Array A n -> len l = n
14 13 anwr 
m <= n /\ l e. Array A n -> len l = n
15 14 leeq2d 
m <= n /\ l e. Array A n -> (m <= len l <-> m <= n)
16 anl 
m <= n /\ l e. Array A n -> m <= n
17 15, 16 mpbird 
m <= n /\ l e. Array A n -> m <= len l
18 12, 17 syl 
m <= n /\ l e. Array A n -> min (len l) m = m
19 11, 18 syl5eq 
m <= n /\ l e. Array A n -> len (take l m) = m
20 10, 19 iand 
m <= n /\ l e. Array A n -> take l m e. List A /\ len (take l m) = m
21 1, 20 sylibr 
m <= n /\ l e. Array A n -> take l m e. Array A m

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)