let n be Element of NAT ; :: thesis: for s being Real_Sequence st ( for n being Element of 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 Element of NAT holds
( s . n > 0 & s . n >= s . (n - 1) ) ) implies (Partial_Sums s) . n >= (n + 1) * ((n + 1) -root ((Partial_Product s) . n)) )
assume A1:
for n being Element of NAT holds
( s . n > 0 & s . n >= s . (n - 1) )
; :: thesis: (Partial_Sums s) . n >= (n + 1) * ((n + 1) -root ((Partial_Product s) . n))
defpred S1[ Element of NAT ] means (Partial_Sums s) . $1 >= ($1 + 1) * (($1 + 1) -root ((Partial_Product s) . $1));
A2:
(Partial_Sums s) . 0 = s . 0
by SERIES_1:def 1;
(0 + 1) * ((0 + 1) -root ((Partial_Product s) . 0 )) =
(0 + 1) -root (s . 0 )
by Def1
.=
(Partial_Sums s) . 0
by A2, POWER:10
;
then A3:
S1[ 0 ]
;
A4:
for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be
Element of
NAT ;
:: thesis: ( S1[n] implies S1[n + 1] )
assume A5:
(Partial_Sums s) . n >= (n + 1) * ((n + 1) -root ((Partial_Product s) . n))
;
:: thesis: S1[n + 1]
A6:
((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)
;
set u =
(Partial_Sums s) . n;
set v =
s . (n + 1);
A7:
((Partial_Sums s) . (n + 1)) / (n + 2) =
(((((n + 2) * ((Partial_Sums s) . n)) - ((Partial_Sums s) . n)) / (n + 1)) + (s . (n + 1))) / (n + 2)
by A6
.=
(((((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:79
.=
((((Partial_Sums s) . n) / (n + 1)) - ((((Partial_Sums s) . n) / (n + 1)) / (n + 2))) + ((s . (n + 1)) / (n + 2))
by XCMPLX_1:92
.=
(((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))
;
(Partial_Sums s) . n > 0
by A1, Th33;
then A8:
((Partial_Sums s) . n) / (n + 1) > 0
;
A9:
((s . (n + 1)) - (((Partial_Sums s) . n) / (n + 1))) / (n + 2) >= 0
by A1, Lm13;
set w =
((((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)) + (((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 A8, A9, 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:11;
then A10:
((((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:88;
((Partial_Sums s) . n) / (n + 1) >= ((n + 1) * ((n + 1) -root ((Partial_Product s) . n))) / (n + 1)
by A5, XREAL_1:74;
then A11:
(n + 1) -root ((Partial_Product s) . n) <= ((Partial_Sums s) . n) / (n + 1)
by XCMPLX_1:90;
set h =
(n + 1) -root ((Partial_Product s) . n);
set j =
((Partial_Sums s) . n) / (n + 1);
(n + 1) -root ((Partial_Product s) . n) > 0
by A1, Lm12;
then A12:
((n + 1) -root ((Partial_Product s) . n)) |^ (n + 1) <= (((Partial_Sums s) . n) / (n + 1)) |^ (n + 1)
by A11, PREPOWER:17;
A13:
(Partial_Product s) . n > 0
by A1, Th43;
A14:
n + 1
>= 0 + 1
by XREAL_1:8;
then
(n + 1) -root ((Partial_Product s) . n) = (n + 1) -Root ((Partial_Product s) . n)
by A13, POWER:def 1;
then A15:
(Partial_Product s) . n <= (((Partial_Sums s) . n) / (n + 1)) |^ (n + 1)
by A12, A13, A14, PREPOWER:28;
s . (n + 1) > 0
by A1;
then
((Partial_Product s) . n) * (s . (n + 1)) <= ((((Partial_Sums s) . n) / (n + 1)) |^ (n + 1)) * (s . (n + 1))
by A15, XREAL_1:66;
then
(Partial_Product s) . (n + 1) <= ((((Partial_Sums s) . n) / (n + 1)) |^ (n + 1)) * (s . (n + 1))
by Def1;
then A16:
(((Partial_Sums s) . (n + 1)) / (n + 2)) |^ (n + 2) >= (Partial_Product s) . (n + 1)
by A7, A10, XXREAL_0:2;
(n + 1) + 1
>= 1
+ 1
by A14, XREAL_1:8;
then A17:
n + 2
>= 1
by XXREAL_0:2;
A18:
(Partial_Product s) . (n + 1) >= 0
by A1, Th43;
(Partial_Sums s) . (n + 1) > 0
by A1, Th33;
then A19:
((Partial_Sums s) . (n + 1)) / (n + 2) > 0
;
(n + 2) -Root ((((Partial_Sums s) . (n + 1)) / (n + 2)) |^ (n + 2)) >= (n + 2) -Root ((Partial_Product s) . (n + 1))
by A16, A17, A18, PREPOWER:36;
then
((Partial_Sums s) . (n + 1)) / (n + 2) >= (n + 2) -Root ((Partial_Product s) . (n + 1))
by A17, A19, PREPOWER:28;
then
((Partial_Sums s) . (n + 1)) / (n + 2) >= (n + 2) -root ((Partial_Product s) . (n + 1))
by A17, A18, 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:66;
hence
S1[
n + 1]
by XCMPLX_1:88;
:: thesis: verum
end;
for n being Element of NAT holds S1[n]
from NAT_1:sch 1(A3, A4);
hence
(Partial_Sums s) . n >= (n + 1) * ((n + 1) -root ((Partial_Product s) . n))
; :: thesis: verum