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:49, POWER:29, RVSUM_1:124; :: thesis: verum

end;

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

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

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:44;
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:50
.= 2 by RVSUM_1:125 ;
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: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 ;
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:8;
(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 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:68;
then A19: 2 * ((((2 * k) + 1) choose k) * (((2 * k) + 3) / (k + 2))) <= 2 * ((2 to_power (2 * k)) * 2) by XREAL_1:66;
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:21
.= ((k ! ) * (k + 1)) * ((r ! ) * (r + 1)) by NEWTON:21
.= (((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:79
.= 1 / ((k + 1) * (r + 1)) by XCMPLX_1:60 ;
A22: ((2 * k) + 1) ! = ((((2 * k) + 1) ! ) / ((k ! ) * (r ! ))) * ((k ! ) * (r ! )) by XCMPLX_1:88
.= (((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:8;
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:21
.= (((((2 * k) + 1) ! ) * ((2 * k) + 2)) * ((2 * k) + 3)) / (((k + 1) ! ) * (r9 ! )) by NEWTON:21
.= ((((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:75
.= ((2 * (k + 1)) * ((2 * k) + 3)) * ((((2 * k) + 1) choose k) * (((k ! ) * (r ! )) / (((k + 1) ! ) * (r9 ! )))) by XCMPLX_1:75
.= (((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: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)) ;
hence S₂[k + 1] by A15, A19; :: thesis: verum

end;

((2 * 0 ) + 1) choose 0 = 1 by NEWTON:29;
then A23: S₂[ 0 ] by POWER:29;
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:218;
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:3; :: 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:12;
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:3; :: 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:12;
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:8;
then ((2 * k) + 1) choose k = (((2 * k) + 1) ! ) / ((k ! ) * (r ! )) by NEWTON:def 3;
then A40: ((2 * k) + 1) choose k > 0 ;
A42: 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 A43: p is prime ; :: thesis: p |-count (Product SY) <= p |-count (((2 * k) + 1) choose k)
A44: 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;
A45: ( 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 A43, NAT_3:8;
then ex y9 being prime Element of NAT st
( y9 = p & y9 > k + 1 & y9 <= (2 * k) + 1 ) by A44;
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 A46: ( p > k + 1 & p <= (2 * k) + 1 ) ; :: thesis: p |-count (Product SY) <= p |-count (((2 * k) + 1) choose k)

set c = (k ! ) * (r ! );
A47: (((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:88 ;
A48: 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 A43, A46, A47, NEWTON:54, NEWTON:98;

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

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

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

end;

suppose p divides r ! ; :: thesis: contradiction

hence contradiction by A43, A46, Th19; :: thesis: verum

end;

end;

end;

p <> 1 by A43, INT_2:def 5;
then p |-count (((2 * k) + 1) choose k) <> 0 by A40, A48, NAT_3:27;
then 0 + 1 < (p |-count (((2 * k) + 1) choose k)) + 1 by XREAL_1:8;
then A51: 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 A52: { 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 A43, A44, A46;
hence p |-count (Product SY) <= p |-count (((2 * k) + 1) choose k) by A33, A43, A52, A51, 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 A53: not p |^ (0 + 1) divides Product SY by A45, NEWTON:10;
1 divides Product SY by NAT_D:6;
then A54: p |^ 0 divides Product SY by NEWTON:9;
( p <> 1 & Product SY <> 0 ) by A34, A43, Th42, INT_2:def 5;
hence p |-count (Product SY) <= p |-count (((2 * k) + 1) choose k) by A54, A53, 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 A40, A42, Th20;
then Product SY divides ((2 * k) + 1) choose k by NAT_D:def 3;
hence Product SY <= ((2 * k) + 1) choose k by A40, 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 ) } )

A55: now

assume A56: 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 A56, 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
A57: y9 = y and
A58: y9 <= k + 1 ;
1 * k <= 2 * k by XREAL_1:70;
then k + 1 <= (2 * k) + 1 by XREAL_1:8;
then y9 <= (2 * k) + 1 by A58, XXREAL_0:2;
hence y in { p where p is prime Element of NAT : p <= (2 * k) + 1 } by A57; :: 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
A59: ( 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 A59;

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

end;

then A60: { 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;
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 ;
then A61: 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, A61, A29, RVSUM_1:127, XREAL_1:68;
then Product (SX ^ SY) <= 4 to_power (k + k) by POWER:32;
hence S₁[m] by A12, A27, A33, A60, A30, FINSEQ_3:48; :: thesis: verum

end;

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

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

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

end;

then A68: { p where p is prime Element of NAT : p <= m + 1 } = { p where p is prime Element of NAT : p <= m } by TARSKI:2;
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:44;
hence S₁[m] by A68, 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