series_3.miz



    begin

    reserve a,b,c for positive Real,

m,x,y,z for Real,

n for Nat,

s,s1,s2,s3,s4,s5 for Real_Sequence;

    registration

      let x;

      cluster |.x.| -> non negative;

      coherence ;

    end

    

     Lm1: (x ^2 ) = (x |^ 2)

    proof

      (x ^2 ) = ((x |^ 1) * x)

      .= (x |^ (1 + 1)) by NEWTON: 6

      .= (x |^ 2);

      hence thesis;

    end;

    

     Lm2: (2 |^ 3) = 8

    proof

      (2 |^ 3) = (2 |^ (2 + 1))

      .= ((2 |^ 2) * 2) by NEWTON: 6

      .= ((2 ^2 ) * 2) by Lm1

      .= 8;

      hence thesis;

    end;

    

     Lm3: (3 |^ 3) = 27

    proof

      (3 |^ 3) = (3 |^ (2 + 1))

      .= ((3 |^ 2) * 3) by NEWTON: 6

      .= ((3 ^2 ) * 3) by Lm1

      .= 27;

      hence thesis;

    end;

    

     Lm4: (( - x) |^ 3) = ( - (x |^ 3))

    proof

      3 = ((2 * 1) + 1);

      then 3 is odd by ABIAN: 1;

      hence thesis by POWER: 2;

    end;

    

     Lm5: ((x + y) |^ 3) = ((((x |^ 3) + ((3 * (x ^2 )) * y)) + ((3 * x) * (y ^2 ))) + (y |^ 3))

    proof

      ((x + y) |^ 3) = (((x |^ 3) + (((3 * y) * (x ^2 )) + ((3 * (y ^2 )) * x))) + (y |^ 3)) by POLYEQ_1: 14

      .= ((((x |^ 3) + ((3 * (x ^2 )) * y)) + ((3 * x) * (y ^2 ))) + (y |^ 3));

      hence thesis;

    end;

    

     Lm6: ((x |^ 3) + (y |^ 3)) = ((x + y) * (((x ^2 ) - (x * y)) + (y ^2 )))

    proof

      ((((x ^2 ) - (x * y)) + (y ^2 )) * (x + y)) = (((((x ^2 ) * x) + (y * (x ^2 ))) - ((x * (x * y)) + (y * (x * y)))) + (((x * (y ^2 )) + (y * (y ^2 ))) + ( 0 * (y ^2 ))))

      .= ((((x |^ 3) + (y * (x ^2 ))) - ((x * (x * y)) + (y * (x * y)))) + ((x * (y ^2 )) + (y * (y ^2 )))) by POLYEQ_2: 4

      .= ((((x |^ 3) + (y * (x ^2 ))) - (((x ^2 ) * y) + ((y * y) * x))) + ((x * (y ^2 )) + (y |^ 3))) by POLYEQ_2: 4

      .= ((x |^ 3) + (y |^ 3));

      hence thesis;

    end;

    

     Lm7: (x ^2 ) <= (y * z) implies |.x.| <= ( sqrt (y * z))

    proof

      

       A1: (x ^2 ) >= 0 by XREAL_1: 63;

      assume (x ^2 ) <= (y * z);

      then

       A2: ( sqrt (x ^2 )) <= ( sqrt (y * z)) by A1, SQUARE_1: 26;

      per cases ;

        suppose

         A3: x >= 0 ;

        then x <= ( sqrt (y * z)) by A2, SQUARE_1: 22;

        hence thesis by A3, ABSVALUE:def 1;

      end;

        suppose

         A4: x < 0 ;

        then ( - x) <= ( sqrt (y * z)) by A2, SQUARE_1: 23;

        hence thesis by A4, ABSVALUE:def 1;

      end;

    end;

    theorem :: SERIES_3:1

    y > x & x >= 0 & m >= 0 implies (x / y) <= ((x + m) / (y + m))

    proof

      assume that

       A1: y > x and

       A2: x >= 0 and

       A3: m >= 0 ;

      (y - x) > 0 by A1, XREAL_1: 50;

      then (m * (y - x)) >= 0 by A3;

      then (((y * (x + m)) - (x * (m + y))) / (y * (y + m))) >= 0 by A1, A2, A3;

      then (((x + m) / (y + m)) - (x / y)) >= 0 by A1, A2, A3, XCMPLX_1: 130;

      then ((((x + m) / (y + m)) - (x / y)) + (x / y)) >= ( 0 + (x / y)) by XREAL_1: 6;

      hence thesis;

    end;

    theorem :: SERIES_3:2

    

     Th2: ((a + b) / 2) >= ( sqrt (a * b))

    proof

      ((a + b) / 2) >= ((2 * ( sqrt (a * b))) / 2) by SIN_COS2: 1, XREAL_1: 72;

      hence thesis;

    end;

    theorem :: SERIES_3:3

    ((b / a) + (a / b)) >= 2

    proof

      ((a - b) ^2 ) >= 0 by XREAL_1: 63;

      then ((((a ^2 ) - ((2 * a) * b)) + (b ^2 )) + ((2 * a) * b)) >= ( 0 + ((2 * a) * b)) by XREAL_1: 7;

      then (((a ^2 ) + (b ^2 )) / (a * b)) >= ((2 * (a * b)) / (1 * (a * b))) by XREAL_1: 72;

      then

       A1: (((a ^2 ) + (b ^2 )) / (a * b)) >= (2 / 1) by XCMPLX_1: 91;

      ((b / a) + (a / b)) = (((b * b) / (a * b)) + (a / b)) by XCMPLX_1: 91

      .= (((b * b) / (a * b)) + ((a * a) / (a * b))) by XCMPLX_1: 91

      .= (((b ^2 ) + (a ^2 )) / (a * b));

      hence thesis by A1;

    end;

    theorem :: SERIES_3:4

    

     Th4: (((x + y) / 2) ^2 ) >= (x * y)

    proof

      ((x - y) ^2 ) >= 0 by XREAL_1: 63;

      then ((((x ^2 ) - ((2 * x) * y)) + (y ^2 )) + ((2 * x) * y)) >= ( 0 + ((2 * x) * y)) by XREAL_1: 7;

      then (((x ^2 ) + (y ^2 )) + ((2 * x) * y)) >= (((2 * x) * y) + ((2 * x) * y)) by XREAL_1: 7;

      then (((x + y) ^2 ) / (2 * 2)) >= ((4 * (x * y)) / 4) by XREAL_1: 72;

      hence thesis;

    end;

    theorem :: SERIES_3:5

    (((x ^2 ) + (y ^2 )) / 2) >= (((x + y) / 2) ^2 )

    proof

      ((x - y) ^2 ) >= 0 by XREAL_1: 63;

      then ((((x ^2 ) - ((2 * x) * y)) + (y ^2 )) + ((2 * x) * y)) >= ( 0 + ((2 * x) * y)) by XREAL_1: 7;

      then (((x ^2 ) + (y ^2 )) + ((x ^2 ) + (y ^2 ))) >= (((2 * x) * y) + ((x ^2 ) + (y ^2 ))) by XREAL_1: 7;

      then ((2 * ((x ^2 ) + (y ^2 ))) / 4) >= (((x + y) ^2 ) / 4) by XREAL_1: 72;

      hence thesis;

    end;

    theorem :: SERIES_3:6

    

     Th6: ((x ^2 ) + (y ^2 )) >= ((2 * x) * y)

    proof

      ((x - y) ^2 ) >= 0 by XREAL_1: 63;

      then ((((x ^2 ) - ((2 * x) * y)) + (y ^2 )) + ((2 * x) * y)) >= ( 0 + ((2 * x) * y)) by XREAL_1: 6;

      hence thesis;

    end;

    theorem :: SERIES_3:7

    

     Th7: (((x ^2 ) + (y ^2 )) / 2) >= (x * y)

    proof

      (((x ^2 ) + (y ^2 )) / 2) >= (((2 * x) * y) / 2) by Th6, XREAL_1: 72;

      hence thesis;

    end;

    theorem :: SERIES_3:8

    

     Th8: ((x ^2 ) + (y ^2 )) >= ((2 * |.x.|) * |.y.|)

    proof

      

       A1: (x ^2 ) >= 0 & (y ^2 ) >= 0 by XREAL_1: 63;

      then ((x ^2 ) + (y ^2 )) >= (2 * ( sqrt ((x ^2 ) * (y ^2 )))) by SIN_COS2: 1;

      then ((x ^2 ) + (y ^2 )) >= (2 * (( sqrt (x ^2 )) * ( sqrt (y ^2 )))) by A1, SQUARE_1: 29;

      then ((x ^2 ) + (y ^2 )) >= (2 * (( sqrt ( |.x.| ^2 )) * ( sqrt (y ^2 )))) by COMPLEX1: 75;

      then ((x ^2 ) + (y ^2 )) >= (2 * (( sqrt ( |.x.| ^2 )) * ( sqrt ( |.y.| ^2 )))) by COMPLEX1: 75;

      then ((x ^2 ) + (y ^2 )) >= (2 * ( |.x.| * ( sqrt ( |.y.| ^2 )))) by SQUARE_1: 22;

      then ((x ^2 ) + (y ^2 )) >= (2 * ( |.x.| * |.y.|)) by SQUARE_1: 22;

      hence thesis;

    end;

    theorem :: SERIES_3:9

    

     Th9: ((x + y) ^2 ) >= ((4 * x) * y)

    proof

      (2 * (((x ^2 ) + (y ^2 )) / 2)) >= (2 * (x * y)) by Th7, XREAL_1: 64;

      then (((x ^2 ) + (y ^2 )) + ((2 * x) * y)) >= (((2 * x) * y) + ((2 * x) * y)) by XREAL_1: 6;

      hence thesis;

    end;

    theorem :: SERIES_3:10

    

     Th10: (((x ^2 ) + (y ^2 )) + (z ^2 )) >= (((x * y) + (y * z)) + (x * z))

    proof

      ((x ^2 ) + (y ^2 )) >= ((2 * x) * y) & ((y ^2 ) + (z ^2 )) >= ((2 * y) * z) by Th6;

      then

       A1: (((x ^2 ) + (y ^2 )) + ((y ^2 ) + (z ^2 ))) >= (((2 * x) * y) + ((2 * y) * z)) by XREAL_1: 7;

      ((z ^2 ) + (x ^2 )) >= ((2 * z) * x) by Th6;

      then ((((x ^2 ) + (y ^2 )) + ((y ^2 ) + (z ^2 ))) + ((z ^2 ) + (x ^2 ))) >= ((((2 * x) * y) + ((2 * y) * z)) + ((2 * z) * x)) by A1, XREAL_1: 7;

      then ((2 * (((x ^2 ) + (y ^2 )) + (z ^2 ))) / 2) >= ((2 * (((x * y) + (y * z)) + (z * x))) / 2) by XREAL_1: 72;

      hence thesis;

    end;

    theorem :: SERIES_3:11

    (((x + y) + z) ^2 ) >= (3 * (((x * y) + (y * z)) + (x * z)))

    proof

      (((x ^2 ) + (y ^2 )) + (z ^2 )) >= (((x * y) + (y * z)) + (x * z)) by Th10;

      then ((((x ^2 ) + (y ^2 )) + (z ^2 )) + ((((2 * x) * y) + ((2 * y) * z)) + ((2 * z) * x))) >= ((((x * y) + (y * z)) + (x * z)) + ((((2 * x) * y) + ((2 * y) * z)) + ((2 * z) * x))) by XREAL_1: 6;

      hence thesis;

    end;

    theorem :: SERIES_3:12

    

     Th12: (((a |^ 3) + (b |^ 3)) + (c |^ 3)) >= (((3 * a) * b) * c)

    proof

      

       A1: (((a + c) |^ 3) - (((3 * (a ^2 )) * c) + ((3 * a) * (c ^2 )))) = (((((a |^ 3) + ((3 * (a ^2 )) * c)) + ((3 * a) * (c ^2 ))) + (c |^ 3)) - (((3 * (a ^2 )) * c) + ((3 * a) * (c ^2 )))) by Lm5;

      (a * ((b ^2 ) + (c ^2 ))) >= (a * ((2 * b) * c)) & (b * ((a ^2 ) + (c ^2 ))) >= (b * ((2 * a) * c)) by Th6, XREAL_1: 64;

      then

       A2: ((b * ((a ^2 ) + (c ^2 ))) + (a * ((b ^2 ) + (c ^2 )))) >= ((((2 * a) * b) * c) + (((2 * a) * b) * c)) by XREAL_1: 7;

      (((a + c) ^2 ) * (a + c)) >= (((4 * a) * c) * (a + c)) by Th9, XREAL_1: 64;

      then (((a + c) |^ 2) * (a + c)) >= (((4 * a) * c) * (a + c)) by Lm1;

      then

       A3: ((a + c) |^ (2 + 1)) >= (((4 * a) * c) * (a + c)) by NEWTON: 6;

      (((b + c) ^2 ) * (b + c)) >= (((4 * b) * c) * (b + c)) by Th9, XREAL_1: 64;

      then (((b + c) |^ 2) * (b + c)) >= (((4 * b) * c) * (b + c)) by Lm1;

      then

       A4: ((b + c) |^ (2 + 1)) >= (((4 * b) * c) * (b + c)) by NEWTON: 6;

      (((a + b) ^2 ) * (a + b)) >= (((4 * a) * b) * (a + b)) by Th9, XREAL_1: 64;

      then (((a + b) |^ 2) * (a + b)) >= (((4 * a) * b) * (a + b)) by Lm1;

      then ((a + b) |^ (2 + 1)) >= (((4 * a) * b) * (a + b)) by NEWTON: 6;

      then (((a + b) |^ 3) + ((b + c) |^ 3)) >= ((((4 * (a ^2 )) * b) + ((4 * a) * (b ^2 ))) + (((4 * (b ^2 )) * c) + ((4 * b) * (c ^2 )))) by A4, XREAL_1: 7;

      then ((((a + b) |^ 3) + ((b + c) |^ 3)) + ((a + c) |^ 3)) >= ((((((4 * (a ^2 )) * b) + ((4 * a) * (b ^2 ))) + ((4 * (b ^2 )) * c)) + ((4 * b) * (c ^2 ))) + (((4 * (a ^2 )) * c) + ((4 * a) * (c ^2 )))) by A3, XREAL_1: 7;

      then

       A5: (((((a + b) |^ 3) + ((b + c) |^ 3)) + ((a + c) |^ 3)) + (((((( - ((3 * (a ^2 )) * b)) - ((3 * a) * (b ^2 ))) - ((3 * (b ^2 )) * c)) - ((3 * b) * (c ^2 ))) - ((3 * (a ^2 )) * c)) - ((3 * a) * (c ^2 )))) >= ((((((((4 * (a ^2 )) * b) + ((4 * a) * (b ^2 ))) + ((4 * (b ^2 )) * c)) + ((4 * b) * (c ^2 ))) + ((4 * (a ^2 )) * c)) + ((4 * a) * (c ^2 ))) + (((((( - ((3 * (a ^2 )) * b)) - ((3 * a) * (b ^2 ))) - ((3 * (b ^2 )) * c)) - ((3 * b) * (c ^2 ))) - ((3 * (a ^2 )) * c)) - ((3 * a) * (c ^2 )))) by XREAL_1: 6;

      (c * ((a ^2 ) + (b ^2 ))) >= (((2 * a) * b) * c) by Th6, XREAL_1: 64;

      then

       A6: (((b * ((a ^2 ) + (c ^2 ))) + (a * ((b ^2 ) + (c ^2 )))) + (c * ((a ^2 ) + (b ^2 )))) >= ((((4 * a) * b) * c) + (((2 * a) * b) * c)) by A2, XREAL_1: 7;

      (((a + b) |^ 3) - (((3 * (a ^2 )) * b) + ((3 * a) * (b ^2 )))) = (((((a |^ 3) + ((3 * (a ^2 )) * b)) + ((3 * a) * (b ^2 ))) + (b |^ 3)) - (((3 * (a ^2 )) * b) + ((3 * a) * (b ^2 )))) & (((b + c) |^ 3) - (((3 * (b ^2 )) * c) + ((3 * b) * (c ^2 )))) = (((((b |^ 3) + ((3 * (b ^2 )) * c)) + ((3 * b) * (c ^2 ))) + (c |^ 3)) - (((3 * (b ^2 )) * c) + ((3 * b) * (c ^2 )))) by Lm5;

      then (2 * (((a |^ 3) + (b |^ 3)) + (c |^ 3))) >= (((6 * a) * b) * c) by A1, A5, A6, XXREAL_0: 2;

      then ((2 * (((a |^ 3) + (b |^ 3)) + (c |^ 3))) / 2) >= ((((6 * a) * b) * c) / 2) by XREAL_1: 72;

      hence thesis;

    end;

    theorem :: SERIES_3:13

    

     Th13: ((((a |^ 3) + (b |^ 3)) + (c |^ 3)) / 3) >= ((a * b) * c)

    proof

      ((((a |^ 3) + (b |^ 3)) + (c |^ 3)) / 3) >= ((((3 * a) * b) * c) / 3) by Th12, XREAL_1: 72;

      hence thesis;

    end;

    theorem :: SERIES_3:14

    ((((a / b) |^ 3) + ((b / c) |^ 3)) + ((c / a) |^ 3)) >= (((b / a) + (c / b)) + (a / c))

    proof

      

       A1: 1 = (((a / a) * 1) * 1) by XCMPLX_1: 60

      .= (((a / a) * (b / b)) * 1) by XCMPLX_1: 60

      .= (((a / a) * (b / b)) * (c / c)) by XCMPLX_1: 60

      .= (((a / b) * (b / a)) * (c / c))

      .= ((a / b) * ((b / a) * (c / c)))

      .= ((a / b) * ((b / c) * (c / a)))

      .= (((a / b) * (b / c)) * (c / a));

      (c / b) = ((c / b) * 1)

      .= ((c / b) * (a / a)) by XCMPLX_1: 60

      .= (((a / b) * (c / a)) * 1);

      then

       A2: (c / b) <= (((((a / b) |^ 3) + ((c / a) |^ 3)) + (1 |^ 3)) / 3) by Th13;

      (a / c) = ((a / c) * 1)

      .= ((a / c) * (b / b)) by XCMPLX_1: 60

      .= (((a / b) * (b / c)) * 1);

      then

       A3: (a / c) <= (((((a / b) |^ 3) + ((b / c) |^ 3)) + (1 |^ 3)) / 3) by Th13;

      (b / a) = ((b / a) * 1)

      .= ((b / a) * (c / c)) by XCMPLX_1: 60

      .= (((b / c) * (c / a)) * 1);

      then (b / a) <= (((((b / c) |^ 3) + ((c / a) |^ 3)) + (1 |^ 3)) / 3) by Th13;

      then ((b / a) + (c / b)) <= ((((((b / c) |^ 3) / 3) + (((c / a) |^ 3) / 3)) + (1 / 3)) + (((((a / b) |^ 3) / 3) + (((c / a) |^ 3) / 3)) + (1 / 3))) by A2, XREAL_1: 7;

      then

       A4: (((b / a) + (c / b)) + (a / c)) <= (((((((b / c) |^ 3) / 3) + (((a / b) |^ 3) / 3)) + ((2 * ((c / a) |^ 3)) / 3)) + (2 / 3)) + (((((a / b) |^ 3) / 3) + (((b / c) |^ 3) / 3)) + (1 / 3))) by A3, XREAL_1: 7;

      (((a / b) * (b / c)) * (c / a)) <= (((((a / b) |^ 3) + ((b / c) |^ 3)) + ((c / a) |^ 3)) / 3) by Th13;

      then ((((b / a) + (c / b)) + (a / c)) + 1) <= ((((((2 * ((b / c) |^ 3)) / 3) + ((2 * ((a / b) |^ 3)) / 3)) + ((2 * ((c / a) |^ 3)) / 3)) + 1) + (((((a / b) |^ 3) / 3) + (((b / c) |^ 3) / 3)) + (((c / a) |^ 3) / 3))) by A1, A4, XREAL_1: 7;

      then (((((b / a) + (c / b)) + (a / c)) + 1) - 1) <= ((((((b / c) |^ 3) + ((a / b) |^ 3)) + ((c / a) |^ 3)) + 1) - 1) by XREAL_1: 9;

      hence thesis;

    end;

    theorem :: SERIES_3:15

    

     Th15: ((a + b) + c) >= (3 * (3 -root ((a * b) * c)))

    proof

      

       A1: (3 -Root c) > 0 by PREPOWER:def 2;

      (3 -Root a) > 0 & (3 -Root b) > 0 by PREPOWER:def 2;

      then ((((3 -Root a) |^ 3) + ((3 -Root b) |^ 3)) + ((3 -Root c) |^ 3)) >= (((3 * (3 -Root a)) * (3 -Root b)) * (3 -Root c)) by A1, Th12;

      then ((a + ((3 -Root b) |^ 3)) + ((3 -Root c) |^ 3)) >= (((3 * (3 -Root a)) * (3 -Root b)) * (3 -Root c)) by PREPOWER: 19;

      then ((a + b) + ((3 -Root c) |^ 3)) >= (((3 * (3 -Root a)) * (3 -Root b)) * (3 -Root c)) by PREPOWER: 19;

      then ((a + b) + c) >= ((3 * ((3 -Root a) * (3 -Root b))) * (3 -Root c)) by PREPOWER: 19;

      then ((a + b) + c) >= ((3 * (3 -Root (a * b))) * (3 -Root c)) by PREPOWER: 22;

      then ((a + b) + c) >= (3 * ((3 -Root (a * b)) * (3 -Root c)));

      then ((a + b) + c) >= (3 * (3 -Root ((a * b) * c))) by PREPOWER: 22;

      hence thesis by POWER:def 1;

    end;

    theorem :: SERIES_3:16

    (((a + b) + c) / 3) >= (3 -root ((a * b) * c))

    proof

      (((a + b) + c) / 3) >= ((3 * (3 -root ((a * b) * c))) / 3) by Th15, XREAL_1: 72;

      hence thesis;

    end;

    theorem :: SERIES_3:17

    ((x + y) + z) = 1 implies (((x * y) + (y * z)) + (x * z)) <= (1 / 3)

    proof

      ((x ^2 ) + (y ^2 )) >= ((2 * x) * y) & ((x ^2 ) + (z ^2 )) >= ((2 * x) * z) by Th6;

      then

       A1: (((x ^2 ) + (y ^2 )) + ((x ^2 ) + (z ^2 ))) >= (((2 * x) * y) + ((2 * x) * z)) by XREAL_1: 7;

      ((y ^2 ) + (z ^2 )) >= ((2 * y) * z) by Th6;

      then (((((x ^2 ) + (y ^2 )) + (x ^2 )) + (z ^2 )) + ((y ^2 ) + (z ^2 ))) >= ((((2 * x) * y) + ((2 * x) * z)) + ((2 * y) * z)) by A1, XREAL_1: 7;

      then ((2 * (((x ^2 ) + (y ^2 )) + (z ^2 ))) / 2) >= ((2 * (((x * y) + (x * z)) + (y * z))) / 2) by XREAL_1: 72;

      then

       A2: ((((x ^2 ) + (y ^2 )) + (z ^2 )) + (2 * (((x * z) + (y * z)) + (x * y)))) >= ((((x * y) + (x * z)) + (y * z)) + (2 * (((x * z) + (y * z)) + (x * y)))) by XREAL_1: 7;

      assume ((x + y) + z) = 1;

      

      then (1 ^2 ) = ((((x + y) ^2 ) + ((2 * (x + y)) * z)) + (z ^2 )) by SQUARE_1: 4

      .= ((((x ^2 ) + (y ^2 )) + (z ^2 )) + (2 * (((x * z) + (y * z)) + (x * y))));

      then (1 / 3) >= ((3 * (((x * z) + (y * z)) + (x * y))) / 3) by A2, XREAL_1: 72;

      hence thesis;

    end;

    theorem :: SERIES_3:18

    

     Th18: (x + y) = 1 implies (x * y) <= (1 / 4)

    proof

      ((x - y) ^2 ) >= 0 by XREAL_1: 63;

      then

       A1: ((((x ^2 ) - ((2 * x) * y)) + (y ^2 )) - (((x ^2 ) + ((2 * x) * y)) + (y ^2 ))) >= ( 0 - (((x ^2 ) + ((2 * x) * y)) + (y ^2 ))) by XREAL_1: 9;

      assume (x + y) = 1;

      then (1 ^2 ) = (((x ^2 ) + ((2 * x) * y)) + (y ^2 )) by SQUARE_1: 4;

      then ( - ((4 * x) * y)) >= ( - 1) by A1;

      then (4 * (x * y)) <= 1 by XREAL_1: 24;

      then ((4 * (x * y)) / 4) <= (1 / 4) by XREAL_1: 72;

      hence thesis;

    end;

    theorem :: SERIES_3:19

    (x + y) = 1 implies ((x ^2 ) + (y ^2 )) >= (1 / 2)

    proof

      ((x - y) ^2 ) >= 0 by XREAL_1: 63;

      then

       A1: ((((x ^2 ) - ((2 * x) * y)) + (y ^2 )) + (((x ^2 ) + ((2 * x) * y)) + (y ^2 ))) >= ( 0 + (((x ^2 ) + ((2 * x) * y)) + (y ^2 ))) by XREAL_1: 7;

      assume (x + y) = 1;

      then (1 ^2 ) = (((x ^2 ) + ((2 * x) * y)) + (y ^2 )) by SQUARE_1: 4;

      then ((2 * ((x ^2 ) + (y ^2 ))) / 2) >= (1 / 2) by A1, XREAL_1: 72;

      hence thesis;

    end;

    theorem :: SERIES_3:20

    (a + b) = 1 implies ((1 + (1 / a)) * (1 + (1 / b))) >= 9

    proof

      assume

       A1: (a + b) = 1;

      then (1 / (a * b)) >= (1 / (1 / 4)) by Th18, XREAL_1: 85;

      then ((1 / (a * b)) * ( - 2)) <= (4 * ( - 2)) by XREAL_1: 65;

      then ( - ((1 / (a * b)) * 2)) <= ( - 8);

      then ((1 / (a * b)) * 2) >= 8 by XREAL_1: 24;

      then

       A2: (1 + (2 * (1 / (a * b)))) >= (1 + 8) by XREAL_1: 7;

      ((1 + (1 / a)) * (1 + (1 / b))) = ((((1 * 1) + (1 * (1 / b))) + ((1 / a) * (1 / b))) + ((1 / a) * 1))

      .= (((1 + (1 / b)) + (1 / (a * b))) + (1 / a)) by XCMPLX_1: 102

      .= ((1 + ((1 / b) + (1 / a))) + (1 / (a * b)))

      .= ((1 + (((1 * a) + (b * 1)) / (a * b))) + (1 / (a * b))) by XCMPLX_1: 116

      .= ((1 + (1 / (a * b))) + (1 / (a * b))) by A1

      .= (1 + (2 * (1 / (a * b))));

      hence thesis by A2;

    end;

    theorem :: SERIES_3:21

    (x + y) = 1 implies ((x |^ 3) + (y |^ 3)) >= (1 / 4)

    proof

      assume

       A1: (x + y) = 1;

      then ((x * y) * ( - 3)) >= ((1 / 4) * ( - 3)) by Th18, XREAL_1: 65;

      then

       A2: (1 + ((x * y) * ( - 3))) >= (((1 / 4) * ( - 3)) + 1) by XREAL_1: 7;

      ((x |^ 3) + (y |^ 3)) = ((x + y) * (((x ^2 ) - (x * y)) + (y ^2 ))) by Lm6;

      

      then ((x |^ 3) + (y |^ 3)) = ((((x ^2 ) + ((2 * x) * y)) + (y ^2 )) - ((3 * x) * y)) by A1

      .= ((1 ^2 ) - (3 * (x * y))) by A1, SQUARE_1: 4;

      hence thesis by A2;

    end;

    theorem :: SERIES_3:22

    (a + b) = 1 implies ((a |^ 3) + (b |^ 3)) < 1

    proof

      assume

       A1: (a + b) = 1;

      

       A2: (1 + ((a * b) * ( - 3))) < ( 0 + 1) by XREAL_1: 8;

      ((a |^ 3) + (b |^ 3)) = ((a + b) * (((a ^2 ) - (a * b)) + (b ^2 ))) by Lm6;

      

      then ((a |^ 3) + (b |^ 3)) = ((((a ^2 ) + ((2 * a) * b)) + (b ^2 )) - ((3 * a) * b)) by A1

      .= ((1 ^2 ) - (3 * (a * b))) by A1, SQUARE_1: 4;

      hence thesis by A2;

    end;

    theorem :: SERIES_3:23

    (a + b) = 1 implies ((a + (1 / a)) * (b + (1 / b))) >= (25 / 4)

    proof

      assume

       A1: (a + b) = 1;

      then

       A2: (a * b) <= ((1 / 2) ^2 ) by Th4;

      then (1 - (a * b)) >= (1 - (1 / 4)) by XREAL_1: 10;

      then ((1 - (a * b)) ^2 ) >= ((3 / 4) ^2 ) by SQUARE_1: 15;

      then (1 + ((1 - (a * b)) ^2 )) >= (1 + (9 / 16)) by XREAL_1: 6;

      then

       A3: (4 * (1 + ((1 - (a * b)) ^2 ))) >= (4 * (25 / 16)) by XREAL_1: 64;

      ((1 - (a * b)) ^2 ) >= 0 by XREAL_1: 63;

      then

       A4: ((1 + ((1 - (a * b)) ^2 )) / (a * b)) >= ((1 + ((1 - (a * b)) ^2 )) / (1 / 4)) by A2, XREAL_1: 118;

      ((a ^2 ) + (b ^2 )) = ((((a ^2 ) + ((2 * a) * b)) + (b ^2 )) - ((2 * a) * b));

      then

       A5: ((a ^2 ) + (b ^2 )) = ((1 ^2 ) - ((2 * a) * b)) by A1, SQUARE_1: 4;

      ((a + (1 / a)) * (b + (1 / b))) = (((1 + (a ^2 )) / a) * (b + (1 / b))) by XCMPLX_1: 113

      .= (((1 + (a ^2 )) / a) * ((1 + (b ^2 )) / b)) by XCMPLX_1: 113

      .= (((1 + (a ^2 )) * (1 + (b ^2 ))) / (a * b)) by XCMPLX_1: 76

      .= ((1 + (((1 ^2 ) - (2 * (a * b))) + ((a ^2 ) * (b ^2 )))) / (a * b)) by A5

      .= ((1 + ((1 - (a * b)) ^2 )) / (a * b));

      hence thesis by A4, A3, XXREAL_0: 2;

    end;

    theorem :: SERIES_3:24

    for x,a be Real st |.x.| <= a holds (x ^2 ) <= (a ^2 )

    proof

      let x,a be Real;

      assume

       A1: |.x.| <= a;

      per cases ;

        suppose

         A2: x >= 0 ;

        x <= a by A1, ABSVALUE:def 1;

        hence thesis by A2, SQUARE_1: 15;

      end;

        suppose

         A3: x < 0 ;

        then ( - x) <= a by A1, ABSVALUE:def 1;

        then (( - x) ^2 ) <= (a ^2 ) by A3, SQUARE_1: 15;

        hence thesis;

      end;

    end;

    theorem :: SERIES_3:25

     |.x.| >= a implies (x ^2 ) >= (a ^2 )

    proof

      assume

       A1: |.x.| >= a;

      per cases ;

        suppose x >= 0 ;

        then x >= a by A1, ABSVALUE:def 1;

        hence thesis by SQUARE_1: 15;

      end;

        suppose x < 0 ;

        then ( - x) >= a by A1, ABSVALUE:def 1;

        then (( - x) ^2 ) >= (a ^2 ) by SQUARE_1: 15;

        hence thesis;

      end;

    end;

    theorem :: SERIES_3:26

     |.( |.x.| - |.y.|).| <= ( |.x.| + |.y.|)

    proof

       |.( |.x.| - |.y.|).| <= |.(x - y).| & |.(x - y).| <= ( |.x.| + |.y.|) by COMPLEX1: 57, COMPLEX1: 64;

      hence thesis by XXREAL_0: 2;

    end;

    theorem :: SERIES_3:27

    ((a * b) * c) = 1 implies (((1 / a) + (1 / b)) + (1 / c)) >= ((( sqrt a) + ( sqrt b)) + ( sqrt c))

    proof

      assume

       A1: ((a * b) * c) = 1;

      (((1 / a) + (1 / b)) / 2) >= ( sqrt ((1 / a) * (1 / b))) by Th2;

      then (((1 / a) + (1 / b)) / 2) >= ( sqrt (1 / (a * b))) by XCMPLX_1: 102;

      then

       A2: (((1 / a) + (1 / b)) / 2) >= ( sqrt ((1 * c) / ((a * b) * c))) by XCMPLX_1: 91;

      (((1 / c) + (1 / a)) / 2) >= ( sqrt ((1 / c) * (1 / a))) by Th2;

      then (((1 / c) + (1 / a)) / 2) >= ( sqrt (1 / (c * a))) by XCMPLX_1: 102;

      then

       A3: (((1 / c) + (1 / a)) / 2) >= ( sqrt ((1 * b) / ((c * a) * b))) by XCMPLX_1: 91;

      (((1 / b) + (1 / c)) / 2) >= ( sqrt ((1 / b) * (1 / c))) by Th2;

      then (((1 / b) + (1 / c)) / 2) >= ( sqrt (1 / (b * c))) by XCMPLX_1: 102;

      then (((1 / b) + (1 / c)) / 2) >= ( sqrt ((1 * a) / ((b * c) * a))) by XCMPLX_1: 91;

      then ((((1 / b) + (1 / c)) / 2) + (((1 / c) + (1 / a)) / 2)) >= (( sqrt a) + ( sqrt b)) by A1, A3, XREAL_1: 7;

      then (((((1 / b) + (1 / c)) / 2) + (((1 / c) + (1 / a)) / 2)) + (((1 / a) + (1 / b)) / 2)) >= ((( sqrt a) + ( sqrt b)) + ( sqrt c)) by A1, A2, XREAL_1: 7;

      hence thesis;

    end;

    theorem :: SERIES_3:28

    x > 0 & y > 0 & z < 0 & ((x + y) + z) = 0 implies ((((x |^ 2) + (y |^ 2)) + (z |^ 2)) |^ 3) >= (6 * ((((x |^ 3) + (y |^ 3)) + (z |^ 3)) ^2 ))

    proof

      assume that

       A1: x > 0 & y > 0 and

       A2: z < 0 and

       A3: ((x + y) + z) = 0 ;

      (3 -Root ((((x ^2 ) * (y ^2 )) * (z ^2 )) / 4)) > 0 by A1, A2, PREPOWER:def 2;

      then

       A4: (3 -root ((((x ^2 ) * (y ^2 )) * (z ^2 )) / 4)) > 0 by A1, A2, POWER:def 1;

      ((((x * (x + y)) / 2) + ((y * (x + y)) / 2)) + (x * y)) >= (3 * (3 -root ((((x * (x + y)) / 2) * ((y * (x + y)) / 2)) * (x * y)))) by A1, Th15;

      then ((((x * (x + y)) / 2) + ((y * (x + y)) / 2)) + (x * y)) >= (3 * (3 -root ((((x ^2 ) * (y ^2 )) * ((x + y) * (x + y))) / 4)));

      then

       A5: ((((x * (x + y)) / 2) + ((y * (x + y)) / 2)) + (x * y)) >= (3 * (3 -root ((((x ^2 ) * (y ^2 )) * (( - z) ^2 )) / 4))) by A3;

      ((3 * (3 -root ((((x ^2 ) * (y ^2 )) * (z ^2 )) / 4))) |^ 3) = ((3 |^ 3) * ((3 -root ((((x ^2 ) * (y ^2 )) * (z ^2 )) / 4)) |^ 3)) by NEWTON: 7

      .= (27 * ((3 -Root ((((x ^2 ) * (y ^2 )) * (z ^2 )) / 4)) |^ 3)) by A1, A2, Lm3, POWER:def 1

      .= (27 * ((((x ^2 ) * (y ^2 )) * (z ^2 )) / 4)) by A1, A2, PREPOWER: 19;

      then (((((x * (x + y)) / 2) + ((y * (x + y)) / 2)) + (x * y)) |^ 3) >= (27 * ((((x ^2 ) * (y ^2 )) * (z ^2 )) / 4)) by A5, A4, PREPOWER: 9;

      then

       A6: (8 * (((((x * (x + y)) / 2) + ((y * (x + y)) / 2)) + (x * y)) |^ 3)) >= (8 * (27 * ((((x ^2 ) * (y ^2 )) * (z ^2 )) / 4))) by XREAL_1: 64;

      (((x ^2 ) + (y ^2 )) / 2) >= (x * y) by Th7;

      then (((x |^ 2) + (y ^2 )) / 2) >= (x * y) by Lm1;

      then (((x |^ 2) + (y |^ 2)) / 2) >= (x * y) by Lm1;

      then (((((x |^ 2) + (x * y)) / 2) + (((x * y) + (y |^ 2)) / 2)) + (((x |^ 2) + (y |^ 2)) / 2)) >= (((((x |^ 2) + (x * y)) / 2) + (((x * y) + (y |^ 2)) / 2)) + (x * y)) by XREAL_1: 6;

      then (((((x |^ 2) + (x * y)) / 2) + (((x * y) + (y |^ 2)) / 2)) + (((x |^ 2) + (y |^ 2)) / 2)) >= (((((x ^2 ) + (x * y)) / 2) + (((x * y) + (y |^ 2)) / 2)) + (x * y)) by Lm1;

      then (((((x |^ 2) + (x * y)) / 2) + (((x * y) + (y |^ 2)) / 2)) + (((x |^ 2) + (y |^ 2)) / 2)) >= (((((x * x) + (x * y)) / 2) + (((x * y) + (y ^2 )) / 2)) + (x * y)) by Lm1;

      then ((((((x |^ 2) + (x * y)) / 2) + (((x * y) + (y |^ 2)) / 2)) + (((x |^ 2) + (y |^ 2)) / 2)) |^ 3) >= (((((x * (x + y)) / 2) + ((y * (x + y)) / 2)) + (x * y)) |^ 3) by A1, PREPOWER: 9;

      then (8 * ((((((x |^ 2) + (x * y)) / 2) + (((x * y) + (y |^ 2)) / 2)) + (((x |^ 2) + (y |^ 2)) / 2)) |^ 3)) >= (8 * (((((x * (x + y)) / 2) + ((y * (x + y)) / 2)) + (x * y)) |^ 3)) by XREAL_1: 64;

      then (8 * ((((x |^ 2) + (x * y)) + (y |^ 2)) |^ 3)) >= (54 * (((x ^2 ) * (y ^2 )) * (z ^2 ))) by A6, XXREAL_0: 2;

      then ((2 * (((x |^ 2) + (x * y)) + (y |^ 2))) |^ 3) >= (54 * (((x ^2 ) * (y ^2 )) * (z ^2 ))) by Lm2, NEWTON: 7;

      then ((((((x |^ 2) + ((2 * x) * y)) + (y |^ 2)) + (x |^ 2)) + (y |^ 2)) |^ 3) >= (54 * (((x ^2 ) * (y ^2 )) * (z ^2 )));

      then ((((((x ^2 ) + ((2 * x) * y)) + (y |^ 2)) + (x |^ 2)) + (y |^ 2)) |^ 3) >= (54 * (((x ^2 ) * (y ^2 )) * (z ^2 ))) by Lm1;

      then ((((((x ^2 ) + ((2 * x) * y)) + (y |^ 2)) + (x ^2 )) + (y |^ 2)) |^ 3) >= (54 * (((x ^2 ) * (y ^2 )) * (z ^2 ))) by Lm1;

      then ((((((x ^2 ) + ((2 * x) * y)) + (y ^2 )) + (x ^2 )) + (y |^ 2)) |^ 3) >= (54 * (((x ^2 ) * (y ^2 )) * (z ^2 ))) by Lm1;

      then

       A7: ((((((x ^2 ) + ((2 * x) * y)) + (y ^2 )) + (x ^2 )) + (y ^2 )) |^ 3) >= (54 * (((x ^2 ) * (y ^2 )) * (z ^2 ))) by Lm1;

      

       A8: z = ( - (x + y)) by A3;

      

      then (z |^ 3) = ( - ((x + y) |^ 3)) by Lm4

      .= ( - ((((x |^ 3) + ((3 * (x ^2 )) * y)) + ((3 * x) * (y ^2 ))) + (y |^ 3))) by Lm5;

      then ((((z |^ 2) + (x ^2 )) + (y ^2 )) |^ 3) >= (6 * ((((x |^ 3) + (y |^ 3)) + (z |^ 3)) ^2 )) by A8, A7, Lm1;

      then ((((z |^ 2) + (x |^ 2)) + (y ^2 )) |^ 3) >= (6 * ((((x |^ 3) + (y |^ 3)) + (z |^ 3)) ^2 )) by Lm1;

      then ((((z |^ 2) + (x |^ 2)) + (y |^ 2)) |^ 3) >= (6 * ((((x |^ 3) + (y |^ 3)) + (z |^ 3)) ^2 )) by Lm1;

      hence thesis;

    end;

    theorem :: SERIES_3:29

    a >= 1 implies ((a to_power b) + (a to_power c)) >= (2 * (a to_power ( sqrt (b * c))))

    proof

      

       A1: ((b + c) / 2) >= ((2 * ( sqrt (b * c))) / 2) by SIN_COS2: 1, XREAL_1: 72;

      set p = (a to_power c);

      set o = (a to_power b);

      o > 0 & p > 0 by POWER: 34;

      then ((a to_power b) + (a to_power c)) >= (2 * ( sqrt ((a to_power b) * (a to_power c)))) by SIN_COS2: 1;

      then (a to_power (b + c)) > 0 & ((a to_power b) + (a to_power c)) >= (2 * ( sqrt (a to_power (b + c)))) by POWER: 27, POWER: 34;

      then ((a to_power b) + (a to_power c)) >= (2 * ((a to_power (b + c)) to_power (1 / 2))) by ASYMPT_1: 83;

      then

       A2: ((a to_power b) + (a to_power c)) >= (2 * (a to_power ((1 / 2) * (b + c)))) by POWER: 33;

      assume a >= 1;

      then (a #R ((b + c) / 2)) >= (a #R ( sqrt (b * c))) by A1, PREPOWER: 82;

      then (a to_power ((b + c) / 2)) >= (a #R ( sqrt (b * c))) by POWER:def 2;

      then (a to_power ((b + c) / 2)) >= (a to_power ( sqrt (b * c))) by POWER:def 2;

      then (2 * (a to_power ((b + c) / 2))) >= (2 * (a to_power ( sqrt (b * c)))) by XREAL_1: 64;

      hence thesis by A2, XXREAL_0: 2;

    end;

    theorem :: SERIES_3:30

    a >= b & b >= c implies (((a to_power a) * (b to_power b)) * (c to_power c)) >= (((a * b) * c) to_power (((a + b) + c) / 3))

    proof

      assume that

       A1: a >= b and

       A2: b >= c;

      

       A3: ((b / c) to_power ((b - c) / 3)) = ((b / c) #R ((b - c) / 3)) by POWER:def 2;

      (b / c) >= 1 & (b - c) >= (c - c) by A2, XREAL_1: 9, XREAL_1: 181;

      then

       A4: ((b / c) to_power ((b - c) / 3)) >= 1 by A3, PREPOWER: 85;

      

       A5: ((a / b) to_power ((a - b) / 3)) = ((a / b) #R ((a - b) / 3)) by POWER:def 2;

      (a / b) >= 1 & (a - b) >= (b - b) by A1, XREAL_1: 9, XREAL_1: 181;

      then ((a / b) to_power ((a - b) / 3)) >= 1 by A5, PREPOWER: 85;

      then

       A6: (((a / b) to_power ((a - b) / 3)) * ((b / c) to_power ((b - c) / 3))) >= (1 * 1) by A4, XREAL_1: 66;

      a >= c by A1, A2, XXREAL_0: 2;

      then

       A7: (a / c) >= 1 & (a - c) >= (c - c) by XREAL_1: 9, XREAL_1: 181;

      ((a / c) to_power ((a - c) / 3)) = ((a / c) #R ((a - c) / 3)) by POWER:def 2;

      then ((a / c) to_power ((a - c) / 3)) >= 1 by A7, PREPOWER: 85;

      then ((((a / b) to_power ((a - b) / 3)) * ((b / c) to_power ((b - c) / 3))) * ((a / c) to_power ((a - c) / 3))) >= 1 by A6, XREAL_1: 66;

      then ((((a to_power ((a - b) / 3)) / (b to_power ((a - b) / 3))) * ((b / c) to_power ((b - c) / 3))) * ((a / c) to_power ((a - c) / 3))) >= 1 by POWER: 31;

      then

       A8: ((((a to_power ((a - b) / 3)) / (b to_power ((a - b) / 3))) * ((b to_power ((b - c) / 3)) / (c to_power ((b - c) / 3)))) * ((a / c) to_power ((a - c) / 3))) >= 1 by POWER: 31;

      set t = (b to_power (((a + b) + c) / 3));

      set s = (b to_power b);

      set r = (c to_power (((a + b) + c) / 3));

      set q = (c to_power c);

      set p = (a to_power (((a + b) + c) / 3));

      set o = (a to_power a);

      set j = (c to_power ((a - c) / 3));

      set i = (a to_power ((a - c) / 3));

      set h = (c to_power ((b - c) / 3));

      set w = (b to_power ((b - c) / 3));

      set v = (b to_power ((a - b) / 3));

      set u = (a to_power ((a - b) / 3));

      

       A9: p > 0 & r > 0 by POWER: 34;

      

       A10: t > 0 by POWER: 34;

      ((((a to_power ((a - b) / 3)) / (b to_power ((a - b) / 3))) * ((b to_power ((b - c) / 3)) / (c to_power ((b - c) / 3)))) * ((a to_power ((a - c) / 3)) / (c to_power ((a - c) / 3)))) = (((u * w) / (v * h)) * (i / j)) by XCMPLX_1: 76

      .= (((u * w) * i) / ((v * h) * j)) by XCMPLX_1: 76

      .= ((((a to_power ((a - b) / 3)) * (a to_power ((a - c) / 3))) * (b to_power ((b - c) / 3))) / (((b to_power ((a - b) / 3)) * (c to_power ((a - c) / 3))) * (c to_power ((b - c) / 3))))

      .= (((a to_power (((a - b) / 3) + ((a - c) / 3))) * (b to_power ((b - c) / 3))) / (((b to_power ((a - b) / 3)) * (c to_power ((a - c) / 3))) * (c to_power ((b - c) / 3)))) by POWER: 27

      .= (((a to_power ((((2 * a) - b) - c) / 3)) * (b to_power ((b - c) / 3))) / ((b to_power ((a - b) / 3)) * ((c to_power ((a - c) / 3)) * (c to_power ((b - c) / 3)))))

      .= (((a to_power ((((2 * a) - b) - c) / 3)) * (b to_power ((b - c) / 3))) / ((b to_power ((a - b) / 3)) * (c to_power (((a - c) / 3) + ((b - c) / 3))))) by POWER: 27

      .= (((a to_power ((((2 * a) - b) - c) / 3)) / (c to_power (((a + b) - (2 * c)) / 3))) * ((b to_power ((b - c) / 3)) / (b to_power ((a - b) / 3)))) by XCMPLX_1: 76

      .= (((a to_power ((((2 * a) - b) - c) / 3)) / (c to_power (((a + b) - (2 * c)) / 3))) * (b to_power (((b - c) / 3) - ((a - b) / 3)))) by POWER: 29

      .= (((1 / (c to_power (((a + b) - (2 * c)) / 3))) * (b to_power ((((2 * b) - a) - c) / 3))) * (a to_power ((((2 * a) - b) - c) / 3)))

      .= (((c to_power ( - (((a + b) - (2 * c)) / 3))) * (b to_power ((((2 * b) - a) - c) / 3))) * (a to_power ((((2 * a) - b) - c) / 3))) by POWER: 28

      .= (((a to_power (((3 * a) / 3) - (((a + b) + c) / 3))) * (c to_power (((3 * c) / 3) - (((a + b) + c) / 3)))) * (b to_power (((3 * b) / 3) - (((a + b) + c) / 3))))

      .= ((((a to_power ((3 * a) / 3)) / (a to_power (((a + b) + c) / 3))) * (c to_power (((3 * c) / 3) - (((a + b) + c) / 3)))) * (b to_power (((3 * b) / 3) - (((a + b) + c) / 3)))) by POWER: 29

      .= ((((a to_power ((3 * a) / 3)) / (a to_power (((a + b) + c) / 3))) * ((c to_power ((3 * c) / 3)) / (c to_power (((a + b) + c) / 3)))) * (b to_power (((3 * b) / 3) - (((a + b) + c) / 3)))) by POWER: 29

      .= ((((a to_power a) / (a to_power (((a + b) + c) / 3))) * ((c to_power c) / (c to_power (((a + b) + c) / 3)))) * ((b to_power b) / (b to_power (((a + b) + c) / 3)))) by POWER: 29

      .= (((o * q) / (p * r)) * (s / t)) by XCMPLX_1: 76

      .= ((((a to_power a) * (c to_power c)) * (b to_power b)) / (((a to_power (((a + b) + c) / 3)) * (c to_power (((a + b) + c) / 3))) * (b to_power (((a + b) + c) / 3)))) by XCMPLX_1: 76;

      then (((o * q) * s) / ((p * r) * t)) >= 1 by A8, POWER: 31;

      then ((((o * q) * s) / ((p * r) * t)) * ((p * r) * t)) >= (1 * ((p * r) * t)) by A9, A10, XREAL_1: 64;

      then (((a to_power a) * (c to_power c)) * (b to_power b)) >= (((a to_power (((a + b) + c) / 3)) * (c to_power (((a + b) + c) / 3))) * (b to_power (((a + b) + c) / 3))) by A9, A10, XCMPLX_1: 87;

      then (((a to_power a) * (c to_power c)) * (b to_power b)) >= (((a * c) to_power (((a + b) + c) / 3)) * (b to_power (((a + b) + c) / 3))) by POWER: 30;

      then ((a to_power a) * ((b to_power b) * (c to_power c))) >= (((a * c) * b) to_power (((a + b) + c) / 3)) by POWER: 30;

      hence thesis;

    end;

    theorem :: SERIES_3:31

    

     Th31: for a,b be non negative Real holds ((a + b) |^ (n + 2)) >= ((a |^ (n + 2)) + (((n + 2) * (a |^ (n + 1))) * b))

    proof

      let a,b be non negative Real;

      defpred X[ Nat] means ((a + b) |^ ($1 + 2)) >= ((a |^ ($1 + 2)) + ((($1 + 2) * (a |^ ($1 + 1))) * b));

      

       A1: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        (a |^ (n + 1)) >= 0

        proof

          per cases ;

            suppose a = 0 ;

            hence thesis;

          end;

            suppose a > 0 ;

            hence thesis by PREPOWER: 6;

          end;

        end;

        then

         A2: ((a |^ (n + 3)) + (((n + 3) * (a |^ (n + 2))) * b)) <= ((((n + 2) * (a |^ (n + 1))) * (b ^2 )) + ((a |^ (n + 3)) + (((n + 3) * (a |^ (n + 2))) * b))) by XREAL_1: 31;

        assume ((a + b) |^ (n + 2)) >= ((a |^ (n + 2)) + (((n + 2) * (a |^ (n + 1))) * b));

        then (((a + b) |^ (n + 2)) * (a + b)) >= (((a |^ (n + 2)) + (((n + 2) * (a |^ (n + 1))) * b)) * (a + b)) by XREAL_1: 64;

        then ((a + b) |^ ((n + 2) + 1)) >= (((a |^ (n + 2)) + (((n + 2) * (a |^ (n + 1))) * b)) * (a + b)) by NEWTON: 6;

        then ((a + b) |^ (n + 3)) >= ((((a |^ (n + 2)) * a) + (b * (a |^ (n + 2)))) + ((((n + 2) * (a + b)) * (a |^ (n + 1))) * b));

        then ((a + b) |^ (n + 3)) >= (((a |^ ((n + 2) + 1)) + (b * (a |^ (n + 2)))) + ((((n + 2) * (a + b)) * (a |^ (n + 1))) * b)) by NEWTON: 6;

        then ((a + b) |^ (n + 3)) >= ((((a |^ (n + 3)) + ((a |^ (n + 2)) * b)) + (((n + 2) * (a * (a |^ (n + 1)))) * b)) + (((n + 2) * (a |^ (n + 1))) * (b * b)));

        then ((a + b) |^ (n + 3)) >= ((((a |^ (n + 3)) + ((a |^ (n + 2)) * b)) + (((n + 2) * (a |^ ((n + 1) + 1))) * b)) + (((n + 2) * (a |^ (n + 1))) * (b * b))) by NEWTON: 6;

        hence thesis by A2, XXREAL_0: 2;

      end;

      

       A3: ((a |^ ( 0 + 2)) + ((( 0 + 2) * (a |^ ( 0 + 1))) * b)) = ((a ^2 ) + ((2 * (a |^ 1)) * b)) by Lm1

      .= ((a ^2 ) + ((2 * a) * b));

      ((a + b) |^ ( 0 + 2)) = ((a + b) ^2 ) by Lm1

      .= (((a ^2 ) + ((2 * a) * b)) + (b ^2 ));

      then

       A4: X[ 0 ] by A3, XREAL_1: 31;

      for n holds X[n] from NAT_1:sch 2( A4, A1);

      hence thesis;

    end;

    theorem :: SERIES_3:32

    (((a |^ n) + (b |^ n)) / 2) >= (((a + b) / 2) |^ n)

    proof

      defpred X[ Nat] means (((a |^ $1) + (b |^ $1)) / 2) >= (((a + b) / 2) |^ $1);

      

       A1: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        assume X[n];

        then

         A2: ((((a |^ n) + (b |^ n)) / 2) * (a + b)) >= ((((a + b) / 2) |^ n) * (a + b)) by XREAL_1: 64;

        per cases ;

          suppose

           A3: (a - b) >= 0 ;

          then ((a - b) + b) >= ( 0 + b) by XREAL_1: 6;

          then (a |^ n) >= (b |^ n) by PREPOWER: 9;

          then ((a |^ n) - (b |^ n)) >= 0 by XREAL_1: 48;

          then ((a - b) * ((a |^ n) - (b |^ n))) >= 0 by A3;

          then ((((a |^ n) * a) - ((a |^ n) * b)) - (((b |^ n) * a) - ((b |^ n) * b))) >= 0 ;

          then (((a |^ (n + 1)) - ((a |^ n) * b)) - (((b |^ n) * a) - ((b |^ n) * b))) >= 0 by NEWTON: 6;

          then ((((a |^ (n + 1)) - ((a |^ n) * b)) - ((b |^ n) * a)) + ((b |^ n) * b)) >= 0 ;

          then ((((a |^ (n + 1)) - ((a |^ n) * b)) - ((b |^ n) * a)) + (b |^ (n + 1))) >= 0 by NEWTON: 6;

          then (((((a |^ (n + 1)) - ((a |^ n) * b)) - ((b |^ n) * a)) + (b |^ (n + 1))) + (((a |^ n) * b) + ((b |^ n) * a))) >= ( 0 + (((a |^ n) * b) + ((b |^ n) * a))) by XREAL_1: 6;

          then (((a |^ (n + 1)) + (b |^ (n + 1))) + ((a |^ (n + 1)) + (b |^ (n + 1)))) >= ((((a |^ n) * b) + ((b |^ n) * a)) + ((a |^ (n + 1)) + (b |^ (n + 1)))) by XREAL_1: 6;

          then ((2 * (a |^ (n + 1))) + (2 * (b |^ (n + 1)))) >= ((((a |^ (n + 1)) + ((a |^ n) * b)) + ((b |^ n) * a)) + (b |^ (n + 1)));

          then ((2 * (a |^ (n + 1))) + (2 * (b |^ (n + 1)))) >= (((((a |^ n) * a) + ((a |^ n) * b)) + ((b |^ n) * a)) + (b |^ (n + 1))) by NEWTON: 6;

          then ((2 * (a |^ (n + 1))) + (2 * (b |^ (n + 1)))) >= (((((a |^ n) * a) + ((a |^ n) * b)) + ((b |^ n) * a)) + ((b |^ n) * b)) by NEWTON: 6;

          then ((2 * ((a |^ (n + 1)) + (b |^ (n + 1)))) / 2) >= ((((a |^ n) + (b |^ n)) * (a + b)) / 2) by XREAL_1: 72;

          then ((a |^ (n + 1)) + (b |^ (n + 1))) >= ((((a + b) / 2) |^ n) * (a + b)) by A2, XXREAL_0: 2;

          then ((a |^ (n + 1)) + (b |^ (n + 1))) >= ((((a + b) |^ n) / (2 |^ n)) * (a + b)) by PREPOWER: 8;

          then ((a |^ (n + 1)) + (b |^ (n + 1))) >= ((((a + b) |^ n) * (a + b)) / (2 |^ n));

          then ((a |^ (n + 1)) + (b |^ (n + 1))) >= (((a + b) |^ (n + 1)) / (2 |^ n)) by NEWTON: 6;

          then (((a |^ (n + 1)) + (b |^ (n + 1))) / 2) >= ((((a + b) |^ (n + 1)) / (2 |^ n)) / 2) by XREAL_1: 72;

          then (((a |^ (n + 1)) + (b |^ (n + 1))) / 2) >= (((a + b) |^ (n + 1)) / ((2 |^ n) * 2)) by XCMPLX_1: 78;

          then (((a |^ (n + 1)) + (b |^ (n + 1))) / 2) >= (((a + b) |^ (n + 1)) / (2 |^ (n + 1))) by NEWTON: 6;

          hence thesis by PREPOWER: 8;

        end;

          suppose

           A4: (a - b) < 0 ;

          then ((a - b) + b) < ( 0 + b) by XREAL_1: 6;

          then (a |^ n) <= (b |^ n) by PREPOWER: 9;

          then ((a |^ n) - (b |^ n)) <= 0 by XREAL_1: 47;

          then ((a - b) * ((a |^ n) - (b |^ n))) >= 0 by A4;

          then ((((a |^ n) * a) - ((a |^ n) * b)) - (((b |^ n) * a) - ((b |^ n) * b))) >= 0 ;

          then (((a |^ (n + 1)) - ((a |^ n) * b)) - (((b |^ n) * a) - ((b |^ n) * b))) >= 0 by NEWTON: 6;

          then ((((a |^ (n + 1)) - ((a |^ n) * b)) - ((b |^ n) * a)) + ((b |^ n) * b)) >= 0 ;

          then ((((a |^ (n + 1)) - ((a |^ n) * b)) - ((b |^ n) * a)) + (b |^ (n + 1))) >= 0 by NEWTON: 6;

          then (((((a |^ (n + 1)) - ((a |^ n) * b)) - ((b |^ n) * a)) + (b |^ (n + 1))) + (((a |^ n) * b) + ((b |^ n) * a))) >= ( 0 + (((a |^ n) * b) + ((b |^ n) * a))) by XREAL_1: 6;

          then (((a |^ (n + 1)) + (b |^ (n + 1))) + ((a |^ (n + 1)) + (b |^ (n + 1)))) >= ((((a |^ n) * b) + ((b |^ n) * a)) + ((a |^ (n + 1)) + (b |^ (n + 1)))) by XREAL_1: 6;

          then ((2 * (a |^ (n + 1))) + (2 * (b |^ (n + 1)))) >= ((((a |^ (n + 1)) + ((a |^ n) * b)) + ((b |^ n) * a)) + (b |^ (n + 1)));

          then ((2 * (a |^ (n + 1))) + (2 * (b |^ (n + 1)))) >= (((((a |^ n) * a) + ((a |^ n) * b)) + ((b |^ n) * a)) + (b |^ (n + 1))) by NEWTON: 6;

          then ((2 * (a |^ (n + 1))) + (2 * (b |^ (n + 1)))) >= (((((a |^ n) * a) + ((a |^ n) * b)) + ((b |^ n) * a)) + ((b |^ n) * b)) by NEWTON: 6;

          then ((2 * ((a |^ (n + 1)) + (b |^ (n + 1)))) / 2) >= ((((a |^ n) + (b |^ n)) * (a + b)) / 2) by XREAL_1: 72;

          then ((a |^ (n + 1)) + (b |^ (n + 1))) >= ((((a + b) / 2) |^ n) * (a + b)) by A2, XXREAL_0: 2;

          then ((a |^ (n + 1)) + (b |^ (n + 1))) >= ((((a + b) |^ n) / (2 |^ n)) * (a + b)) by PREPOWER: 8;

          then ((a |^ (n + 1)) + (b |^ (n + 1))) >= ((((a + b) |^ n) * (a + b)) / (2 |^ n));

          then ((a |^ (n + 1)) + (b |^ (n + 1))) >= (((a + b) |^ (n + 1)) / (2 |^ n)) by NEWTON: 6;

          then (((a |^ (n + 1)) + (b |^ (n + 1))) / 2) >= ((((a + b) |^ (n + 1)) / (2 |^ n)) / 2) by XREAL_1: 72;

          then (((a |^ (n + 1)) + (b |^ (n + 1))) / 2) >= (((a + b) |^ (n + 1)) / ((2 |^ n) * 2)) by XCMPLX_1: 78;

          then (((a |^ (n + 1)) + (b |^ (n + 1))) / 2) >= (((a + b) |^ (n + 1)) / (2 |^ (n + 1))) by NEWTON: 6;

          hence thesis by PREPOWER: 8;

        end;

      end;

      (((a |^ 0 ) + (b |^ 0 )) / 2) = ((1 + (b |^ 0 )) / 2) by NEWTON: 4

      .= ((1 + 1) / 2) by NEWTON: 4

      .= (((a + b) / 2) |^ 0 ) by NEWTON: 4;

      then

       A5: X[ 0 ];

      for n holds X[n] from NAT_1:sch 2( A5, A1);

      hence thesis;

    end;

    theorem :: SERIES_3:33

    

     Th33: (for n holds (s . n) > 0 ) implies for n holds (( Partial_Sums s) . n) > 0

    proof

      defpred X[ Nat] means (( Partial_Sums s) . $1) > 0 ;

      assume

       A1: for n holds (s . n) > 0 ;

      

       A2: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        

         A3: (( Partial_Sums s) . (n + 1)) = ((( Partial_Sums s) . n) + (s . (n + 1))) by SERIES_1:def 1;

        assume (( Partial_Sums s) . n) > 0 ;

        hence thesis by A1, A3, XREAL_1: 34;

      end;

      (( Partial_Sums s) . 0 ) = (s . 0 ) by SERIES_1:def 1;

      then

       A4: X[ 0 ] by A1;

      for n holds X[n] from NAT_1:sch 2( A4, A2);

      hence thesis;

    end;

    theorem :: SERIES_3:34

    

     Th34: (for n holds (s . n) >= 0 ) implies for n holds (( Partial_Sums s) . n) >= 0

    proof

      defpred X[ Nat] means (( Partial_Sums s) . $1) >= 0 ;

      assume

       A1: for n holds (s . n) >= 0 ;

      

       A2: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        assume

         A3: (( Partial_Sums s) . n) >= 0 ;

        (( Partial_Sums s) . (n + 1)) = ((( Partial_Sums s) . n) + (s . (n + 1))) & (s . (n + 1)) >= 0 by A1, SERIES_1:def 1;

        hence thesis by A3;

      end;

      (( Partial_Sums s) . 0 ) = (s . 0 ) by SERIES_1:def 1;

      then

       A4: X[ 0 ] by A1;

      for n holds X[n] from NAT_1:sch 2( A4, A2);

      hence thesis;

    end;

    theorem :: SERIES_3:35

    

     Th35: (for n holds (s . n) < 0 ) implies (( Partial_Sums s) . n) < 0

    proof

      defpred X[ Nat] means (( Partial_Sums s) . $1) < 0 ;

      assume

       A1: for n holds (s . n) < 0 ;

      

       A2: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        assume

         A3: (( Partial_Sums s) . n) < 0 ;

        (( Partial_Sums s) . (n + 1)) = ((( Partial_Sums s) . n) + (s . (n + 1))) & (s . (n + 1)) < 0 by A1, SERIES_1:def 1;

        hence thesis by A3;

      end;

      (( Partial_Sums s) . 0 ) = (s . 0 ) by SERIES_1:def 1;

      then

       A4: X[ 0 ] by A1;

      for n holds X[n] from NAT_1:sch 2( A4, A2);

      hence thesis;

    end;

    theorem :: SERIES_3:36

    

     Th36: s = (s1 (#) s1) implies for n holds (( Partial_Sums s) . n) >= 0

    proof

      defpred X[ Nat] means (( Partial_Sums s) . $1) >= 0 ;

      assume

       A1: s = (s1 (#) s1);

      

       A2: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        assume

         A3: (( Partial_Sums s) . n) >= 0 ;

        

         A4: ((s1 . (n + 1)) ^2 ) >= 0 by XREAL_1: 63;

        (( Partial_Sums s) . (n + 1)) = ((( Partial_Sums s) . n) + (s . (n + 1))) by SERIES_1:def 1

        .= ((( Partial_Sums s) . n) + ((s1 . (n + 1)) ^2 )) by A1, SEQ_1: 8;

        hence thesis by A3, A4;

      end;

      (( Partial_Sums s) . 0 ) = (s . 0 ) by SERIES_1:def 1

      .= ((s1 . 0 ) ^2 ) by A1, SEQ_1: 8;

      then

       A5: X[ 0 ] by XREAL_1: 63;

      for n holds X[n] from NAT_1:sch 2( A5, A2);

      hence thesis;

    end;

    theorem :: SERIES_3:37

    (for n holds (s . n) > 0 & (s . n) > (s . (n - 1))) implies ((n + 1) * (s . (n + 1))) > (( Partial_Sums s) . n)

    proof

      defpred X[ Nat] means (($1 + 1) * (s . ($1 + 1))) > (( Partial_Sums s) . $1);

      assume

       A1: for n holds (s . n) > 0 & (s . n) > (s . (n - 1));

      

       A2: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        assume ((n + 1) * (s . (n + 1))) > (( Partial_Sums s) . n);

        then

         A3: ((( Partial_Sums s) . n) + (s . (n + 1))) < (((n + 1) * (s . (n + 1))) + (s . (n + 1))) by XREAL_1: 6;

        (s . (n + 2)) > (s . ((n + 2) - 1)) by A1;

        then ((n + 2) * (s . (n + 2))) > ((n + 2) * (s . (n + 1))) by XREAL_1: 68;

        then ((( Partial_Sums s) . n) + (s . (n + 1))) < ((n + 2) * (s . (n + 2))) by A3, XXREAL_0: 2;

        hence thesis by SERIES_1:def 1;

      end;

      (s . 1) > (s . (1 - 1)) by A1;

      then

       A4: X[ 0 ] by SERIES_1:def 1;

      for n holds X[n] from NAT_1:sch 2( A4, A2);

      hence thesis;

    end;

    theorem :: SERIES_3:38

    

     Th38: (for n holds (s . n) > 0 & (s . n) >= (s . (n - 1))) implies ((n + 1) * (s . (n + 1))) >= (( Partial_Sums s) . n)

    proof

      defpred X[ Nat] means (($1 + 1) * (s . ($1 + 1))) >= (( Partial_Sums s) . $1);

      assume

       A1: for n holds (s . n) > 0 & (s . n) >= (s . (n - 1));

      

       A2: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        assume ((n + 1) * (s . (n + 1))) >= (( Partial_Sums s) . n);

        then

         A3: ((( Partial_Sums s) . n) + (s . (n + 1))) <= (((n + 1) * (s . (n + 1))) + (s . (n + 1))) by XREAL_1: 6;

        (s . (n + 2)) >= (s . ((n + 2) - 1)) by A1;

        then ((n + 2) * (s . (n + 2))) >= ((n + 2) * (s . (n + 1))) by XREAL_1: 64;

        then ((( Partial_Sums s) . n) + (s . (n + 1))) <= ((n + 2) * (s . (n + 2))) by A3, XXREAL_0: 2;

        hence thesis by SERIES_1:def 1;

      end;

      (s . 1) >= (s . (1 - 1)) by A1;

      then

       A4: X[ 0 ] by SERIES_1:def 1;

      for n holds X[n] from NAT_1:sch 2( A4, A2);

      hence thesis;

    end;

    theorem :: SERIES_3:39

    (s = (s1 (#) s2) & for n holds (s1 . n) >= 0 & (s2 . n) >= 0 ) implies for n holds (( Partial_Sums s) . n) <= ((( Partial_Sums s1) . n) * (( Partial_Sums s2) . n))

    proof

      assume that

       A1: s = (s1 (#) s2) and

       A2: for n holds (s1 . n) >= 0 & (s2 . n) >= 0 ;

      defpred X[ Nat] means (( Partial_Sums s) . $1) <= ((( Partial_Sums s1) . $1) * (( Partial_Sums s2) . $1));

      

       A3: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        set j = (( Partial_Sums s) . n);

        set u = (( Partial_Sums s1) . n);

        set v = (( Partial_Sums s2) . n);

        set w = (s1 . (n + 1));

        set h = (s2 . (n + 1));

        

         A4: ((( Partial_Sums s1) . (n + 1)) * (( Partial_Sums s2) . (n + 1))) = (((( Partial_Sums s1) . n) + (s1 . (n + 1))) * (( Partial_Sums s2) . (n + 1))) by SERIES_1:def 1

        .= ((u + w) * (v + h)) by SERIES_1:def 1

        .= ((((u * v) + (u * h)) + (w * v)) + (w * h));

        assume (( Partial_Sums s) . n) <= ((( Partial_Sums s1) . n) * (( Partial_Sums s2) . n));

        then

         A5: (j + (w * h)) <= ((u * v) + (w * h)) by XREAL_1: 6;

        

         A6: w >= 0 & h >= 0 by A2;

        u >= 0 & v >= 0 by A2, Th34;

        then

         A7: ((u * v) + (w * h)) <= (((u * v) + (w * h)) + ((u * h) + (w * v))) by A6, XREAL_1: 31;

        (( Partial_Sums s) . (n + 1)) = ((( Partial_Sums s) . n) + (s . (n + 1))) by SERIES_1:def 1

        .= ((( Partial_Sums s) . n) + ((s1 . (n + 1)) * (s2 . (n + 1)))) by A1, SEQ_1: 8;

        hence thesis by A4, A5, A7, XXREAL_0: 2;

      end;

      

       A8: ((( Partial_Sums s1) . 0 ) * (( Partial_Sums s2) . 0 )) = ((s1 . 0 ) * (( Partial_Sums s2) . 0 )) by SERIES_1:def 1

      .= ((s1 . 0 ) * (s2 . 0 )) by SERIES_1:def 1;

      (( Partial_Sums s) . 0 ) = (s . 0 ) by SERIES_1:def 1

      .= ((s1 . 0 ) * (s2 . 0 )) by A1, SEQ_1: 8;

      then

       A9: X[ 0 ] by A8;

      for n holds X[n] from NAT_1:sch 2( A9, A3);

      hence thesis;

    end;

    theorem :: SERIES_3:40

    (s = (s1 (#) s2) & for n holds (s1 . n) < 0 & (s2 . n) < 0 ) implies (( Partial_Sums s) . n) <= ((( Partial_Sums s1) . n) * (( Partial_Sums s2) . n))

    proof

      assume that

       A1: s = (s1 (#) s2) and

       A2: for n holds (s1 . n) < 0 & (s2 . n) < 0 ;

      defpred X[ Nat] means (( Partial_Sums s) . $1) <= ((( Partial_Sums s1) . $1) * (( Partial_Sums s2) . $1));

      

       A3: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        set j = (( Partial_Sums s) . n);

        set u = (( Partial_Sums s1) . n);

        set v = (( Partial_Sums s2) . n);

        set w = (s1 . (n + 1));

        set h = (s2 . (n + 1));

        

         A4: ((( Partial_Sums s1) . (n + 1)) * (( Partial_Sums s2) . (n + 1))) = (((( Partial_Sums s1) . n) + (s1 . (n + 1))) * (( Partial_Sums s2) . (n + 1))) by SERIES_1:def 1

        .= ((u + w) * (v + h)) by SERIES_1:def 1

        .= ((((u * v) + (u * h)) + (w * v)) + (w * h));

        assume (( Partial_Sums s) . n) <= ((( Partial_Sums s1) . n) * (( Partial_Sums s2) . n));

        then

         A5: (j + (w * h)) <= ((u * v) + (w * h)) by XREAL_1: 6;

        

         A6: w < 0 & h < 0 by A2;

        u < 0 & v < 0 by A2, Th35;

        then

         A7: ((u * v) + (w * h)) <= (((u * v) + (w * h)) + ((u * h) + (w * v))) by A6, XREAL_1: 31;

        (( Partial_Sums s) . (n + 1)) = ((( Partial_Sums s) . n) + (s . (n + 1))) by SERIES_1:def 1

        .= ((( Partial_Sums s) . n) + ((s1 . (n + 1)) * (s2 . (n + 1)))) by A1, SEQ_1: 8;

        hence thesis by A4, A5, A7, XXREAL_0: 2;

      end;

      

       A8: ((( Partial_Sums s1) . 0 ) * (( Partial_Sums s2) . 0 )) = ((s1 . 0 ) * (( Partial_Sums s2) . 0 )) by SERIES_1:def 1

      .= ((s1 . 0 ) * (s2 . 0 )) by SERIES_1:def 1;

      (( Partial_Sums s) . 0 ) = (s . 0 ) by SERIES_1:def 1

      .= ((s1 . 0 ) * (s2 . 0 )) by A1, SEQ_1: 8;

      then

       A9: X[ 0 ] by A8;

      for n holds X[n] from NAT_1:sch 2( A9, A3);

      hence thesis;

    end;

    theorem :: SERIES_3:41

    

     Th41: for n holds |.(( Partial_Sums s) . n).| <= (( Partial_Sums ( abs s)) . n)

    proof

      set s1 = ( abs s);

      defpred X[ Nat] means |.(( Partial_Sums s) . $1).| <= (( Partial_Sums s1) . $1);

      let n;

      

       A1: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        assume |.(( Partial_Sums s) . n).| <= (( Partial_Sums s1) . n);

        then

         A2: ( |.(( Partial_Sums s) . n).| + |.(s . (n + 1)).|) <= ((( Partial_Sums s1) . n) + |.(s . (n + 1)).|) by XREAL_1: 6;

        (( Partial_Sums s1) . (n + 1)) = ((( Partial_Sums s1) . n) + (s1 . (n + 1))) by SERIES_1:def 1;

        then

         A3: (( Partial_Sums s1) . (n + 1)) = ((( Partial_Sums s1) . n) + |.(s . (n + 1)).|) by SEQ_1: 12;

         |.(( Partial_Sums s) . (n + 1)).| = |.((( Partial_Sums s) . n) + (s . (n + 1))).| & |.((( Partial_Sums s) . n) + (s . (n + 1))).| <= ( |.(( Partial_Sums s) . n).| + |.(s . (n + 1)).|) by COMPLEX1: 56, SERIES_1:def 1;

        hence thesis by A3, A2, XXREAL_0: 2;

      end;

      (s1 . 0 ) = |.(s . 0 ).| by SEQ_1: 12;

      then (( Partial_Sums s1) . 0 ) = |.(s . 0 ).| by SERIES_1:def 1;

      then

       A4: X[ 0 ] by SERIES_1:def 1;

      for n holds X[n] from NAT_1:sch 2( A4, A1);

      hence thesis;

    end;

    theorem :: SERIES_3:42

    (( Partial_Sums s) . n) <= (( Partial_Sums ( abs s)) . n)

    proof

      set s1 = ( abs s);

      (( Partial_Sums s) . n) <= |.(( Partial_Sums s) . n).| & |.(( Partial_Sums s) . n).| <= (( Partial_Sums s1) . n) by Th41, ABSVALUE: 4;

      hence thesis by XXREAL_0: 2;

    end;

    definition

      let s;

      :: SERIES_3:def1

      func Partial_Product (s) -> Real_Sequence means

      : Def1: (it . 0 ) = (s . 0 ) & for n holds (it . (n + 1)) = ((it . n) * (s . (n + 1)));

      existence

      proof

        deffunc U( Nat, Real) = ( In (($2 * (s . ($1 + 1))), REAL ));

        consider f be sequence of REAL such that

         A1: (f . 0 ) = (s . 0 ) & for n be Nat holds (f . (n + 1)) = U(n,.) from NAT_1:sch 12;

        reconsider f as Real_Sequence;

        take f;

        thus (f . 0 ) = (s . 0 ) by A1;

        let n be Nat;

        (f . (n + 1)) = U(n,.) by A1;

        hence thesis;

      end;

      uniqueness

      proof

        let s1, s2;

        assume that

         A2: (s1 . 0 ) = (s . 0 ) and

         A3: for n holds (s1 . (n + 1)) = ((s1 . n) * (s . (n + 1))) and

         A4: (s2 . 0 ) = (s . 0 ) and

         A5: for n holds (s2 . (n + 1)) = ((s2 . n) * (s . (n + 1)));

        defpred X[ Nat] means (s1 . $1) = (s2 . $1);

        

         A6: for n st X[n] holds X[(n + 1)]

        proof

          let n;

          assume (s1 . n) = (s2 . n);

          

          hence (s1 . (n + 1)) = ((s2 . n) * (s . (n + 1))) by A3

          .= (s2 . (n + 1)) by A5;

        end;

        

         A7: X[ 0 ] by A2, A4;

        for n holds X[n] from NAT_1:sch 2( A7, A6);

        then for n be Element of NAT holds X[n];

        hence s1 = s2 by FUNCT_2: 63;

      end;

    end

    theorem :: SERIES_3:43

    

     Th43: (for n holds (s . n) > 0 ) implies (( Partial_Product s) . n) > 0

    proof

      defpred X[ Nat] means (( Partial_Product s) . $1) > 0 ;

      assume

       A1: for n holds (s . n) > 0 ;

      

       A2: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        assume

         A3: (( Partial_Product s) . n) > 0 ;

        (( Partial_Product s) . (n + 1)) = ((( Partial_Product s) . n) * (s . (n + 1))) & (s . (n + 1)) > 0 by A1, Def1;

        hence thesis by A3;

      end;

      (s . 0 ) > 0 by A1;

      then

       A4: X[ 0 ] by Def1;

      for n holds X[n] from NAT_1:sch 2( A4, A2);

      hence thesis;

    end;

    theorem :: SERIES_3:44

    

     Th44: (for n holds (s . n) >= 0 ) implies (( Partial_Product s) . n) >= 0

    proof

      defpred X[ Nat] means (( Partial_Product s) . $1) >= 0 ;

      assume

       A1: for n holds (s . n) >= 0 ;

      

       A2: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        assume

         A3: (( Partial_Product s) . n) >= 0 ;

        (( Partial_Product s) . (n + 1)) = ((( Partial_Product s) . n) * (s . (n + 1))) & (s . (n + 1)) >= 0 by A1, Def1;

        hence thesis by A3;

      end;

      (s . 0 ) >= 0 by A1;

      then

       A4: X[ 0 ] by Def1;

      for n holds X[n] from NAT_1:sch 2( A4, A2);

      hence thesis;

    end;

    theorem :: SERIES_3:45

    (for n holds (s . n) > 0 & (s . n) < 1) implies for n holds (( Partial_Product s) . n) > 0 & (( Partial_Product s) . n) < 1

    proof

      defpred X[ Nat] means (( Partial_Product s) . $1) > 0 & (( Partial_Product s) . $1) < 1;

      assume

       A1: for n holds (s . n) > 0 & (s . n) < 1;

      

       A2: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        assume

         A3: (( Partial_Product s) . n) > 0 & (( Partial_Product s) . n) < 1;

        (( Partial_Product s) . (n + 1)) = ((( Partial_Product s) . n) * (s . (n + 1))) & (s . (n + 1)) > 0 by A1, Def1;

        hence thesis by A1, A3, XREAL_1: 162;

      end;

      (( Partial_Product s) . 0 ) = (s . 0 ) by Def1;

      then

       A4: X[ 0 ] by A1;

      for n holds X[n] from NAT_1:sch 2( A4, A2);

      hence thesis;

    end;

    theorem :: SERIES_3:46

    (for n holds (s . n) >= 1) implies for n holds (( Partial_Product s) . n) >= 1

    proof

      defpred X[ Nat] means (( Partial_Product s) . $1) >= 1;

      assume

       A1: for n holds (s . n) >= 1;

      

       A2: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        

         A3: (( Partial_Product s) . (n + 1)) = ((( Partial_Product s) . n) * (s . (n + 1))) by Def1;

        assume

         A4: (( Partial_Product s) . n) >= 1;

        then (( Partial_Product s) . n) <= ((( Partial_Product s) . n) * (s . (n + 1))) by A1, XREAL_1: 151;

        hence thesis by A4, A3, XXREAL_0: 2;

      end;

      (( Partial_Product s) . 0 ) = (s . 0 ) by Def1;

      then

       A5: X[ 0 ] by A1;

      for n holds X[n] from NAT_1:sch 2( A5, A2);

      hence thesis;

    end;

    theorem :: SERIES_3:47

    (for n holds (s1 . n) >= 0 & (s2 . n) >= 0 ) implies for n holds ((( Partial_Product s1) . n) + (( Partial_Product s2) . n)) <= (( Partial_Product (s1 + s2)) . n)

    proof

      set s = (s1 + s2);

      defpred X[ Nat] means ((( Partial_Product s1) . $1) + (( Partial_Product s2) . $1)) <= (( Partial_Product s) . $1);

      

       A1: (( Partial_Product s) . 0 ) = (s . 0 ) by Def1

      .= ((s1 . 0 ) + (s2 . 0 )) by SEQ_1: 7;

      assume

       A2: for n holds (s1 . n) >= 0 & (s2 . n) >= 0 ;

      

       A3: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        set u = (( Partial_Product s1) . n);

        set v = (( Partial_Product s2) . n);

        set w = (( Partial_Product s) . n);

        set h = (s1 . (n + 1));

        set j = (s2 . (n + 1));

        

         A4: h >= 0 & j >= 0 by A2;

        u >= 0 & v >= 0 by A2, Th44;

        then

         A5: ((u * h) + (v * j)) <= (((u * h) + (v * j)) + ((u * j) + (v * h))) by A4, XREAL_1: 31;

        

         A6: (( Partial_Product s) . (n + 1)) = ((( Partial_Product s) . n) * (s . (n + 1))) by Def1

        .= (w * (h + j)) by SEQ_1: 7;

        assume ((( Partial_Product s1) . n) + (( Partial_Product s2) . n)) <= (( Partial_Product s) . n);

        then

         A7: ((u + v) * (h + j)) <= (w * (h + j)) by A4, XREAL_1: 64;

        ((( Partial_Product s1) . (n + 1)) + (( Partial_Product s2) . (n + 1))) = (((( Partial_Product s1) . n) * (s1 . (n + 1))) + (( Partial_Product s2) . (n + 1))) by Def1

        .= ((u * h) + (v * j)) by Def1;

        hence thesis by A7, A6, A5, XXREAL_0: 2;

      end;

      ((( Partial_Product s1) . 0 ) + (( Partial_Product s2) . 0 )) = ((s1 . 0 ) + (( Partial_Product s2) . 0 )) by Def1

      .= ((s1 . 0 ) + (s2 . 0 )) by Def1;

      then

       A8: X[ 0 ] by A1;

      for n holds X[n] from NAT_1:sch 2( A8, A3);

      hence thesis;

    end;

    theorem :: SERIES_3:48

    (for n holds (s . n) = (((2 * n) + 1) / ((2 * n) + 2))) implies (( Partial_Product s) . n) <= (1 / ( sqrt ((3 * n) + 4)))

    proof

      defpred X[ Nat] means (( Partial_Product s) . $1) <= (1 / ( sqrt ((3 * $1) + 4)));

      assume

       A1: for n holds (s . n) = (((2 * n) + 1) / ((2 * n) + 2));

      

       A2: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        assume (( Partial_Product s) . n) <= (1 / ( sqrt ((3 * n) + 4)));

        then ((( Partial_Product s) . n) * (((2 * n) + 3) / ((2 * n) + 4))) <= ((1 / ( sqrt ((3 * n) + 4))) * (((2 * n) + 3) / ((2 * n) + 4))) by XREAL_1: 64;

        then

         A3: ((( Partial_Product s) . n) * (((2 * n) + 3) / ((2 * n) + 4))) <= ((1 * ((2 * n) + 3)) / (( sqrt ((3 * n) + 4)) * ((2 * n) + 4))) by XCMPLX_1: 76;

        (111 * n) <= (112 * n) by XREAL_1: 64;

        then ((111 * n) + 63) <= ((112 * n) + 64) by XREAL_1: 7;

        then (((12 * (n |^ 3)) + (64 * (n ^2 ))) + ((111 * n) + 63)) <= (((12 * (n |^ 3)) + (64 * (n ^2 ))) + ((112 * n) + 64)) by XREAL_1: 6;

        then ((((((12 * (n |^ (2 + 1))) + (36 * (n * n))) + (27 * n)) + (28 * (n ^2 ))) + (84 * n)) + 63) <= ((((((12 * (n |^ (2 + 1))) + (48 * (n ^2 ))) + (48 * n)) + (16 * (n ^2 ))) + (64 * n)) + 64);

        then ((((((12 * ((n |^ 2) * (n |^ 1))) + (36 * (n * n))) + (27 * n)) + (28 * (n ^2 ))) + (84 * n)) + 63) <= ((((((12 * (n |^ (2 + 1))) + (48 * (n * n))) + (48 * n)) + (16 * (n ^2 ))) + (64 * n)) + 64) by NEWTON: 8;

        then ((((((((4 * (n |^ 2)) * 3) * (n |^ 1)) + ((36 * n) * n)) + (27 * n)) + (28 * (n ^2 ))) + (84 * n)) + 63) <= ((((((12 * (n |^ (2 + 1))) + ((48 * n) * n)) + (48 * n)) + (16 * (n ^2 ))) + (64 * n)) + 64);

        then ((((((((4 * (n |^ 2)) * 3) * n) + ((36 * n) * n)) + (27 * n)) + (28 * (n ^2 ))) + (84 * n)) + 63) <= ((((((12 * (n |^ (2 + 1))) + ((48 * n) * n)) + (48 * n)) + (16 * (n ^2 ))) + (64 * n)) + 64);

        then ((((((((4 * (n ^2 )) * 3) * n) + ((36 * n) * n)) + (27 * n)) + (28 * (n ^2 ))) + (84 * n)) + 63) <= ((((((12 * (n |^ (2 + 1))) + ((48 * n) * n)) + (48 * n)) + (16 * (n ^2 ))) + (64 * n)) + 64) by Lm1;

        then ((((((((4 * (n ^2 )) * 3) * n) + ((36 * n) * n)) + (27 * n)) + (28 * (n ^2 ))) + (84 * n)) + 63) <= ((((((12 * ((n |^ 2) * (n |^ 1))) + ((48 * n) * n)) + (48 * n)) + (16 * (n ^2 ))) + (64 * n)) + 64) by NEWTON: 8;

        then ((((((((4 * (n ^2 )) * 3) * n) + ((36 * n) * n)) + (27 * n)) + (28 * (n ^2 ))) + (84 * n)) + 63) <= ((((((12 * ((n ^2 ) * (n |^ 1))) + ((48 * n) * n)) + (48 * n)) + (16 * (n ^2 ))) + (64 * n)) + 64) by Lm1;

        then ((((((((4 * (n ^2 )) * 3) * n) + ((36 * n) * n)) + (27 * n)) + (28 * (n ^2 ))) + (84 * n)) + 63) <= ((((((12 * ((n ^2 ) * n)) + ((48 * n) * n)) + (48 * n)) + (16 * (n ^2 ))) + (64 * n)) + 64);

        then ( sqrt ((((2 * n) + 3) ^2 ) * ((3 * n) + 7))) <= ( sqrt ((((2 * n) + 4) ^2 ) * ((3 * n) + 4))) by SQUARE_1: 26;

        then (( sqrt (((2 * n) + 3) ^2 )) * ( sqrt ((3 * n) + 7))) <= ( sqrt ((((2 * n) + 4) ^2 ) * ((3 * n) + 4))) by SQUARE_1: 29;

        then (( sqrt (((2 * n) + 3) ^2 )) * ( sqrt ((3 * n) + 7))) <= (( sqrt (((2 * n) + 4) ^2 )) * ( sqrt ((3 * n) + 4))) by SQUARE_1: 29;

        then (((2 * n) + 3) * ( sqrt ((3 * n) + 7))) <= (( sqrt (((2 * n) + 4) ^2 )) * ( sqrt ((3 * n) + 4))) by SQUARE_1: 22;

        then

         A4: (((2 * n) + 3) * ( sqrt ((3 * n) + 7))) <= ((((2 * n) + 4) * ( sqrt ((3 * n) + 4))) * 1) by SQUARE_1: 22;

        ( sqrt ((3 * n) + 4)) > 0 & ( sqrt ((3 * n) + 7)) > 0 by SQUARE_1: 25;

        then ((1 * ((2 * n) + 3)) / (((2 * n) + 4) * ( sqrt ((3 * n) + 4)))) <= (1 / ( sqrt ((3 * n) + 7))) by A4, XREAL_1: 102;

        then ((( Partial_Product s) . n) * (((2 * (n + 1)) + 1) / ((2 * (n + 1)) + 2))) <= (1 / ( sqrt ((3 * (n + 1)) + 4))) by A3, XXREAL_0: 2;

        then ((( Partial_Product s) . n) * (s . (n + 1))) <= (1 / ( sqrt ((3 * (n + 1)) + 4))) by A1;

        hence thesis by Def1;

      end;

      (( Partial_Product s) . 0 ) = (s . 0 ) by Def1

      .= (((2 * 0 ) + 1) / ((2 * 0 ) + 2)) by A1

      .= (1 / ( sqrt ((3 * 0 ) + 4))) by SQUARE_1: 20;

      then

       A5: X[ 0 ];

      for n holds X[n] from NAT_1:sch 2( A5, A2);

      hence thesis;

    end;

    

     Lm8: (for n holds (s . n) > ( - 1) & (s . n) < 0 ) implies for n holds ((( Partial_Sums s) . n) * (s . (n + 1))) >= 0

    proof

      defpred X[ Nat] means ((( Partial_Sums s) . $1) * (s . ($1 + 1))) >= 0 ;

      

       A1: ((( Partial_Sums s) . 0 ) * (s . 1)) = ((s . 0 ) * (s . 1)) by SERIES_1:def 1;

      assume

       A2: for n holds (s . n) > ( - 1) & (s . n) < 0 ;

      

       A3: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        assume

         A4: ((( Partial_Sums s) . n) * (s . (n + 1))) >= 0 ;

        (s . (n + 1)) < 0 by A2;

        then

         A5: ((( Partial_Sums s) . n) * 1) <= 0 by A4;

        

         A6: ((( Partial_Sums s) . (n + 1)) * (s . (n + 2))) = (((( Partial_Sums s) . n) + (s . (n + 1))) * (s . (n + 2))) by SERIES_1:def 1

        .= (((( Partial_Sums s) . n) * (s . (n + 2))) + ((s . (n + 1)) * (s . (n + 2))));

        (s . (n + 2)) <= 0 & (s . (n + 1)) <= 0 by A2;

        hence thesis by A5, A6;

      end;

      let n;

      (s . 0 ) < 0 & (s . 1) < 0 by A2;

      then

       A7: X[ 0 ] by A1;

      for n holds X[n] from NAT_1:sch 2( A7, A3);

      hence thesis;

    end;

    theorem :: SERIES_3:49

    (for n holds (s1 . n) = (1 + (s . n)) & (s . n) > ( - 1) & (s . n) < 0 ) implies for n holds (1 + (( Partial_Sums s) . n)) <= (( Partial_Product s1) . n)

    proof

      defpred X[ Nat] means (1 + (( Partial_Sums s) . $1)) <= (( Partial_Product s1) . $1);

      assume

       A1: for n holds (s1 . n) = (1 + (s . n)) & (s . n) > ( - 1) & (s . n) < 0 ;

      

       A2: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        

         A3: ((( Partial_Product s1) . n) * (1 + (s . (n + 1)))) = ((( Partial_Product s1) . n) * (s1 . (n + 1))) by A1;

        (s . (n + 1)) > ( - 1) by A1;

        then

         A4: ((s . (n + 1)) + 1) > (( - 1) + 1) by XREAL_1: 8;

        assume (1 + (( Partial_Sums s) . n)) <= (( Partial_Product s1) . n);

        then ((1 + (( Partial_Sums s) . n)) * (1 + (s . (n + 1)))) <= ((( Partial_Product s1) . n) * (1 + (s . (n + 1)))) by A4, XREAL_1: 64;

        then

         A5: ((1 + (( Partial_Sums s) . n)) * (1 + (s . (n + 1)))) <= (( Partial_Product s1) . (n + 1)) by A3, Def1;

        ((( Partial_Sums s) . n) * (s . (n + 1))) >= 0 by A1, Lm8;

        then

         A6: (((( Partial_Sums s) . n) * (s . (n + 1))) + ((1 + (s . (n + 1))) + (( Partial_Sums s) . n))) >= ( 0 + ((1 + (s . (n + 1))) + (( Partial_Sums s) . n))) by XREAL_1: 6;

        (1 + (( Partial_Sums s) . (n + 1))) = (1 + ((( Partial_Sums s) . n) + (s . (n + 1)))) by SERIES_1:def 1;

        hence thesis by A5, A6, XXREAL_0: 2;

      end;

      let n;

      (( Partial_Sums s) . 0 ) = (s . 0 ) & (( Partial_Product s1) . 0 ) = (s1 . 0 ) by Def1, SERIES_1:def 1;

      then

       A7: X[ 0 ] by A1;

      for n holds X[n] from NAT_1:sch 2( A7, A2);

      hence thesis;

    end;

    

     Lm9: (for n holds (s . n) >= 0 ) implies for n holds ((( Partial_Sums s) . n) * (s . (n + 1))) >= 0

    proof

      assume

       A1: for n holds (s . n) >= 0 ;

      let n;

      (( Partial_Sums s) . n) >= 0 & (s . (n + 1)) >= 0 by A1, Th34;

      hence thesis;

    end;

    theorem :: SERIES_3:50

    (for n holds (s1 . n) = (1 + (s . n)) & (s . n) >= 0 ) implies for n holds (1 + (( Partial_Sums s) . n)) <= (( Partial_Product s1) . n)

    proof

      defpred X[ Nat] means (1 + (( Partial_Sums s) . $1)) <= (( Partial_Product s1) . $1);

      assume

       A1: for n holds (s1 . n) = (1 + (s . n)) & (s . n) >= 0 ;

      

       A2: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        

         A3: ((( Partial_Product s1) . n) * (1 + (s . (n + 1)))) = ((( Partial_Product s1) . n) * (s1 . (n + 1))) by A1;

        (s . (n + 1)) > ( - 1) by A1;

        then

         A4: ((s . (n + 1)) + 1) > (( - 1) + 1) by XREAL_1: 8;

        assume (1 + (( Partial_Sums s) . n)) <= (( Partial_Product s1) . n);

        then ((1 + (( Partial_Sums s) . n)) * (1 + (s . (n + 1)))) <= ((( Partial_Product s1) . n) * (1 + (s . (n + 1)))) by A4, XREAL_1: 64;

        then

         A5: ((1 + (( Partial_Sums s) . n)) * (1 + (s . (n + 1)))) <= (( Partial_Product s1) . (n + 1)) by A3, Def1;

        ((( Partial_Sums s) . n) * (s . (n + 1))) >= 0 by A1, Lm9;

        then

         A6: (((( Partial_Sums s) . n) * (s . (n + 1))) + ((1 + (s . (n + 1))) + (( Partial_Sums s) . n))) >= ( 0 + ((1 + (s . (n + 1))) + (( Partial_Sums s) . n))) by XREAL_1: 6;

        (1 + (( Partial_Sums s) . (n + 1))) = (1 + ((( Partial_Sums s) . n) + (s . (n + 1)))) by SERIES_1:def 1;

        hence thesis by A5, A6, XXREAL_0: 2;

      end;

      (( Partial_Sums s) . 0 ) = (s . 0 ) & (( Partial_Product s1) . 0 ) = (s1 . 0 ) by Def1, SERIES_1:def 1;

      then

       A7: X[ 0 ] by A1;

      for n holds X[n] from NAT_1:sch 2( A7, A2);

      hence thesis;

    end;

    theorem :: SERIES_3:51

    s3 = (s1 (#) s2) & s4 = (s1 (#) s1) & s5 = (s2 (#) s2) implies for n holds ((( Partial_Sums s3) . n) ^2 ) <= ((( Partial_Sums s4) . n) * (( Partial_Sums s5) . n))

    proof

      assume that

       A1: s3 = (s1 (#) s2) and

       A2: s4 = (s1 (#) s1) and

       A3: s5 = (s2 (#) s2);

      let n;

      

       A4: (( Partial_Sums s3) . 0 ) = (s3 . 0 ) by SERIES_1:def 1

      .= ((s1 . 0 ) * (s2 . 0 )) by A1, SEQ_1: 8;

      defpred X[ Nat] means ((( Partial_Sums s3) . $1) ^2 ) <= ((( Partial_Sums s4) . $1) * (( Partial_Sums s5) . $1));

      

       A5: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        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));

        then |.u.| <= ( sqrt (v * w)) by Lm7;

        then

         A7: ((2 * ( |.j.| * |.h.|)) * ( sqrt (v * w))) >= ((2 * ( |.j.| * |.h.|)) * |.u.|) by XREAL_1: 64;

        

         A8: w >= 0 by A3, Th36;

        then

         A9: w = (( sqrt w) ^2 ) by SQUARE_1:def 2;

        (((( sqrt v) * j) ^2 ) + ((( sqrt w) * h) ^2 )) >= ((2 * |.(( sqrt v) * j).|) * |.(( sqrt w) * h).|) by Th8;

        then (((( sqrt v) * j) ^2 ) + ((( sqrt w) * h) ^2 )) >= ((2 * ( |.( sqrt v).| * |.j.|)) * |.(( sqrt w) * h).|) by COMPLEX1: 65;

        then

         A10: (((( sqrt v) * j) ^2 ) + ((( sqrt w) * h) ^2 )) >= ((2 * ( |.( sqrt v).| * |.j.|)) * ( |.( sqrt w).| * |.h.|)) by COMPLEX1: 65;

        

         A11: v >= 0 by A2, Th36;

        then ( sqrt v) >= 0 by SQUARE_1:def 2;

        then

         A12: (((( sqrt v) * j) ^2 ) + ((( sqrt w) * h) ^2 )) >= ((2 * (( sqrt v) * |.j.|)) * ( |.( sqrt w).| * |.h.|)) by A10, ABSVALUE:def 1;

        ( sqrt w) >= 0 by A8, SQUARE_1:def 2;

        then (((( sqrt v) * j) ^2 ) + ((( sqrt w) * h) ^2 )) >= ((2 * (( sqrt v) * |.j.|)) * (( sqrt w) * |.h.|)) by A12, ABSVALUE:def 1;

        then

         A13: (((( sqrt v) * j) ^2 ) + ((( sqrt w) * h) ^2 )) >= (((2 * (( sqrt v) * ( sqrt w))) * |.j.|) * |.h.|);

        v = (( sqrt v) ^2 ) by A11, SQUARE_1:def 2;

        then ((v * (j ^2 )) + (w * (h ^2 ))) >= (((2 * ( sqrt (v * w))) * |.j.|) * |.h.|) by A11, A8, A9, A13, SQUARE_1: 29;

        then ((v * (j ^2 )) + (w * (h ^2 ))) >= ((2 * ( |.u.| * |.j.|)) * |.h.|) by A7, XXREAL_0: 2;

        then ((v * (j ^2 )) + (w * (h ^2 ))) >= ((2 * |.(u * j).|) * |.h.|) by COMPLEX1: 65;

        then ((v * (j ^2 )) + (w * (h ^2 ))) >= (2 * ( |.(u * j).| * |.h.|));

        then

         A14: ((v * (j ^2 )) + (w * (h ^2 ))) >= (2 * |.((u * j) * h).|) by COMPLEX1: 65;

        (2 * |.((u * j) * h).|) >= (2 * ((u * j) * h)) by ABSVALUE: 4, XREAL_1: 64;

        then ((v * (j ^2 )) + (w * (h ^2 ))) >= (((2 * u) * j) * h) by A14, XXREAL_0: 2;

        then

         A15: (((v * (j ^2 )) + (w * (h ^2 ))) - (((2 * u) * j) * h)) >= 0 by XREAL_1: 48;

        ((v * w) - (u ^2 )) >= 0 by A6, XREAL_1: 48;

        then

         A16: (((v * w) - (u ^2 )) + (((v * (j ^2 )) + (w * (h ^2 ))) - (((2 * u) * j) * h))) >= 0 by A15;

        (( Partial_Sums s3) . (n + 1)) = (u + (s3 . (n + 1))) by SERIES_1:def 1;

        then (( Partial_Sums s3) . (n + 1)) = (u + (h * (s2 . (n + 1)))) by A1, SEQ_1: 8;

        then

         A17: ((( Partial_Sums s3) . (n + 1)) ^2 ) = (((u ^2 ) + ((2 * u) * (h * j))) + ((h * j) ^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))) = ((v + (s4 . (n + 1))) * (w + (s5 . (n + 1)))) by SERIES_1:def 1

        .= ((v + (h * h)) * (w + (s5 . (n + 1)))) by A2, SEQ_1: 8

        .= ((v + (h * h)) * (w + ((s2 . (n + 1)) * (s2 . (n + 1))))) by A3, SEQ_1: 8

        .= ((((v * w) + (v * (j ^2 ))) + (w * (h ^2 ))) + ((h ^2 ) * (j ^2 )));

        

        then (((( Partial_Sums s4) . (n + 1)) * (( Partial_Sums s5) . (n + 1))) - ((( Partial_Sums s3) . (n + 1)) ^2 )) = (((((((v * w) - (u ^2 )) + (v * (j ^2 ))) + (w * (h ^2 ))) + ((h ^2 ) * (j ^2 ))) - ((2 * u) * (h * j))) - ((h * j) ^2 )) by A17

        .= (((((v * w) - (u ^2 )) + (v * (j ^2 ))) + (w * (h ^2 ))) - (((2 * u) * h) * j));

        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 thesis;

      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: X[ 0 ] by A4;

      for n holds X[n] from NAT_1:sch 2( A18, A5);

      hence thesis;

    end;

    

     Lm10: (for n holds (s . n) = (((s1 . n) + (s2 . n)) ^2 )) implies (( Partial_Sums s) . n) >= 0

    proof

      assume

       A1: for n holds (s . n) = (((s1 . n) + (s2 . n)) ^2 );

      now

        let n;

        (s . n) = (((s1 . n) + (s2 . n)) ^2 ) by A1;

        hence (s . n) >= 0 by XREAL_1: 63;

      end;

      hence thesis by Th34;

    end;

    theorem :: SERIES_3:52

    (s4 = (s1 (#) s1) & s5 = (s2 (#) s2) & for n holds (s1 . n) >= 0 & (s2 . n) >= 0 & (s3 . n) = (((s1 . n) + (s2 . n)) ^2 )) implies for n holds ( sqrt (( Partial_Sums s3) . n)) <= (( sqrt (( Partial_Sums s4) . n)) + ( sqrt (( Partial_Sums s5) . n)))

    proof

      assume that

       A1: s4 = (s1 (#) s1) and

       A2: s5 = (s2 (#) s2) and

       A3: for n holds (s1 . n) >= 0 & (s2 . n) >= 0 & (s3 . n) = (((s1 . n) + (s2 . n)) ^2 );

      

       A4: (s1 . 0 ) >= 0 by A3;

      defpred X[ Nat] means ( sqrt (( Partial_Sums s3) . $1)) <= (( sqrt (( Partial_Sums s4) . $1)) + ( sqrt (( Partial_Sums s5) . $1)));

      

       A5: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        assume

         A6: ( sqrt (( Partial_Sums s3) . n)) <= (( sqrt (( Partial_Sums s4) . n)) + ( sqrt (( Partial_Sums s5) . n)));

        set j = (s2 . (n + 1));

        set h = (s1 . (n + 1));

        set w = (( Partial_Sums s5) . n);

        set v = (( Partial_Sums s4) . n);

        set u = (( Partial_Sums s3) . n);

        

         A7: w >= 0 by A2, Th36;

        

         A8: (j ^2 ) >= 0 by XREAL_1: 63;

        then

         A9: ( sqrt (w + (j ^2 ))) >= 0 by A7, SQUARE_1:def 2;

        

         A10: v >= 0 by A1, Th36;

        then

         A11: ( sqrt (v * w)) >= 0 by A7, SQUARE_1:def 2;

        

         A12: u >= 0 by A3, Lm10;

        then ( sqrt u) >= 0 by SQUARE_1:def 2;

        then (( sqrt u) ^2 ) <= ((( sqrt v) + ( sqrt w)) ^2 ) by A6, SQUARE_1: 15;

        then u <= (((( sqrt v) ^2 ) + ((2 * ( sqrt v)) * ( sqrt w))) + (( sqrt w) ^2 )) by A12, SQUARE_1:def 2;

        then u <= ((v + ((2 * ( sqrt v)) * ( sqrt w))) + (( sqrt w) ^2 )) by A10, SQUARE_1:def 2;

        then u <= ((v + ((2 * ( sqrt v)) * ( sqrt w))) + w) by A7, SQUARE_1:def 2;

        then (u + ((2 * h) * j)) <= (((v + w) + (2 * (( sqrt v) * ( sqrt w)))) + ((2 * h) * j)) by XREAL_1: 6;

        then

         A13: (u + ((2 * h) * j)) <= (((v + w) + (2 * ( sqrt (v * w)))) + ((2 * h) * j)) by A10, A7, SQUARE_1: 29;

        

         A14: h >= 0 by A3;

        

         A15: j >= 0 by A3;

        

         A16: (h ^2 ) >= 0 by XREAL_1: 63;

        then

         A17: ( sqrt (v + (h ^2 ))) >= 0 by A10, SQUARE_1:def 2;

        (((h ^2 ) * w) + ((j ^2 ) * v)) >= (2 * ( sqrt (((h ^2 ) * w) * ((j ^2 ) * v)))) by A10, A7, A16, A8, SIN_COS2: 1;

        then (((h ^2 ) * w) + ((j ^2 ) * v)) >= (2 * ( sqrt (((h ^2 ) * (j ^2 )) * (w * v))));

        then (((h ^2 ) * w) + ((j ^2 ) * v)) >= (2 * (( sqrt ((h ^2 ) * (j ^2 ))) * ( sqrt (w * v)))) by A10, A7, A16, A8, SQUARE_1: 29;

        then (((h ^2 ) * w) + ((j ^2 ) * v)) >= ((2 * ( sqrt ((h ^2 ) * (j ^2 )))) * ( sqrt (w * v)));

        then (((h ^2 ) * w) + ((j ^2 ) * v)) >= ((2 * (( sqrt (h ^2 )) * ( sqrt (j ^2 )))) * ( sqrt (w * v))) by A16, A8, SQUARE_1: 29;

        then (((h ^2 ) * w) + ((j ^2 ) * v)) >= (((2 * ( sqrt (h ^2 ))) * ( sqrt (j ^2 ))) * ( sqrt (w * v)));

        then (((h ^2 ) * w) + ((j ^2 ) * v)) >= (((2 * h) * ( sqrt (j ^2 ))) * ( sqrt (w * v))) by A14, SQUARE_1: 22;

        then (((h ^2 ) * w) + ((j ^2 ) * v)) >= (((2 * h) * j) * ( sqrt (w * v))) by A15, SQUARE_1: 22;

        then ((((h ^2 ) * w) + ((j ^2 ) * v)) + ((v * w) + ((h ^2 ) * (j ^2 )))) >= ((((2 * h) * j) * ( sqrt (w * v))) + ((v * w) + ((h ^2 ) * (j ^2 )))) by XREAL_1: 6;

        then ((((v * w) + ((j ^2 ) * v)) + ((h ^2 ) * w)) + ((h ^2 ) * (j ^2 ))) >= (((v * w) + ((2 * ( sqrt (w * v))) * (h * j))) + ((h ^2 ) * (j ^2 )));

        then ((( sqrt (v * w)) + (h * j)) ^2 ) >= 0 & ((v + (h ^2 )) * (w + (j ^2 ))) >= (((( sqrt (v * w)) ^2 ) + ((2 * ( sqrt (w * v))) * (h * j))) + ((h * j) ^2 )) by A10, A7, SQUARE_1:def 2, XREAL_1: 63;

        then ( sqrt ((( sqrt (v * w)) + (h * j)) ^2 )) <= ( sqrt ((v + (h ^2 )) * (w + (j ^2 )))) by SQUARE_1: 26;

        then (( sqrt (v * w)) + (h * j)) <= ( sqrt ((v + (h ^2 )) * (w + (j ^2 )))) by A14, A15, A11, SQUARE_1: 22;

        then (2 * (( sqrt (v * w)) + (h * j))) <= (2 * ( sqrt ((v + (h ^2 )) * (w + (j ^2 ))))) by XREAL_1: 64;

        then ((v + w) + ((2 * ( sqrt (v * w))) + ((2 * h) * j))) <= ((v + w) + (2 * ( sqrt ((v + (h ^2 )) * (w + (j ^2 )))))) by XREAL_1: 6;

        then (u + ((2 * h) * j)) <= ((v + w) + (2 * ( sqrt ((v + (h ^2 )) * (w + (j ^2 )))))) by A13, XXREAL_0: 2;

        then ((u + ((2 * h) * j)) + ((h ^2 ) + (j ^2 ))) <= (((v + w) + (2 * ( sqrt ((v + (h ^2 )) * (w + (j ^2 )))))) + ((h ^2 ) + (j ^2 ))) by XREAL_1: 6;

        then (u + (((h ^2 ) + ((2 * h) * j)) + (j ^2 ))) <= (((v + (h ^2 )) + (2 * ( sqrt ((v + (h ^2 )) * (w + (j ^2 )))))) + (w + (j ^2 )));

        then (u + ((h + j) ^2 )) <= (((( sqrt (v + (h ^2 ))) ^2 ) + (2 * ( sqrt ((v + (h ^2 )) * (w + (j ^2 )))))) + (w + (j ^2 ))) by A10, A16, SQUARE_1:def 2;

        then (u + ((h + j) ^2 )) <= (((( sqrt (v + (h ^2 ))) ^2 ) + (2 * ( sqrt ((v + (h ^2 )) * (w + (j ^2 )))))) + (( sqrt (w + (j ^2 ))) ^2 )) by A7, A8, SQUARE_1:def 2;

        then ((h + j) ^2 ) >= 0 & (u + ((h + j) ^2 )) <= (((( sqrt (v + (h ^2 ))) ^2 ) + (2 * (( sqrt (v + (h ^2 ))) * ( sqrt (w + (j ^2 )))))) + (( sqrt (w + (j ^2 ))) ^2 )) by A10, A7, A16, A8, SQUARE_1: 29, XREAL_1: 63;

        then

         A18: ( sqrt (u + ((h + j) ^2 ))) <= ( sqrt ((( sqrt (v + (h ^2 ))) + ( sqrt (w + (j ^2 )))) ^2 )) by A12, SQUARE_1: 26;

        

         A19: ( sqrt (( Partial_Sums s3) . (n + 1))) = ( sqrt ((( Partial_Sums s3) . n) + (s3 . (n + 1)))) by SERIES_1:def 1

        .= ( sqrt (u + ((h + j) ^2 ))) by A3;

        (( sqrt (( Partial_Sums s4) . (n + 1))) + ( sqrt (( Partial_Sums s5) . (n + 1)))) = (( sqrt ((( Partial_Sums s4) . n) + (s4 . (n + 1)))) + ( sqrt (( Partial_Sums s5) . (n + 1)))) by SERIES_1:def 1

        .= (( sqrt (v + (s4 . (n + 1)))) + ( sqrt (w + (s5 . (n + 1))))) by SERIES_1:def 1

        .= (( sqrt (v + ((s1 . (n + 1)) * (s1 . (n + 1))))) + ( sqrt (w + (s5 . (n + 1))))) by A1, SEQ_1: 8

        .= (( sqrt (v + (h ^2 ))) + ( sqrt (w + (j ^2 )))) by A2, SEQ_1: 8;

        hence thesis by A19, A17, A9, A18, SQUARE_1: 22;

      end;

      

       A20: (s2 . 0 ) >= 0 by A3;

      (( sqrt (( Partial_Sums s4) . 0 )) + ( sqrt (( Partial_Sums s5) . 0 ))) = (( sqrt (s4 . 0 )) + ( sqrt (( Partial_Sums s5) . 0 ))) by SERIES_1:def 1

      .= (( sqrt (s4 . 0 )) + ( sqrt (s5 . 0 ))) by SERIES_1:def 1

      .= (( sqrt ((s1 . 0 ) * (s1 . 0 ))) + ( sqrt (s5 . 0 ))) by A1, SEQ_1: 8

      .= (( sqrt ((s1 . 0 ) ^2 )) + ( sqrt ((s2 . 0 ) * (s2 . 0 )))) by A2, SEQ_1: 8

      .= ((s1 . 0 ) + ( sqrt ((s2 . 0 ) ^2 ))) by A4, SQUARE_1: 22

      .= ((s1 . 0 ) + (s2 . 0 )) by A20, SQUARE_1: 22

      .= ( sqrt (((s1 . 0 ) + (s2 . 0 )) ^2 )) by A4, A20, SQUARE_1: 22

      .= ( sqrt (s3 . 0 )) by A3

      .= ( sqrt (( Partial_Sums s3) . 0 )) by SERIES_1:def 1;

      then

       A21: X[ 0 ];

      for n holds X[n] from NAT_1:sch 2( A21, A5);

      hence thesis;

    end;

    

     Lm11: (for n holds (s . n) > 0 ) implies ((n + 1) -root (( Partial_Product s) . n)) > 0

    proof

      assume for n holds (s . n) > 0 ;

      then

       A1: (( Partial_Product s) . n) > 0 by Th43;

      

       A2: (n + 1) >= ( 0 + 1) by XREAL_1: 6;

      then ((n + 1) -root (( Partial_Product s) . n)) = ((n + 1) -Root (( Partial_Product s) . n)) by A1, POWER:def 1;

      hence thesis by A1, A2, PREPOWER:def 2;

    end;

    

     Lm12: (for n holds (s . n) > 0 & (s . n) >= (s . (n - 1))) implies (((s . (n + 1)) - ((( Partial_Sums s) . n) / (n + 1))) / (n + 2)) >= 0

    proof

      assume for n holds (s . n) > 0 & (s . n) >= (s . (n - 1));

      then (((n + 1) * (s . (n + 1))) / (n + 1)) >= ((( Partial_Sums s) . n) / (n + 1)) by Th38, XREAL_1: 72;

      then (s . (n + 1)) >= ((( Partial_Sums s) . n) / (n + 1)) by XCMPLX_1: 89;

      then ((s . (n + 1)) - ((( Partial_Sums s) . n) / (n + 1))) >= 0 by XREAL_1: 48;

      hence thesis;

    end;

    theorem :: SERIES_3:53

    (for n holds (s . n) > 0 & (s . n) >= (s . (n - 1))) implies (( Partial_Sums s) . n) >= ((n + 1) * ((n + 1) -root (( Partial_Product s) . n)))

    proof

      defpred X[ Nat] means (( Partial_Sums s) . $1) >= (($1 + 1) * (($1 + 1) -root (( Partial_Product s) . $1)));

      

       A1: (( Partial_Sums s) . 0 ) = (s . 0 ) by SERIES_1:def 1;

      assume

       A2: for n holds (s . n) > 0 & (s . n) >= (s . (n - 1));

      

       A3: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        set u = (( Partial_Sums s) . n);

        set v = (s . (n + 1));

        set w = (((u / (n + 1)) + ((v - (u / (n + 1))) / (n + 2))) |^ (n + 2));

        set h = ((n + 1) -root (( Partial_Product s) . n));

        set j = (u / (n + 1));

        

         A4: v > 0 by A2;

        

         A5: (n + 1) >= ( 0 + 1) by XREAL_1: 6;

        then ((n + 1) + 1) >= (1 + 1) by XREAL_1: 6;

        then

         A6: (n + 2) >= 1 by XXREAL_0: 2;

        assume (( Partial_Sums s) . n) >= ((n + 1) * ((n + 1) -root (( Partial_Product s) . n)));

        then (u / (n + 1)) >= (((n + 1) * ((n + 1) -root (( Partial_Product s) . n))) / (n + 1)) by XREAL_1: 72;

        then ((n + 1) -root (( Partial_Product s) . n)) <= (u / (n + 1)) by XCMPLX_1: 89;

        then

         A7: (h |^ (n + 1)) <= (j |^ (n + 1)) by A2, Lm11, PREPOWER: 9;

        

         A8: (( Partial_Product s) . n) > 0 by A2, Th43;

        then h = ((n + 1) -Root (( Partial_Product s) . n)) by A5, POWER:def 1;

        then (( Partial_Product s) . n) <= (j |^ (n + 1)) by A7, A8, A5, PREPOWER: 19;

        then ((( Partial_Product s) . n) * v) <= ((j |^ (n + 1)) * v) by A4, XREAL_1: 64;

        then

         A9: (( Partial_Product s) . (n + 1)) <= ((j |^ (n + 1)) * v) by Def1;

        

         A10: (( Partial_Product s) . (n + 1)) >= 0 by A2, Th43;

        u > 0 & ((v - (u / (n + 1))) / (n + 2)) >= 0 by A2, Lm12, Th33;

        then w >= (((u / (n + 1)) |^ ((n + 1) + 1)) + (((n + 2) * ((u / (n + 1)) |^ (n + 1))) * ((v - (u / (n + 1))) / (n + 2)))) by Th31;

        then w >= ((((u / (n + 1)) |^ (n + 1)) * (u / (n + 1))) + (((u / (n + 1)) |^ (n + 1)) * (((v - (u / (n + 1))) / (n + 2)) * (n + 2)))) by NEWTON: 6;

        then

         A11: w >= ((((u / (n + 1)) |^ (n + 1)) * (u / (n + 1))) + (((u / (n + 1)) |^ (n + 1)) * (v - (u / (n + 1))))) by XCMPLX_1: 87;

        

         A12: (( Partial_Sums s) . (n + 1)) > 0 by A2, Th33;

        ((( Partial_Sums s) . (n + 1)) / (n + 2)) = (((1 * (( Partial_Sums s) . n)) + (s . (n + 1))) / (n + 2)) by SERIES_1:def 1

        .= (((((n + 1) / (n + 1)) * (( Partial_Sums s) . n)) + (s . (n + 1))) / (n + 2)) by XCMPLX_1: 60

        .= ((((((n + 2) - 1) * (( Partial_Sums s) . n)) / (n + 1)) + (s . (n + 1))) / (n + 2));

        

        then ((( Partial_Sums s) . (n + 1)) / (n + 2)) = ((((((n + 2) * u) - u) / (n + 1)) + v) / (n + 2))

        .= ((((((n + 2) * u) / (n + 1)) - (u / (n + 1))) + v) / (n + 2))

        .= ((((((n + 2) * u) / (n + 1)) - (u / (n + 1))) / (n + 2)) + (v / (n + 2)))

        .= ((((((n + 2) * u) / (n + 1)) / (n + 2)) - ((u / (n + 1)) / (n + 2))) + (v / (n + 2)))

        .= (((((n + 2) * u) / ((n + 1) * (n + 2))) - ((u / (n + 1)) / (n + 2))) + (v / (n + 2))) by XCMPLX_1: 78

        .= (((u / (n + 1)) - ((u / (n + 1)) / (n + 2))) + (v / (n + 2))) by XCMPLX_1: 91

        .= ((u / (n + 1)) + ((v / (n + 2)) - ((u / (n + 1)) / (n + 2))))

        .= ((u / (n + 1)) + ((v - (u / (n + 1))) / (n + 2)));

        then (((( Partial_Sums s) . (n + 1)) / (n + 2)) |^ (n + 2)) >= (( Partial_Product s) . (n + 1)) by A11, A9, XXREAL_0: 2;

        then ((n + 2) -Root (((( Partial_Sums s) . (n + 1)) / (n + 2)) |^ (n + 2))) >= ((n + 2) -Root (( Partial_Product s) . (n + 1))) by A6, A10, PREPOWER: 27;

        then ((( Partial_Sums s) . (n + 1)) / (n + 2)) >= ((n + 2) -Root (( Partial_Product s) . (n + 1))) by A6, A12, PREPOWER: 19;

        then ((( Partial_Sums s) . (n + 1)) / (n + 2)) >= ((n + 2) -root (( Partial_Product s) . (n + 1))) by A6, A10, POWER:def 1;

        then (((( Partial_Sums s) . (n + 1)) / (n + 2)) * (n + 2)) >= ((n + 2) * ((n + 2) -root (( Partial_Product s) . (n + 1)))) by XREAL_1: 64;

        hence thesis by XCMPLX_1: 87;

      end;

      (( 0 + 1) * (( 0 + 1) -root (( Partial_Product s) . 0 ))) = (( 0 + 1) -root (s . 0 )) by Def1

      .= (( Partial_Sums s) . 0 ) by A1, POWER: 9;

      then

       A13: X[ 0 ];

      for n holds X[n] from NAT_1:sch 2( A13, A3);

      hence thesis;

    end;