let n be Nat; :: thesis: for s being Real_Sequence st ( for n being Nat holds s . n = ((2 * n) + 1) / ((2 * n) + 2) ) holds
(Partial_Product s) . n <= 1 / (sqrt ((3 * n) + 4))
let s be Real_Sequence; :: thesis: ( ( for n being Nat holds s . n = ((2 * n) + 1) / ((2 * n) + 2) ) implies (Partial_Product s) . n <= 1 / (sqrt ((3 * n) + 4)) )
defpred S₁[ Nat] means (Partial_Product s) . $1 <= 1 / (sqrt ((3 * $1) + 4));
assume A1: for n being Nat holds s . n = ((2 * n) + 1) / ((2 * n) + 2) ; :: thesis: (Partial_Product s) . n <= 1 / (sqrt ((3 * n) + 4))
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume (Partial_Product s) . n <= 1 / (sqrt ((3 * n) + 4)) ; :: thesis: S₁[n + 1]
then ((Partial_Product s) . n) * (((2 * n) + 3) / ((2 * n) + 4)) <= (1 / (sqrt ((3 * n) + 4))) * (((2 * n) + 3) / ((2 * n) + 4)) by XREAL_1:64;
then A3: ((Partial_Product s) . n) * (((2 * n) + 3) / ((2 * n) + 4)) <= (1 * ((2 * n) + 3)) / ((sqrt ((3 * n) + 4)) * ((2 * n) + 4)) by XCMPLX_1:76;
111 * n <= 112 * n by XREAL_1:64;
then (111 * n) + 63 <= (112 * n) + 64 by XREAL_1:7;
then ((12 * (n |^ 3)) + (64 * (n ^2))) + ((111 * n) + 63) <= ((12 * (n |^ 3)) + (64 * (n ^2))) + ((112 * n) + 64) by XREAL_1:6;
then (((((12 * (n |^ (2 + 1))) + (36 * (n * n))) + (27 * n)) + (28 * (n ^2))) + (84 * n)) + 63 <= (((((12 * (n |^ (2 + 1))) + (48 * (n ^2))) + (48 * n)) + (16 * (n ^2))) + (64 * n)) + 64 ;
then (((((12 * ((n |^ 2) * (n |^ 1))) + (36 * (n * n))) + (27 * n)) + (28 * (n ^2))) + (84 * n)) + 63 <= (((((12 * (n |^ (2 + 1))) + (48 * (n * n))) + (48 * n)) + (16 * (n ^2))) + (64 * n)) + 64 by NEWTON:8;
then (((((((4 * (n |^ 2)) * 3) * (n |^ 1)) + ((36 * n) * n)) + (27 * n)) + (28 * (n ^2))) + (84 * n)) + 63 <= (((((12 * (n |^ (2 + 1))) + ((48 * n) * n)) + (48 * n)) + (16 * (n ^2))) + (64 * n)) + 64 ;
then (((((((4 * (n |^ 2)) * 3) * n) + ((36 * n) * n)) + (27 * n)) + (28 * (n ^2))) + (84 * n)) + 63 <= (((((12 * (n |^ (2 + 1))) + ((48 * n) * n)) + (48 * n)) + (16 * (n ^2))) + (64 * n)) + 64 ;
then (((((((4 * (n ^2)) * 3) * n) + ((36 * n) * n)) + (27 * n)) + (28 * (n ^2))) + (84 * n)) + 63 <= (((((12 * (n |^ (2 + 1))) + ((48 * n) * n)) + (48 * n)) + (16 * (n ^2))) + (64 * n)) + 64 by Lm1;
then (((((((4 * (n ^2)) * 3) * n) + ((36 * n) * n)) + (27 * n)) + (28 * (n ^2))) + (84 * n)) + 63 <= (((((12 * ((n |^ 2) * (n |^ 1))) + ((48 * n) * n)) + (48 * n)) + (16 * (n ^2))) + (64 * n)) + 64 by NEWTON:8;
then (((((((4 * (n ^2)) * 3) * n) + ((36 * n) * n)) + (27 * n)) + (28 * (n ^2))) + (84 * n)) + 63 <= (((((12 * ((n ^2) * (n |^ 1))) + ((48 * n) * n)) + (48 * n)) + (16 * (n ^2))) + (64 * n)) + 64 by Lm1;
then (((((((4 * (n ^2)) * 3) * n) + ((36 * n) * n)) + (27 * n)) + (28 * (n ^2))) + (84 * n)) + 63 <= (((((12 * ((n ^2) * n)) + ((48 * n) * n)) + (48 * n)) + (16 * (n ^2))) + (64 * n)) + 64 ;
then sqrt ((((2 * n) + 3) ^2) * ((3 * n) + 7)) <= sqrt ((((2 * n) + 4) ^2) * ((3 * n) + 4)) by SQUARE_1:26;
then (sqrt (((2 * n) + 3) ^2)) * (sqrt ((3 * n) + 7)) <= sqrt ((((2 * n) + 4) ^2) * ((3 * n) + 4)) by SQUARE_1:29;
then (sqrt (((2 * n) + 3) ^2)) * (sqrt ((3 * n) + 7)) <= (sqrt (((2 * n) + 4) ^2)) * (sqrt ((3 * n) + 4)) by SQUARE_1:29;
then ((2 * n) + 3) * (sqrt ((3 * n) + 7)) <= (sqrt (((2 * n) + 4) ^2)) * (sqrt ((3 * n) + 4)) by SQUARE_1:22;
then A4: ((2 * n) + 3) * (sqrt ((3 * n) + 7)) <= (((2 * n) + 4) * (sqrt ((3 * n) + 4))) * 1 by SQUARE_1:22;
( sqrt ((3 * n) + 4) > 0 & sqrt ((3 * n) + 7) > 0 ) by SQUARE_1:25;
then (1 * ((2 * n) + 3)) / (((2 * n) + 4) * (sqrt ((3 * n) + 4))) <= 1 / (sqrt ((3 * n) + 7)) by A4, XREAL_1:102;
then ((Partial_Product s) . n) * (((2 * (n + 1)) + 1) / ((2 * (n + 1)) + 2)) <= 1 / (sqrt ((3 * (n + 1)) + 4)) by A3, XXREAL_0:2;
then ((Partial_Product s) . n) * (s . (n + 1)) <= 1 / (sqrt ((3 * (n + 1)) + 4)) by A1;
hence S₁[n + 1] by Def1; :: thesis: verum

end;

(Partial_Product s) . 0 = s . 0 by Def1
.= ((2 * 0) + 1) / ((2 * 0) + 2) by A1
.= 1 / (sqrt ((3 * 0) + 4)) by SQUARE_1:20 ;
then A5: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A5, A2);
hence (Partial_Product s) . n <= 1 / (sqrt ((3 * n) + 4)) ; :: thesis: verum