deffunc H₁( Element of NAT , Element of NAT ) -> Element of NAT = $1 |^ ($1 |-count $2);
defpred S₁[ Element of NAT , Element of NAT ] means $1 |-count $2 > 0 ;
let n, m be Element of NAT ; :: thesis: ( 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 ; :: thesis: ( 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 = { H₁(k,m) where k is prime Element of NAT : ( k <= r & S₁[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 ; :: thesis: 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;

now :: thesis: for x being object st x in { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } holds
x in Seg m

let x be object ; :: thesis: ( x in { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } implies x in Seg m )
assume x in { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } ; :: thesis: x in Seg m
then consider p being prime Element of NAT such that
B1: ( p |^ (p |-count m) = x & p <= sqrt (2 * n) & p |-count m > 0 ) ;
( 1 <= p |^ (p |-count m) & p |^ (p |-count m) <= m ) by A5, Th16;
hence x in Seg m by B1, FINSEQ_1:1; :: thesis: verum

end;

then A6: { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } c= Seg m ;
then a6: { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } is included_in_Seg by FINSEQ_1:def 13;

A7: now :: thesis: for k being Element of NAT st k in dom (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } ) holds
( (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } ) . k <= ((len (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } )) |-> (2 * n)) . k & (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } ) . k > 0 )

let k be Element of NAT ; :: thesis: ( k in dom (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } ) implies ( (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } ) . k <= ((len (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } )) |-> (2 * n)) . k & (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } ) . k > 0 ) )
assume A8: k in dom (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } ) ; :: thesis: ( (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } ) . k <= ((len (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } )) |-> (2 * n)) . k & (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } ) . k > 0 )
rng (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } ) = { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } by a6, FINSEQ_1:def 14;
then (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } ) . k in { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } by A8, FUNCT_1:3;
then A9: ex p being prime Element of NAT st
( p |^ (p |-count m) = (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } ) . k & p <= sqrt (2 * n) & p |-count m > 0 ) ;
k in Seg (len (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } )) by A8, FINSEQ_1:def 3;
then ((len (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } )) |-> (2 * n)) . k = 2 * n by FUNCOP_1:7;
hence ( (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } ) . k <= ((len (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } )) |-> (2 * n)) . k & (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } ) . k > 0 ) by A1, A4, A9, Lm9; :: thesis: verum

end;

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; :: thesis: verum