Theorem nattrue ≪ | index | src | ≫ 

theorem nattrue (n: nat): $ bool n -> nat (true n) = n $;
StepHypRefExpression
1 bool01 
bool n <-> n = 0 \/ n = 1
2 eor 
(n = 0 -> nat (true n) = n) -> (n = 1 -> nat (true n) = n) -> n = 0 \/ n = 1 -> nat (true n) = n
3 trueeq 
n = 0 -> (true n <-> true 0)
4 3 nateqd 
n = 0 -> nat (true n) = nat (true 0)
5 ifneg 
~true 0 -> if (true 0) 1 0 = 0
6 5 conv nat 
~true 0 -> nat (true 0) = 0
7 true0 
~true 0
8 6, 7 ax_mp 
nat (true 0) = 0
9 id 
n = 0 -> n = 0
10 8, 9 syl6eqr 
n = 0 -> n = nat (true 0)
11 4, 10 eqtr4d 
n = 0 -> nat (true n) = n
12 2, 11 ax_mp 
(n = 1 -> nat (true n) = n) -> n = 0 \/ n = 1 -> nat (true n) = n
13 trueeq 
n = 1 -> (true n <-> true 1)
14 13 nateqd 
n = 1 -> nat (true n) = nat (true 1)
15 ifpos 
true 1 -> if (true 1) 1 0 = 1
16 15 conv nat 
true 1 -> nat (true 1) = 1
17 true1 
true 1
18 16, 17 ax_mp 
nat (true 1) = 1
19 id 
n = 1 -> n = 1
20 18, 19 syl6eqr 
n = 1 -> n = nat (true 1)
21 14, 20 eqtr4d 
n = 1 -> nat (true n) = n
22 12, 21 ax_mp 
n = 0 \/ n = 1 -> nat (true n) = n
23 1, 22 sylbi 
bool n -> nat (true n) = 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_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, add0, addS)