Theorem sublistAt_len_le ≪ | index | src | ≫ 

theorem sublistAt_len_le (L1 L2 n: nat):
  $ sublistAt n L1 L2 -> n + len L2 <= len L1 $;
StepHypRefExpression
1 leeq2 
len (L2 ++ a2) = len L2 + len a2 -> (len L2 <= len (L2 ++ a2) <-> len L2 <= len L2 + len a2)
2 appendlen 
len (L2 ++ a2) = len L2 + len a2
3 1, 2 ax_mp 
len L2 <= len (L2 ++ a2) <-> len L2 <= len L2 + len a2
4 leaddid1 
len L2 <= len L2 + len a2
5 3, 4 mpbir 
len L2 <= len (L2 ++ a2)
6 leadd2 
len L2 <= len (L2 ++ a2) <-> len a1 + len L2 <= len a1 + len (L2 ++ a2)
7 anr 
L1 = a1 ++ L2 ++ a2 /\ len a1 = n -> len a1 = n
8 7 addeq1d 
L1 = a1 ++ L2 ++ a2 /\ len a1 = n -> len a1 + len L2 = n + len L2
9 appendlen 
len (a1 ++ L2 ++ a2) = len a1 + len (L2 ++ a2)
10 anl 
L1 = a1 ++ L2 ++ a2 /\ len a1 = n -> L1 = a1 ++ L2 ++ a2
11 10 eqcomd 
L1 = a1 ++ L2 ++ a2 /\ len a1 = n -> a1 ++ L2 ++ a2 = L1
12 11 leneqd 
L1 = a1 ++ L2 ++ a2 /\ len a1 = n -> len (a1 ++ L2 ++ a2) = len L1
13 9, 12 syl5eqr 
L1 = a1 ++ L2 ++ a2 /\ len a1 = n -> len a1 + len (L2 ++ a2) = len L1
14 8, 13 leeqd 
L1 = a1 ++ L2 ++ a2 /\ len a1 = n -> (len a1 + len L2 <= len a1 + len (L2 ++ a2) <-> n + len L2 <= len L1)
15 6, 14 syl5bb 
L1 = a1 ++ L2 ++ a2 /\ len a1 = n -> (len L2 <= len (L2 ++ a2) <-> n + len L2 <= len L1)
16 5, 15 mpbii 
L1 = a1 ++ L2 ++ a2 /\ len a1 = n -> n + len L2 <= len L1
17 16 eex 
E. a2 (L1 = a1 ++ L2 ++ a2 /\ len a1 = n) -> n + len L2 <= len L1
18 17 eex 
E. a1 E. a2 (L1 = a1 ++ L2 ++ a2 /\ len a1 = n) -> n + len L2 <= len L1
19 18 conv sublistAt 
sublistAt n L1 L2 -> n + len L2 <= len L1

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)