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 A1: ( s3 = s1 (#) s2 & s4 = s1 (#) s1 & s5 = s2 (#) s2 ) ; :: thesis: for n being Element of NAT holds ((Partial_Sums s3) . n) ^2 <= ((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)
defpred S₁[ Element of NAT ] means ((Partial_Sums s3) . $1) ^2 <= ((Partial_Sums s4) . $1) * ((Partial_Sums s5) . $1);
let n be Element of NAT ; :: thesis: ((Partial_Sums s3) . n) ^2 <= ((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)
A2: (Partial_Sums s3) . 0 = s3 . 0 by SERIES_1:def 1
.= (s1 . 0 ) * (s2 . 0 ) by A1, SEQ_1:12 ;
((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 A1, SEQ_1:12
.= ((s1 . 0 ) ^2 ) * ((s2 . 0 ) ^2 ) by A1, SEQ_1:12 ;
then A3: S₁[ 0 ] by A2;
A4: 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] )
assume A5: ((Partial_Sums s3) . n) ^2 <= ((Partial_Sums s4) . n) * ((Partial_Sums s5) . n) ; :: thesis: 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);
(Partial_Sums s3) . (n + 1) = ((Partial_Sums s3) . n) + (s3 . (n + 1)) by SERIES_1:def 1;
then A6: (Partial_Sums s3) . (n + 1) = ((Partial_Sums s3) . n) + ((s1 . (n + 1)) * (s2 . (n + 1))) by A1, SEQ_1:12;
((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 A7: ((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 A1, SEQ_1:12
.= (((Partial_Sums s4) . n) + ((s1 . (n + 1)) * (s1 . (n + 1)))) * (((Partial_Sums s5) . n) + ((s2 . (n + 1)) * (s2 . (n + 1)))) by A1, SEQ_1:12
.= (((((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 )) ;
A8: ( (Partial_Sums s4) . n >= 0 & (Partial_Sums s5) . n >= 0 ) by A1, Th36;
then A9: ( (Partial_Sums s4) . n = (sqrt ((Partial_Sums s4) . n)) ^2 & (Partial_Sums s5) . n = (sqrt ((Partial_Sums s5) . n)) ^2 ) by SQUARE_1:def 4;
((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 ) by A6;
then A10: (((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 A7
.= ((((((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))) ;
A11: ( sqrt ((Partial_Sums s4) . n) >= 0 & sqrt ((Partial_Sums s5) . n) >= 0 ) by A8, SQUARE_1:def 4;
(((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:151;
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))) * (abs (s1 . (n + 1)))) by COMPLEX1:151;
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))))) * ((abs (sqrt ((Partial_Sums s5) . n))) * (abs (s1 . (n + 1)))) by A11, ABSVALUE:def 1;
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 A11, ABSVALUE:def 1;
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)) * (sqrt ((Partial_Sums s5) . n)))) * (abs (s2 . (n + 1)))) * (abs (s1 . (n + 1))) ;
then A12: (((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 A8, A9, SQUARE_1:97;
abs ((Partial_Sums s3) . n) <= sqrt (((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)) by A5, Lm8;
then (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:66;
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 A12, 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:151;
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 A13: (((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:151;
abs ((((Partial_Sums s3) . n) * (s2 . (n + 1))) * (s1 . (n + 1))) >= (((Partial_Sums s3) . n) * (s2 . (n + 1))) * (s1 . (n + 1)) by ABSVALUE:11;
then 2 * (abs ((((Partial_Sums s3) . n) * (s2 . (n + 1))) * (s1 . (n + 1)))) >= 2 * ((((Partial_Sums s3) . n) * (s2 . (n + 1))) * (s1 . (n + 1))) by XREAL_1:66;
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 A13, XXREAL_0:2;
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))) >= 0 by XREAL_1:50;
(((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)) - (((Partial_Sums s3) . n) ^2 ) >= 0 by A5, XREAL_1:50;
then ((((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 A14;
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 A10, XREAL_1:8;
hence S₁[n + 1] ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A3, A4);
hence ((Partial_Sums s3) . n) ^2 <= ((Partial_Sums s4) . n) * ((Partial_Sums s5) . n) ; :: thesis: verum