Theorem lesubeq0 ≪ | index | src | ≫ 

theorem lesubeq0 (a b: nat): $ a <= b <-> a - b = 0 $;
StepHypRefExpression
1 leloe 
a <= b <-> a < b \/ a = b
2 eor 
(a < b -> a - b = 0) -> (a = b -> a - b = 0) -> a < b \/ a = b -> a - b = 0
3 ltsubeq0 
a < b -> a - b = 0
4 2, 3 ax_mp 
(a = b -> a - b = 0) -> a < b \/ a = b -> a - b = 0
5 subid 
b - b = 0
6 subeq1 
a = b -> a - b = b - b
7 5, 6 syl6eq 
a = b -> a - b = 0
8 4, 7 ax_mp 
a < b \/ a = b -> a - b = 0
9 1, 8 sylbi 
a <= b -> a - b = 0
10 contra 
(~a <= b -> a <= b) -> a <= b
11 eqle 
a = b -> a <= b
12 npcan 
b <= a -> a - b + b = a
13 leorle 
a <= b \/ b <= a
14 13 conv or 
~a <= b -> b <= a
15 14 anwr 
a - b = 0 /\ ~a <= b -> b <= a
16 12, 15 syl 
a - b = 0 /\ ~a <= b -> a - b + b = a
17 add01 
0 + b = b
18 addeq1 
a - b = 0 -> a - b + b = 0 + b
19 18 anwl 
a - b = 0 /\ ~a <= b -> a - b + b = 0 + b
20 17, 19 syl6eq 
a - b = 0 /\ ~a <= b -> a - b + b = b
21 16, 20 eqtr3d 
a - b = 0 /\ ~a <= b -> a = b
22 11, 21 syl 
a - b = 0 /\ ~a <= b -> a <= b
23 10, 22 syla 
a - b = 0 -> a <= b
24 9, 23 ibii 
a <= b <-> a - b = 0

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)