Theorem boolnat | index | src |

theorem boolnat (p: wff): $ bool (nat p) $;
StepHypRefExpression
1 d1lt2
1 < 2
2 ifpos
p -> if p 1 0 = 1
3 2 conv nat
p -> nat p = 1
4 3 lteq1d
p -> (nat p < 2 <-> 1 < 2)
5 4 conv bool
p -> (bool (nat p) <-> 1 < 2)
6 1, 5 mpbiri
p -> bool (nat p)
7 d0lt2
0 < 2
8 ifneg
~p -> if p 1 0 = 0
9 8 conv nat
~p -> nat p = 0
10 9 lteq1d
~p -> (nat p < 2 <-> 0 < 2)
11 10 conv bool
~p -> (bool (nat p) <-> 0 < 2)
12 7, 11 mpbiri
~p -> bool (nat p)
13 6, 12 cases
bool (nat p)

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), axs_peano (peano1, peano2, peano5, addeq, add0, addS)