Theorem card0 ≪ | index | src | ≫ 

pub theorem card0: $ card 0 = 0 $;
StepHypRefExpression
1 eqtr 
card 0 = ((\ i, card i) |` upto 0) @ (0 // 2) + 0 % 2 -> ((\ i, card i) |` upto 0) @ (0 // 2) + 0 % 2 = 0 -> card 0 = 0
2 cardvallem 
card 0 = ((\ i, card i) |` upto 0) @ (0 // 2) + 0 % 2
3 1, 2 ax_mp 
((\ i, card i) |` upto 0) @ (0 // 2) + 0 % 2 = 0 -> card 0 = 0
4 eqtr 
((\ i, card i) |` upto 0) @ (0 // 2) + 0 % 2 = 0 + 0 -> 0 + 0 = 0 -> ((\ i, card i) |` upto 0) @ (0 // 2) + 0 % 2 = 0
5 addeq 
((\ i, card i) |` upto 0) @ (0 // 2) = 0 -> 0 % 2 = 0 -> ((\ i, card i) |` upto 0) @ (0 // 2) + 0 % 2 = 0 + 0
6 ndmapp 
~0 // 2 e. Dom ((\ i, card i) |` upto 0) -> ((\ i, card i) |` upto 0) @ (0 // 2) = 0
7 eleq2 
Dom ((\ i, card i) |` upto 0) == 0 -> (0 // 2 e. Dom ((\ i, card i) |` upto 0) <-> 0 // 2 e. 0)
8 eqstr 
Dom ((\ i, card i) |` upto 0) == upto 0 -> upto 0 == 0 -> Dom ((\ i, card i) |` upto 0) == 0
9 dmreslam 
Dom ((\ i, card i) |` upto 0) == upto 0
10 8, 9 ax_mp 
upto 0 == 0 -> Dom ((\ i, card i) |` upto 0) == 0
11 nseq 
upto 0 = 0 -> upto 0 == 0
12 upto0 
upto 0 = 0
13 11, 12 ax_mp 
upto 0 == 0
14 10, 13 ax_mp 
Dom ((\ i, card i) |` upto 0) == 0
15 7, 14 ax_mp 
0 // 2 e. Dom ((\ i, card i) |` upto 0) <-> 0 // 2 e. 0
16 el02 
~0 // 2 e. 0
17 15, 16 mtbir 
~0 // 2 e. Dom ((\ i, card i) |` upto 0)
18 6, 17 ax_mp 
((\ i, card i) |` upto 0) @ (0 // 2) = 0
19 5, 18 ax_mp 
0 % 2 = 0 -> ((\ i, card i) |` upto 0) @ (0 // 2) + 0 % 2 = 0 + 0
20 mod01 
0 % 2 = 0
21 19, 20 ax_mp 
((\ i, card i) |` upto 0) @ (0 // 2) + 0 % 2 = 0 + 0
22 4, 21 ax_mp 
0 + 0 = 0 -> ((\ i, card i) |` upto 0) @ (0 // 2) + 0 % 2 = 0
23 add0 
0 + 0 = 0
24 22, 23 ax_mp 
((\ i, card i) |` upto 0) @ (0 // 2) + 0 % 2 = 0
25 3, 24 ax_mp 
card 0 = 0

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)