let s, s1 be Real_Sequence; :: thesis: ( ( 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 S₁[ 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) ) ; :: thesis: 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 S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[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 ; :: thesis: S₁[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 S₁[n + 1] by A9, A5, XXREAL_0:2; :: thesis: 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: S₁[ 0 ] ;
for n being Nat holds S₁[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 ; :: thesis: verum