Theorem leloe ≪ | index | src | ≫ 

theorem leloe (a b: nat): $ a <= b <-> a < b \/ a = b $;
StepHypRefExpression
1 add0 
a + 0 = a
2 addeq2 
x = 0 -> a + x = a + 0
3 2 anwr 
a + x = b /\ x = 0 -> a + x = a + 0
4 anl 
a + x = b /\ x = 0 -> a + x = b
5 3, 4 eqtr3d 
a + x = b /\ x = 0 -> a + 0 = b
6 1, 5 syl5eqr 
a + x = b /\ x = 0 -> a = b
7 6 orrd 
a + x = b /\ x = 0 -> a < b \/ a = b
8 7 exp 
a + x = b -> x = 0 -> a < b \/ a = b
9 exsuc 
x != 0 <-> E. y x = suc y
10 9 conv ne 
~x = 0 <-> E. y x = suc y
11 leaddid1 
suc a <= suc a + y
12 addSass 
suc a + y = a + suc y
13 addeq2 
x = suc y -> a + x = a + suc y
14 13 anwr 
a + x = b /\ x = suc y -> a + x = a + suc y
15 anl 
a + x = b /\ x = suc y -> a + x = b
16 14, 15 eqtr3d 
a + x = b /\ x = suc y -> a + suc y = b
17 12, 16 syl5eq 
a + x = b /\ x = suc y -> suc a + y = b
18 17 leeq2d 
a + x = b /\ x = suc y -> (suc a <= suc a + y <-> suc a <= b)
19 18 conv lt 
a + x = b /\ x = suc y -> (suc a <= suc a + y <-> a < b)
20 11, 19 mpbii 
a + x = b /\ x = suc y -> a < b
21 20 orld 
a + x = b /\ x = suc y -> a < b \/ a = b
22 21 eexda 
a + x = b -> E. y x = suc y -> a < b \/ a = b
23 10, 22 syl5bi 
a + x = b -> ~x = 0 -> a < b \/ a = b
24 8, 23 casesd 
a + x = b -> a < b \/ a = b
25 24 eex 
E. x a + x = b -> a < b \/ a = b
26 25 conv le 
a <= b -> a < b \/ a = b
27 eor 
(a < b -> a <= b) -> (a = b -> a <= b) -> a < b \/ a = b -> a <= b
28 ltle 
a < b -> a <= b
29 27, 28 ax_mp 
(a = b -> a <= b) -> a < b \/ a = b -> a <= b
30 eqle 
a = b -> a <= b
31 29, 30 ax_mp 
a < b \/ a = b -> a <= b
32 26, 31 ibii 
a <= b <-> a < b \/ a = b

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)