Theorem ltorle ≪ | index | src | ≫ 

theorem ltorle (a b: nat): $ a < b \/ b <= a $;
StepHypRefExpression
1 lteq2 
x = b -> (a < x <-> a < b)
2 leeq1 
x = b -> (x <= a <-> b <= a)
3 1, 2 oreqd 
x = b -> (a < x \/ x <= a <-> a < b \/ b <= a)
4 lteq2 
x = 0 -> (a < x <-> a < 0)
5 leeq1 
x = 0 -> (x <= a <-> 0 <= a)
6 4, 5 oreqd 
x = 0 -> (a < x \/ x <= a <-> a < 0 \/ 0 <= a)
7 lteq2 
x = y -> (a < x <-> a < y)
8 leeq1 
x = y -> (x <= a <-> y <= a)
9 7, 8 oreqd 
x = y -> (a < x \/ x <= a <-> a < y \/ y <= a)
10 lteq2 
x = suc y -> (a < x <-> a < suc y)
11 leeq1 
x = suc y -> (x <= a <-> suc y <= a)
12 10, 11 oreqd 
x = suc y -> (a < x \/ x <= a <-> a < suc y \/ suc y <= a)
13 orr 
0 <= a -> a < 0 \/ 0 <= a
14 le01 
0 <= a
15 13, 14 ax_mp 
a < 0 \/ 0 <= a
16 eor 
(a < y -> a < suc y \/ suc y <= a) -> (y <= a -> a < suc y \/ suc y <= a) -> a < y \/ y <= a -> a < suc y \/ suc y <= a
17 ltsucid 
y < suc y
18 lttr 
a < y -> y < suc y -> a < suc y
19 17, 18 mpi 
a < y -> a < suc y
20 19 orld 
a < y -> a < suc y \/ suc y <= a
21 16, 20 ax_mp 
(y <= a -> a < suc y \/ suc y <= a) -> a < y \/ y <= a -> a < suc y \/ suc y <= a
22 con3 
(a <= y -> a < suc y) -> ~a < suc y -> ~a <= y
23 bi1 
(a <= y <-> a < suc y) -> a <= y -> a < suc y
24 lesuc 
a <= y <-> suc a <= suc y
25 24 conv lt 
a <= y <-> a < suc y
26 23, 25 ax_mp 
a <= y -> a < suc y
27 22, 26 ax_mp 
~a < suc y -> ~a <= y
28 bi2 
(suc y <= a <-> y <= a /\ ~a <= y) -> y <= a /\ ~a <= y -> suc y <= a
29 ltlenle 
y < a <-> y <= a /\ ~a <= y
30 29 conv lt 
suc y <= a <-> y <= a /\ ~a <= y
31 28, 30 ax_mp 
y <= a /\ ~a <= y -> suc y <= a
32 31 exp 
y <= a -> ~a <= y -> suc y <= a
33 27, 32 syl5 
y <= a -> ~a < suc y -> suc y <= a
34 33 conv or 
y <= a -> a < suc y \/ suc y <= a
35 21, 34 ax_mp 
a < y \/ y <= a -> a < suc y \/ suc y <= a
36 3, 6, 9, 12, 15, 35 ind 
a < b \/ b <= a

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_peano (peano1, peano2, peano5, addeq, add0, addS)