polyeq_2.miz



    begin

    4 = (2 * 2);

    then 2 divides 4 by INT_1:def 3;

    then

     Lm1: 4 is even by ABIAN:def 1;

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

    then

     Lm2: 3 is odd by ABIAN: 1;

    definition

      let a,b,c,d,e,x be Complex;

      :: POLYEQ_2:def1

      func Polynom (a,b,c,d,e,x) -> set equals (((((a * (x |^ 4)) + (b * (x |^ 3))) + (c * (x ^2 ))) + (d * x)) + e);

      correctness ;

    end

    registration

      let a,b,c,d,e,x be Complex;

      cluster ( Polynom (a,b,c,d,e,x)) -> complex;

      coherence ;

    end

    registration

      let a,b,c,d,e,x be Real;

      cluster ( Polynom (a,b,c,d,e,x)) -> real;

      coherence ;

    end

    theorem :: POLYEQ_2:1

    for a,c,e,x be Real st a <> 0 & e <> 0 & ((c ^2 ) - ((4 * a) * e)) > 0 holds ( Polynom (a, 0 ,c, 0 ,e,x)) = 0 implies x <> 0 & (x = ( sqrt ((( - c) + ( sqrt ( delta (a,c,e)))) / (2 * a))) or x = ( sqrt ((( - c) - ( sqrt ( delta (a,c,e)))) / (2 * a))) or x = ( - ( sqrt ((( - c) + ( sqrt ( delta (a,c,e)))) / (2 * a)))) or x = ( - ( sqrt ((( - c) - ( sqrt ( delta (a,c,e)))) / (2 * a)))))

    proof

      let a,c,e,x be Real;

      assume that

       A1: a <> 0 and

       A2: e <> 0 and

       A3: ((c ^2 ) - ((4 * a) * e)) > 0 ;

      set y = (x ^2 );

      assume

       A4: ( Polynom (a, 0 ,c, 0 ,e,x)) = 0 ;

       A5:

      now

        assume x = 0 ;

        then (((a * 0 ) + ( 0 * ( 0 |^ 3))) + e) = 0 by A4, NEWTON: 11;

        hence contradiction by A2;

      end;

      per cases by A5, XXREAL_0: 1;

        suppose

         A6: x > 0 ;

        (x |^ 4) = (x to_power (2 + 2)) by POWER: 41

        .= ((x to_power 2) * (x to_power 2)) by A6, POWER: 27

        .= ((x ^2 ) * (x to_power 2)) by POWER: 46

        .= ((x ^2 ) * (x ^2 )) by POWER: 46;

        then (((a * (y ^2 )) + (c * y)) + e) = 0 by A4;

        then

         A7: ( Polynom (a,c,e,y)) = 0 by POLYEQ_1:def 2;

        ( delta (a,c,e)) >= 0 by A3, QUIN_1:def 1;

        then y = ((( - c) + ( sqrt ( delta (a,c,e)))) / (2 * a)) or y = ((( - c) - ( sqrt ( delta (a,c,e)))) / (2 * a)) by A1, A7, POLYEQ_1: 5;

        then |.x.| = ( sqrt ((( - c) + ( sqrt ( delta (a,c,e)))) / (2 * a))) or |.x.| = ( sqrt ((( - c) - ( sqrt ( delta (a,c,e)))) / (2 * a))) by COMPLEX1: 72;

        hence thesis by A6, ABSVALUE:def 1;

      end;

        suppose

         A8: x < 0 ;

        then

         A9: 0 < ( - x) by XREAL_1: 58;

        (( - x) |^ 4) = (x |^ 4) by Lm1, POWER: 1;

        

        then (x |^ 4) = (( - x) to_power (2 + 2)) by POWER: 41

        .= ((( - x) to_power 2) * (( - x) to_power 2)) by A9, POWER: 27

        .= ((( - x) ^2 ) * (( - x) to_power 2)) by POWER: 46

        .= ((x ^2 ) * (x ^2 )) by POWER: 46;

        then (((a * (y ^2 )) + (c * y)) + e) = 0 by A4;

        then

         A10: ( Polynom (a,c,e,y)) = 0 by POLYEQ_1:def 2;

        ((c ^2 ) - ((4 * a) * e)) = ( delta (a,c,e)) by QUIN_1:def 1;

        then y = ((( - c) + ( sqrt ( delta (a,c,e)))) / (2 * a)) or y = ((( - c) - ( sqrt ( delta (a,c,e)))) / (2 * a)) by A1, A3, A10, POLYEQ_1: 5;

        then |.x.| = ( sqrt ((( - c) + ( sqrt ( delta (a,c,e)))) / (2 * a))) or |.x.| = ( sqrt ((( - c) - ( sqrt ( delta (a,c,e)))) / (2 * a))) by COMPLEX1: 72;

        then (( - 1) * ( - x)) = (( - 1) * ( sqrt ((( - c) + ( sqrt ( delta (a,c,e)))) / (2 * a)))) or (( - 1) * ( - x)) = (( - 1) * ( sqrt ((( - c) - ( sqrt ( delta (a,c,e)))) / (2 * a)))) by A8, ABSVALUE:def 1;

        hence thesis by A5;

      end;

    end;

    theorem :: POLYEQ_2:2

    

     Th2: for a,b,c,x,y be Real st a <> 0 & y = (x + (1 / x)) holds ( Polynom (a,b,c,b,a,x)) = 0 implies x <> 0 & ((((a * (y ^2 )) + (b * y)) + c) - (2 * a)) = 0

    proof

      let a,b,c,x,y be Real;

      assume that

       A1: a <> 0 and

       A2: y = (x + (1 / x));

      assume

       A3: ( Polynom (a,b,c,b,a,x)) = 0 ;

      

       A4: x <> 0

      proof

        assume x = 0 ;

        then (((a * ( 0 to_power 4)) + (b * ( 0 |^ 3))) + a) = 0 by A3;

        then (((a * 0 ) + (b * ( 0 |^ 3))) + a) = 0 by POWER:def 2;

        then (((a * 0 ) + (b * 0 )) + a) = 0 by NEWTON: 11;

        hence contradiction by A1;

      end;

      then

       A5: (x ^2 ) > 0 by SQUARE_1: 12;

      

       A6: (x |^ 4) = (x to_power (2 + 2)) by POWER: 41;

       A7:

      now

        per cases by A4, XXREAL_0: 1;

          case

           A8: x > 0 ;

          set n = ( - ((b * x) + a));

          set m = ((a * (x ^2 )) + ((b * x) + c));

          (x |^ 3) = (x to_power (2 + 1)) by POWER: 41

          .= ((x to_power 2) * (x to_power 1)) by A8, POWER: 27;

          

          then

           A9: (x |^ 3) = ((x to_power 2) * x)

          .= ((x ^2 ) * x) by POWER: 46;

          (x |^ 4) = ((x to_power 2) * (x to_power 2)) by A6, A8, POWER: 27

          .= ((x ^2 ) * (x to_power 2)) by POWER: 46

          .= ((x ^2 ) * (x ^2 )) by POWER: 46;

          then (m * (x ^2 )) = (n * 1) by A3, A9;

          then (m / 1) = (n / (x ^2 )) by A5, XCMPLX_1: 94;

          

          then ((a * (x ^2 )) + ((b * x) + c)) = (( - ((b * x) + a)) * (1 / (x ^2 ))) by XCMPLX_1: 99

          .= (( - ((b * x) + a)) * ((x ^2 ) " )) by XCMPLX_1: 215

          .= (( - (b * (x * ((x ^2 ) " )))) - (a * ((x ^2 ) " )));

          then (a * ((x ^2 ) + ((x ^2 ) " ))) = (( - (b * ((x * ((x ^2 ) " )) + x))) - c);

          

          then

           A10: (a * ((x ^2 ) + (1 / (x ^2 )))) = (( - (b * ((x * ((x ^2 ) " )) + x))) - c) by XCMPLX_1: 215

          .= (( - (b * ((x * (1 / (x ^2 ))) + x))) - c) by XCMPLX_1: 215;

          (1 / (x * x)) = ((1 / x) * (1 / x)) by XCMPLX_1: 102;

          then (a * ((x ^2 ) + (1 / (x ^2 )))) = (( - (b * (((x * (1 / x)) * (1 / x)) + x))) - c) by A10;

          then

           A11: (a * ((x ^2 ) + (1 / (x ^2 )))) = (( - (b * ((1 * (1 / x)) + x))) - c) by A8, XCMPLX_1: 106;

          (x * y) = ((x * x) + (x * (1 / x))) by A2;

          then ((x * y) + 0 ) = ((x ^2 ) + 1) by A4, XCMPLX_1: 106;

          hence (a * ((x ^2 ) + (1 / (x ^2 )))) = (( - (b * (x + (1 / x)))) - c) & (((x ^2 ) - (x * y)) + 1) = 0 by A11;

        end;

          case

           A12: x < 0 ;

          set n = ( - ((b * x) + a));

          set m = ((a * (x ^2 )) + ((b * x) + c));

          ((( - x) |^ 3) + (x |^ 3)) = ( - ((x |^ 3) + ( - (x |^ 3)))) by Lm2, POWER: 2

          .= ((x |^ 3) - (x |^ 3));

          then

           A13: (x |^ 3) = ( - (( - x) |^ 3));

          

           A14: 0 < ( - x) by A12, XREAL_1: 58;

          (( - x) |^ 4) = (x |^ 4) by Lm1, POWER: 1;

          

          then

           A15: (x |^ 4) = (( - x) to_power (2 + 2)) by POWER: 41

          .= ((( - x) to_power 2) * (( - x) to_power 2)) by A14, POWER: 27

          .= ((( - x) ^2 ) * (( - x) to_power 2)) by POWER: 46

          .= ((x ^2 ) * (( - x) ^2 )) by POWER: 46;

          (( - x) |^ 3) = (( - x) to_power (2 + 1)) by POWER: 41

          .= ((( - x) to_power 2) * (( - x) to_power 1)) by A14, POWER: 27;

          then

           A16: (( - x) |^ 3) = ((( - x) to_power 2) * ( - x));

          (( - x) to_power 2) = (( - x) ^2 ) by POWER: 46

          .= (x ^2 );

          then (m * (x ^2 )) = (n * 1) by A3, A15, A16, A13;

          then (m / 1) = (n / (x ^2 )) by A5, XCMPLX_1: 94;

          

          then m = (n * (1 / (x ^2 ))) by XCMPLX_1: 99

          .= (n * ((x ^2 ) " )) by XCMPLX_1: 215

          .= (( - (b * (x * ((x ^2 ) " )))) - (a * ((x ^2 ) " )));

          then (a * ((x ^2 ) + ((x ^2 ) " ))) = (( - (b * ((x * ((x ^2 ) " )) + x))) - c);

          

          then (a * ((x ^2 ) + (1 / (x ^2 )))) = (( - (b * ((x * ((x ^2 ) " )) + x))) - c) by XCMPLX_1: 215

          .= (( - (b * ((x * (1 / (x ^2 ))) + x))) - c) by XCMPLX_1: 215;

          

          then (a * ((x ^2 ) + (1 / (x ^2 )))) = (( - (b * ((x * ((1 / x) * (1 / x))) + x))) - c) by XCMPLX_1: 102

          .= (( - (b * (((x * (1 / x)) * (1 / x)) + x))) - c);

          then

           A17: (a * ((x ^2 ) + (1 / (x ^2 )))) = (( - (b * ((1 * (1 / x)) + x))) - c) by A12, XCMPLX_1: 106;

          (x * y) = ((x * x) + (x * (1 / x))) by A2

          .= ((x * x) + 1) by A12, XCMPLX_1: 106;

          hence (a * ((x ^2 ) + (1 / (x ^2 )))) = (( - (b * (x + (1 / x)))) - c) & (((x ^2 ) - (x * y)) + 1) = 0 by A17;

        end;

      end;

      (y ^2 ) = (((x ^2 ) + (2 * (x * (1 / x)))) + ((1 / x) ^2 )) by A2

      .= (((x ^2 ) + (2 * 1)) + ((1 / x) ^2 )) by A4, XCMPLX_1: 106

      .= (((x ^2 ) + 2) + ((1 ^2 ) / (x ^2 ))) by XCMPLX_1: 76

      .= ((x ^2 ) - (( - 2) - (1 / (x ^2 ))));

      then ((a * (y ^2 )) - (2 * a)) = (( - (b * y)) - c) by A2, A7;

      hence thesis by A4;

    end;

    theorem :: POLYEQ_2:3

    for a,b,c,x,y be Real st a <> 0 & (((b ^2 ) - ((4 * a) * c)) + (8 * (a ^2 ))) > 0 & y = (x + (1 / x)) holds ( Polynom (a,b,c,b,a,x)) = 0 implies for y1,y2 be Real st y1 = ((( - b) + ( sqrt (((b ^2 ) - ((4 * a) * c)) + (8 * (a ^2 ))))) / (2 * a)) & y2 = ((( - b) - ( sqrt (((b ^2 ) - ((4 * a) * c)) + (8 * (a ^2 ))))) / (2 * a)) holds x <> 0 & (x = ((y1 + ( sqrt ( delta (1,( - y1),1)))) / 2) or x = ((y2 + ( sqrt ( delta (1,( - y2),1)))) / 2) or x = ((y1 - ( sqrt ( delta (1,( - y1),1)))) / 2) or x = ((y2 - ( sqrt ( delta (1,( - y2),1)))) / 2))

    proof

      let a,b,c,x,y be Real;

      assume that

       A1: a <> 0 and

       A2: (((b ^2 ) - ((4 * a) * c)) + (8 * (a ^2 ))) > 0 and

       A3: y = (x + (1 / x)) and

       A4: ( Polynom (a,b,c,b,a,x)) = 0 ;

      

       A5: x <> 0 by A1, A3, A4, Th2;

      set f = (c - (2 * a));

      ((((a * (y ^2 )) + (b * y)) + c) - (2 * a)) = 0 by A1, A3, A4, Th2;

      then (((a * (y ^2 )) + (b * y)) + (c - (2 * a))) = 0 ;

      then

       A6: ( Polynom (a,b,f,y)) = 0 by POLYEQ_1:def 2;

      let y1,y2 be Real;

      assume

       A7: y1 = ((( - b) + ( sqrt (((b ^2 ) - ((4 * a) * c)) + (8 * (a ^2 ))))) / (2 * a)) & y2 = ((( - b) - ( sqrt (((b ^2 ) - ((4 * a) * c)) + (8 * (a ^2 ))))) / (2 * a));

      (x * y) = ((x ^2 ) + (x * (1 / x))) by A3;

      then ((x * y) + 0 ) = ((x ^2 ) + 1) by A5, XCMPLX_1: 106;

      then (((1 * (x ^2 )) + (( - y) * x)) + 1) = 0 ;

      then

       A8: ( Polynom (1,( - y),1,x)) = 0 by POLYEQ_1:def 2;

      ( delta (1,( - y),1)) = ((( - y) ^2 ) - ((4 * 1) * 1)) by QUIN_1:def 1

      .= ((((x ^2 ) + (2 * (x * (1 / x)))) + ((1 / x) ^2 )) - 4) by A3

      .= ((((x ^2 ) + (2 * 1)) + ((1 / x) ^2 )) - 4) by A5, XCMPLX_1: 106

      .= ((x ^2 ) + (( - (2 * 1)) + ((1 / x) ^2 )))

      .= ((x ^2 ) + (( - (2 * (x * (1 / x)))) + ((1 / x) ^2 ))) by A5, XCMPLX_1: 106

      .= ((x - (1 / x)) ^2 );

      then

       A9: x = ((( - ( - y)) + ( sqrt ( delta (1,( - y),1)))) / (2 * 1)) or x = ((( - ( - y)) - ( sqrt ( delta (1,( - y),1)))) / (2 * 1)) by A8, POLYEQ_1: 5, XREAL_1: 63;

      

       A10: ((b ^2 ) - ((4 * a) * f)) = (((b ^2 ) - ((4 * a) * c)) + (8 * (a ^2 )));

      then ( delta (a,b,f)) > 0 by A2, QUIN_1:def 1;

      then y = ((( - b) + ( sqrt ( delta (a,b,f)))) / (2 * a)) or y = ((( - b) - ( sqrt ( delta (a,b,f)))) / (2 * a)) by A1, A6, POLYEQ_1: 5;

      then y = y1 or y = y2 by A7, A10, QUIN_1:def 1;

      hence thesis by A1, A3, A4, A9, Th2;

    end;

    theorem :: POLYEQ_2:4

    

     Th4: for x be Real holds (x |^ 3) = ((x ^2 ) * x) & ((x |^ 3) * x) = (x |^ 4) & ((x ^2 ) * (x ^2 )) = (x |^ 4)

    proof

      let x be Real;

      per cases by XXREAL_0: 1;

        suppose x = 0 ;

        hence thesis by NEWTON: 11;

      end;

        suppose

         A1: x > 0 ;

        ((x |^ 3) * x) = ((x |^ 3) * (x to_power 1))

        .= ((x to_power 3) * (x to_power 1));

        then

         A2: ((x |^ 3) * x) = (x to_power (3 + 1)) by A1, POWER: 27;

        (x ^2 ) = (x to_power 2) by POWER: 46;

        

        then ((x ^2 ) * x) = ((x to_power 2) * (x to_power 1))

        .= (x to_power (2 + 1)) by A1, POWER: 27

        .= (x |^ 3) by POWER: 41;

        hence thesis by A2, POWER: 41;

      end;

        suppose x < 0 ;

        then

         A3: ( - x) > 0 by XREAL_1: 58;

        ((( - x) |^ 3) + (x |^ 3)) = ( - ((x |^ 3) + ( - (x |^ 3)))) by Lm2, POWER: 2

        .= ((x |^ 3) - (x |^ 3));

        then

         A4: ((x |^ 3) + ((( - x) |^ 3) - (( - x) |^ 3))) = ( 0 - (( - x) |^ 3));

        

         A5: (( - x) to_power 2) = (( - x) ^2 ) by POWER: 46

        .= (x ^2 );

        (( - x) |^ 3) = (( - x) to_power (2 + 1)) by POWER: 41

        .= ((( - x) to_power 2) * (( - x) to_power 1)) by A3, POWER: 27;

        then

         A6: (( - x) |^ 3) = ((( - x) to_power 2) * ( - x));

        (( - x) |^ 4) = (x |^ 4) by Lm1, POWER: 1;

        

        then (x |^ 4) = (( - x) to_power (3 + 1)) by POWER: 41

        .= ((( - x) to_power 3) * (( - x) to_power 1)) by A3, POWER: 27

        .= ((( - x) |^ 3) * (( - x) to_power 1));

        

        then (x |^ 4) = ((( - x) |^ 3) * ( - x))

        .= ((x ^2 ) * (x * x)) by A6, A5;

        hence thesis by A6, A5, A4;

      end;

    end;

    theorem :: POLYEQ_2:5

    

     Th5: for x,y be Real st (x + y) <> 0 holds ((x + y) |^ 4) = (((((x |^ 3) + (((3 * y) * (x ^2 )) + ((3 * (y ^2 )) * x))) + (y |^ 3)) * x) + ((((x |^ 3) + (((3 * y) * (x ^2 )) + ((3 * (y ^2 )) * x))) + (y |^ 3)) * y))

    proof

      let x,y be Real;

      assume

       A1: (x + y) <> 0 ;

      per cases by A1, XXREAL_0: 1;

        suppose

         A2: (x + y) > 0 ;

        ((x + y) |^ 4) = ((x + y) to_power (3 + 1)) by POWER: 41

        .= (((x + y) to_power 3) * ((x + y) to_power 1)) by A2, POWER: 27

        .= (((x + y) to_power 3) * (x + y));

        

        then ((x + y) |^ 4) = (((x + y) |^ 3) * (x + y))

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

        hence thesis;

      end;

        suppose (x + y) < 0 ;

        then

         A3: ( - (x + y)) > 0 by XREAL_1: 58;

        (( - (x + y)) |^ 4) = ((x + y) |^ 4) by Lm1, POWER: 1;

        

        then ((x + y) |^ 4) = (( - (x + y)) to_power (3 + 1)) by POWER: 41

        .= ((( - (x + y)) to_power 3) * (( - (x + y)) to_power 1)) by A3, POWER: 27

        .= ((( - (x + y)) |^ 3) * (( - (x + y)) to_power 1));

        then ((x + y) |^ 4) = ((( - (x + y)) |^ 3) * ( - (x + y)));

        

        then ((x + y) |^ 4) = (( - ((x + y) |^ 3)) * ( - (x + y))) by Lm2, POWER: 2

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

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

        hence thesis;

      end;

    end;

    theorem :: POLYEQ_2:6

    for x,y be Real st (x + y) <> 0 holds ((x + y) |^ 4) = (((x |^ 4) + ((((4 * y) * (x |^ 3)) + ((6 * (y ^2 )) * (x ^2 ))) + ((4 * (y |^ 3)) * x))) + (y |^ 4))

    proof

      let x,y be Real;

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

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

      set p = (y |^ 3), q = (x |^ 3), u = (x |^ 4), v = (y |^ 4);

      

       A1: g = ((((x |^ 3) * x) + ((((3 * y) * (x ^2 )) + ((3 * (y ^2 )) * x)) * x)) + ((y |^ 3) * x));

      

       A2: (y |^ 3) = ((y ^2 ) * y) by Th4;

      assume (x + y) <> 0 ;

      then

       A3: ((x + y) |^ 4) = (g + h) by Th5;

      h = ((((x |^ 3) * y) + ((((3 * y) * (x ^2 )) + ((3 * (y ^2 )) * x)) * y)) + ((y |^ 3) * y))

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

      

      then ((x + y) |^ 4) = (((u + (((3 * y) * ((x ^2 ) * x)) - (( - ((3 * (y ^2 )) * x)) * x))) + (p * x)) + (((q * y) + ((((3 * y) * (x ^2 )) + ((3 * (y ^2 )) * x)) * y)) + v)) by A3, A1, Th4

      .= (((u + (((3 * y) * q) - ( - ((3 * (y ^2 )) * (x ^2 ))))) + (p * x)) + (((q * y) + ((((3 * y) * (x ^2 )) + ((3 * (y ^2 )) * x)) * y)) + v)) by Th4

      .= (((u + ((3 * y) * q)) + (((3 * (y ^2 )) * (x ^2 )) + (p * x))) + (((q * y) + (((3 * (y ^2 )) * (x ^2 )) + (((3 * (y ^2 )) * x) * y))) + v));

      hence thesis by A2;

    end;

    theorem :: POLYEQ_2:7

    

     Th7: for a1,a2,a3,a4,a5,b1,b2,b3,b4,b5 be Real holds (for x be Real holds ( Polynom (a1,a2,a3,a4,a5,x)) = ( Polynom (b1,b2,b3,b4,b5,x))) implies a5 = b5 & (((a1 - a2) + a3) - a4) = (((b1 - b2) + b3) - b4) & (((a1 + a2) + a3) + a4) = (((b1 + b2) + b3) + b4)

    proof

      set x = ( - 1);

      let a1,a2,a3,a4,a5,b1,b2,b3,b4,b5 be Real;

      

       A1: ( 0 |^ 3) = 0 & ( 0 |^ 4) = 0 by NEWTON: 11;

      assume

       A2: for x be Real holds ( Polynom (a1,a2,a3,a4,a5,x)) = ( Polynom (b1,b2,b3,b4,b5,x));

      then

       A3: ( Polynom (a1,a2,a3,a4,a5,( - 1))) = ( Polynom (b1,b2,b3,b4,b5,( - 1)));

      

       A5: (x |^ 3) = ((x ^2 ) * x) & ((x |^ 3) * x) = (x |^ 4) by Th4;

      ( Polynom (a1,a2,a3,a4,a5, 0 )) = ( Polynom (b1,b2,b3,b4,b5, 0 )) & ( Polynom (a1,a2,a3,a4,a5,1)) = ( Polynom (b1,b2,b3,b4,b5,1)) by A2;

      hence thesis by A1, A3, A5;

    end;

    theorem :: POLYEQ_2:8

    

     Th8: for a1,a2,a3,a4,a5,b1,b2,b3,b4,b5 be Real holds (for x be Real holds ( Polynom (a1,a2,a3,a4,a5,x)) = ( Polynom (b1,b2,b3,b4,b5,x))) implies (a1 - b1) = (b3 - a3) & (a2 - b2) = (b4 - a4)

    proof

      let a1,a2,a3,a4,a5,b1,b2,b3,b4,b5 be Real;

      assume for x be Real holds ( Polynom (a1,a2,a3,a4,a5,x)) = ( Polynom (b1,b2,b3,b4,b5,x));

      then (((a1 - a2) + a3) - a4) = (((b1 - b2) + b3) - b4) & (((a1 + a2) + a3) + a4) = (((b1 + b2) + b3) + b4) by Th7;

      hence thesis;

    end;

    theorem :: POLYEQ_2:9

    

     Th9: for a1,a2,a3,a4,a5,b1,b2,b3,b4,b5 be Real st (for x be Real holds ( Polynom (a1,a2,a3,a4,a5,x)) = ( Polynom (b1,b2,b3,b4,b5,x))) holds a1 = b1 & a2 = b2 & a3 = b3 & a4 = b4 & a5 = b5

    proof

      

       A1: (( - 2) |^ 3) = ((( - 2) ^2 ) * ( - 2)) by Th4

      .= ( - (4 * 2));

      

       A2: (( - 2) |^ 4) = 16 by Lm1, POWER: 1, POWER: 62;

      let a1,a2,a3,a4,a5,b1,b2,b3,b4,b5 be Real;

      assume

       A3: for x be Real holds ( Polynom (a1,a2,a3,a4,a5,x)) = ( Polynom (b1,b2,b3,b4,b5,x));

      then

       A4: ( Polynom (a1,a2,a3,a4,a5,( - 2))) = ( Polynom (b1,b2,b3,b4,b5,( - 2)));

      

       A5: a5 = b5 & ( Polynom (a1,a2,a3,a4,a5,2)) = ( Polynom (b1,b2,b3,b4,b5,2)) by A3, Th7;

      (a1 - b1) = (b3 - a3) & (a2 - b2) = (b4 - a4) by A3, Th8;

      hence thesis by A5, A4, A2, A1, POWER: 61, POWER: 62;

    end;

    definition

      let a1,x1,x2,x3,x4,x be Real;

      :: POLYEQ_2:def2

      func Four0 (a1,x1,x2,x3,x4,x) -> set equals (a1 * ((((x - x1) * (x - x2)) * (x - x3)) * (x - x4)));

      correctness ;

    end

    registration

      let a1,x1,x2,x3,x4,x be Real;

      cluster ( Four0 (a1,x1,x2,x3,x4,x)) -> real;

      coherence ;

    end

    theorem :: POLYEQ_2:10

    

     Th10: for a1,a2,a3,a4,a5,x,x1,x2,x3,x4 be Real st a1 <> 0 holds (for x be Real holds ( Polynom (a1,a2,a3,a4,a5,x)) = ( Four0 (a1,x1,x2,x3,x4,x))) implies ((((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2 ))) + (a4 * x)) + a5) / a1) = ((((((x ^2 ) * (x ^2 )) - (((x1 + x2) + x3) * ((x ^2 ) * x))) + ((((x1 * x3) + (x2 * x3)) + (x1 * x2)) * (x ^2 ))) - (((x1 * x2) * x3) * x)) - ((((x - x1) * (x - x2)) * (x - x3)) * x4))

    proof

      let a1,a2,a3,a4,a5,x,x1,x2,x3,x4 be Real;

      assume

       A1: a1 <> 0 ;

      set z = ((((x - x1) * (x - x2)) * (x - x3)) * (x - x4));

      set w = (((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2 ))) + (a4 * x)) + a5);

      assume for x be Real holds ( Polynom (a1,a2,a3,a4,a5,x)) = ( Four0 (a1,x1,x2,x3,x4,x));

      then ( Polynom (a1,a2,a3,a4,a5,x)) = ( Four0 (a1,x1,x2,x3,x4,x));

      then (((w / a1) * a1) - (z * a1)) = ((z * a1) - (z * a1)) by A1, XCMPLX_1: 87;

      then (((w / a1) - z) * a1) = 0 ;

      then ((w / a1) + ( - z)) = ( 0 - 0 ) by A1, XCMPLX_1: 6;

      hence thesis;

    end;

    theorem :: POLYEQ_2:11

    

     Th11: for a1,a2,a3,a4,a5,x,x1,x2,x3,x4 be Real st a1 <> 0 holds (for x be Real holds ( Polynom (a1,a2,a3,a4,a5,x)) = ( Four0 (a1,x1,x2,x3,x4,x))) implies ((((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2 ))) + (a4 * x)) + a5) / a1) = (((((x |^ 4) - ((((x1 + x2) + x3) + x4) * (x |^ 3))) + ((((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)) * (x ^2 ))) - ((((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) * x)) + (((x1 * x2) * x3) * x4))

    proof

      let a1,a2,a3,a4,a5,x,x1,x2,x3,x4 be Real;

      assume

       A1: a1 <> 0 ;

      set w = (((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2 ))) + (a4 * x)) + a5);

      assume for x be Real holds ( Polynom (a1,a2,a3,a4,a5,x)) = ( Four0 (a1,x1,x2,x3,x4,x));

      then ((((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2 ))) + (a4 * x)) + a5) / a1) = ((((((x ^2 ) * (x ^2 )) - (((x1 + x2) + x3) * ((x ^2 ) * x))) + ((((x1 * x3) + (x2 * x3)) + (x1 * x2)) * (x ^2 ))) - (((x1 * x2) * x3) * x)) - ((((x - x1) * (x - x2)) * (x - x3)) * x4)) by A1, Th10;

      then (w / a1) = ((((((x ^2 ) * (x ^2 )) - ((((x1 + x2) + x3) + x4) * ((x ^2 ) * x))) + (((((x1 * x3) + (x2 * x3)) + (x1 * x2)) + (((x2 * x4) + (x1 * x4)) + (x3 * x4))) * (x ^2 ))) - ((((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ( - ( - ((x1 * x3) * x4)))) + ((x2 * x3) * x4)) * x)) + (((x1 * x2) * x3) * x4));

      then (w / a1) = (((((x |^ 4) - ((((x1 + x2) + x3) + x4) * ((x ^2 ) * x))) + ((((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)) * (x ^2 ))) - ((((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) * x)) + (((x1 * x2) * x3) * x4)) by Th4;

      hence thesis by Th4;

    end;

    theorem :: POLYEQ_2:12

    for a1,a2,a3,a4,a5,x1,x2,x3,x4 be Real st a1 <> 0 & (for x be Real holds ( Polynom (a1,a2,a3,a4,a5,x)) = ( Four0 (a1,x1,x2,x3,x4,x))) holds (a2 / a1) = ( - (((x1 + x2) + x3) + x4)) & (a3 / a1) = (((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)) & (a4 / a1) = ( - (((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4))) & (a5 / a1) = (((x1 * x2) * x3) * x4)

    proof

      set b1 = 1;

      let a1,a2,a3,a4,a5,x1,x2,x3,x4 be Real;

      assume

       A1: a1 <> 0 ;

      set b5 = (((x1 * x2) * x3) * x4);

      set b4 = ( - (((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)));

      set b3 = (((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4));

      set b2 = ( - (((x1 + x2) + x3) + x4));

      assume

       A2: for x be Real holds ( Polynom (a1,a2,a3,a4,a5,x)) = ( Four0 (a1,x1,x2,x3,x4,x));

      now

        let x be Real;

        set t = (((((b1 * (x |^ 4)) + (b2 * (x |^ 3))) + (b3 * (x ^2 ))) + (b4 * x)) + b5);

        ((((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2 ))) + (a4 * x)) + a5) / a1) = (((((x |^ 4) - ((((x1 + x2) + x3) + x4) * (x |^ 3))) + ((((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)) * (x ^2 ))) - ((((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) * x)) + (((x1 * x2) * x3) * x4)) by A1, A2, Th11;

        

        then t = ((a1 " ) * ((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + ((a3 * (x ^2 )) + (a4 * x))) + a5)) by XCMPLX_0:def 9

        .= (((((a1 " ) * a1) * (x |^ 4)) + ((a1 " ) * (a2 * (x |^ 3)))) + ((((a1 " ) * (a3 * (x ^2 ))) + ((a1 " ) * (a4 * x))) + ((a1 " ) * a5)))

        .= ((((a1 / a1) * (x |^ 4)) + ((a1 " ) * (a2 * (x |^ 3)))) + ((((a1 " ) * (a3 * (x ^2 ))) + ((a1 " ) * (a4 * x))) + ((a1 " ) * a5))) by XCMPLX_0:def 9

        .= (((1 * (x |^ 4)) + ((a1 " ) * (a2 * (x |^ 3)))) + ((((a1 " ) * (a3 * (x ^2 ))) + ((a1 " ) * (a4 * x))) + ((a1 " ) * a5))) by A1, XCMPLX_1: 60

        .= (((x |^ 4) + (((a1 " ) * a2) * (x |^ 3))) + ((((a1 " ) * (a3 * (x ^2 ))) + ((a1 " ) * (a4 * x))) + ((a1 " ) * a5)))

        .= (((x |^ 4) + ((a2 / a1) * (x |^ 3))) + (((((a1 " ) * a3) * (x ^2 )) + ((a1 " ) * (a4 * x))) + ((a1 " ) * a5))) by XCMPLX_0:def 9

        .= (((x |^ 4) + ((a2 / a1) * (x |^ 3))) + ((((a3 / a1) * (x ^2 )) + (((a1 " ) * a4) * x)) + ((a1 " ) * a5))) by XCMPLX_0:def 9

        .= (((x |^ 4) + ((a2 / a1) * (x |^ 3))) + ((((a3 / a1) * (x ^2 )) + ((a4 / a1) * x)) + ((a1 " ) * a5))) by XCMPLX_0:def 9

        .= (((x |^ 4) + ((a2 / a1) * (x |^ 3))) + ((((a3 / a1) * (x ^2 )) + ((a4 / a1) * x)) + (a5 / a1))) by XCMPLX_0:def 9

        .= ( Polynom (1,(a2 / a1),(a3 / a1),(a4 / a1),(a5 / a1),x));

        hence ( Polynom (1,(a2 / a1),(a3 / a1),(a4 / a1),(a5 / a1),x)) = ( Polynom (b1,b2,b3,b4,b5,x));

      end;

      hence thesis by Th9;

    end;

    theorem :: POLYEQ_2:13

    for a,k,y be Real st a <> 0 holds (for x be Real holds ((x |^ 4) + (a |^ 4)) = (((k * a) * x) * ((x ^2 ) + (a ^2 )))) implies ((((y |^ 4) - (k * (y |^ 3))) - (k * y)) + 1) = 0

    proof

      let a,k,y be Real;

      assume that

       A1: a <> 0 and

       A2: for x be Real holds ((x |^ 4) + (a |^ 4)) = (((k * a) * x) * ((x ^2 ) + (a ^2 )));

      (((a * y) |^ 4) + (a |^ 4)) = (((k * a) * (a * y)) * (((a * y) ^2 ) + (a ^2 ))) by A2

      .= ((k * ((a ^2 ) * y)) * (((a ^2 ) * (y ^2 )) + ((a ^2 ) * 1)));

      

      then (((a * y) |^ 4) + (a |^ 4)) = (k * ((((a ^2 ) * (a ^2 )) * y) * ((y ^2 ) + 1)))

      .= (k * (((a |^ 4) * y) * ((y ^2 ) + 1))) by Th4

      .= (((a |^ 4) * (k * y)) * ((y ^2 ) + 1));

      then (((a |^ 4) * (y |^ 4)) + ((a |^ 4) * 1)) = ((a |^ 4) * ((k * y) * ((y ^2 ) + 1))) by NEWTON: 7;

      then (((a |^ 4) " ) * ((a |^ 4) * (((y |^ 4) + 1) - ((k * y) * ((y ^2 ) + 1))))) = 0 ;

      then ((((a |^ 4) " ) * (a |^ 4)) * (((y |^ 4) + 1) - ((k * y) * ((y ^2 ) + 1)))) = 0 ;

      then

       A3: (((1 / (a |^ 4)) * (a |^ 4)) * (((y |^ 4) + 1) - ((k * y) * ((y ^2 ) + 1)))) = 0 by XCMPLX_1: 215;

      (a |^ 4) <> 0 by A1, PREPOWER: 5;

      then (1 * (((y |^ 4) + 1) - ((k * y) * ((y ^2 ) + 1)))) = 0 by A3, XCMPLX_1: 106;

      then ((((y |^ 4) - (k * ((y ^2 ) * y))) - (k * y)) + 1) = 0 ;

      hence thesis by Th4;

    end;