Theorem b0ltid ≪ | index | src | ≫ 

theorem b0ltid (n: nat): $ n != 0 <-> n < b0 n $;
StepHypRefExpression
1 bitr3 
(0 < n <-> n != 0) -> (0 < n <-> n < b0 n) -> (n != 0 <-> n < b0 n)
2 lt01 
0 < n <-> n != 0
3 1, 2 ax_mp 
(0 < n <-> n < b0 n) -> (n != 0 <-> n < b0 n)
4 bitr 
(0 < n <-> n + 0 < n + n) -> (n + 0 < n + n <-> n < b0 n) -> (0 < n <-> n < b0 n)
5 ltadd2 
0 < n <-> n + 0 < n + n
6 4, 5 ax_mp 
(n + 0 < n + n <-> n < b0 n) -> (0 < n <-> n < b0 n)
7 lteq1 
n + 0 = n -> (n + 0 < n + n <-> n < n + n)
8 7 conv b0 
n + 0 = n -> (n + 0 < n + n <-> n < b0 n)
9 add0 
n + 0 = n
10 8, 9 ax_mp 
n + 0 < n + n <-> n < b0 n
11 6, 10 ax_mp 
0 < n <-> n < b0 n
12 3, 11 ax_mp 
n != 0 <-> n < b0 n

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)