defpred S₁[ Nat] means Product (Sgm { p where p is prime Element of NAT : p <= $1 + 1 } ) <= 4 to_power $1;
let n be Element of NAT ; :: thesis: Product (Sgm { p where p is prime Element of NAT : p <= n + 1 } ) <= 4 to_power n
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 A3: m < 1 ; :: thesis: S₁[m]

A4: now

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

end;

m = 0 by A3, NAT_1:14;
hence S₁[m] by A4, FINSEQ_3:43, POWER:24, RVSUM_1:94; :: thesis: verum

end;

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

A7: 4 to_power 1 = 4 by POWER:25;

A8: 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 y9 being prime Element of NAT such that
A9: ( y9 = y & y9 <= 2 ) ;
y9 > 1 by Lm1;
then y9 >= 1 + 1 by NAT_1:13;
hence y = 2 by A9, 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:28;
then A10: { p where p is prime Element of NAT : p <= 2 } = {2} by A8, TARSKI:def 1;
Product (Sgm {2}) = Product <*2*> by FINSEQ_3:44
.= 2 by RVSUM_1:95 ;
hence S₁[m] by A6, A10, A7; :: thesis: verum

end;

suppose A11: 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
A12: m + 1 = (2 * k) + 1 by ABIAN:9;
A13: ((2 * k) + 1) choose k <= 2 to_power (2 * k)

proof

defpred S₂[ Nat] means ((2 * $1) + 1) choose $1 <= 2 to_power (2 * $1);
A14: 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] )
set r = ((2 * k) + 1) - k;
set r9 = ((2 * k) + 3) - (k + 1);
set r99 = k + 1;
A15: 2 * ((2 to_power (2 * k)) * 2) = 2 * ((2 to_power (2 * k)) * (2 to_power 1)) by POWER:25
.= 2 * (2 to_power ((2 * k) + 1)) by POWER:27
.= (2 to_power 1) * (2 to_power ((2 * k) + 1)) by POWER:25
.= 2 to_power ((1 + (2 * k)) + 1) by POWER:27 ;
A16: k + 1 >= 0 ;
then reconsider r = ((2 * k) + 1) - k as Element of NAT ;
A17: (((2 * k) + 1) - k) + k >= 0 + k by A16, XREAL_1:6;
(2 * k) + 3 < (2 * k) + 4 by XREAL_1:6;
then ((2 * k) + 3) / (k + 2) < (2 * (k + 2)) / (k + 2) by XREAL_1:74;
then ((2 * k) + 3) / (k + 2) < 2 * ((k + 2) / (k + 2)) by XCMPLX_1:74;
then A18: ((2 * k) + 3) / (k + 2) < 2 * 1 by XCMPLX_1:60;
assume ((2 * k) + 1) choose k <= 2 to_power (2 * k) ; :: thesis: S₂[k + 1]
then (((2 * k) + 1) choose k) * (((2 * k) + 3) / (k + 2)) <= (2 to_power (2 * k)) * 2 by A18, XREAL_1:66;
then A19: 2 * ((((2 * k) + 1) choose k) * (((2 * k) + 3) / (k + 2))) <= 2 * ((2 to_power (2 * k)) * 2) by XREAL_1:64;
A20: k + 2 >= 0 ;
then reconsider r9 = ((2 * k) + 3) - (k + 1) as Element of NAT ;
((k + 1) !) * (r9 !) = ((k !) * (k + 1)) * ((r + 1) !) by NEWTON:15
.= ((k !) * (k + 1)) * ((r !) * (r + 1)) by NEWTON:15
.= (((k !) * (r !)) * (k + 1)) * (r + 1) ;
then A21: ((k !) * (r !)) / (((k + 1) !) * (r9 !)) = ((k !) * (r !)) / (((k !) * (r !)) * ((k + 1) * (r + 1)))
.= (((k !) * (r !)) / ((k !) * (r !))) / ((k + 1) * (r + 1)) by XCMPLX_1:78
.= 1 / ((k + 1) * (r + 1)) by XCMPLX_1:60 ;
A22: ((2 * k) + 1) ! = ((((2 * k) + 1) !) / ((k !) * (r !))) * ((k !) * (r !)) by XCMPLX_1:87
.= (((2 * k) + 1) choose k) * ((k !) * (r !)) by A17, NEWTON:def 3 ;
(((2 * k) + 3) - (k + 1)) + (k + 1) >= 0 + (k + 1) by A20, XREAL_1:6;
then ((2 * (k + 1)) + 1) choose (k + 1) = ((((2 * k) + 2) + 1) !) / (((k + 1) !) * (r9 !)) by NEWTON:def 3
.= (((((2 * k) + 1) + 1) !) * ((2 * k) + 3)) / (((k + 1) !) * (r9 !)) by NEWTON:15
.= (((((2 * k) + 1) !) * ((2 * k) + 2)) * ((2 * k) + 3)) / (((k + 1) !) * (r9 !)) by NEWTON:15
.= ((((2 * k) + 2) * ((2 * k) + 3)) * (((2 * k) + 1) !)) / (((k + 1) !) * (r9 !))
.= ((2 * (k + 1)) * ((2 * k) + 3)) * (((((2 * k) + 1) choose k) * ((k !) * (r !))) / (((k + 1) !) * (r9 !))) by A22, XCMPLX_1:74
.= ((2 * (k + 1)) * ((2 * k) + 3)) * ((((2 * k) + 1) choose k) * (((k !) * (r !)) / (((k + 1) !) * (r9 !)))) by XCMPLX_1:74
.= (((2 * (k + 1)) * ((2 * k) + 3)) * (((2 * k) + 1) choose k)) * (1 / ((k + 1) * (r + 1))) by A21
.= ((2 * (((2 * k) + 1) choose k)) * ((k + 1) * ((2 * k) + 3))) / ((k + 1) * (r + 1)) by XCMPLX_1:99
.= (2 * (((2 * k) + 1) choose k)) * (((k + 1) * ((2 * k) + 3)) / ((k + 1) * (r + 1))) by XCMPLX_1:74
.= (2 * (((2 * k) + 1) choose k)) * (((k + 1) / (k + 1)) * (((2 * k) + 3) / (r + 1))) by XCMPLX_1:76
.= (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)) ;
hence S₂[k + 1] by A15, A19; :: thesis: verum

end;

((2 * 0) + 1) choose 0 = 1 by NEWTON:19;
then A23: S₂[ 0 ] by POWER:24;
for k being Element of NAT holds S₂[k] from NAT_1:sch 1(A23, A14);
hence ((2 * k) + 1) choose k <= 2 to_power (2 * k) ; :: thesis: verum

end;

set Y = { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } ;
set SY = Sgm { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } ;
A24: rng (Sgm { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } ) c= REAL ;
set X = { p where p is prime Element of NAT : p <= k + 1 } ;
set SX = Sgm { p where p is prime Element of NAT : p <= k + 1 } ;
rng (Sgm { p where p is prime Element of NAT : p <= k + 1 } ) c= REAL ;
then reconsider SX = Sgm { p where p is prime Element of NAT : p <= k + 1 } as FinSequence of REAL by FINSEQ_1:def 4;
m / 2 = (k * 2) / 2 by A12;
then A25: Product SX <= 4 to_power k by A2, A11, XREAL_1:216;
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 A26: ex y9 being prime Element of NAT st
( y9 = y & y9 <= k + 1 ) ;
then reconsider y = y as prime Element of NAT ;
y >= 1 by Lm1;
hence y in Seg (k + 1) by A26, FINSEQ_1:1; :: thesis: verum

end;

then A27: { p where p is prime Element of NAT : p <= k + 1 } c= Seg (k + 1) by TARSKI:def 3;
for k9 being Element of NAT st k9 in dom SX holds
SX . k9 > 0

proof

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

end;

then A29: 0 <= Product SX by Th42;
reconsider SY = Sgm { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } as FinSequence of REAL by A24, FINSEQ_1:def 4;
A30: 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 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 )
then A31: ex y9 being prime Element of NAT st
( y9 = a & y9 <= k + 1 ) ;
assume b in { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } ; :: thesis: a < b
then ex y99 being prime Element of NAT st
( y99 = b & y99 > k + 1 & y99 <= (2 * k) + 1 ) ;
hence a < b by A31, XXREAL_0:2; :: thesis: verum

end;

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 A32: ex y9 being prime Element of NAT st
( y9 = y & y9 > k + 1 & y9 <= (2 * k) + 1 ) ;
then reconsider y = y as prime Element of NAT ;
y >= 1 by Lm1;
hence y in Seg ((2 * k) + 1) by A32, FINSEQ_1:1; :: thesis: verum

end;

then A33: { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } c= Seg ((2 * k) + 1) by TARSKI:def 3;
A34: for k9 being Element of NAT st k9 in dom SY holds
SY . k9 > 0

proof

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

end;

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

proof

set r = ((2 * k) + 1) - k;
set b = ((2 * k) + 1) choose k;
reconsider SY = SY as FinSequence of NAT ;
set a = Product SY;
A37: k + 1 >= 0 ;
then reconsider r = ((2 * k) + 1) - k as Element of NAT ;
A38: (((2 * k) + 1) - k) + k >= 0 + k by A37, XREAL_1:6;
then ((2 * k) + 1) choose k = (((2 * k) + 1) !) / ((k !) * (r !)) by NEWTON:def 3;
then A39: ((2 * k) + 1) choose k > 0 ;
A40: for p being Element of NAT st p is prime holds
p |-count (Product SY) <= p |-count (((2 * k) + 1) choose k)

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 y9 being prime Element of NAT st
( y9 = y & y9 > k + 1 & y9 <= (2 * k) + 1 ) ;
hence y in SetPrimes by NEWTON:def 6; :: thesis: verum

end;

then { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } c= SetPrimes by TARSKI:def 3;
then rng SY c= SetPrimes by A33, FINSEQ_1:def 13;
then reconsider SY = SY as FinSequence of SetPrimes by FINSEQ_1:def 4;
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 A33, FINSEQ_1:def 13;
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 y9 being prime Element of NAT st
( y9 = p & y9 > k + 1 & y9 <= (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: (((2 * k) + 1) choose k) * ((k !) * (r !)) = ((((2 * k) + 1) !) / ((k !) * (r !))) * ((k !) * (r !)) by A38, NEWTON:def 3
.= ((2 * k) + 1) ! by XCMPLX_1:87 ;
A46: p divides ((2 * k) + 1) choose k

proof

assume not p divides ((2 * k) + 1) choose k ; :: thesis: contradiction
then A47: p divides (k !) * (r !) by A41, A44, A45, NEWTON:41, NEWTON:80;

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

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

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

end;

suppose p divides r ! ; :: thesis: contradiction

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

end;

end;

end;

p <> 1 by A41, INT_2:def 4;
then p |-count (((2 * k) + 1) choose k) <> 0 by A39, A46, NAT_3:27;
then 0 + 1 < (p |-count (((2 * k) + 1) choose k)) + 1 by XREAL_1:6;
then A49: 1 <= p |-count (((2 * k) + 1) choose k) by NAT_1:13;

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 y9 being prime Element of NAT st
( y9 = y & y9 > k + 1 & y9 <= (2 * k) + 1 ) ;
hence y in SetPrimes by NEWTON:def 6; :: thesis: verum

end;

then A50: { p where p is prime Element of NAT : ( p > k + 1 & p <= (2 * k) + 1 ) } c= SetPrimes by TARSKI:def 3;
p in rng SY by A41, A42, A44;
hence p |-count (Product SY) <= p |-count (((2 * k) + 1) choose k) by A33, A41, A50, A49, Th44; :: thesis: verum

end;

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

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

end;

end;

end;

Product SY is non empty Nat by A34, Th42;
then ex n being Element of NAT st ((2 * k) + 1) choose k = (Product SY) * n by A39, A40, Th20;
then Product SY divides ((2 * k) + 1) choose k by NAT_D:def 3;
hence Product SY <= ((2 * k) + 1) choose k by A39, NAT_D:7; :: thesis: verum

end;

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 ) } )

A53: now

assume A54: 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 A54, 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 y9 being prime Element of NAT such that
A55: y9 = y and
A56: y9 <= k + 1 ;
1 * k <= 2 * k by XREAL_1:68;
then k + 1 <= (2 * k) + 1 by XREAL_1:6;
then y9 <= (2 * k) + 1 by A56, XXREAL_0:2;
hence y in { p where p is prime Element of NAT : p <= (2 * k) + 1 } by A55; :: 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 y9 being prime Element of NAT st
( y9 = y & y9 > k + 1 & y9 <= (2 * k) + 1 ) ;
hence y in { p where p is prime Element of NAT : p <= (2 * k) + 1 } ; :: thesis: verum

end;

end;

end;

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 y9 being prime Element of NAT such that
A57: ( y9 = y & y9 <= (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 ( ( y9 = y & y9 <= k + 1 ) or ( y9 = y & y9 > k + 1 & y9 <= (2 * k) + 1 ) ) by A57;

suppose ( y9 = y & y9 <= 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 ( y9 = y & y9 > k + 1 & y9 <= (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;

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

end;

then A58: { 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:1;
2 to_power (2 * k) = 2 to_power (k + k)
.= (2 to_power k) * (2 to_power k) by POWER:27
.= (2 * 2) to_power k by POWER:30 ;
then A59: Product SY <= 4 to_power k by A36, A13, XXREAL_0:2;
0 < Product SY by A34, Th42;
then ( Product (SX ^ SY) = (Product SX) * (Product SY) & (Product SX) * (Product SY) <= (4 to_power k) * (4 to_power k) ) by A25, A59, A29, RVSUM_1:97, XREAL_1:66;
then Product (SX ^ SY) <= 4 to_power (k + k) by POWER:27;
hence S₁[m] by A12, A27, A33, A58, A30, FINSEQ_3:42; :: thesis: verum

end;

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

set k = m - 1;
m - 1 > 1 - 1 by A11, XREAL_1:9;
then reconsider k = m - 1 as Element of NAT by INT_1:3;
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 } )

A61: 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 y9 being prime Element of NAT such that
A62: y = y9 and
A63: y9 <= m + 1 ;
m + 1 > 1 + 1 by A11, XREAL_1:6;
then m + 1 is not Prime by A60, PEPIN:17;
then y9 < m + 1 by A63, XXREAL_0:1;
then y9 <= m by NAT_1:13;
hence y in { p where p is prime Element of NAT : p <= m } by A62; :: 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 y9 being prime Element of NAT such that
A64: y = y9 and
A65: y9 <= m ;
0 + m <= 1 + m by XREAL_1:6;
then y9 <= m + 1 by A65, XXREAL_0:2;
hence y in { p where p is prime Element of NAT : p <= m + 1 } by A64; :: 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 A61; :: thesis: verum

end;

then A66: { p where p is prime Element of NAT : p <= m + 1 } = { p where p is prime Element of NAT : p <= m } by TARSKI:1;
k + 1 = m ;
then k < m by NAT_1:13;
then ( Product (Sgm { p where p is prime Element of NAT : p <= k + 1 } ) <= 4 to_power k & 4 to_power k <= 4 to_power m ) by A2, POWER:39;
hence S₁[m] by A66, 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