Theorem cardval ≪ | index | src | ≫ 

theorem cardval (n: nat): $ n != 0 -> card n = card (n // 2) + n % 2 $;
StepHypRefExpression
1 cardvallem 
card n = ((\ i, card i) |` upto n) @ (n // 2) + n % 2
2 cardeq 
i = n // 2 -> card i = card (n // 2)
3 2 applame 
(\ i, card i) @ (n // 2) = card (n // 2)
4 resapp 
n // 2 e. upto n -> ((\ i, card i) |` upto n) @ (n // 2) = (\ i, card i) @ (n // 2)
5 elupto 
n // 2 e. upto n <-> n // 2 < n
6 lt01 
0 < n <-> n != 0
7 div2lt 
0 < n -> n // 2 < n
8 6, 7 sylbir 
n != 0 -> n // 2 < n
9 5, 8 sylibr 
n != 0 -> n // 2 e. upto n
10 4, 9 syl 
n != 0 -> ((\ i, card i) |` upto n) @ (n // 2) = (\ i, card i) @ (n // 2)
11 3, 10 syl6eq 
n != 0 -> ((\ i, card i) |` upto n) @ (n // 2) = card (n // 2)
12 11 addeq1d 
n != 0 -> ((\ i, card i) |` upto n) @ (n // 2) + n % 2 = card (n // 2) + n % 2
13 1, 12 syl5eq 
n != 0 -> card n = card (n // 2) + n % 2

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)