let s, s1 be Real_Sequence; ( ( for n being Nat holds
( s . n > 0 & s1 . n = 1 / (s . n) ) ) implies for n being Nat holds ((Partial_Sums s) . n) * ((Partial_Sums s1) . n) >= (n + 1) ^2 )
defpred S1[ Nat] means ((Partial_Sums s) . $1) * ((Partial_Sums s1) . $1) >= ($1 + 1) ^2 ;
assume A1:
for n being Nat holds
( s . n > 0 & s1 . n = 1 / (s . n) )
; for n being Nat holds ((Partial_Sums s) . n) * ((Partial_Sums s1) . n) >= (n + 1) ^2
then A2:
s . 0 > 0
;
A3:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
set x =
(Partial_Sums s) . n;
set y =
(Partial_Sums s1) . n;
assume A4:
((Partial_Sums s) . n) * ((Partial_Sums s1) . n) >= (n + 1) ^2
;
S1[n + 1]
then A5:
(((Partial_Sums s) . n) * ((Partial_Sums s1) . n)) + (((((Partial_Sums s) . n) / (s . (n + 1))) + (((Partial_Sums s1) . n) * (s . (n + 1)))) + 1) >= ((n + 1) ^2) + (((((Partial_Sums s) . n) / (s . (n + 1))) + (((Partial_Sums s1) . n) * (s . (n + 1)))) + 1)
by XREAL_1:7;
sqrt (((Partial_Sums s) . n) * ((Partial_Sums s1) . n)) >= sqrt ((n + 1) ^2)
by A4, SQUARE_1:26;
then
sqrt (((Partial_Sums s) . n) * ((Partial_Sums s1) . n)) >= n + 1
by SQUARE_1:22;
then A6:
2
* (sqrt (((Partial_Sums s) . n) * ((Partial_Sums s1) . n))) >= 2
* (n + 1)
by XREAL_1:64;
A7:
s . (n + 1) > 0
by A1;
A8:
(Partial_Sums s) . n > 0
by A1, SERIES_3:33;
(Partial_Sums s1) . n > 0
by A1, Th52;
then
(((Partial_Sums s) . n) / (s . (n + 1))) + (((Partial_Sums s1) . n) * (s . (n + 1))) >= 2
* (sqrt ((((Partial_Sums s1) . n) * (s . (n + 1))) * (((Partial_Sums s) . n) / (s . (n + 1)))))
by A7, A8, SIN_COS2:1;
then
(((Partial_Sums s) . n) / (s . (n + 1))) + (((Partial_Sums s1) . n) * (s . (n + 1))) >= 2
* (sqrt (((Partial_Sums s) . n) / ((1 * (s . (n + 1))) / (((Partial_Sums s1) . n) * (s . (n + 1))))))
by XCMPLX_1:81;
then
(((Partial_Sums s) . n) / (s . (n + 1))) + (((Partial_Sums s1) . n) * (s . (n + 1))) >= 2
* (sqrt (((Partial_Sums s) . n) / (1 / ((Partial_Sums s1) . n))))
by A7, XCMPLX_1:91;
then
(((Partial_Sums s) . n) / (s . (n + 1))) + (((Partial_Sums s1) . n) * (s . (n + 1))) >= 2
* (sqrt (((Partial_Sums s1) . n) * (((Partial_Sums s) . n) / 1)))
by XCMPLX_1:81;
then
(((Partial_Sums s) . n) / (s . (n + 1))) + (((Partial_Sums s1) . n) * (s . (n + 1))) >= (2 * n) + 2
by A6, XXREAL_0:2;
then A9:
((((Partial_Sums s) . n) / (s . (n + 1))) + (((Partial_Sums s1) . n) * (s . (n + 1)))) + (((n ^2) + (2 * n)) + 2) >= ((2 * n) + 2) + (((n ^2) + (2 * n)) + 2)
by XREAL_1:7;
((Partial_Sums s) . (n + 1)) * ((Partial_Sums s1) . (n + 1)) =
(((Partial_Sums s) . n) + (s . (n + 1))) * ((Partial_Sums s1) . (n + 1))
by SERIES_1:def 1
.=
(((Partial_Sums s) . n) + (s . (n + 1))) * (((Partial_Sums s1) . n) + (s1 . (n + 1)))
by SERIES_1:def 1
.=
(((((Partial_Sums s) . n) * ((Partial_Sums s1) . n)) + (((Partial_Sums s) . n) * (s1 . (n + 1)))) + ((s . (n + 1)) * ((Partial_Sums s1) . n))) + ((s . (n + 1)) * (s1 . (n + 1)))
.=
(((((Partial_Sums s) . n) * ((Partial_Sums s1) . n)) + (((Partial_Sums s) . n) * (1 / (s . (n + 1))))) + ((s . (n + 1)) * ((Partial_Sums s1) . n))) + ((s . (n + 1)) * (s1 . (n + 1)))
by A1
.=
(((((Partial_Sums s) . n) * ((Partial_Sums s1) . n)) + (((Partial_Sums s) . n) * (1 / (s . (n + 1))))) + ((s . (n + 1)) * ((Partial_Sums s1) . n))) + ((s . (n + 1)) * (1 / (s . (n + 1))))
by A1
.=
(((((Partial_Sums s) . n) * ((Partial_Sums s1) . n)) + (((Partial_Sums s) . n) * (1 / (s . (n + 1))))) + ((s . (n + 1)) * ((Partial_Sums s1) . n))) + (((s . (n + 1)) * 1) / (s . (n + 1)))
by XCMPLX_1:74
.=
(((((Partial_Sums s) . n) * ((Partial_Sums s1) . n)) + (((Partial_Sums s) . n) * (1 / (s . (n + 1))))) + ((s . (n + 1)) * ((Partial_Sums s1) . n))) + 1
by A7, XCMPLX_1:60
.=
(((((Partial_Sums s) . n) * ((Partial_Sums s1) . n)) + (((Partial_Sums s) . n) / ((s . (n + 1)) / 1))) + ((s . (n + 1)) * ((Partial_Sums s1) . n))) + 1
by XCMPLX_1:79
.=
(((((Partial_Sums s) . n) * ((Partial_Sums s1) . n)) + (((Partial_Sums s) . n) / (s . (n + 1)))) + ((s . (n + 1)) * ((Partial_Sums s1) . n))) + 1
;
hence
S1[
n + 1]
by A9, A5, XXREAL_0:2;
verum
end;
((Partial_Sums s) . 0) * ((Partial_Sums s1) . 0) =
(s . 0) * ((Partial_Sums s1) . 0)
by SERIES_1:def 1
.=
(s . 0) * (s1 . 0)
by SERIES_1:def 1
.=
(s . 0) * (1 / (s . 0))
by A1
.=
(s . 0) / ((s . 0) / 1)
by XCMPLX_1:79
.=
1
by A2, XCMPLX_1:60
;
then A10:
S1[ 0 ]
;
for n being Nat holds S1[n]
from NAT_1:sch 2(A10, A3);
hence
for n being Nat holds ((Partial_Sums s) . n) * ((Partial_Sums s1) . n) >= (n + 1) ^2
; verum