Theorem lemax ≪ | index | src | ≫ 

theorem lemax (a b c: nat): $ a <= max b c <-> a <= b \/ a <= c $;
StepHypRefExpression
1 con4b 
(~a <= max b c <-> ~(a <= b \/ a <= c)) -> (a <= max b c <-> a <= b \/ a <= c)
2 bitr3 
(max b c < a <-> ~a <= max b c) -> (max b c < a <-> ~(a <= b \/ a <= c)) -> (~a <= max b c <-> ~(a <= b \/ a <= c))
3 ltnle 
max b c < a <-> ~a <= max b c
4 2, 3 ax_mp 
(max b c < a <-> ~(a <= b \/ a <= c)) -> (~a <= max b c <-> ~(a <= b \/ a <= c))
5 bitr 
(max b c < a <-> b < a /\ c < a) -> (b < a /\ c < a <-> ~(a <= b \/ a <= c)) -> (max b c < a <-> ~(a <= b \/ a <= c))
6 maxlt 
max b c < a <-> b < a /\ c < a
7 5, 6 ax_mp 
(b < a /\ c < a <-> ~(a <= b \/ a <= c)) -> (max b c < a <-> ~(a <= b \/ a <= c))
8 bitr4 
(b < a /\ c < a <-> ~a <= b /\ ~a <= c) -> (~(a <= b \/ a <= c) <-> ~a <= b /\ ~a <= c) -> (b < a /\ c < a <-> ~(a <= b \/ a <= c))
9 aneq 
(b < a <-> ~a <= b) -> (c < a <-> ~a <= c) -> (b < a /\ c < a <-> ~a <= b /\ ~a <= c)
10 ltnle 
b < a <-> ~a <= b
11 9, 10 ax_mp 
(c < a <-> ~a <= c) -> (b < a /\ c < a <-> ~a <= b /\ ~a <= c)
12 ltnle 
c < a <-> ~a <= c
13 11, 12 ax_mp 
b < a /\ c < a <-> ~a <= b /\ ~a <= c
14 8, 13 ax_mp 
(~(a <= b \/ a <= c) <-> ~a <= b /\ ~a <= c) -> (b < a /\ c < a <-> ~(a <= b \/ a <= c))
15 notor 
~(a <= b \/ a <= c) <-> ~a <= b /\ ~a <= c
16 14, 15 ax_mp 
b < a /\ c < a <-> ~(a <= b \/ a <= c)
17 7, 16 ax_mp 
max b c < a <-> ~(a <= b \/ a <= c)
18 4, 17 ax_mp 
~a <= max b c <-> ~(a <= b \/ a <= c)
19 1, 18 ax_mp 
a <= max 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)