let s1, s2, s3, s4, s5 be Real_Sequence; :: thesis: ( s3 = s1 (#) s2 & s4 = s1 (#) s1 & s5 = s2 (#) s2 implies for n being 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 Nat holds ((Partial_Sums s3) . n) ^2 <= ((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)
let n be 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₁[ Nat] means ((Partial_Sums s3) . $1) ^2 <= ((Partial_Sums s4) . $1) * ((Partial_Sums s5) . $1);
A5: 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 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 |.((Partial_Sums s3) . n).| <= sqrt (((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)) by Lm7;
then A7: (2 * (|.(s2 . (n + 1)).| * |.(s1 . (n + 1)).|)) * (sqrt (((Partial_Sums s4) . n) * ((Partial_Sums s5) . n))) >= (2 * (|.(s2 . (n + 1)).| * |.(s1 . (n + 1)).|)) * |.((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 * |.((sqrt ((Partial_Sums s4) . n)) * (s2 . (n + 1))).|) * |.((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 * (|.(sqrt ((Partial_Sums s4) . n)).| * |.(s2 . (n + 1)).|)) * |.((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 * (|.(sqrt ((Partial_Sums s4) . n)).| * |.(s2 . (n + 1)).|)) * (|.(sqrt ((Partial_Sums s5) . n)).| * |.(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)) * |.(s2 . (n + 1)).|)) * (|.(sqrt ((Partial_Sums s5) . n)).| * |.(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)) * |.(s2 . (n + 1)).|)) * ((sqrt ((Partial_Sums s5) . n)) * |.(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)))) * |.(s2 . (n + 1)).|) * |.(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)))) * |.(s2 . (n + 1)).|) * |.(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 * (|.((Partial_Sums s3) . n).| * |.(s2 . (n + 1)).|)) * |.(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 * |.(((Partial_Sums s3) . n) * (s2 . (n + 1))).|) * |.(s1 . (n + 1)).| by COMPLEX1:65;
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)).|) ;
then A14: (((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 COMPLEX1:65;
2 * |.((((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 Nat holds S₁[n] from NAT_1:sch 2(A18, A5);
hence ((Partial_Sums s3) . n) ^2 <= ((Partial_Sums s4) . n) * ((Partial_Sums s5) . n) ; :: thesis: verum