Theorem takemin | index | src |

theorem takemin (l n: nat): $ take l (min (len l) n) = take l n $;
StepHypRefExpression
1 eor
(n <= len l -> take l (min (len l) n) = take l n) ->
  (len l <= n -> take l (min (len l) n) = take l n) ->
  n <= len l \/ len l <= n ->
  take l (min (len l) n) = take l n
2 eqmin2
n <= len l -> min (len l) n = n
3 2 takeeq2d
n <= len l -> take l (min (len l) n) = take l n
4 1, 3 ax_mp
(len l <= n -> take l (min (len l) n) = take l n) -> n <= len l \/ len l <= n -> take l (min (len l) n) = take l n
5 eqmin1
len l <= n -> min (len l) n = len l
6 5 takeeq2d
len l <= n -> take l (min (len l) n) = take l (len l)
7 takeall
len l <= len l -> take l (len l) = l
8 leid
len l <= len l
9 7, 8 ax_mp
take l (len l) = l
10 takeall
len l <= n -> take l n = l
11 9, 10 syl6eqr
len l <= n -> take l n = take l (len l)
12 6, 11 eqtr4d
len l <= n -> take l (min (len l) n) = take l n
13 4, 12 ax_mp
n <= len l \/ len l <= n -> take l (min (len l) n) = take l n
14 leorle
n <= len l \/ len l <= n
15 13, 14 ax_mp
take l (min (len l) n) = take l 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)