Theorem maxle ≪ | index | src | ≫ 

theorem maxle (a b c: nat): $ max a b <= c <-> a <= c /\ b <= c $;
StepHypRefExpression
1 letr 
a <= max a b -> max a b <= c -> a <= c
2 lemax1 
a <= max a b
3 1, 2 ax_mp 
max a b <= c -> a <= c
4 letr 
b <= max a b -> max a b <= c -> b <= c
5 lemax2 
b <= max a b
6 4, 5 ax_mp 
max a b <= c -> b <= c
7 3, 6 iand 
max a b <= c -> a <= c /\ b <= c
8 ifpos 
a < b -> if (a < b) b a = b
9 8 conv max 
a < b -> max a b = b
10 9 leeq1d 
a < b -> (max a b <= c <-> b <= c)
11 10 anwr 
a <= c /\ b <= c /\ a < b -> (max a b <= c <-> b <= c)
12 anlr 
a <= c /\ b <= c /\ a < b -> b <= c
13 11, 12 mpbird 
a <= c /\ b <= c /\ a < b -> max a b <= c
14 ifneg 
~a < b -> if (a < b) b a = a
15 14 conv max 
~a < b -> max a b = a
16 15 leeq1d 
~a < b -> (max a b <= c <-> a <= c)
17 16 anwr 
a <= c /\ b <= c /\ ~a < b -> (max a b <= c <-> a <= c)
18 anll 
a <= c /\ b <= c /\ ~a < b -> a <= c
19 17, 18 mpbird 
a <= c /\ b <= c /\ ~a < b -> max a b <= c
20 13, 19 casesda 
a <= c /\ b <= c -> max a b <= c
21 7, 20 ibii 
max a b <= c <-> a <= c /\ b <= 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)