Theorem cardb1 | index | src |

theorem cardb1 (n: nat): $ card (b1 n) = suc (card n) $;
StepHypRefExpression
1 eqtr
card (b1 n) = card (b1 n // 2) + b1 n % 2 -> card (b1 n // 2) + b1 n % 2 = suc (card n) -> card (b1 n) = suc (card n)
2 cardval
b1 n != 0 -> card (b1 n) = card (b1 n // 2) + b1 n % 2
3 b1ne0
b1 n != 0
4 2, 3 ax_mp
card (b1 n) = card (b1 n // 2) + b1 n % 2
5 1, 4 ax_mp
card (b1 n // 2) + b1 n % 2 = suc (card n) -> card (b1 n) = suc (card n)
6 eqtr
card (b1 n // 2) + b1 n % 2 = card n + 1 -> card n + 1 = suc (card n) -> card (b1 n // 2) + b1 n % 2 = suc (card n)
7 addeq
card (b1 n // 2) = card n -> b1 n % 2 = 1 -> card (b1 n // 2) + b1 n % 2 = card n + 1
8 cardeq
b1 n // 2 = n -> card (b1 n // 2) = card n
9 b1div2
b1 n // 2 = n
10 8, 9 ax_mp
card (b1 n // 2) = card n
11 7, 10 ax_mp
b1 n % 2 = 1 -> card (b1 n // 2) + b1 n % 2 = card n + 1
12 b1mod2
b1 n % 2 = 1
13 11, 12 ax_mp
card (b1 n // 2) + b1 n % 2 = card n + 1
14 6, 13 ax_mp
card n + 1 = suc (card n) -> card (b1 n // 2) + b1 n % 2 = suc (card n)
15 add12
card n + 1 = suc (card n)
16 14, 15 ax_mp
card (b1 n // 2) + b1 n % 2 = suc (card n)
17 5, 16 ax_mp
card (b1 n) = suc (card 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, muleq, add0, addS, mul0, mulS)