let n be Element of NAT ; :: thesis: Product (Sgm { p where p is prime Element of NAT : p <= n + 1 } ) <= 4 to_power n
defpred S₁[ Nat] means Product (Sgm { p where p is prime Element of NAT : p <= $1 + 1 } ) <= 4 to_power $1;
A1: for m being Nat st ( for n being Nat st n < m holds
S₁[n] ) holds
S₁[m]

proof

let m be Nat; :: thesis: ( ( for n being Nat st n < m holds
S₁[n] ) implies S₁[m] )
assume A2: for n being Nat st n < m holds
S₁[n] ; :: thesis: S₁[m]

per cases ( m < 1 or m = 1 or m > 1 ) by XXREAL_0:1;

suppose m < 1 ; :: thesis: S₁[m]

then A3: m = 0 by NAT_1:14;

now

assume { p where p is prime Element of NAT : p <= 0 + 1 } <> {} ; :: thesis: contradiction
then consider y being set such that
A4: y in { p where p is prime Element of NAT : p <= 1 } by XBOOLE_0:def 1;
ex y' being prime Element of NAT st
( y' = y & y' <= 1 ) by A4;
hence contradiction by Lm1; :: thesis: verum

end;

hence S₁[m] by A3, FINSEQ_3:49, POWER:29, RVSUM_1:124; :: thesis: verum

end;

suppose A5: m = 1 ; :: thesis: S₁[m]

A6: { p where p is prime Element of NAT : p <= 2 } = {2}

proof

A7: now

let y be set ; :: thesis: ( y in { p where p is prime Element of NAT : p <= 2 } implies y = 2 )
assume y in { p where p is prime Element of NAT : p <= 2 } ; :: thesis: y = 2
then consider y' being prime Element of NAT such that
A8: ( y' = y & y' <= 2 ) ;
y' > 1 by Lm1;
then y' >= 1 + 1 by NAT_1:13;
hence y = 2 by A8, XXREAL_0:1; :: thesis: verum

end;

for y being set st y = 2 holds
y in { p where p is prime Element of NAT : p <= 2 } by INT_2:44;
hence { p where p is prime Element of NAT : p <= 2 } = {2} by A7, TARSKI:def 1; :: thesis: verum

end;

A9: Product (Sgm {2}) = Product <*2*> by FINSEQ_3:50
.= 2 by RVSUM_1:125 ;
4 to_power 1 = 4 by POWER:30;
hence S₁[m] by A5, A6, A9; :: thesis: verum

end;

suppose A10: m > 1 ; :: thesis: S₁[m]

per cases ( not m + 1 is even or m + 1 is even ) ;

suppose not m + 1 is even ; :: thesis: S₁[m]

then consider k being Element of NAT such that
A11: m + 1 = (2 * k) + 1 by ABIAN:9;
set X = { p where p is prime Element of NAT : p <= k + 1 } ;
set Y = { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } ;
A12: { p where p is prime Element of NAT : p <= k + 1 } c= Seg (k + 1)

proof

for y being set st y in { p where p is prime Element of NAT : p <= k + 1 } holds
y in Seg (k + 1)

proof

let y be set ; :: thesis: ( y in { p where p is prime Element of NAT : p <= k + 1 } implies y in Seg (k + 1) )
assume y in { p where p is prime Element of NAT : p <= k + 1 } ; :: thesis: y in Seg (k + 1)
then A13: ex y' being prime Element of NAT st
( y' = y & y' <= k + 1 ) ;
then reconsider y = y as prime Element of NAT ;
y >= 1 by Lm1;
hence y in Seg (k + 1) by A13, FINSEQ_1:3; :: thesis: verum

end;

hence { p where p is prime Element of NAT : p <= k + 1 } c= Seg (k + 1) by TARSKI:def 3; :: thesis: verum

end;

A14: { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } c= Seg ((2 * k) + 1)

proof

for y being set st y in { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } holds
y in Seg ((2 * k) + 1)

proof

let y be set ; :: thesis: ( y in { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } implies y in Seg ((2 * k) + 1) )
assume y in { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } ; :: thesis: y in Seg ((2 * k) + 1)
then A15: ex y' being prime Element of NAT st
( y' = y & y' > k + 1 & y' <= (2 * k) + 1 ) ;
then reconsider y = y as prime Element of NAT ;
y >= 1 by Lm1;
hence y in Seg ((2 * k) + 1) by A15, FINSEQ_1:3; :: thesis: verum

end;

hence { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } c= Seg ((2 * k) + 1) by TARSKI:def 3; :: thesis: verum

end;

A16: { p where p is prime Element of NAT : p <= (2 * k) + 1 } = { p where p is prime Element of NAT : p <= k + 1 } \/ { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) }

proof

for y being set holds
( y in { p where p is prime Element of NAT : p <= (2 * k) + 1 } iff y in { p where p is prime Element of NAT : p <= k + 1 } \/ { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } )

proof

let y be set ; :: thesis: ( y in { p where p is prime Element of NAT : p <= (2 * k) + 1 } iff y in { p where p is prime Element of NAT : p <= k + 1 } \/ { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } )

A17: now

assume y in { p where p is prime Element of NAT : p <= (2 * k) + 1 } ; :: thesis: y in { p where p is prime Element of NAT : p <= k + 1 } \/ { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) }
then consider y' being prime Element of NAT such that
A18: ( y' = y & y' <= (2 * k) + 1 ) ;
( y in { p where p is prime Element of NAT : p <= k + 1 } or y in { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } )

proof

per cases ( ( y' = y & y' <= k + 1 ) or ( y' = y & y' > k + 1 & y' <= (2 * k) + 1 ) ) by A18;

suppose ( y' = y & y' <= k + 1 ) ; :: thesis: ( y in { p where p is prime Element of NAT : p <= k + 1 } or y in { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } )

hence ( y in { p where p is prime Element of NAT : p <= k + 1 } or y in { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } ) ; :: thesis: verum

end;

suppose ( y' = y & y' > k + 1 & y' <= (2 * k) + 1 ) ; :: thesis: ( y in { p where p is prime Element of NAT : p <= k + 1 } or y in { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } )

hence ( y in { p where p is prime Element of NAT : p <= k + 1 } or y in { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } ) ; :: thesis: verum

end;

end;

end;

hence y in { p where p is prime Element of NAT : p <= k + 1 } \/ { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } by XBOOLE_0:def 3; :: thesis: verum

end;

now

assume A19: y in { p where p is prime Element of NAT : p <= k + 1 } \/ { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } ; :: thesis: y in { p where p is prime Element of NAT : p <= (2 * k) + 1 }

per cases ( y in { p where p is prime Element of NAT : p <= k + 1 } or y in { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } ) by A19, XBOOLE_0:def 3;

suppose y in { p where p is prime Element of NAT : p <= k + 1 } ; :: thesis: y in { p where p is prime Element of NAT : p <= (2 * k) + 1 }

then consider y' being prime Element of NAT such that
A20: ( y' = y & y' <= k + 1 ) ;
1 * k <= 2 * k by XREAL_1:70;
then k + 1 <= (2 * k) + 1 by XREAL_1:8;
then ( y' = y & y' <= (2 * k) + 1 ) by A20, XXREAL_0:2;
hence y in { p where p is prime Element of NAT : p <= (2 * k) + 1 } ; :: thesis: verum

end;

suppose y in { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } ; :: thesis: y in { p where p is prime Element of NAT : p <= (2 * k) + 1 }

then ex y' being prime Element of NAT st
( y' = y & y' > k + 1 & y' <= (2 * k) + 1 ) ;
hence y in { p where p is prime Element of NAT : p <= (2 * k) + 1 } ; :: thesis: verum

end;

end;

end;

hence ( y in { p where p is prime Element of NAT : p <= (2 * k) + 1 } iff y in { p where p is prime Element of NAT : p <= k + 1 } \/ { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } ) by A17; :: thesis: verum

end;

hence { p where p is prime Element of NAT : p <= (2 * k) + 1 } = { p where p is prime Element of NAT : p <= k + 1 } \/ { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } by TARSKI:2; :: thesis: verum

end;

A21: for a, b being Element of NAT st a in { p where p is prime Element of NAT : p <= k + 1 } & b in { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } holds
a < b

proof

let a, b be Element of NAT ; :: thesis: ( a in { p where p is prime Element of NAT : p <= k + 1 } & b in { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } implies a < b )
assume A22: a in { p where p is prime Element of NAT : p <= k + 1 } ; :: thesis: ( not b in { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } or a < b )
assume A23: b in { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } ; :: thesis: a < b
A24: ex y' being prime Element of NAT st
( y' = a & y' <= k + 1 ) by A22;
ex y'' being prime Element of NAT st
( y'' = b & y'' > k + 1 & y'' <= (2 * k) + 1 ) by A23;
hence a < b by A24, XXREAL_0:2; :: thesis: verum

end;

set SX = Sgm { p where p is prime Element of NAT : p <= k + 1 } ;
set SY = Sgm { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } ;
A25: Sgm { p where p is prime Element of NAT : p <= k + 1 } is FinSequence of REAL

proof

rng (Sgm { p where p is prime Element of NAT : p <= k + 1 } ) c= REAL ;
hence Sgm { p where p is prime Element of NAT : p <= k + 1 } is FinSequence of REAL by FINSEQ_1:def 4; :: thesis: verum

end;

A26: Sgm { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } is FinSequence of REAL

proof

rng (Sgm { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } ) c= REAL ;
hence Sgm { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } is FinSequence of REAL by FINSEQ_1:def 4; :: thesis: verum

end;

reconsider SX = Sgm { p where p is prime Element of NAT : p <= k + 1 } as FinSequence of REAL by A25;
reconsider SY = Sgm { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } as FinSequence of REAL by A26;
A27: Product (SX ^ SY) = (Product SX) * (Product SY) by RVSUM_1:127;
m / 2 = (k * 2) / 2 by A11;
then A28: Product SX <= 4 to_power k by A2, A10, XREAL_1:218;
A29: for k' being Element of NAT st k' in dom SY holds
SY . k' > 0

proof

let k' be Element of NAT ; :: thesis: ( k' in dom SY implies SY . k' > 0 )
assume A30: k' in dom SY ; :: thesis: SY . k' > 0
rng SY = { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } by A14, FINSEQ_1:def 13;
then SY . k' in { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } by A30, FUNCT_1:12;
then ex y' being prime Element of NAT st
( y' = SY . k' & y' > k + 1 & y' <= (2 * k) + 1 ) ;
hence SY . k' > 0 ; :: thesis: verum

end;

then A31: 0 < Product SY by Th42;
A32: Product SY <= 4 to_power k

proof

A33: Product SY <= ((2 * k) + 1) choose k

proof

reconsider SY = SY as FinSequence of NAT ;
set a = Product SY;
set b = ((2 * k) + 1) choose k;
A34: k + 1 >= 0 ;
set r = ((2 * k) + 1) - k;
reconsider r = ((2 * k) + 1) - k as Element of NAT by A34;
A35: (((2 * k) + 1) - k) + k >= 0 + k by A34, XREAL_1:8;
then A36: ((2 * k) + 1) choose k = (((2 * k) + 1) ! ) / ((k ! ) * (r ! )) by NEWTON:def 3;
A37: Product SY is non empty Nat by A29, Th42;
A38: ((2 * k) + 1) choose k > 0

proof

assume B39: ((2 * k) + 1) choose k <= 0 ; :: thesis: contradiction
A40: (k ! ) * (r ! ) <> 0 by NEWTON:25;
((2 * k) + 1) ! <> 0 by NEWTON:23;
hence contradiction by A36, B39, A40; :: thesis: verum

end;

for p being Element of NAT st p is prime holds
p |-count (Product SY) <= p |-count (((2 * k) + 1) choose k)

proof

let p be Element of NAT ; :: thesis: ( p is prime implies p |-count (Product SY) <= p |-count (((2 * k) + 1) choose k) )
assume A41: p is prime ; :: thesis: p |-count (Product SY) <= p |-count (((2 * k) + 1) choose k)
A42: rng (Sgm { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } ) = { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } by A14, FINSEQ_1:def 13;
{ p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } c= SetPrimes

proof

now

let y be set ; :: thesis: ( y in { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } implies y in SetPrimes )
assume y in { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } ; :: thesis: y in SetPrimes
then ex y' being prime Element of NAT st
( y' = y & y' > k + 1 & y' <= (2 * k) + 1 ) ;
hence y in SetPrimes by NEWTON:def 6; :: thesis: verum

end;

hence { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } c= SetPrimes by TARSKI:def 3; :: thesis: verum

end;

then rng SY c= SetPrimes by A14, FINSEQ_1:def 13;
then reconsider SY = SY as FinSequence of SetPrimes by FINSEQ_1:def 4;
A43: ( p divides Product SY implies ( p > k + 1 & p <= (2 * k) + 1 ) )

proof

assume p divides Product SY ; :: thesis: ( p > k + 1 & p <= (2 * k) + 1 )
then p in rng SY by A41, NAT_3:8;
then ex y' being prime Element of NAT st
( y' = p & y' > k + 1 & y' <= (2 * k) + 1 ) by A42;
hence ( p > k + 1 & p <= (2 * k) + 1 ) ; :: thesis: verum

end;

per cases ( ( p > k + 1 & p <= (2 * k) + 1 ) or not p > k + 1 or not p <= (2 * k) + 1 ) ;

suppose A44: ( p > k + 1 & p <= (2 * k) + 1 ) ; :: thesis: p |-count (Product SY) <= p |-count (((2 * k) + 1) choose k)

set c = (k ! ) * (r ! );
A45: { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } c= SetPrimes

proof

now

let y be set ; :: thesis: ( y in { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } implies y in SetPrimes )
assume y in { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } ; :: thesis: y in SetPrimes
then ex y' being prime Element of NAT st
( y' = y & y' > k + 1 & y' <= (2 * k) + 1 ) ;
hence y in SetPrimes by NEWTON:def 6; :: thesis: verum

end;

hence { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } c= SetPrimes by TARSKI:def 3; :: thesis: verum

end;

A46: p in rng SY by A41, A42, A44;
A47: ( p <> 1 & ((2 * k) + 1) choose k <> 0 ) by A38, A41, INT_2:def 5;
A48: (((2 * k) + 1) choose k) * ((k ! ) * (r ! )) = ((((2 * k) + 1) ! ) / ((k ! ) * (r ! ))) * ((k ! ) * (r ! )) by A35, NEWTON:def 3
.= ((2 * k) + 1) ! by NEWTON:25, XCMPLX_1:88 ;
p divides ((2 * k) + 1) choose k

proof

assume not p divides ((2 * k) + 1) choose k ; :: thesis: contradiction
then A49: p divides (k ! ) * (r ! ) by A41, A44, A48, NEWTON:54, NEWTON:98;

per cases ( p divides k ! or p divides r ! ) by A41, A49, NEWTON:98;

suppose A50: p divides k ! ; :: thesis: contradiction

k + 0 < k + 1 by XREAL_1:8;
then k < p by A44, XXREAL_0:2;
hence contradiction by A41, A50, Th19; :: thesis: verum

end;

suppose p divides r ! ; :: thesis: contradiction

hence contradiction by A41, A44, Th19; :: thesis: verum

end;

end;

end;

then p |-count (((2 * k) + 1) choose k) <> 0 by A47, NAT_3:27;
then 0 + 1 < (p |-count (((2 * k) + 1) choose k)) + 1 by XREAL_1:8;
then 1 <= p |-count (((2 * k) + 1) choose k) by NAT_1:13;
hence p |-count (Product SY) <= p |-count (((2 * k) + 1) choose k) by A14, A41, A45, A46, Th44; :: thesis: verum

end;

suppose A51: ( not p > k + 1 or not p <= (2 * k) + 1 ) ; :: thesis: p |-count (Product SY) <= p |-count (((2 * k) + 1) choose k)

1 divides Product SY by NAT_D:6;
then A52: ( p |^ 0 divides Product SY & not p |^ (0 + 1) divides Product SY ) by A43, A51, NEWTON:9, NEWTON:10;
( p <> 1 & Product SY <> 0 ) by A29, A41, Th42, INT_2:def 5;
hence p |-count (Product SY) <= p |-count (((2 * k) + 1) choose k) by A52, NAT_3:def 7; :: thesis: verum

end;

end;

end;

then ex n being Element of NAT st ((2 * k) + 1) choose k = (Product SY) * n by A37, A38, Th20;
then Product SY divides ((2 * k) + 1) choose k by NAT_D:def 3;
hence Product SY <= ((2 * k) + 1) choose k by A38, NAT_D:7; :: thesis: verum

end;

A53: ((2 * k) + 1) choose k <= 2 to_power (2 * k)

proof

defpred S₂[ Element of NAT ] means ((2 * $1) + 1) choose $1 <= 2 to_power (2 * $1);
((2 * 0 ) + 1) choose 0 = 1 by NEWTON:29;
then A54: S₂[ 0 ] by POWER:29;
A55: for k being Element of NAT st S₂[k] holds
S₂[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume A56: ((2 * k) + 1) choose k <= 2 to_power (2 * k) ; :: thesis: S₂[k + 1]
A57: k + 1 >= 0 ;
set r = ((2 * k) + 1) - k;
reconsider r = ((2 * k) + 1) - k as Element of NAT by A57;
A58: (((2 * k) + 1) - k) + k >= 0 + k by A57, XREAL_1:8;
A59: ((2 * k) + 1) ! = ((((2 * k) + 1) ! ) / ((k ! ) * (r ! ))) * ((k ! ) * (r ! )) by NEWTON:25, XCMPLX_1:88
.= (((2 * k) + 1) choose k) * ((k ! ) * (r ! )) by A58, NEWTON:def 3 ;
A60: k + 2 >= 0 ;
set r' = ((2 * k) + 3) - (k + 1);
set r'' = k + 1;
reconsider r' = ((2 * k) + 3) - (k + 1) as Element of NAT by A60;
A61: (((2 * k) + 3) - (k + 1)) + (k + 1) >= 0 + (k + 1) by A60, XREAL_1:8;
((k + 1) ! ) * (r' ! ) = ((k ! ) * (k + 1)) * ((r + 1) ! ) by NEWTON:21
.= ((k ! ) * (k + 1)) * ((r ! ) * (r + 1)) by NEWTON:21
.= (((k ! ) * (r ! )) * (k + 1)) * (r + 1) ;
then A62: ((k ! ) * (r ! )) / (((k + 1) ! ) * (r' ! )) = ((k ! ) * (r ! )) / (((k ! ) * (r ! )) * ((k + 1) * (r + 1)))
.= (((k ! ) * (r ! )) / ((k ! ) * (r ! ))) / ((k + 1) * (r + 1)) by XCMPLX_1:79
.= 1 / ((k + 1) * (r + 1)) by NEWTON:25, XCMPLX_1:60 ;
A63: ((2 * (k + 1)) + 1) choose (k + 1) = ((((2 * k) + 2) + 1) ! ) / (((k + 1) ! ) * (r' ! )) by A61, NEWTON:def 3
.= (((((2 * k) + 1) + 1) ! ) * ((2 * k) + 3)) / (((k + 1) ! ) * (r' ! )) by NEWTON:21
.= (((((2 * k) + 1) ! ) * ((2 * k) + 2)) * ((2 * k) + 3)) / (((k + 1) ! ) * (r' ! )) by NEWTON:21
.= ((((2 * k) + 2) * ((2 * k) + 3)) * (((2 * k) + 1) ! )) / (((k + 1) ! ) * (r' ! ))
.= ((2 * (k + 1)) * ((2 * k) + 3)) * (((((2 * k) + 1) choose k) * ((k ! ) * (r ! ))) / (((k + 1) ! ) * (r' ! ))) by A59, XCMPLX_1:75
.= ((2 * (k + 1)) * ((2 * k) + 3)) * ((((2 * k) + 1) choose k) * (((k ! ) * (r ! )) / (((k + 1) ! ) * (r' ! )))) by XCMPLX_1:75
.= (((2 * (k + 1)) * ((2 * k) + 3)) * (((2 * k) + 1) choose k)) * (1 / ((k + 1) * (r + 1))) by A62
.= ((2 * (((2 * k) + 1) choose k)) * ((k + 1) * ((2 * k) + 3))) / ((k + 1) * (r + 1)) by XCMPLX_1:100
.= (2 * (((2 * k) + 1) choose k)) * (((k + 1) * ((2 * k) + 3)) / ((k + 1) * (r + 1))) by XCMPLX_1:75
.= (2 * (((2 * k) + 1) choose k)) * (((k + 1) / (k + 1)) * (((2 * k) + 3) / (r + 1))) by XCMPLX_1:77
.= (2 * (((2 * k) + 1) choose k)) * (1 * (((2 * k) + 3) / (r + 1))) by XCMPLX_1:60
.= (2 * (((2 * k) + 1) choose k)) * (((2 * k) + 3) / (k + 2)) ;
(2 * k) + 3 < (2 * k) + 4 by XREAL_1:8;
then ((2 * k) + 3) / (k + 2) < (2 * (k + 2)) / (k + 2) by XREAL_1:76;
then ((2 * k) + 3) / (k + 2) < 2 * ((k + 2) / (k + 2)) by XCMPLX_1:75;
then A64: ((2 * k) + 3) / (k + 2) < 2 * 1 by XCMPLX_1:60;
A65: 2 * ((2 to_power (2 * k)) * 2) = 2 * ((2 to_power (2 * k)) * (2 to_power 1)) by POWER:30
.= 2 * (2 to_power ((2 * k) + 1)) by POWER:32
.= (2 to_power 1) * (2 to_power ((2 * k) + 1)) by POWER:30
.= 2 to_power ((1 + (2 * k)) + 1) by POWER:32 ;
(((2 * k) + 1) choose k) * (((2 * k) + 3) / (k + 2)) <= (2 to_power (2 * k)) * 2 by A56, A64, XREAL_1:68;
then 2 * ((((2 * k) + 1) choose k) * (((2 * k) + 3) / (k + 2))) <= 2 * ((2 to_power (2 * k)) * 2) by XREAL_1:66;
hence S₂[k + 1] by A63, A65; :: thesis: verum

end;

for k being Element of NAT holds S₂[k] from NAT_1:sch 1(A54, A55);
hence ((2 * k) + 1) choose k <= 2 to_power (2 * k) ; :: thesis: verum

end;

2 to_power (2 * k) = 2 to_power (k + k)
.= (2 to_power k) * (2 to_power k) by POWER:32
.= (2 * 2) to_power k by POWER:35 ;
hence Product SY <= 4 to_power k by A33, A53, XXREAL_0:2; :: thesis: verum

end;

for k' being Element of NAT st k' in dom SX holds
SX . k' > 0

proof

let k' be Element of NAT ; :: thesis: ( k' in dom SX implies SX . k' > 0 )
assume A66: k' in dom SX ; :: thesis: SX . k' > 0
rng SX = { p where p is prime Element of NAT : p <= k + 1 } by A12, FINSEQ_1:def 13;
then SX . k' in { p where p is prime Element of NAT : p <= k + 1 } by A66, FUNCT_1:12;
then ex y' being prime Element of NAT st
( y' = SX . k' & y' <= k + 1 ) ;
hence SX . k' > 0 ; :: thesis: verum

end;

then 0 <= Product SX by Th42;
then (Product SX) * (Product SY) <= (4 to_power k) * (4 to_power k) by A28, A31, A32, XREAL_1:68;
then Product (SX ^ SY) <= 4 to_power (k + k) by A27, POWER:32;
hence S₁[m] by A11, A12, A14, A16, A21, FINSEQ_3:48; :: thesis: verum

end;

suppose A67: m + 1 is even ; :: thesis: S₁[m]

A68: m - 1 > 1 - 1 by A10, XREAL_1:11;
set k = m - 1;
reconsider k = m - 1 as Element of NAT by A68, INT_1:16;
k + 1 = m ;
then A69: k < m by NAT_1:13;
A70: { p where p is prime Element of NAT : p <= m + 1 } = { p where p is prime Element of NAT : p <= m }

proof

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

proof

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

A71: now

assume y in { p where p is prime Element of NAT : p <= m + 1 } ; :: thesis: y in { p where p is prime Element of NAT : p <= m }
then consider y' being prime Element of NAT such that
A72: ( y = y' & y' <= m + 1 ) ;
m + 1 > 1 + 1 by A10, XREAL_1:8;
then m + 1 is not Prime by A67, PEPIN:17;
then y' < m + 1 by A72, XXREAL_0:1;
then y' <= m by NAT_1:13;
hence y in { p where p is prime Element of NAT : p <= m } by A72; :: thesis: verum

end;

now

assume y in { p where p is prime Element of NAT : p <= m } ; :: thesis: y in { p where p is prime Element of NAT : p <= m + 1 }
then consider y' being prime Element of NAT such that
A73: ( y = y' & y' <= m ) ;
0 + m <= 1 + m by XREAL_1:8;
then y' <= m + 1 by A73, XXREAL_0:2;
hence y in { p where p is prime Element of NAT : p <= m + 1 } by A73; :: thesis: verum

end;

hence ( y in { p where p is prime Element of NAT : p <= m + 1 } iff y in { p where p is prime Element of NAT : p <= m } ) by A71; :: thesis: verum

end;

hence { p where p is prime Element of NAT : p <= m + 1 } = { p where p is prime Element of NAT : p <= m } by TARSKI:2; :: thesis: verum

end;

A74: Product (Sgm { p where p is prime Element of NAT : p <= k + 1 } ) <= 4 to_power k by A2, A69;
4 to_power k <= 4 to_power m by A69, POWER:44;
hence S₁[m] by A70, A74, XXREAL_0:2; :: thesis: verum

end;

end;

end;

end;

end;

for n being Nat holds S₁[n] from NAT_1:sch 4(A1);
hence Product (Sgm { p where p is prime Element of NAT : p <= n + 1 } ) <= 4 to_power n ; :: thesis: verum