Theorem ltmax ≪ | index | src | ≫ 

theorem ltmax (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 lenlt 
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 maxle 
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 lenlt 
b <= a <-> ~a < b
11 9, 10 ax_mp 
(c <= a <-> ~a < c) -> (b <= a /\ c <= a <-> ~a < b /\ ~a < c)
12 lenlt 
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)