Theorem cardvallem ≪ | index | src | ≫ 

theorem cardvallem {i: nat} (n: nat):
  $ card n = ((\ i, card i) |` upto n) @ (n // 2) + n % 2 $;
StepHypRefExpression
1 eqtr 
card n = (\ f, f @ (size (Dom f) // 2) + size (Dom f) % 2) @ (\. i e. upto n, srec (\ f, f @ (size (Dom f) // 2) + size (Dom f) % 2) i) ->
  (\ f, f @ (size (Dom f) // 2) + size (Dom f) % 2) @ (\. i e. upto n, srec (\ f, f @ (size (Dom f) // 2) + size (Dom f) % 2) i) =
    ((\ i, card i) |` upto n) @ (n // 2) + n % 2 ->
  card n = ((\ i, card i) |` upto n) @ (n // 2) + n % 2
2 srecval 
srec (\ f, f @ (size (Dom f) // 2) + size (Dom f) % 2) n =
  (\ f, f @ (size (Dom f) // 2) + size (Dom f) % 2) @ (\. i e. upto n, srec (\ f, f @ (size (Dom f) // 2) + size (Dom f) % 2) i)
3 2 conv card 
card n = (\ f, f @ (size (Dom f) // 2) + size (Dom f) % 2) @ (\. i e. upto n, srec (\ f, f @ (size (Dom f) // 2) + size (Dom f) % 2) i)
4 1, 3 ax_mp 
(\ f, f @ (size (Dom f) // 2) + size (Dom f) % 2) @ (\. i e. upto n, srec (\ f, f @ (size (Dom f) // 2) + size (Dom f) % 2) i) =
    ((\ i, card i) |` upto n) @ (n // 2) + n % 2 ->
  card n = ((\ i, card i) |` upto n) @ (n // 2) + n % 2
5 bi2 
(f == (\ i, card i) |` upto n <-> f = \. i e. upto n, card i) -> f = \. i e. upto n, card i -> f == (\ i, card i) |` upto n
6 eqlower2 
finite ((\ i, card i) |` upto n) -> (f == (\ i, card i) |` upto n <-> f = lower ((\ i, card i) |` upto n))
7 6 conv rlam 
finite ((\ i, card i) |` upto n) -> (f == (\ i, card i) |` upto n <-> f = \. i e. upto n, card i)
8 finlam 
finite (upto n) -> finite ((\ i, card i) |` upto n)
9 finns 
finite (upto n)
10 8, 9 ax_mp 
finite ((\ i, card i) |` upto n)
11 7, 10 ax_mp 
f == (\ i, card i) |` upto n <-> f = \. i e. upto n, card i
12 5, 11 ax_mp 
f = \. i e. upto n, card i -> f == (\ i, card i) |` upto n
13 sreclem 
f = \. i e. upto n, card i -> size (Dom f) = n
14 13 diveq1d 
f = \. i e. upto n, card i -> size (Dom f) // 2 = n // 2
15 12, 14 appeqd 
f = \. i e. upto n, card i -> f @ (size (Dom f) // 2) = ((\ i, card i) |` upto n) @ (n // 2)
16 13 modeq1d 
f = \. i e. upto n, card i -> size (Dom f) % 2 = n % 2
17 15, 16 addeqd 
f = \. i e. upto n, card i -> f @ (size (Dom f) // 2) + size (Dom f) % 2 = ((\ i, card i) |` upto n) @ (n // 2) + n % 2
18 17 applame 
(\ f, f @ (size (Dom f) // 2) + size (Dom f) % 2) @ (\. i e. upto n, card i) = ((\ i, card i) |` upto n) @ (n // 2) + n % 2
19 18 conv card 
(\ f, f @ (size (Dom f) // 2) + size (Dom f) % 2) @ (\. i e. upto n, srec (\ f, f @ (size (Dom f) // 2) + size (Dom f) % 2) i) =
  ((\ i, card i) |` upto n) @ (n // 2) + n % 2
20 4, 19 ax_mp 
card n = ((\ i, card i) |` upto n) @ (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)