Theorem subpos ≪ | index | src | ≫ 

theorem subpos (a b: nat): $ a < b <-> 0 < b - a $;
StepHypRefExpression
1 bitr 
(a < b <-> ~b <= a) -> (~b <= a <-> 0 < b - a) -> (a < b <-> 0 < b - a)
2 ltnle 
a < b <-> ~b <= a
3 1, 2 ax_mp 
(~b <= a <-> 0 < b - a) -> (a < b <-> 0 < b - a)
4 bitr4 
(~b <= a <-> ~b - a = 0) -> (0 < b - a <-> ~b - a = 0) -> (~b <= a <-> 0 < b - a)
5 noteq 
(b <= a <-> b - a = 0) -> (~b <= a <-> ~b - a = 0)
6 lesubeq0 
b <= a <-> b - a = 0
7 5, 6 ax_mp 
~b <= a <-> ~b - a = 0
8 4, 7 ax_mp 
(0 < b - a <-> ~b - a = 0) -> (~b <= a <-> 0 < b - a)
9 lt01 
0 < b - a <-> b - a != 0
10 9 conv ne 
0 < b - a <-> ~b - a = 0
11 8, 10 ax_mp 
~b <= a <-> 0 < b - a
12 3, 11 ax_mp 
a < b <-> 0 < 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_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, add0, addS)