Theorem lemin | index | src |

theorem lemin (a b c: nat): $ a <= min b c <-> a <= b /\ a <= c $;
StepHypRefExpression
1 minle1
min b c <= b
2 letr
a <= min b c -> min b c <= b -> a <= b
3 1, 2 mpi
a <= min b c -> a <= b
4 minle2
min b c <= c
5 letr
a <= min b c -> min b c <= c -> a <= c
6 4, 5 mpi
a <= min b c -> a <= c
7 3, 6 iand
a <= min b c -> a <= b /\ a <= c
8 ifpos
b < c -> if (b < c) b c = b
9 8 conv min
b < c -> min b c = b
10 9 leeq2d
b < c -> (a <= min b c <-> a <= b)
11 10 anwr
a <= b /\ a <= c /\ b < c -> (a <= min b c <-> a <= b)
12 anll
a <= b /\ a <= c /\ b < c -> a <= b
13 11, 12 mpbird
a <= b /\ a <= c /\ b < c -> a <= min b c
14 ifneg
~b < c -> if (b < c) b c = c
15 14 conv min
~b < c -> min b c = c
16 15 leeq2d
~b < c -> (a <= min b c <-> a <= c)
17 16 anwr
a <= b /\ a <= c /\ ~b < c -> (a <= min b c <-> a <= c)
18 anlr
a <= b /\ a <= c /\ ~b < c -> a <= c
19 17, 18 mpbird
a <= b /\ a <= c /\ ~b < c -> a <= min b c
20 13, 19 casesda
a <= b /\ a <= c -> a <= min b c
21 7, 20 ibii
a <= min b c <-> a <= b /\ a <= c

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, add0, addS)