Theorem le11 ≪ | index | src | ≫ 

theorem le11 (a: nat): $ 1 <= a <-> a != 0 $;
StepHypRefExpression
1 bitr4 
(1 <= a <-> E. x a = suc x) -> (a != 0 <-> E. x a = suc x) -> (1 <= a <-> a != 0)
2 bitr 
(1 + x = a <-> a = 1 + x) -> (a = 1 + x <-> a = suc x) -> (1 + x = a <-> a = suc x)
3 eqcomb 
1 + x = a <-> a = 1 + x
4 2, 3 ax_mp 
(a = 1 + x <-> a = suc x) -> (1 + x = a <-> a = suc x)
5 eqeq2 
1 + x = suc x -> (a = 1 + x <-> a = suc x)
6 add11 
1 + x = suc x
7 5, 6 ax_mp 
a = 1 + x <-> a = suc x
8 4, 7 ax_mp 
1 + x = a <-> a = suc x
9 8 exeqi 
E. x 1 + x = a <-> E. x a = suc x
10 9 conv le 
1 <= a <-> E. x a = suc x
11 1, 10 ax_mp 
(a != 0 <-> E. x a = suc x) -> (1 <= a <-> a != 0)
12 exsuc 
a != 0 <-> E. x a = suc x
13 11, 12 ax_mp 
1 <= a <-> a != 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_peano (peano1, peano2, peano5, addeq, add0, addS)