let n, k be Nat; ( k > 0 & n > (2 * k) |^ (k + 1) implies k ! = [\((n |^ k) / (n choose k))/] )
set k1 = k + 1;
assume A1:
( k > 0 & n > (2 * k) |^ (k + 1) )
; k ! = [\((n |^ k) / (n choose k))/]
A2:
( 2 * k >= 1 & k >= 1 )
by A1, NAT_1:14;
k + 1 >= 1
by NAT_1:11;
then
(2 * k) |^ (k + 1) >= 2 * k
by A2, PREPOWER:12;
then A3:
n > 2 * k
by A1, XXREAL_0:2;
k + 1 > 1 + 0
by A1, XREAL_1:6;
then
k + 1 >= 1 + 1
by NAT_1:13;
then A4:
(2 * k) |^ (k + 1) >= (2 * k) |^ (1 + 1)
by A1, NAT_6:1;
(2 * k) |^ (1 + 1) =
((2 * k) |^ 1) * (2 * k)
by NEWTON:6
.=
(2 * k) * (2 * k)
;
then A5:
n > (4 * k) * k
by A1, A4, XXREAL_0:2;
(4 * k) * k >= (4 * k) * 1
by A1, NAT_1:14, XREAL_1:64;
then A6:
1 * n > 2 * (2 * k)
by A5, XXREAL_0:2;
k + k >= k
by NAT_1:11;
then A7:
n > k
by A3, XXREAL_0:2;
then A8:
(n |^ k) / (n choose k) <= ((k !) * 1) / ((1 - (k / n)) |^ k)
by Lm2;
A9:
1 / ((1 - (k / n)) |^ k) = (1 / (1 - (k / n))) |^ k
by PREPOWER:7;
A10:
n - k > 0
by A7, XREAL_1:50;
A11:
1 / (1 - (k / n)) = n / (n - k)
by A7, Lm1;
1 / (1 - (k / n)) <= 1 + ((2 * k) / n)
by A1, A3, Lm3;
then A12:
1 / ((1 - (k / n)) |^ k) <= (1 + ((2 * k) / n)) |^ k
by A9, A11, A1, A10, PREPOWER:9;
(1 + ((2 * k) / n)) |^ k < 1 + (((2 * k) / n) * (2 |^ k))
by A6, XREAL_1:106, A1, Lm5;
then
1 / ((1 - (k / n)) |^ k) < 1 + (((2 * k) / n) * (2 |^ k))
by A12, XXREAL_0:2;
then
(k !) * (1 / ((1 - (k / n)) |^ k)) < (k !) * (1 + (((2 * k) / n) * (2 |^ k)))
by XREAL_1:68;
then
((k !) * 1) / ((1 - (k / n)) |^ k) < (k !) * (1 + (((2 * k) / n) * (2 |^ k)))
by XCMPLX_1:74;
then A13:
(n |^ k) / (n choose k) < (k !) * (1 + (((2 * k) / n) * (2 |^ k)))
by A8, XXREAL_0:2;
((2 * k) / n) * (2 |^ k) = ((2 * k) * (2 |^ k)) / n
by XCMPLX_1:74;
then A14: ((k !) * ((2 * k) / n)) * (2 |^ k) =
(k !) * (((2 * k) * (2 |^ k)) / n)
.=
((k !) * ((2 * k) * (2 |^ k))) / n
by XCMPLX_1:74
.=
(((k !) * (2 * k)) * (2 |^ k)) / n
;
(((k !) * (2 * k)) * (2 |^ k)) / n < (((k !) * (2 * k)) * (2 |^ k)) / ((2 * k) |^ (k + 1))
by A1, XREAL_1:76;
then
(k !) + ((((k !) * (2 * k)) * (2 |^ k)) / n) < (k !) + ((((k !) * (2 * k)) * (2 |^ k)) / ((2 * k) |^ (k + 1)))
by XREAL_1:6;
then A15:
(n |^ k) / (n choose k) < (k !) + ((((k !) * (2 * k)) * (2 |^ k)) / ((2 * k) |^ (k + 1)))
by A13, XXREAL_0:2, A14;
A16: (2 * k) * (2 |^ k) =
k * (2 * (2 |^ k))
.=
k * (2 |^ (k + 1))
by NEWTON:6
;
A17: ((2 * k) * (2 |^ k)) / ((2 * k) |^ (k + 1)) =
(k * (2 |^ (k + 1))) / ((2 |^ (k + 1)) * (k |^ (k + 1)))
by A16, NEWTON:7
.=
k / (k |^ (k + 1))
by XCMPLX_1:91
.=
k / (k * (k |^ k))
by NEWTON:6
;
A18: (((k !) * (2 * k)) * (2 |^ k)) / ((2 * k) |^ (k + 1)) =
((k !) * ((2 * k) * (2 |^ k))) / ((2 * k) |^ (k + 1))
.=
(k !) * (k / (k * (k |^ k)))
by A17, XCMPLX_1:74
.=
((k !) * k) / (k * (k |^ k))
by XCMPLX_1:74
.=
(k !) / (k |^ k)
by A1, XCMPLX_1:91
;
(k !) / (k |^ k) <= 1
by XREAL_1:183, NEWTON02:124;
then
(k !) + ((((k !) * (2 * k)) * (2 |^ k)) / ((2 * k) |^ (k + 1))) <= (k !) + 1
by A18, XREAL_1:6;
then
(n |^ k) / (n choose k) < (k !) + 1
by A15, XXREAL_0:2;
then A19:
((n |^ k) / (n choose k)) - 1 < k !
by XREAL_1:19;
k ! <= (n |^ k) / (n choose k)
by A7, Lm4;
hence
k ! = [\((n |^ k) / (n choose k))/]
by INT_1:def 6, A19; verum