let n be Nat; :: thesis: for s being Real_Sequence st ( for n being Nat holds
( s . n > 0 & s . n >= s . (n - 1) ) ) holds
(Partial_Sums s) . n >= (n + 1) * ((n + 1) -root ((Partial_Product s) . n))
let s be Real_Sequence; :: thesis: ( ( for n being Nat holds
( s . n > 0 & s . n >= s . (n - 1) ) ) implies (Partial_Sums s) . n >= (n + 1) * ((n + 1) -root ((Partial_Product s) . n)) )
defpred S₁[ Nat] means (Partial_Sums s) . $1 >= ($1 + 1) * (($1 + 1) -root ((Partial_Product s) . $1));
A1: (Partial_Sums s) . 0 = s . 0 by SERIES_1:def 1;
assume A2: for n being Nat holds
( s . n > 0 & s . n >= s . (n - 1) ) ; :: thesis: (Partial_Sums s) . n >= (n + 1) * ((n + 1) -root ((Partial_Product s) . n))
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
set u = (Partial_Sums s) . n;
set v = s . (n + 1);
set w = ((((Partial_Sums s) . n) / (n + 1)) + (((s . (n + 1)) - (((Partial_Sums s) . n) / (n + 1))) / (n + 2))) |^ (n + 2);
set h = (n + 1) -root ((Partial_Product s) . n);
set j = ((Partial_Sums s) . n) / (n + 1);
A4: s . (n + 1) > 0 by A2;
A5: n + 1 >= 0 + 1 by XREAL_1:6;
then (n + 1) + 1 >= 1 + 1 by XREAL_1:6;
then A6: n + 2 >= 1 by XXREAL_0:2;
assume (Partial_Sums s) . n >= (n + 1) * ((n + 1) -root ((Partial_Product s) . n)) ; :: thesis: S₁[n + 1]
then ((Partial_Sums s) . n) / (n + 1) >= ((n + 1) * ((n + 1) -root ((Partial_Product s) . n))) / (n + 1) by XREAL_1:72;
then (n + 1) -root ((Partial_Product s) . n) <= ((Partial_Sums s) . n) / (n + 1) by XCMPLX_1:89;
then A7: ((n + 1) -root ((Partial_Product s) . n)) |^ (n + 1) <= (((Partial_Sums s) . n) / (n + 1)) |^ (n + 1) by A2, Lm11, PREPOWER:9;
A8: (Partial_Product s) . n > 0 by A2, Th43;
then (n + 1) -root ((Partial_Product s) . n) = (n + 1) -Root ((Partial_Product s) . n) by A5, POWER:def 1;
then (Partial_Product s) . n <= (((Partial_Sums s) . n) / (n + 1)) |^ (n + 1) by A7, A8, A5, PREPOWER:19;
then ((Partial_Product s) . n) * (s . (n + 1)) <= ((((Partial_Sums s) . n) / (n + 1)) |^ (n + 1)) * (s . (n + 1)) by A4, XREAL_1:64;
then A9: (Partial_Product s) . (n + 1) <= ((((Partial_Sums s) . n) / (n + 1)) |^ (n + 1)) * (s . (n + 1)) by Def1;
A10: (Partial_Product s) . (n + 1) >= 0 by A2, Th43;
( (Partial_Sums s) . n > 0 & ((s . (n + 1)) - (((Partial_Sums s) . n) / (n + 1))) / (n + 2) >= 0 ) by A2, Lm12, Th33;
then ((((Partial_Sums s) . n) / (n + 1)) + (((s . (n + 1)) - (((Partial_Sums s) . n) / (n + 1))) / (n + 2))) |^ (n + 2) >= ((((Partial_Sums s) . n) / (n + 1)) |^ ((n + 1) + 1)) + (((n + 2) * ((((Partial_Sums s) . n) / (n + 1)) |^ (n + 1))) * (((s . (n + 1)) - (((Partial_Sums s) . n) / (n + 1))) / (n + 2))) by Th31;
then ((((Partial_Sums s) . n) / (n + 1)) + (((s . (n + 1)) - (((Partial_Sums s) . n) / (n + 1))) / (n + 2))) |^ (n + 2) >= (((((Partial_Sums s) . n) / (n + 1)) |^ (n + 1)) * (((Partial_Sums s) . n) / (n + 1))) + (((((Partial_Sums s) . n) / (n + 1)) |^ (n + 1)) * ((((s . (n + 1)) - (((Partial_Sums s) . n) / (n + 1))) / (n + 2)) * (n + 2))) by NEWTON:6;
then A11: ((((Partial_Sums s) . n) / (n + 1)) + (((s . (n + 1)) - (((Partial_Sums s) . n) / (n + 1))) / (n + 2))) |^ (n + 2) >= (((((Partial_Sums s) . n) / (n + 1)) |^ (n + 1)) * (((Partial_Sums s) . n) / (n + 1))) + (((((Partial_Sums s) . n) / (n + 1)) |^ (n + 1)) * ((s . (n + 1)) - (((Partial_Sums s) . n) / (n + 1)))) by XCMPLX_1:87;
A12: (Partial_Sums s) . (n + 1) > 0 by A2, Th33;
((Partial_Sums s) . (n + 1)) / (n + 2) = ((1 * ((Partial_Sums s) . n)) + (s . (n + 1))) / (n + 2) by SERIES_1:def 1
.= ((((n + 1) / (n + 1)) * ((Partial_Sums s) . n)) + (s . (n + 1))) / (n + 2) by XCMPLX_1:60
.= (((((n + 2) - 1) * ((Partial_Sums s) . n)) / (n + 1)) + (s . (n + 1))) / (n + 2) ;
then ((Partial_Sums s) . (n + 1)) / (n + 2) = (((((n + 2) * ((Partial_Sums s) . n)) - ((Partial_Sums s) . n)) / (n + 1)) + (s . (n + 1))) / (n + 2)
.= (((((n + 2) * ((Partial_Sums s) . n)) / (n + 1)) - (((Partial_Sums s) . n) / (n + 1))) + (s . (n + 1))) / (n + 2)
.= (((((n + 2) * ((Partial_Sums s) . n)) / (n + 1)) - (((Partial_Sums s) . n) / (n + 1))) / (n + 2)) + ((s . (n + 1)) / (n + 2))
.= (((((n + 2) * ((Partial_Sums s) . n)) / (n + 1)) / (n + 2)) - ((((Partial_Sums s) . n) / (n + 1)) / (n + 2))) + ((s . (n + 1)) / (n + 2))
.= ((((n + 2) * ((Partial_Sums s) . n)) / ((n + 1) * (n + 2))) - ((((Partial_Sums s) . n) / (n + 1)) / (n + 2))) + ((s . (n + 1)) / (n + 2)) by XCMPLX_1:78
.= ((((Partial_Sums s) . n) / (n + 1)) - ((((Partial_Sums s) . n) / (n + 1)) / (n + 2))) + ((s . (n + 1)) / (n + 2)) by XCMPLX_1:91
.= (((Partial_Sums s) . n) / (n + 1)) + (((s . (n + 1)) / (n + 2)) - ((((Partial_Sums s) . n) / (n + 1)) / (n + 2)))
.= (((Partial_Sums s) . n) / (n + 1)) + (((s . (n + 1)) - (((Partial_Sums s) . n) / (n + 1))) / (n + 2)) ;
then (((Partial_Sums s) . (n + 1)) / (n + 2)) |^ (n + 2) >= (Partial_Product s) . (n + 1) by A11, A9, XXREAL_0:2;
then (n + 2) -Root ((((Partial_Sums s) . (n + 1)) / (n + 2)) |^ (n + 2)) >= (n + 2) -Root ((Partial_Product s) . (n + 1)) by A6, A10, PREPOWER:27;
then ((Partial_Sums s) . (n + 1)) / (n + 2) >= (n + 2) -Root ((Partial_Product s) . (n + 1)) by A6, A12, PREPOWER:19;
then ((Partial_Sums s) . (n + 1)) / (n + 2) >= (n + 2) -root ((Partial_Product s) . (n + 1)) by A6, A10, POWER:def 1;
then (((Partial_Sums s) . (n + 1)) / (n + 2)) * (n + 2) >= (n + 2) * ((n + 2) -root ((Partial_Product s) . (n + 1))) by XREAL_1:64;
hence S₁[n + 1] by XCMPLX_1:87; :: thesis: verum

end;

(0 + 1) * ((0 + 1) -root ((Partial_Product s) . 0)) = (0 + 1) -root (s . 0) by Def1
.= (Partial_Sums s) . 0 by A1, POWER:9 ;
then A13: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A13, A3);
hence (Partial_Sums s) . n >= (n + 1) * ((n + 1) -root ((Partial_Product s) . n)) ; :: thesis: verum