Theorem dropArray ≪ | index | src | ≫ 

theorem dropArray (A: set) (l m n: nat):
  $ l e. Array A (m + n) -> drop l m e. Array A n $;
StepHypRefExpression
1 elArray 
drop l m e. Array A n <-> drop l m e. List A /\ len (drop l m) = n
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 (m + n) -> l e. List A
7 5, 6 sylibr 
l e. Array A (m + n) -> take l m ++ drop l m e. List A
8 2, 7 sylib 
l e. Array A (m + n) -> take l m e. List A /\ drop l m e. List A
9 8 anrd 
l e. Array A (m + n) -> drop l m e. List A
10 droplen 
len (drop l m) = len l - m
11 pncan2 
m + n - m = n
12 elArraylen 
l e. Array A (m + n) -> len l = m + n
13 12 subeq1d 
l e. Array A (m + n) -> len l - m = m + n - m
14 11, 13 syl6eq 
l e. Array A (m + n) -> len l - m = n
15 10, 14 syl5eq 
l e. Array A (m + n) -> len (drop l m) = n
16 9, 15 iand 
l e. Array A (m + n) -> drop l m e. List A /\ len (drop l m) = n
17 1, 16 sylibr 
l e. Array A (m + n) -> drop l m e. Array A 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)