let s3, s1, s2, s4, s5 be Real_Sequence; :: thesis: ( s3 = s1 (#) s2 & s4 = s1 (#) s1 & s5 = s2 (#) s2 implies for n being Element of NAT holds ((Partial_Sums s3) . n) ^2 <= ((Partial_Sums s4) . n) * ((Partial_Sums s5) . n) )
assume that
A1: s3 = s1 (#) s2 and
A2: s4 = s1 (#) s1 and
A3: s5 = s2 (#) s2 ; :: thesis: for n being Element of NAT holds ((Partial_Sums s3) . n) ^2 <= ((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)
let n be Element of NAT ; :: thesis: ((Partial_Sums s3) . n) ^2 <= ((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)
A4: (Partial_Sums s3) . 0 = s3 . 0 by SERIES_1:def 1
.= (s1 . 0) * (s2 . 0) by A1, SEQ_1:8 ;
defpred S₁[ Element of NAT ] means ((Partial_Sums s3) . $1) ^2 <= ((Partial_Sums s4) . $1) * ((Partial_Sums s5) . $1);
A5: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
set u = (Partial_Sums s3) . n;
set v = (Partial_Sums s4) . n;
set w = (Partial_Sums s5) . n;
set h = s1 . (n + 1);
set j = s2 . (n + 1);
assume A6: ((Partial_Sums s3) . n) ^2 <= ((Partial_Sums s4) . n) * ((Partial_Sums s5) . n) ; :: thesis: S₁[n + 1]
then abs ((Partial_Sums s3) . n) <= sqrt (((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)) by Lm8;
then A7: (2 * ((abs (s2 . (n + 1))) * (abs (s1 . (n + 1))))) * (sqrt (((Partial_Sums s4) . n) * ((Partial_Sums s5) . n))) >= (2 * ((abs (s2 . (n + 1))) * (abs (s1 . (n + 1))))) * (abs ((Partial_Sums s3) . n)) by XREAL_1:64;
A8: (Partial_Sums s5) . n >= 0 by A3, Th36;
then A9: (Partial_Sums s5) . n = (sqrt ((Partial_Sums s5) . n)) ^2 by SQUARE_1:def 2;
(((sqrt ((Partial_Sums s4) . n)) * (s2 . (n + 1))) ^2) + (((sqrt ((Partial_Sums s5) . n)) * (s1 . (n + 1))) ^2) >= (2 * (abs ((sqrt ((Partial_Sums s4) . n)) * (s2 . (n + 1))))) * (abs ((sqrt ((Partial_Sums s5) . n)) * (s1 . (n + 1)))) by Th8;
then (((sqrt ((Partial_Sums s4) . n)) * (s2 . (n + 1))) ^2) + (((sqrt ((Partial_Sums s5) . n)) * (s1 . (n + 1))) ^2) >= (2 * ((abs (sqrt ((Partial_Sums s4) . n))) * (abs (s2 . (n + 1))))) * (abs ((sqrt ((Partial_Sums s5) . n)) * (s1 . (n + 1)))) by COMPLEX1:65;
then A10: (((sqrt ((Partial_Sums s4) . n)) * (s2 . (n + 1))) ^2) + (((sqrt ((Partial_Sums s5) . n)) * (s1 . (n + 1))) ^2) >= (2 * ((abs (sqrt ((Partial_Sums s4) . n))) * (abs (s2 . (n + 1))))) * ((abs (sqrt ((Partial_Sums s5) . n))) * (abs (s1 . (n + 1)))) by COMPLEX1:65;
A11: (Partial_Sums s4) . n >= 0 by A2, Th36;
then sqrt ((Partial_Sums s4) . n) >= 0 by SQUARE_1:def 2;
then A12: (((sqrt ((Partial_Sums s4) . n)) * (s2 . (n + 1))) ^2) + (((sqrt ((Partial_Sums s5) . n)) * (s1 . (n + 1))) ^2) >= (2 * ((sqrt ((Partial_Sums s4) . n)) * (abs (s2 . (n + 1))))) * ((abs (sqrt ((Partial_Sums s5) . n))) * (abs (s1 . (n + 1)))) by A10, ABSVALUE:def 1;
sqrt ((Partial_Sums s5) . n) >= 0 by A8, SQUARE_1:def 2;
then (((sqrt ((Partial_Sums s4) . n)) * (s2 . (n + 1))) ^2) + (((sqrt ((Partial_Sums s5) . n)) * (s1 . (n + 1))) ^2) >= (2 * ((sqrt ((Partial_Sums s4) . n)) * (abs (s2 . (n + 1))))) * ((sqrt ((Partial_Sums s5) . n)) * (abs (s1 . (n + 1)))) by A12, ABSVALUE:def 1;
then A13: (((sqrt ((Partial_Sums s4) . n)) * (s2 . (n + 1))) ^2) + (((sqrt ((Partial_Sums s5) . n)) * (s1 . (n + 1))) ^2) >= ((2 * ((sqrt ((Partial_Sums s4) . n)) * (sqrt ((Partial_Sums s5) . n)))) * (abs (s2 . (n + 1)))) * (abs (s1 . (n + 1))) ;
(Partial_Sums s4) . n = (sqrt ((Partial_Sums s4) . n)) ^2 by A11, SQUARE_1:def 2;
then (((Partial_Sums s4) . n) * ((s2 . (n + 1)) ^2)) + (((Partial_Sums s5) . n) * ((s1 . (n + 1)) ^2)) >= ((2 * (sqrt (((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)))) * (abs (s2 . (n + 1)))) * (abs (s1 . (n + 1))) by A11, A8, A9, A13, SQUARE_1:29;
then (((Partial_Sums s4) . n) * ((s2 . (n + 1)) ^2)) + (((Partial_Sums s5) . n) * ((s1 . (n + 1)) ^2)) >= (2 * ((abs ((Partial_Sums s3) . n)) * (abs (s2 . (n + 1))))) * (abs (s1 . (n + 1))) by A7, XXREAL_0:2;
then (((Partial_Sums s4) . n) * ((s2 . (n + 1)) ^2)) + (((Partial_Sums s5) . n) * ((s1 . (n + 1)) ^2)) >= (2 * (abs (((Partial_Sums s3) . n) * (s2 . (n + 1))))) * (abs (s1 . (n + 1))) by COMPLEX1:65;
then (((Partial_Sums s4) . n) * ((s2 . (n + 1)) ^2)) + (((Partial_Sums s5) . n) * ((s1 . (n + 1)) ^2)) >= 2 * ((abs (((Partial_Sums s3) . n) * (s2 . (n + 1)))) * (abs (s1 . (n + 1)))) ;
then A14: (((Partial_Sums s4) . n) * ((s2 . (n + 1)) ^2)) + (((Partial_Sums s5) . n) * ((s1 . (n + 1)) ^2)) >= 2 * (abs ((((Partial_Sums s3) . n) * (s2 . (n + 1))) * (s1 . (n + 1)))) by COMPLEX1:65;
2 * (abs ((((Partial_Sums s3) . n) * (s2 . (n + 1))) * (s1 . (n + 1)))) >= 2 * ((((Partial_Sums s3) . n) * (s2 . (n + 1))) * (s1 . (n + 1))) by ABSVALUE:4, XREAL_1:64;
then (((Partial_Sums s4) . n) * ((s2 . (n + 1)) ^2)) + (((Partial_Sums s5) . n) * ((s1 . (n + 1)) ^2)) >= ((2 * ((Partial_Sums s3) . n)) * (s2 . (n + 1))) * (s1 . (n + 1)) by A14, XXREAL_0:2;
then A15: ((((Partial_Sums s4) . n) * ((s2 . (n + 1)) ^2)) + (((Partial_Sums s5) . n) * ((s1 . (n + 1)) ^2))) - (((2 * ((Partial_Sums s3) . n)) * (s2 . (n + 1))) * (s1 . (n + 1))) >= 0 by XREAL_1:48;
(((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)) - (((Partial_Sums s3) . n) ^2) >= 0 by A6, XREAL_1:48;
then A16: ((((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)) - (((Partial_Sums s3) . n) ^2)) + (((((Partial_Sums s4) . n) * ((s2 . (n + 1)) ^2)) + (((Partial_Sums s5) . n) * ((s1 . (n + 1)) ^2))) - (((2 * ((Partial_Sums s3) . n)) * (s2 . (n + 1))) * (s1 . (n + 1)))) >= 0 by A15;
(Partial_Sums s3) . (n + 1) = ((Partial_Sums s3) . n) + (s3 . (n + 1)) by SERIES_1:def 1;
then (Partial_Sums s3) . (n + 1) = ((Partial_Sums s3) . n) + ((s1 . (n + 1)) * (s2 . (n + 1))) by A1, SEQ_1:8;
then A17: ((Partial_Sums s3) . (n + 1)) ^2 = ((((Partial_Sums s3) . n) ^2) + ((2 * ((Partial_Sums s3) . n)) * ((s1 . (n + 1)) * (s2 . (n + 1))))) + (((s1 . (n + 1)) * (s2 . (n + 1))) ^2) ;
((Partial_Sums s4) . (n + 1)) * ((Partial_Sums s5) . (n + 1)) = (((Partial_Sums s4) . n) + (s4 . (n + 1))) * ((Partial_Sums s5) . (n + 1)) by SERIES_1:def 1;
then ((Partial_Sums s4) . (n + 1)) * ((Partial_Sums s5) . (n + 1)) = (((Partial_Sums s4) . n) + (s4 . (n + 1))) * (((Partial_Sums s5) . n) + (s5 . (n + 1))) by SERIES_1:def 1
.= (((Partial_Sums s4) . n) + ((s1 . (n + 1)) * (s1 . (n + 1)))) * (((Partial_Sums s5) . n) + (s5 . (n + 1))) by A2, SEQ_1:8
.= (((Partial_Sums s4) . n) + ((s1 . (n + 1)) * (s1 . (n + 1)))) * (((Partial_Sums s5) . n) + ((s2 . (n + 1)) * (s2 . (n + 1)))) by A3, SEQ_1:8
.= (((((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)) + (((Partial_Sums s4) . n) * ((s2 . (n + 1)) ^2))) + (((Partial_Sums s5) . n) * ((s1 . (n + 1)) ^2))) + (((s1 . (n + 1)) ^2) * ((s2 . (n + 1)) ^2)) ;
then (((Partial_Sums s4) . (n + 1)) * ((Partial_Sums s5) . (n + 1))) - (((Partial_Sums s3) . (n + 1)) ^2) = ((((((((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)) - (((Partial_Sums s3) . n) ^2)) + (((Partial_Sums s4) . n) * ((s2 . (n + 1)) ^2))) + (((Partial_Sums s5) . n) * ((s1 . (n + 1)) ^2))) + (((s1 . (n + 1)) ^2) * ((s2 . (n + 1)) ^2))) - ((2 * ((Partial_Sums s3) . n)) * ((s1 . (n + 1)) * (s2 . (n + 1))))) - (((s1 . (n + 1)) * (s2 . (n + 1))) ^2) by A17
.= ((((((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)) - (((Partial_Sums s3) . n) ^2)) + (((Partial_Sums s4) . n) * ((s2 . (n + 1)) ^2))) + (((Partial_Sums s5) . n) * ((s1 . (n + 1)) ^2))) - (((2 * ((Partial_Sums s3) . n)) * (s1 . (n + 1))) * (s2 . (n + 1))) ;
then ((((Partial_Sums s4) . (n + 1)) * ((Partial_Sums s5) . (n + 1))) - (((Partial_Sums s3) . (n + 1)) ^2)) + (((Partial_Sums s3) . (n + 1)) ^2) >= 0 + (((Partial_Sums s3) . (n + 1)) ^2) by A16, XREAL_1:6;
hence S₁[n + 1] ; :: thesis: verum

end;

((Partial_Sums s4) . 0) * ((Partial_Sums s5) . 0) = (s4 . 0) * ((Partial_Sums s5) . 0) by SERIES_1:def 1
.= (s4 . 0) * (s5 . 0) by SERIES_1:def 1
.= ((s1 . 0) * (s1 . 0)) * (s5 . 0) by A2, SEQ_1:8
.= ((s1 . 0) ^2) * ((s2 . 0) ^2) by A3, SEQ_1:8 ;
then A18: S₁[ 0 ] by A4;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A18, A5);
hence ((Partial_Sums s3) . n) ^2 <= ((Partial_Sums s4) . n) * ((Partial_Sums s5) . n) ; :: thesis: verum