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) )
set A = { p where p is prime Element of NAT : p <= x } ;
A1: { 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 = |.[/x\].| + 1;
take |.[/x\].| + 1 ; :: thesis: x < |.[/x\].| + 1
( [/x\] <= |.[/x\].| & |.[/x\].| < |.[/x\].| + 1 ) by ABSVALUE:4, NAT_1:13;
then ( x <= [/x\] & [/x\] < |.[/x\].| + 1 ) by INT_1:def 7, XXREAL_0:2;
hence x < |.[/x\].| + 1 by XXREAL_0:2; :: thesis: verum

end;

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

proof

let y be object ; :: 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 y9 being prime Element of NAT such that
A3: y9 = y and
A4: y9 <= x ;
y9 < m by A2, A4, XXREAL_0:2;
hence y in SetPrimenumber m by A3, NEWTON:def 7; :: thesis: verum

end;

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

end;

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

proof

let y be object ; :: 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 y9 being prime Element of NAT st
( y9 = y & y9 <= 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;

assume A6: x >= 2 ; :: thesis: Product (Sgm { p where p is prime Element of NAT : p <= x } ) <= 4 to_power (x - 1)
not { p where p is prime Element of NAT : p <= x } is empty

proof

assume A7: { 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 A6, INT_2:28;
hence contradiction by A7; :: thesis: verum

end;

then reconsider A = { p where p is prime Element of NAT : p <= x } as non empty finite real-membered set by A1, A5;
set q = max A;
max A in A by XXREAL_2:def 8;
then A8: ex q9 being prime Element of NAT st
( q9 = max A & q9 <= x ) ;
then reconsider q = max A as Prime ;
for y being object 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 object ; :: 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 y9 being prime Element of NAT such that
A9: y9 = y and
A10: y9 <= q ;
y9 <= x by A8, A10, XXREAL_0:2;
hence y in { p where p is prime Element of NAT : p <= x } by A9; :: thesis: verum

end;

assume A11: 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 y9 being prime Element of NAT such that
A12: y9 = y and
y9 <= x ;
y9 <= q by A11, A12, XXREAL_2:def 8;
hence y in { p where p is prime Element of NAT : p <= q } by A12; :: thesis: verum

end;

then A13: { p where p is prime Element of NAT : p <= q } = { p where p is prime Element of NAT : p <= x } by TARSKI:2;
A14: 4 to_power (q - 1) <= 4 to_power (x - 1)

proof

per cases ( q = x or q < x ) by A8, 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:14;
hence 4 to_power (q - 1) <= 4 to_power (x - 1) by POWER:39; :: thesis: verum

end;

end;

end;

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

proof

set b = 4 to_power (q - 1);
set a = Product (Sgm { p where p is prime Element of NAT : p <= q } );
set n = q -' 1;
q > 1 by Lm1;
then q -' 1 = q - 1 by XREAL_1:233;
then q = (q -' 1) + 1 ;
then Product (Sgm { p where p is prime Element of NAT : p <= q } ) <= 4 to_power (q - 1) by Th44;
hence Product (Sgm { p where p is prime Element of NAT : p <= x } ) <= 4 to_power (x - 1) by A13, 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