deffunc H1( Element of NAT , Element of NAT ) -> Element of NAT = $1 |^ ($1 |-count $2);
defpred S1[ Element of NAT , Element of NAT ] means $1 |-count $2 > 0 ;
let n, m be Element of NAT ; ( m = (2 * n) choose n & n >= 3 implies Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } ) <= (2 * n) to_power (sqrt (2 * n)) )
assume A1:
m = (2 * n) choose n
; ( not n >= 3 or Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } ) <= (2 * n) to_power (sqrt (2 * n)) )
set r = sqrt (2 * n);
A2:
sqrt (2 * n) >= 0
by SQUARE_1:def 2;
A3:
for n, m being Element of NAT
for r being Real
for X being finite set st X = { H1(k,m) where k is prime Element of NAT : ( k <= r & S1[k,m] ) } & r >= 0 holds
card X <= [\r/]
from NAT_4:sch 4();
set XX = Seg m;
set X = { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } ;
assume A4:
n >= 3
; Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } ) <= (2 * n) to_power (sqrt (2 * n))
set f1 = Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } ;
set f2 = (len (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } )) |-> (2 * n);
m * (2 * n) >= ((4 |^ n) / (2 * n)) * (2 * n)
by A1, Th6, XREAL_1:64;
then A5:
m <> 0
by A4;
then A6:
{ (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } c= Seg m
;
reconsider X = { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } as finite set by A6;
A10:
len (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } ) = len ((len (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } )) |-> (2 * n))
by CARD_1:def 7;
rng (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } ) c= REAL
;
then reconsider f1 = Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } as FinSequence of REAL by FINSEQ_1:def 4;
A11:
rng ((len (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } )) |-> (2 * n)) c= REAL
;
reconsider rr = sqrt (2 * n) as Real ;
A12:
rr >= 0
by A2;
len f1 = card X
by A6, FINSEQ_3:39;
then
( [\(sqrt (2 * n))/] <= sqrt (2 * n) & len f1 <= [\(sqrt (2 * n))/] )
by A12, A3, INT_1:def 6;
then
len f1 <= sqrt (2 * n)
by XXREAL_0:2;
then A13:
( len f1 < sqrt (2 * n) or len f1 = sqrt (2 * n) )
by XXREAL_0:1;
reconsider f2 = (len (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } )) |-> (2 * n) as FinSequence of REAL by A11, FINSEQ_1:def 4;
Product f1 <= Product f2
by A10, A7, Th53;
then A14:
Product f1 <= (2 * n) to_power (len f1)
by A4, Th54;
n * 2 >= 3 * 2
by A4, XREAL_1:64;
then
2 * n > 1
by XXREAL_0:2;
then
(2 * n) to_power (len f1) <= (2 * n) to_power (sqrt (2 * n))
by A13, POWER:39;
hence
Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } ) <= (2 * n) to_power (sqrt (2 * n))
by A14, XXREAL_0:2; verum