let m, n be Nat; ( 2 * m <= n implies card (Domin_0 (n,m)) = (((n + 1) - (2 * m)) / ((n + 1) - m)) * (n choose m) )
assume A1:
2 * m <= n
; card (Domin_0 (n,m)) = (((n + 1) - (2 * m)) / ((n + 1) - m)) * (n choose m)
now card (Domin_0 (n,m)) = (((n + 1) - (2 * m)) / ((n + 1) - m)) * (n choose m)per cases
( m = 0 or m > 0 )
;
suppose A3:
m > 0
;
card (Domin_0 (n,m)) = (((n + 1) - (2 * m)) / ((n + 1) - m)) * (n choose m)A4:
m <= m + m
by NAT_1:11;
then reconsider nm =
n - m as
Nat by A1, NAT_1:21, XXREAL_0:2;
reconsider m1 =
m - 1 as
Nat by A3, NAT_1:20;
set n9 =
n ! ;
set m9 =
m ! ;
set nm19 =
(nm + 1) ! ;
set nm9 =
nm ! ;
m <= n
by A1, A4, XXREAL_0:2;
then A5:
n choose m = (n !) / ((m !) * (nm !))
by NEWTON:def 3;
A6:
2
* (m1 + 1) <= n
by A1;
set m19 =
m1 ! ;
A7: 1
/ ((m1 !) * ((nm + 1) !)) =
((m1 + 1) * 1) / (((m1 !) * ((nm + 1) !)) * (m1 + 1))
by XCMPLX_1:91
.=
m / (((nm + 1) !) * ((m1 !) * (m1 + 1)))
.=
m / (((nm + 1) !) * ((m1 + 1) !))
by NEWTON:15
.=
- ((- m) / (((nm + 1) !) * (m !)))
by XCMPLX_1:190
;
1
/ ((m !) * (nm !)) =
((nm + 1) * 1) / (((m !) * (nm !)) * (nm + 1))
by XCMPLX_1:91
.=
(nm + 1) / ((m !) * ((nm !) * (nm + 1)))
.=
(nm + 1) / ((m !) * ((nm + 1) !))
by NEWTON:15
;
then A8:
(1 / ((m !) * (nm !))) - (1 / ((m1 !) * ((nm + 1) !))) =
((nm + 1) / ((m !) * ((nm + 1) !))) + ((- m) / ((m !) * ((nm + 1) !)))
by A7
.=
((nm + 1) + (- m)) / ((m !) * ((nm + 1) !))
by XCMPLX_1:62
.=
((n + 1) - (2 * m)) / ((m !) * ((nm !) * (nm + 1)))
by NEWTON:15
.=
(1 * ((n + 1) - (2 * m))) / (((m !) * (nm !)) * (nm + 1))
.=
(1 / ((m !) * (nm !))) * (((n + 1) - (2 * m)) / (nm + 1))
by XCMPLX_1:76
;
m1 <= m1 + ((1 + m1) + 1)
by NAT_1:11;
then A9:
m1 <= n
by A1, XXREAL_0:2;
n - m1 = nm + 1
;
then A10:
n choose m1 = (n !) / ((m1 !) * ((nm + 1) !))
by A9, NEWTON:def 3;
((n !) / ((m !) * (nm !))) - ((n !) / ((m1 !) * ((nm + 1) !))) =
((n !) * (1 / ((m !) * (nm !)))) - ((n !) / ((m1 !) * ((nm + 1) !)))
by XCMPLX_1:99
.=
((n !) * (1 / ((m !) * (nm !)))) - ((n !) * (1 / ((m1 !) * ((nm + 1) !))))
by XCMPLX_1:99
.=
(n !) * ((1 / ((m !) * (nm !))) - (1 / ((m1 !) * ((nm + 1) !))))
.=
(n !) * ((1 / ((m !) * (nm !))) * (((n + 1) - (2 * m)) / (nm + 1)))
by A8
.=
((n !) * (1 / ((m !) * (nm !)))) * (((n + 1) - (2 * m)) / (nm + 1))
.=
(((n !) * 1) / ((m !) * (nm !))) * (((n + 1) - (2 * m)) / (nm + 1))
by XCMPLX_1:74
;
hence
card (Domin_0 (n,m)) = (((n + 1) - (2 * m)) / ((n + 1) - m)) * (n choose m)
by A5, A10, A6, Th28;
verum end;
hence
card (Domin_0 (n,m)) = (((n + 1) - (2 * m)) / ((n + 1) - m)) * (n choose m)
; verum