let s be Real_Sequence; :: thesis: ( ( for n being Nat st n >= 1 holds
( s . n = 1 + (1 / ((2 * n) + 1)) & s . 0 = 1 ) ) implies for n being 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));
A1: (1 / 2) * (sqrt ((2 * 1) + 3)) = (sqrt 5) / 2 ;
assume A2: for n being Nat st n >= 1 holds
( s . n = 1 + (1 / ((2 * n) + 1)) & s . 0 = 1 ) ; :: thesis: for n being Nat st n >= 1 holds
(Partial_Product s) . n > (1 / 2) * (sqrt ((2 * n) + 3))
A3: 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 that
A4: n >= 1 and
A5: (Partial_Product s) . n > (1 / 2) * (sqrt ((2 * n) + 3)) ; :: thesis: S₁[n + 1]
n + 1 >= 1 + 1 by A4, XREAL_1:7;
then A6: n + 1 >= 1 by XXREAL_0:2;
A7: sqrt ((2 * n) + 3) > 0 by SQUARE_1:25;
(1 / ((2 * n) + 3)) + ((2 * n) + 5) > 0 + ((2 * n) + 5) by XREAL_1:8;
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 2;
then (((1 / (sqrt ((2 * n) + 3))) ^2) + 2) + ((2 * n) + 3) > (2 * n) + 5 by XCMPLX_1:76;
then (((1 / (sqrt ((2 * n) + 3))) ^2) + (2 * 1)) + ((sqrt ((2 * n) + 3)) ^2) > (2 * n) + 5 by SQUARE_1:def 2;
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 A7, XCMPLX_1:106;
then sqrt (((1 / (sqrt ((2 * n) + 3))) + (sqrt ((2 * n) + 3))) ^2) > sqrt ((2 * n) + 5) by SQUARE_1:27;
then (sqrt ((2 * n) + 3)) + (1 / (sqrt ((2 * n) + 3))) > sqrt ((2 * n) + 5) by A7, SQUARE_1:22;
then A8: (1 / 2) * ((sqrt ((2 * n) + 3)) + (1 / (sqrt ((2 * n) + 3)))) > (1 / 2) * (sqrt ((2 * n) + 5)) by XREAL_1:68;
((Partial_Product s) . n) * (1 + (1 / ((2 * n) + 3))) > ((1 / 2) * (sqrt ((2 * n) + 3))) * (1 + (1 / ((2 * n) + 3))) by A5, XREAL_1:68;
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:74;
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:74;
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:22;
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:29;
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))) * (1 / (sqrt ((2 * n) + 3))))) by XCMPLX_1:76;
then ((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;
then ((Partial_Product s) . n) * (1 + (1 / ((2 * (n + 1)) + 1))) > (1 / 2) * (sqrt ((2 * n) + 5)) by A8, XXREAL_0:2;
then ((Partial_Product s) . n) * (s . (n + 1)) > (1 / 2) * (sqrt ((2 * n) + 5)) by A2, A6;
hence S₁[n + 1] by SERIES_3:def 1; :: thesis: verum

end;

sqrt (16 / 9) > sqrt (5 / 4) by SQUARE_1:27;
then (sqrt (4 ^2)) / (sqrt (3 ^2)) > sqrt (5 / 4) by SQUARE_1:30;
then 4 / (sqrt (3 ^2)) > sqrt (5 / 4) by SQUARE_1:22;
then 4 / 3 > sqrt (5 / 4) by SQUARE_1:22;
then A9: 4 / 3 > (sqrt 5) / (sqrt (2 ^2)) by SQUARE_1:30;
(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 A2
.= 1 + (1 / ((2 * 1) + 1)) by A2
.= 4 / 3 ;
then A10: S₁[1] by A1, A9, SQUARE_1:22;
for n being Nat st n >= 1 holds
S₁[n] from NAT_1:sch 8(A10, A3);
hence for n being Nat st n >= 1 holds
(Partial_Product s) . n > (1 / 2) * (sqrt ((2 * n) + 3)) ; :: thesis: verum