let x be Real; :: thesis: ( x >= 2 implies Product (Sgm { p where p is prime Element of NAT : p <= x } ) <= 4 to_power (x - 1) )
assume A1: x >= 2 ; :: thesis: Product (Sgm { p where p is prime Element of NAT : p <= x } ) <= 4 to_power (x - 1)
set A = { p where p is prime Element of NAT : p <= x } ;
A2: { p where p is prime Element of NAT : p <= x } is finite

proof

ex m being Element of NAT st x < m

proof

set m = (abs [/x\]) + 1;
take (abs [/x\]) + 1 ; :: thesis: x < (abs [/x\]) + 1
A3: x <= [/x\] by INT_1:def 5;
A4: [/x\] <= abs [/x\] by ABSVALUE:11;
abs [/x\] < (abs [/x\]) + 1 by NAT_1:13;
then [/x\] < (abs [/x\]) + 1 by A4, XXREAL_0:2;
hence x < (abs [/x\]) + 1 by A3, XXREAL_0:2; :: thesis: verum

end;

then consider m being Element of NAT such that
A5: x < m ;
set B = SetPrimenumber m;
{ p where p is prime Element of NAT : p <= x } c= SetPrimenumber m

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in { p where p is prime Element of NAT : p <= x } or y in SetPrimenumber m )
assume y in { p where p is prime Element of NAT : p <= x } ; :: thesis: y in SetPrimenumber m
then consider y' being prime Element of NAT such that
A6: ( y' = y & y' <= x ) ;
( y' = y & y' < m ) by A5, A6, XXREAL_0:2;
hence y in SetPrimenumber m by NEWTON:def 7; :: thesis: verum

end;

hence { p where p is prime Element of NAT : p <= x } is finite ; :: thesis: verum

end;

A7: not { p where p is prime Element of NAT : p <= x } is empty

proof

assume A8: { p where p is prime Element of NAT : p <= x } is empty ; :: thesis: contradiction
2 in { p where p is prime Element of NAT : p <= x } by A1, INT_2:44;
hence contradiction by A8; :: thesis: verum

end;

{ p where p is prime Element of NAT : p <= x } is real-membered

proof

let y be set ; :: according to MEMBERED:def 3 :: thesis: ( not y in { p where p is prime Element of NAT : p <= x } or y is real )
( y in { p where p is prime Element of NAT : p <= x } implies y is real )

proof

assume y in { p where p is prime Element of NAT : p <= x } ; :: thesis: y is real
then ex y' being prime Element of NAT st
( y' = y & y' <= x ) ;
hence y is real ; :: thesis: verum

end;

hence ( not y in { p where p is prime Element of NAT : p <= x } or y is real ) ; :: thesis: verum

end;

then reconsider A = { p where p is prime Element of NAT : p <= x } as non empty finite real-membered set by A2, A7;
set q = max A;
max A in A by XXREAL_2:def 8;
then consider q' being prime Element of NAT such that
A9: ( q' = max A & q' <= x ) ;
reconsider q = max A as Prime by A9;
A10: { p where p is prime Element of NAT : p <= q } = { p where p is prime Element of NAT : p <= x }

proof

for y being set holds
( y in { p where p is prime Element of NAT : p <= q } iff y in { p where p is prime Element of NAT : p <= x } )

proof

let y be set ; :: thesis: ( y in { p where p is prime Element of NAT : p <= q } iff y in { p where p is prime Element of NAT : p <= x } )

hereby :: thesis: ( y in { p where p is prime Element of NAT : p <= x } implies y in { p where p is prime Element of NAT : p <= q } )

assume y in { p where p is prime Element of NAT : p <= q } ; :: thesis: y in { p where p is prime Element of NAT : p <= x }
then consider y' being prime Element of NAT such that
A11: ( y' = y & y' <= q ) ;
y' <= x by A9, A11, XXREAL_0:2;
hence y in { p where p is prime Element of NAT : p <= x } by A11; :: thesis: verum

end;

assume A12: y in { p where p is prime Element of NAT : p <= x } ; :: thesis: y in { p where p is prime Element of NAT : p <= q }
then consider y' being prime Element of NAT such that
A13: ( y' = y & y' <= x ) ;
y' <= q by A12, A13, XXREAL_2:def 8;
hence y in { p where p is prime Element of NAT : p <= q } by A13; :: thesis: verum

end;

hence { p where p is prime Element of NAT : p <= q } = { p where p is prime Element of NAT : p <= x } by TARSKI:2; :: thesis: verum

end;

A14: 4 to_power (q - 1) <= 4 to_power (x - 1)

proof

per cases ( q = x or q < x ) by A9, XXREAL_0:1;

suppose q = x ; :: thesis: 4 to_power (q - 1) <= 4 to_power (x - 1)

hence 4 to_power (q - 1) <= 4 to_power (x - 1) ; :: thesis: verum

end;

suppose q < x ; :: thesis: 4 to_power (q - 1) <= 4 to_power (x - 1)

then q - 1 < x - 1 by XREAL_1:16;
hence 4 to_power (q - 1) <= 4 to_power (x - 1) by POWER:44; :: thesis: verum

end;

end;

end;

Product (Sgm { p where p is prime Element of NAT : p <= x } ) <= 4 to_power (x - 1)

proof

q > 1 by Lm1;
then A15: q -' 1 = q - 1 by XREAL_1:235;
set n = q -' 1;
A16: q = (q -' 1) + 1 by A15;
set a = Product (Sgm { p where p is prime Element of NAT : p <= q } );
set b = 4 to_power (q - 1);
Product (Sgm { p where p is prime Element of NAT : p <= q } ) <= 4 to_power (q - 1) by A16, Th45;
hence Product (Sgm { p where p is prime Element of NAT : p <= x } ) <= 4 to_power (x - 1) by A10, A14, XXREAL_0:2; :: thesis: verum

end;

hence Product (Sgm { p where p is prime Element of NAT : p <= x } ) <= 4 to_power (x - 1) ; :: thesis: verum