let s be Real_Sequence; :: thesis: ( ( for n being Element of NAT st n >= 1 holds
( s . n = 1 + (1 / ((2 * n) + 1)) & s . 0 = 1 ) ) implies for n being Element of NAT st n >= 1 holds
(Partial_Product s) . n > (1 / 2) * (sqrt ((2 * n) + 3)) )
assume A1: for n being Element of NAT st n >= 1 holds
( s . n = 1 + (1 / ((2 * n) + 1)) & s . 0 = 1 ) ; :: thesis: for n being Element of NAT st n >= 1 holds
(Partial_Product s) . n > (1 / 2) * (sqrt ((2 * n) + 3))
defpred S₁[ Nat] means (Partial_Product s) . $1 > (1 / 2) * (sqrt ((2 * $1) + 3));
A2: (Partial_Product s) . (1 + 0 ) = ((Partial_Product s) . 0 ) * (s . (1 + 0 )) by SERIES_3:def 1
.= (s . 0 ) * (s . 1) by SERIES_3:def 1
.= 1 * (s . 1) by A1
.= 1 + (1 / ((2 * 1) + 1)) by A1
.= 4 / 3 ;
A3: (1 / 2) * (sqrt ((2 * 1) + 3)) = (sqrt 5) / 2 ;
sqrt (16 / 9) > sqrt (5 / 4) by SQUARE_1:95;
then (sqrt (4 ^2 )) / (sqrt (3 ^2 )) > sqrt (5 / 4) by SQUARE_1:99;
then 4 / (sqrt (3 ^2 )) > sqrt (5 / 4) by SQUARE_1:89;
then 4 / 3 > sqrt (5 / 4) by SQUARE_1:89;
then 4 / 3 > (sqrt 5) / (sqrt (2 ^2 )) by SQUARE_1:99;
then A4: S₁[1] by A2, A3, SQUARE_1:89;
A5: for n being Nat st n >= 1 & S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( n >= 1 & S₁[n] implies S₁[n + 1] )
assume A6: ( n >= 1 & (Partial_Product s) . n > (1 / 2) * (sqrt ((2 * n) + 3)) ) ; :: thesis: S₁[n + 1]
then ((Partial_Product s) . n) * (1 + (1 / ((2 * n) + 3))) > ((1 / 2) * (sqrt ((2 * n) + 3))) * (1 + (1 / ((2 * n) + 3))) by XREAL_1:70;
then ((Partial_Product s) . n) * (1 + (1 / ((2 * n) + 3))) > (((1 / 2) * (sqrt ((2 * n) + 3))) * 1) + (((1 / 2) * (sqrt ((2 * n) + 3))) * (1 / ((2 * n) + 3))) ;
then ((Partial_Product s) . n) * (1 + (1 / ((2 * n) + 3))) > ((1 / 2) * (sqrt ((2 * n) + 3))) + (((1 / 2) * (sqrt ((2 * n) + 3))) / ((2 * n) + 3)) by XCMPLX_1:75;
then ((Partial_Product s) . n) * (1 + (1 / ((2 * n) + 3))) > ((1 / 2) * (sqrt ((2 * n) + 3))) + ((1 / 2) * ((sqrt ((2 * n) + 3)) / ((2 * n) + 3))) by XCMPLX_1:75;
then ((Partial_Product s) . n) * (1 + (1 / ((2 * n) + 3))) > ((1 / 2) * (sqrt ((2 * n) + 3))) + ((1 / 2) * ((sqrt ((2 * n) + 3)) / (sqrt (((2 * n) + 3) ^2 )))) by SQUARE_1:89;
then ((Partial_Product s) . n) * (1 + (1 / ((2 * n) + 3))) > ((1 / 2) * (sqrt ((2 * n) + 3))) + ((1 / 2) * (((sqrt ((2 * n) + 3)) * 1) / ((sqrt ((2 * n) + 3)) * (sqrt ((2 * n) + 3))))) by SQUARE_1:97;
then A7: ((Partial_Product s) . n) * (1 + (1 / ((2 * n) + 3))) > ((1 / 2) * (sqrt ((2 * n) + 3))) + ((1 / 2) * (((sqrt ((2 * n) + 3)) / (sqrt ((2 * n) + 3))) * (1 / (sqrt ((2 * n) + 3))))) by XCMPLX_1:77;
A8: sqrt ((2 * n) + 3) > 0 by SQUARE_1:93;
then A9: ((Partial_Product s) . n) * (1 + (1 / ((2 * n) + 3))) > ((1 / 2) * (sqrt ((2 * n) + 3))) + ((1 / 2) * (1 * (1 / (sqrt ((2 * n) + 3))))) by A7, XCMPLX_1:60;
(1 / ((2 * n) + 3)) + ((2 * n) + 5) > 0 + ((2 * n) + 5) by XREAL_1:10;
then ((1 / ((2 * n) + 3)) + 2) + ((2 * n) + 3) > (2 * n) + 5 ;
then (((1 ^2 ) / ((sqrt ((2 * n) + 3)) ^2 )) + 2) + ((2 * n) + 3) > (2 * n) + 5 by SQUARE_1:def 4;
then (((1 / (sqrt ((2 * n) + 3))) ^2 ) + 2) + ((2 * n) + 3) > (2 * n) + 5 by XCMPLX_1:77;
then (((1 / (sqrt ((2 * n) + 3))) ^2 ) + (2 * 1)) + ((sqrt ((2 * n) + 3)) ^2 ) > (2 * n) + 5 by SQUARE_1:def 4;
then (((1 / (sqrt ((2 * n) + 3))) ^2 ) + (2 * ((sqrt ((2 * n) + 3)) * (1 / (sqrt ((2 * n) + 3)))))) + ((sqrt ((2 * n) + 3)) ^2 ) > (2 * n) + 5 by A8, XCMPLX_1:107;
then A10: sqrt (((1 / (sqrt ((2 * n) + 3))) + (sqrt ((2 * n) + 3))) ^2 ) > sqrt ((2 * n) + 5) by SQUARE_1:95;
(1 / (sqrt ((2 * n) + 3))) + (sqrt ((2 * n) + 3)) > 0 by A8;
then (sqrt ((2 * n) + 3)) + (1 / (sqrt ((2 * n) + 3))) > sqrt ((2 * n) + 5) by A10, SQUARE_1:89;
then (1 / 2) * ((sqrt ((2 * n) + 3)) + (1 / (sqrt ((2 * n) + 3)))) > (1 / 2) * (sqrt ((2 * n) + 5)) by XREAL_1:70;
then A11: ((Partial_Product s) . n) * (1 + (1 / ((2 * (n + 1)) + 1))) > (1 / 2) * (sqrt ((2 * n) + 5)) by A9, XXREAL_0:2;
A12: n in NAT by ORDINAL1:def 13;
n + 1 >= 1 + 1 by A6, XREAL_1:9;
then n + 1 >= 1 by XXREAL_0:2;
then ((Partial_Product s) . n) * (s . (n + 1)) > (1 / 2) * (sqrt ((2 * n) + 5)) by A1, A11;
hence S₁[n + 1] by A12, SERIES_3:def 1; :: thesis: verum

end;

for n being Nat st n >= 1 holds
S₁[n] from NAT_1:sch 8(A4, A5);
hence for n being Element of NAT st n >= 1 holds
(Partial_Product s) . n > (1 / 2) * (sqrt ((2 * n) + 3)) ; :: thesis: verum