Theorem cardb0 | index | src |

theorem cardb0 (n: nat): $ card (b0 n) = card n $;
StepHypRefExpression
1 b00
b0 0 = 0
2 b0eq
n = 0 -> b0 n = b0 0
3 id
n = 0 -> n = 0
4 2, 3 eqeqd
n = 0 -> (b0 n = n <-> b0 0 = 0)
5 1, 4 mpbiri
n = 0 -> b0 n = n
6 5 cardeqd
n = 0 -> card (b0 n) = card n
7 add0
card n + 0 = card n
8 addeq
card (b0 n // 2) = card n -> b0 n % 2 = 0 -> card (b0 n // 2) + b0 n % 2 = card n + 0
9 cardeq
b0 n // 2 = n -> card (b0 n // 2) = card n
10 b0div2
b0 n // 2 = n
11 9, 10 ax_mp
card (b0 n // 2) = card n
12 8, 11 ax_mp
b0 n % 2 = 0 -> card (b0 n // 2) + b0 n % 2 = card n + 0
13 b0mod2
b0 n % 2 = 0
14 12, 13 ax_mp
card (b0 n // 2) + b0 n % 2 = card n + 0
15 b0ne0
b0 n != 0 <-> n != 0
16 15 conv ne
b0 n != 0 <-> ~n = 0
17 cardval
b0 n != 0 -> card (b0 n) = card (b0 n // 2) + b0 n % 2
18 16, 17 sylbir
~n = 0 -> card (b0 n) = card (b0 n // 2) + b0 n % 2
19 14, 18 syl6eq
~n = 0 -> card (b0 n) = card n + 0
20 7, 19 syl6eq
~n = 0 -> card (b0 n) = card n
21 6, 20 cases
card (b0 n) = 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)