polyeq_4.miz



    begin

    reserve x,y,a,b,c,p,q for Real;

    reserve m,n for Element of NAT ;

    theorem :: POLYEQ_4:1

    

     Th1: (b / a) < 0 & (c / a) > 0 & ( delta (a,b,c)) >= 0 implies ((( - b) + ( sqrt ( delta (a,b,c)))) / (2 * a)) > 0 & ((( - b) - ( sqrt ( delta (a,b,c)))) / (2 * a)) > 0

    proof

      assume that

       A1: (b / a) < 0 and

       A2: (c / a) > 0 and

       A3: ( delta (a,b,c)) >= 0 ;

      

       A4: ((b ^2 ) - ((4 * a) * c)) >= 0 by A3, QUIN_1:def 1;

      now

        per cases by A1, XREAL_1: 143;

          case

           A5: b < 0 & a > 0 ;

          

           A6: 0 <= ( sqrt ((b ^2 ) - ((4 * a) * c))) by A4, SQUARE_1: 17, SQUARE_1: 26;

          

           A7: (2 * a) > 0 by A5, XREAL_1: 129;

          ( - b) > 0 by A5, XREAL_1: 58;

          then (( - b) + ( sqrt ((b ^2 ) - ((4 * a) * c)))) > ( 0 + 0 ) by A6;

          then

           A8: ((( - b) + ( sqrt ((b ^2 ) - ((4 * a) * c)))) / (2 * a)) > 0 by A7, XREAL_1: 139;

          c > 0 & (4 * a) > 0 by A2, A5, XREAL_1: 129;

          then ( - ( - ((4 * a) * c))) > 0 by XREAL_1: 129;

          then ( - ((4 * a) * c)) < 0 ;

          then ((b ^2 ) + ( - ((4 * a) * c))) < ((b ^2 ) + 0 ) by XREAL_1: 8;

          then ( sqrt ((b ^2 ) - ((4 * a) * c))) < ( sqrt (b ^2 )) by A4, SQUARE_1: 27;

          then ( sqrt ((b ^2 ) - ((4 * a) * c))) < ( - b) by A5, SQUARE_1: 23;

          then ( - ( sqrt ((b ^2 ) - ((4 * a) * c)))) > ( - ( - b)) by XREAL_1: 24;

          then (( - ( sqrt ((b ^2 ) - ((4 * a) * c)))) + ( - b)) > (( - ( - b)) + ( - b)) by XREAL_1: 8;

          then ((( - b) - ( sqrt ((b ^2 ) - ((4 * a) * c)))) / (2 * a)) > 0 by A7, XREAL_1: 139;

          hence thesis by A8, QUIN_1:def 1;

        end;

          case

           A9: b > 0 & a < 0 ;

          then

           A10: (a * 2) < ( 0 * 2) by XREAL_1: 68;

          c < 0 by A2, A9;

          then (a * c) > 0 by A9, XREAL_1: 130;

          then (4 * (a * c)) > 0 by XREAL_1: 129;

          then ( - ( - ((4 * a) * c))) > 0 ;

          then ( - ((4 * a) * c)) < 0 ;

          then ((b ^2 ) + ( - ((4 * a) * c))) < ((b ^2 ) + 0 ) by XREAL_1: 8;

          then ( sqrt ((b ^2 ) - ((4 * a) * c))) < ( sqrt (b ^2 )) by A4, SQUARE_1: 27;

          then ( sqrt ((b ^2 ) - ((4 * a) * c))) < b by A9, SQUARE_1: 22;

          then (( - b) + ( sqrt ((b ^2 ) - ((4 * a) * c)))) < (( 0 + b) + ( - b)) by XREAL_1: 8;

          then

           A11: ((( - b) + ( sqrt ((b ^2 ) - ((4 * a) * c)))) / (2 * a)) > 0 by A10, XREAL_1: 140;

          

           A12: 0 <= ( sqrt ((b ^2 ) - ((4 * a) * c))) by A4, SQUARE_1: 17, SQUARE_1: 26;

          ( - ( - b)) > 0 by A9;

          then (( - b) + 0 ) < ( 0 + ( sqrt ((b ^2 ) - ((4 * a) * c)))) by A12;

          then ( - ( - (( sqrt ((b ^2 ) - ((4 * a) * c))) + b))) > 0 by XREAL_1: 62;

          then (( - b) - ( sqrt ((b ^2 ) - ((4 * a) * c)))) < 0 ;

          then ((( - b) - ( sqrt ((b ^2 ) - ((4 * a) * c)))) / (2 * a)) > 0 by A10, XREAL_1: 140;

          hence thesis by A11, QUIN_1:def 1;

        end;

      end;

      hence thesis;

    end;

    theorem :: POLYEQ_4:2

    (b / a) > 0 & (c / a) > 0 & ( delta (a,b,c)) >= 0 implies ((( - b) + ( sqrt ( delta (a,b,c)))) / (2 * a)) < 0 & ((( - b) - ( sqrt ( delta (a,b,c)))) / (2 * a)) < 0

    proof

      assume that

       A1: (b / a) > 0 and

       A2: (c / a) > 0 and

       A3: ( delta (a,b,c)) >= 0 ;

      

       A4: ((b ^2 ) - ((4 * a) * c)) >= 0 by A3, QUIN_1:def 1;

      now

        per cases by A1, XREAL_1: 144;

          case

           A5: b > 0 & a > 0 ;

          then c > 0 & (4 * a) > 0 by A2, XREAL_1: 129;

          then ( - ( - ((4 * a) * c))) > 0 by XREAL_1: 129;

          then ( - ((4 * a) * c)) < 0 ;

          then ((b ^2 ) + ( - ((4 * a) * c))) < ((b ^2 ) + 0 ) by XREAL_1: 8;

          then ( sqrt ((b ^2 ) - ((4 * a) * c))) < ( sqrt (b ^2 )) by A4, SQUARE_1: 27;

          then ( sqrt ((b ^2 ) - ((4 * a) * c))) < b by A5, SQUARE_1: 22;

          then (( - b) + ( sqrt ((b ^2 ) - ((4 * a) * c)))) < ( 0 + (b + ( - b))) by XREAL_1: 8;

          then

           A6: ((( - b) + ( sqrt ((b ^2 ) - ((4 * a) * c)))) / (2 * a)) < 0 by A5, XREAL_1: 129, XREAL_1: 141;

           0 <= ( sqrt ((b ^2 ) - ((4 * a) * c))) by A4, SQUARE_1: 17, SQUARE_1: 26;

          then ( 0 + 0 ) < (b + ( sqrt ((b ^2 ) - ((4 * a) * c)))) by A5;

          then ( - ( - (b + ( sqrt ((b ^2 ) - ((4 * a) * c)))))) > 0 ;

          then (( - b) - ( sqrt ((b ^2 ) - ((4 * a) * c)))) < 0 ;

          then ((( - b) - ( sqrt ((b ^2 ) - ((4 * a) * c)))) / (2 * a)) < 0 by A5, XREAL_1: 129, XREAL_1: 141;

          hence thesis by A6, QUIN_1:def 1;

        end;

          case

           A7: b < 0 & a < 0 ;

          

           A8: 0 <= ( sqrt ((b ^2 ) - ((4 * a) * c))) by A4, SQUARE_1: 17, SQUARE_1: 26;

          

           A9: (a * 2) < ( 0 * 2) by A7, XREAL_1: 68;

          ( - b) > 0 by A7, XREAL_1: 58;

          then ( 0 + 0 ) < (( - b) + ( sqrt ((b ^2 ) - ((4 * a) * c)))) by A8;

          then

           A10: ((( - b) + ( sqrt ((b ^2 ) - ((4 * a) * c)))) / (2 * a)) < 0 by A9, XREAL_1: 142;

          c < 0 by A2, A7;

          then (a * c) > 0 by A7, XREAL_1: 130;

          then (4 * (a * c)) > 0 by XREAL_1: 129;

          then ( - ( - ((4 * a) * c))) > 0 ;

          then ( - ((4 * a) * c)) < 0 ;

          then ((b ^2 ) + ( - ((4 * a) * c))) < ((b ^2 ) + 0 ) by XREAL_1: 8;

          then ( sqrt ((b ^2 ) - ((4 * a) * c))) < ( sqrt (b ^2 )) by A4, SQUARE_1: 27;

          then ( sqrt ((b ^2 ) - ((4 * a) * c))) < ( - b) by A7, SQUARE_1: 23;

          then (b + ( sqrt ((b ^2 ) - ((4 * a) * c)))) < (( 0 + b) + ( - b)) by XREAL_1: 8;

          then ( - (b + ( sqrt ((b ^2 ) - ((4 * a) * c))))) > 0 by XREAL_1: 58;

          then ((( - b) - ( sqrt ((b ^2 ) - ((4 * a) * c)))) / (2 * a)) < 0 by A9, XREAL_1: 142;

          hence thesis by A10, QUIN_1:def 1;

        end;

      end;

      hence thesis;

    end;

    theorem :: POLYEQ_4:3

    (c / a) < 0 implies ((( - b) + ( sqrt ( delta (a,b,c)))) / (2 * a)) > 0 & ((( - b) - ( sqrt ( delta (a,b,c)))) / (2 * a)) < 0 or ((( - b) + ( sqrt ( delta (a,b,c)))) / (2 * a)) < 0 & ((( - b) - ( sqrt ( delta (a,b,c)))) / (2 * a)) > 0

    proof

      assume

       A1: (c / a) < 0 ;

      now

        per cases by A1, XREAL_1: 143;

          case

           A2: c > 0 & a < 0 ;

          then (4 * a) < (4 * 0 ) by XREAL_1: 68;

          then ((4 * a) * c) < ( 0 * c) by A2, XREAL_1: 68;

          then

           A3: ( - ((4 * a) * c)) > 0 by XREAL_1: 58;

          then ((b ^2 ) + ( - ((4 * a) * c))) > ((b ^2 ) + 0 ) by XREAL_1: 8;

          then

           A4: ( sqrt ((b ^2 ) - ((4 * a) * c))) > ( sqrt (b ^2 )) by SQUARE_1: 27, XREAL_1: 63;

          

           A5: (2 * a) < (2 * 0 ) by A2, XREAL_1: 68;

          (( - ((4 * a) * c)) + (b ^2 )) > ( 0 + 0 ) by A3, XREAL_1: 8, XREAL_1: 63;

          then

           A6: ( - ( - ( sqrt ((b ^2 ) - ((4 * a) * c))))) > 0 by SQUARE_1: 17, SQUARE_1: 27;

          then

           A7: ( - ( sqrt ((b ^2 ) - ((4 * a) * c)))) < 0 ;

          now

            per cases ;

              suppose

               A8: b >= 0 ;

              then ( - b) <= ( - 0 );

              then (( - ( sqrt ((b ^2 ) - ((4 * a) * c)))) + ( - b)) < ( 0 + 0 ) by A7;

              then (( - b) - ( sqrt ((b ^2 ) - ((4 * a) * c)))) < 0 ;

              then

               A9: (( - b) - ( sqrt ( delta (a,b,c)))) < 0 by QUIN_1:def 1;

              ( sqrt ((b ^2 ) - ((4 * a) * c))) > b by A4, A8, SQUARE_1: 22;

              then (( - b) + ( sqrt ((b ^2 ) - ((4 * a) * c)))) > (( 0 + b) + ( - b)) by XREAL_1: 8;

              then ((( - b) + ( sqrt ((b ^2 ) - ((4 * a) * c)))) / (2 * a)) < 0 by A5, XREAL_1: 142;

              hence thesis by A5, A9, QUIN_1:def 1, XREAL_1: 140;

            end;

              suppose

               A10: b < 0 ;

              then ( sqrt ((b ^2 ) - ((4 * a) * c))) > ( - b) by A4, SQUARE_1: 23;

              then ( - ( - (b + ( sqrt ((b ^2 ) - ((4 * a) * c)))))) > 0 by XREAL_1: 62;

              then (( - b) - ( sqrt ((b ^2 ) - ((4 * a) * c)))) < 0 ;

              then

               A11: ((( - b) - ( sqrt ((b ^2 ) - ((4 * a) * c)))) / (2 * a)) > 0 by A5, XREAL_1: 140;

              ( - b) > 0 by A10, XREAL_1: 58;

              then (( sqrt ((b ^2 ) - ((4 * a) * c))) + ( - b)) > ( 0 + 0 ) by A6;

              then (( sqrt ( delta (a,b,c))) + ( - b)) > ( 0 + 0 ) by QUIN_1:def 1;

              hence thesis by A5, A11, QUIN_1:def 1, XREAL_1: 142;

            end;

          end;

          hence thesis;

        end;

          case

           A12: c < 0 & a > 0 ;

          then (4 * a) > 0 by XREAL_1: 129;

          then ((4 * a) * c) < ((4 * a) * 0 ) by A12, XREAL_1: 68;

          then

           A13: ( - ((4 * a) * c)) > 0 by XREAL_1: 58;

          then ((b ^2 ) + ( - ((4 * a) * c))) > ((b ^2 ) + 0 ) by XREAL_1: 8;

          then

           A14: ( sqrt ((b ^2 ) - ((4 * a) * c))) > ( sqrt (b ^2 )) by SQUARE_1: 27, XREAL_1: 63;

          

           A15: (2 * a) > 0 by A12, XREAL_1: 129;

          (( - ((4 * a) * c)) + (b ^2 )) > ( 0 + 0 ) by A13, XREAL_1: 8, XREAL_1: 63;

          then

           A16: ( - ( - ( sqrt ((b ^2 ) - ((4 * a) * c))))) > 0 by SQUARE_1: 17, SQUARE_1: 27;

          then

           A17: ( - ( sqrt ((b ^2 ) - ((4 * a) * c)))) < 0 ;

          now

            per cases ;

              suppose

               A18: b >= 0 ;

              then ( - b) <= ( - 0 );

              then (( - ( sqrt ((b ^2 ) - ((4 * a) * c)))) + ( - b)) < ( 0 + 0 ) by A17;

              then (( - b) - ( sqrt ((b ^2 ) - ((4 * a) * c)))) < 0 ;

              then

               A19: (( - b) - ( sqrt ( delta (a,b,c)))) < 0 by QUIN_1:def 1;

              ( sqrt ((b ^2 ) - ((4 * a) * c))) > b by A14, A18, SQUARE_1: 22;

              then (( - b) + ( sqrt ((b ^2 ) - ((4 * a) * c)))) > (( 0 + b) + ( - b)) by XREAL_1: 8;

              then ((( - b) + ( sqrt ((b ^2 ) - ((4 * a) * c)))) / (2 * a)) > 0 by A15, XREAL_1: 139;

              hence thesis by A12, A19, QUIN_1:def 1, XREAL_1: 129, XREAL_1: 141;

            end;

              suppose

               A20: b < 0 ;

              then ( sqrt ((b ^2 ) - ((4 * a) * c))) > ( - b) by A14, SQUARE_1: 23;

              then ( - ( - (b + ( sqrt ((b ^2 ) - ((4 * a) * c)))))) > 0 by XREAL_1: 62;

              then (( - b) - ( sqrt ((b ^2 ) - ((4 * a) * c)))) < 0 ;

              then

               A21: ((( - b) - ( sqrt ((b ^2 ) - ((4 * a) * c)))) / (2 * a)) < 0 by A12, XREAL_1: 129, XREAL_1: 141;

              ( - b) > 0 by A20, XREAL_1: 58;

              then (( sqrt ((b ^2 ) - ((4 * a) * c))) + ( - b)) > ( 0 + 0 ) by A16;

              then (( sqrt ( delta (a,b,c))) + ( - b)) > 0 by QUIN_1:def 1;

              hence thesis by A15, A21, QUIN_1:def 1, XREAL_1: 139;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: POLYEQ_4:4

    

     Th4: a > 0 & n is even & n >= 1 & (x |^ n) = a implies x = (n -root a) or x = ( - (n -root a))

    proof

      assume that

       A1: a > 0 and

       A2: n is even and

       A3: n >= 1;

      assume

       A4: (x |^ n) = a;

      then

       A5: x <> 0 by A1, A3, NEWTON: 11;

      now

        per cases by A5;

          case x > 0 ;

          hence thesis by A4, A3, POWER: 4;

        end;

          case x < 0 ;

          then

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

          (n -root a) = (n -root (( - x) |^ n)) by A2, A4, POWER: 1;

          then (( - 1) * (n -root a)) = (( - 1) * ( - x)) by A3, A6, POWER: 4;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: POLYEQ_4:5

    

     Th5: a <> 0 & ( Polynom (a,b, 0 ,x)) = 0 implies x = 0 or x = ( - (b / a))

    proof

      assume that

       A1: a <> 0 and

       A2: ( Polynom (a,b, 0 ,x)) = 0 ;

      (((a * (x ^2 )) + (b * x)) + 0 ) = 0 by A2, POLYEQ_1:def 2;

      then ((((a * x) + b) + 0 ) * x) = 0 ;

      then (((a * x) + b) + ( - b)) = ( 0 + ( - b)) or x = 0 by XCMPLX_1: 6;

      then x = (( - b) / a) or x = 0 by A1, XCMPLX_1: 89;

      hence thesis by XCMPLX_1: 187;

    end;

    theorem :: POLYEQ_4:6

    a <> 0 & ( Polynom (a, 0 , 0 ,x)) = 0 implies x = 0

    proof

      assume that

       A1: a <> 0 and

       A2: ( Polynom (a, 0 , 0 ,x)) = 0 ;

      (((a * (x ^2 )) + ( 0 * x)) + 0 ) = 0 by A2, POLYEQ_1:def 2;

      then (x ^2 ) = 0 by A1;

      hence thesis;

    end;

    theorem :: POLYEQ_4:7

    a <> 0 & n is odd & ( delta (a,b,c)) >= 0 & ( Polynom (a,b,c,(x |^ n))) = 0 implies x = (n -root ((( - b) + ( sqrt ( delta (a,b,c)))) / (2 * a))) or x = (n -root ((( - b) - ( sqrt ( delta (a,b,c)))) / (2 * a)))

    proof

      assume that

       A1: a <> 0 and

       A2: n is odd and

       A3: ( delta (a,b,c)) >= 0 & ( Polynom (a,b,c,(x |^ n))) = 0 ;

      (x |^ n) = ((( - b) + ( sqrt ( delta (a,b,c)))) / (2 * a)) or (x |^ n) = ((( - b) - ( sqrt ( delta (a,b,c)))) / (2 * a)) by A1, A3, POLYEQ_1: 5;

      hence thesis by A2, POWER: 4;

    end;

    theorem :: POLYEQ_4:8

    a <> 0 & (b / a) < 0 & (c / a) > 0 & n is even & n >= 1 & ( delta (a,b,c)) >= 0 & ( Polynom (a,b,c,(x |^ n))) = 0 implies x = (n -root ((( - b) + ( sqrt ( delta (a,b,c)))) / (2 * a))) or x = ( - (n -root ((( - b) + ( sqrt ( delta (a,b,c)))) / (2 * a)))) or x = (n -root ((( - b) - ( sqrt ( delta (a,b,c)))) / (2 * a))) or x = ( - (n -root ((( - b) - ( sqrt ( delta (a,b,c)))) / (2 * a))))

    proof

      assume that

       A1: a <> 0 and

       A2: (b / a) < 0 & (c / a) > 0 & n is even & n >= 1 and

       A3: ( delta (a,b,c)) >= 0 and

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

      now

        per cases by A1, A3, A4, POLYEQ_1: 5;

          suppose (x |^ n) = ((( - b) + ( sqrt ( delta (a,b,c)))) / (2 * a));

          then x = (n -root ((( - b) + ( sqrt ( delta (a,b,c)))) / (2 * a))) or x = ( - (n -root ((( - b) + ( sqrt ( delta (a,b,c)))) / (2 * a)))) by A2, A3, Th1, Th4;

          hence thesis;

        end;

          suppose (x |^ n) = ((( - b) - ( sqrt ( delta (a,b,c)))) / (2 * a));

          then x = (n -root ((( - b) - ( sqrt ( delta (a,b,c)))) / (2 * a))) or x = ( - (n -root ((( - b) - ( sqrt ( delta (a,b,c)))) / (2 * a)))) by A2, A3, Th1, Th4;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: POLYEQ_4:9

    a <> 0 & n is odd & ( Polynom (a,b, 0 ,(x |^ n))) = 0 implies x = 0 or x = (n -root ( - (b / a)))

    proof

      assume that

       A1: a <> 0 and

       A2: n is odd and

       A3: ( Polynom (a,b, 0 ,(x |^ n))) = 0 ;

      now

        per cases by A1, A3, Th5;

          suppose (x |^ n) = 0 ;

          hence thesis by PREPOWER: 5;

        end;

          suppose (x |^ n) = ( - (b / a));

          hence thesis by A2, POWER: 4;

        end;

      end;

      hence thesis;

    end;

    theorem :: POLYEQ_4:10

    a <> 0 & (b / a) < 0 & n is even & n >= 1 & ( Polynom (a,b, 0 ,(x |^ n))) = 0 implies x = 0 or x = (n -root ( - (b / a))) or x = ( - (n -root ( - (b / a))))

    proof

      assume that

       A1: a <> 0 and

       A2: (b / a) < 0 and

       A3: n is even & n >= 1 and

       A4: ( Polynom (a,b, 0 ,(x |^ n))) = 0 ;

      

       A5: ( - (b / a)) > 0 by A2, XREAL_1: 58;

      now

        per cases by A1, A4, Th5;

          suppose (x |^ n) = 0 ;

          hence thesis by PREPOWER: 5;

        end;

          suppose (x |^ n) = ( - (b / a));

          hence thesis by A3, A5, Th4;

        end;

      end;

      hence thesis;

    end;

    theorem :: POLYEQ_4:11

    

     Th11: ((a |^ 3) + (b |^ 3)) = ((a + b) * (((a ^2 ) - (a * b)) + (b ^2 ))) & ((a |^ 5) + (b |^ 5)) = ((a + b) * (((((a |^ 4) - ((a |^ 3) * b)) + ((a |^ 2) * (b |^ 2))) - (a * (b |^ 3))) + (b |^ 4)))

    proof

      

       A1: ((a + b) * (((((a |^ 4) - ((a |^ 3) * b)) + ((a |^ 2) * (b |^ 2))) - (a * (b |^ 3))) + (b |^ 4))) = ((((((((a |^ 4) * a) + (b * (a |^ 4))) + ( 0 * (a |^ 4))) - (((a |^ 3) * b) * (a + b))) + (((a |^ 2) * (b |^ 2)) * (a + b))) - ((a * (b |^ 3)) * (a + b))) + ((b |^ 4) * (a + b)))

      .= ((((((((a |^ 4) * (a |^ 1)) + (b * (a |^ 4))) + ( 0 * (a |^ 4))) - (((a |^ 3) * b) * (a + b))) + (((a |^ 2) * (b |^ 2)) * (a + b))) - ((a * (b |^ 3)) * (a + b))) + ((b |^ 4) * (a + b)))

      .= ((((((a |^ (4 + 1)) + (b * (a |^ 4))) - (((a |^ 3) * b) * ((a + b) + 0 ))) + (((a |^ 2) * (b |^ 2)) * (a + b))) - ((a * (b |^ 3)) * (a + b))) + ((b |^ 4) * (a + b))) by NEWTON: 8

      .= ((((((a |^ 5) + (b * (a |^ 4))) - (((a * (a |^ 3)) * b) + (b * ((a |^ 3) * b)))) + ((a * ((a |^ 2) * (b |^ 2))) + (b * ((a |^ 2) * (b |^ 2))))) - ((a * (a * (b |^ 3))) + (b * (a * (b |^ 3))))) + ((a * (b |^ 4)) + (b * (b |^ 4))))

      .= ((((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + ((((a |^ 2) * a) * (b |^ 2)) + ((b * (b |^ 2)) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b * (b |^ 3)) * a))) + ((a * (b |^ 4)) + (b * (b |^ 4)))) by POLYEQ_2: 4

      .= ((((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + ((((a |^ 2) * a) * (b |^ 2)) + ((b * (b |^ 2)) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b |^ 4) * a))) + ((a * (b |^ 4)) + (b * (b |^ 4)))) by POLYEQ_2: 4

      .= ((((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + (((a |^ (2 + 1)) * (b |^ 2)) + (((b |^ 2) * b) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b |^ 4) * a))) + ((a * (b |^ 4)) + (b * (b |^ 4)))) by NEWTON: 6

      .= ((((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ (2 + 1)) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b |^ 4) * a))) + ((a * (b |^ 4)) + ((b |^ 4) * b))) by NEWTON: 6

      .= ((((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ 3) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b |^ 4) * a))) + ((a * (b |^ 4)) + (b |^ (4 + 1)))) by NEWTON: 6

      .= ((((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + (((b |^ 1) * b) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ 3) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b |^ 4) * a))) + ((a * (b |^ 4)) + (b |^ (4 + 1))))

      .= ((((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + (((b |^ 1) * b) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ 3) * (a |^ 2)))) - ((((a |^ 1) * a) * (b |^ 3)) + ((b |^ 4) * a))) + ((a * (b |^ 4)) + (b |^ (4 + 1))))

      .= ((((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b |^ (1 + 1)) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ 3) * (a |^ 2)))) - ((((a |^ 1) * a) * (b |^ 3)) + ((b |^ 4) * a))) + ((a * (b |^ 4)) + (b |^ 5))) by NEWTON: 6

      .= ((((a |^ 5) + ((a |^ 2) * (b |^ 3))) - (((a |^ 2) * (b |^ 3)) + (a * (b |^ 4)))) + ((a * (b |^ 4)) + (b |^ 5))) by NEWTON: 6

      .= ((a |^ 5) + (b |^ 5));

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

      .= ((((a |^ 3) + (b * (a ^2 ))) - ((a * (a * b)) + (b * (a * b)))) + ((a * (b ^2 )) + (b * (b ^2 )))) by POLYEQ_2: 4

      .= ((((a |^ 3) + (b * (a ^2 ))) - (((a ^2 ) * b) + ((b * b) * a))) + ((a * (b ^2 )) + (b |^ 3))) by POLYEQ_2: 4

      .= ((a |^ 3) + (b |^ 3));

      hence thesis by A1;

    end;

    theorem :: POLYEQ_4:12

    a <> 0 & (((b ^2 ) - ((2 * a) * b)) - (3 * (a ^2 ))) >= 0 & ( Polynom (a,b,b,a,x)) = 0 implies x = ( - 1) or x = (((a - b) + ( sqrt (((b ^2 ) - ((2 * a) * b)) - (3 * (a ^2 ))))) / (2 * a)) or x = (((a - b) - ( sqrt (((b ^2 ) - ((2 * a) * b)) - (3 * (a ^2 ))))) / (2 * a))

    proof

      assume that

       A1: a <> 0 & (((b ^2 ) - ((2 * a) * b)) - (3 * (a ^2 ))) >= 0 and

       A2: ( Polynom (a,b,b,a,x)) = 0 ;

      ((((a * (x |^ 3)) + (b * (x ^2 ))) + (b * x)) + a) = 0 by A2, POLYEQ_1:def 4;

      then ((((x |^ 3) + 1) * a) + ((((x ^2 ) + x) + 0 ) * b)) = 0 ;

      then ((((x |^ 3) + (1 to_power 3)) * a) + (((x + 1) * x) * b)) = 0 ;

      then ((((x + 1) * (((x ^2 ) - (x * 1)) + (1 ^2 ))) * a) + (((x + 1) * x) * b)) = 0 by Th11;

      then

       A3: ((((((x ^2 ) * a) - (x * a)) + (x * b)) + a) * (x + 1)) = 0 ;

      now

        per cases by A3;

          case (x + 1) = 0 ;

          hence thesis;

        end;

          case

           A4: (((a * (x ^2 )) - ((a - b) * x)) + a) = 0 ;

          

           A5: ( delta (a,(( - a) + b),a)) = (((( - a) + b) ^2 ) - ((4 * a) * a)) by QUIN_1:def 1

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

          (((a * (x ^2 )) + ((( - a) + b) * x)) + a) = 0 by A4;

          then ( Polynom (a,(( - a) + b),a,x)) = 0 by POLYEQ_1:def 2;

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

          hence thesis by A5;

        end;

      end;

      hence thesis;

    end;

    definition

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

      :: POLYEQ_4:def1

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

      coherence ;

    end

    registration

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

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

      coherence ;

    end

    registration

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

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

      coherence ;

    end

    theorem :: POLYEQ_4:13

    a <> 0 & ((((b ^2 ) + ((2 * a) * b)) + (5 * (a ^2 ))) - ((4 * a) * c)) > 0 & ( Polynom (a,b,c,c,b,a,x)) = 0 implies for y1,y2 be Real st y1 = (((a - b) + ( sqrt ((((b ^2 ) + ((2 * a) * b)) + (5 * (a ^2 ))) - ((4 * a) * c)))) / (2 * a)) & y2 = (((a - b) - ( sqrt ((((b ^2 ) + ((2 * a) * b)) + (5 * (a ^2 ))) - ((4 * a) * c)))) / (2 * a)) holds x = ( - 1) or 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

      assume that

       A1: a <> 0 & ((((b ^2 ) + ((2 * a) * b)) + (5 * (a ^2 ))) - ((4 * a) * c)) > 0 and

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

      let y1,y2 be Real;

      assume that

       A3: y1 = (((a - b) + ( sqrt ((((b ^2 ) + ((2 * a) * b)) + (5 * (a ^2 ))) - ((4 * a) * c)))) / (2 * a)) and

       A4: y2 = (((a - b) - ( sqrt ((((b ^2 ) + ((2 * a) * b)) + (5 * (a ^2 ))) - ((4 * a) * c)))) / (2 * a));

      

       A5: 0 = (((((x |^ 5) + 1) * a) + ((((x |^ 4) + x) + 0 ) * b)) + (((c * (x |^ 3)) + (c * (x ^2 ))) + ( 0 * c))) by A2

      .= (((((x |^ 5) + (1 |^ 5)) * a) + (((x |^ (3 + 1)) + x) * b)) + (((x |^ 3) + (x ^2 )) * c))

      .= (((((x |^ 5) + (1 |^ 5)) * a) + ((((x |^ 3) * x) + x) * b)) + (((x |^ (2 + 1)) + (x ^2 )) * c)) by NEWTON: 6

      .= (((((x |^ 5) + (1 |^ 5)) * a) + (((((x |^ 3) + 1) + 0 ) * x) * b)) + ((((x * (x |^ (1 + 1))) + (1 * (x ^2 ))) + ( 0 * (x ^2 ))) * c)) by NEWTON: 6

      .= (((((x |^ 5) + (1 |^ 5)) * a) + (((((x |^ 3) + 1) + 0 ) * x) * b)) + ((((x * ((x |^ 1) * x)) + (1 * (x ^2 ))) + ( 0 * (x ^2 ))) * c)) by NEWTON: 6

      .= (((((x |^ 5) + (1 |^ 5)) * a) + (((((x |^ 3) + 1) + 0 ) * x) * b)) + ((((x * (x ^2 )) + (1 * (x ^2 ))) + ( 0 * (x ^2 ))) * c))

      .= (((((x + 1) * (((((x |^ 4) - ((x |^ 3) * 1)) + ((x |^ 2) * (1 |^ 2))) - (x * (1 |^ 3))) + (1 |^ 4))) * a) + ((((x |^ 3) + 1) * x) * b)) + ((((x + 1) + 0 ) * (x ^2 )) * c)) by Th11

      .= (((((x + 1) * (((((x |^ 4) - (x |^ 3)) + ((x |^ 2) * 1)) - (x * (1 |^ 3))) + (1 |^ 4))) * a) + ((((x |^ 3) + 1) * x) * b)) + ((((x + 1) + 0 ) * (x ^2 )) * c))

      .= (((((x + 1) * (((((x |^ 4) - (x |^ 3)) + (x |^ 2)) - (x * 1)) + (1 |^ 4))) * a) + ((((x |^ 3) + 1) * x) * b)) + ((((x + 1) + 0 ) * (x ^2 )) * c))

      .= (((((x + 1) * (((((x |^ 4) - (x |^ 3)) + (x |^ 2)) - x) + 1)) * a) + ((((x |^ 3) + 1) * x) * b)) + ((((x + 1) + 0 ) * (x ^2 )) * c))

      .= (((((x + 1) * (((((x |^ 4) - (x |^ 3)) + (x |^ 2)) - x) + 1)) * a) + ((((x |^ 3) + (1 |^ 3)) * x) * b)) + (((x + 1) * (x ^2 )) * c))

      .= (((((x + 1) * (((((x |^ 4) - (x |^ 3)) + (x |^ 2)) - x) + 1)) * a) + ((((x + 1) * (((x ^2 ) - (x * 1)) + (1 ^2 ))) * x) * b)) + (((x + 1) * (x ^2 )) * c)) by Th11

      .= ((((((((a * (x |^ 4)) - (a * (x |^ 3))) + (a * (x |^ 2))) - (a * x)) + a) + (((((x * x) * x) * b) - ((x * x) * b)) + (b * x))) + ((x * x) * c)) * (x + 1))

      .= ((((((((a * (x |^ 4)) - (a * (x |^ 3))) + (a * (x |^ 2))) - (a * x)) + a) + ((((((x |^ 1) * x) * x) * b) - ((x * x) * b)) + (b * x))) + ((x * x) * c)) * (x + 1))

      .= ((((((((a * (x |^ 4)) - (a * (x |^ 3))) + (a * (x |^ 2))) - (a * x)) + a) + ((((((x |^ 1) * x) * x) * b) - ((x * x) * b)) + (b * x))) + (((x |^ 1) * x) * c)) * (x + 1))

      .= ((((((((a * (x |^ 4)) - (a * (x |^ 3))) + (a * (x |^ 2))) - (a * x)) + a) + ((((((x |^ 1) * x) * x) * b) - ((x * x) * b)) + (b * x))) + ((x |^ (1 + 1)) * c)) * (x + 1)) by NEWTON: 6

      .= ((((((((a * (x |^ 4)) - (a * (x |^ 3))) + (a * (x |^ 2))) - (a * x)) + a) + (((((x |^ (1 + 1)) * x) * b) - ((x * x) * b)) + (b * x))) + ((x |^ 2) * c)) * (x + 1)) by NEWTON: 6

      .= ((((((((a * (x |^ 4)) - (a * (x |^ 3))) + (a * (x |^ 2))) - (a * x)) + a) + ((((x |^ (2 + 1)) * b) - ((x * x) * b)) + (b * x))) + ((x |^ 2) * c)) * (x + 1)) by NEWTON: 6

      .= ((((((((a * (x |^ 4)) - (a * (x |^ 3))) + (a * (x |^ 2))) - (a * x)) + a) + ((((x |^ 3) * b) - (((x |^ 1) * x) * b)) + (b * x))) + ((x |^ 2) * c)) * (x + 1))

      .= ((((((((a * (x |^ 4)) - (a * (x |^ 3))) + (a * (x |^ 2))) - (a * x)) + a) + ((((x |^ 3) * b) - ((x |^ (1 + 1)) * b)) + (b * x))) + ((x |^ 2) * c)) * (x + 1)) by NEWTON: 6

      .= ((((((a * (x |^ 4)) - ((a - b) * (x |^ 3))) + (((a + c) - b) * (x |^ 2))) - ((a - b) * x)) + a) * (x + 1));

      now

        per cases by A5;

          case (x + 1) = 0 ;

          hence thesis;

        end;

          case

           A6: (((((a * (x |^ 4)) - ((a - b) * (x |^ 3))) + (((a + c) - b) * (x |^ 2))) - ((a - b) * x)) + a) = 0 ;

          set y = (x + (1 / x));

           0 = (((((a * (x |^ 4)) + ((( - a) + b) * (x |^ 3))) + (((a + c) - b) * (x |^ (1 + 1)))) + ((( - a) + b) * x)) + a) by A6

          .= (((((a * (x |^ 4)) + ((( - a) + b) * (x |^ 3))) + (((a + c) - b) * ((x |^ 1) * x))) + ((( - a) + b) * x)) + a) by NEWTON: 6

          .= (((((a * (x |^ 4)) + ((( - a) + b) * (x |^ 3))) + (((a + c) - b) * (x ^2 ))) + ((( - a) + b) * x)) + a);

          then

           A7: ( Polynom (a,(( - a) + b),((a + c) - b),(( - a) + b),a,x)) = 0 by POLYEQ_2:def 1;

          y = (x + (1 / x)) & y1 = ((( - (( - a) + b)) + ( sqrt ((((( - a) + b) ^2 ) - ((4 * a) * ((a + c) - b))) + (8 * (a ^2 ))))) / (2 * a)) by A3;

          hence thesis by A1, A4, A7, POLYEQ_2: 3;

        end;

      end;

      hence thesis;

    end;

    theorem :: POLYEQ_4:14

    

     Th14: (x + y) = p & (x * y) = q & ((p ^2 ) - (4 * q)) >= 0 implies x = ((p + ( sqrt ((p ^2 ) - (4 * q)))) / 2) & y = ((p - ( sqrt ((p ^2 ) - (4 * q)))) / 2) or x = ((p - ( sqrt ((p ^2 ) - (4 * q)))) / 2) & y = ((p + ( sqrt ((p ^2 ) - (4 * q)))) / 2)

    proof

      assume that

       A1: (x + y) = p and

       A2: (x * y) = q and

       A3: ((p ^2 ) - (4 * q)) >= 0 ;

      

       A4: ( delta (1,( - p),q)) = ((( - p) ^2 ) - ((4 * 1) * q)) by QUIN_1:def 1

      .= ((p ^2 ) - (4 * q));

      (((1 * (y ^2 )) + (( - p) * y)) + q) = 0 by A1, A2;

      then ( Polynom (1,( - p),q,y)) = 0 by POLYEQ_1:def 2;

      then

       A5: y = ((( - ( - p)) + ( sqrt ( delta (1,( - p),q)))) / (2 * 1)) or y = ((( - ( - p)) - ( sqrt ( delta (1,( - p),q)))) / (2 * 1)) by A3, A4, POLYEQ_1: 5;

      now

        per cases by A5;

          suppose

           A6: y = ((p + ( sqrt ( delta (1,( - p),q)))) / 2);

          

          then x = (((p * 2) / 2) - ((p / 2) + (( sqrt ( delta (1,( - p),q))) / 2))) by A1

          .= (((p * 2) / 2) - ((p / 2) + (( sqrt ((p ^2 ) - (4 * q))) / 2))) by A4;

          hence thesis by A4, A6;

        end;

          suppose

           A7: y = ((p - ( sqrt ( delta (1,( - p),q)))) / 2);

          

          then x = (p - (((p - ( sqrt ( delta (1,( - p),q)))) + 0 ) / 2)) by A1

          .= (p - (((p - ( sqrt ((p ^2 ) - (4 * q)))) + 0 ) / 2)) by A4;

          hence thesis by A4, A7;

        end;

      end;

      hence thesis;

    end;

    theorem :: POLYEQ_4:15

    ((x |^ n) + (y |^ n)) = p & ((x |^ n) * (y |^ n)) = q & ((p ^2 ) - (4 * q)) >= 0 & n is odd implies x = (n -root ((p + ( sqrt ((p ^2 ) - (4 * q)))) / 2)) & y = (n -root ((p - ( sqrt ((p ^2 ) - (4 * q)))) / 2)) or x = (n -root ((p - ( sqrt ((p ^2 ) - (4 * q)))) / 2)) & y = (n -root ((p + ( sqrt ((p ^2 ) - (4 * q)))) / 2))

    proof

      assume that

       A1: ((x |^ n) + (y |^ n)) = p & ((x |^ n) * (y |^ n)) = q & ((p ^2 ) - (4 * q)) >= 0 and

       A2: n is odd;

      (x |^ n) = ((p + ( sqrt ((p ^2 ) - (4 * q)))) / 2) & (y |^ n) = ((p - ( sqrt ((p ^2 ) - (4 * q)))) / 2) or (x |^ n) = ((p - ( sqrt ((p ^2 ) - (4 * q)))) / 2) & (y |^ n) = ((p + ( sqrt ((p ^2 ) - (4 * q)))) / 2) by A1, Th14;

      hence thesis by A2, POWER: 4;

    end;

    theorem :: POLYEQ_4:16

    ((x |^ n) + (y |^ n)) = p & ((x |^ n) * (y |^ n)) = q & ((p ^2 ) - (4 * q)) >= 0 & p > 0 & q > 0 & n is even & n >= 1 implies x = (n -root ((p + ( sqrt ((p ^2 ) - (4 * q)))) / 2)) & y = (n -root ((p - ( sqrt ((p ^2 ) - (4 * q)))) / 2)) or x = ( - (n -root ((p + ( sqrt ((p ^2 ) - (4 * q)))) / 2))) & y = (n -root ((p - ( sqrt ((p ^2 ) - (4 * q)))) / 2)) or x = (n -root ((p + ( sqrt ((p ^2 ) - (4 * q)))) / 2)) & y = ( - (n -root ((p - ( sqrt ((p ^2 ) - (4 * q)))) / 2))) or x = ( - (n -root ((p + ( sqrt ((p ^2 ) - (4 * q)))) / 2))) & y = ( - (n -root ((p - ( sqrt ((p ^2 ) - (4 * q)))) / 2))) or x = (n -root ((p - ( sqrt ((p ^2 ) - (4 * q)))) / 2)) & y = (n -root ((p + ( sqrt ((p ^2 ) - (4 * q)))) / 2)) or x = ( - (n -root ((p - ( sqrt ((p ^2 ) - (4 * q)))) / 2))) & y = (n -root ((p + ( sqrt ((p ^2 ) - (4 * q)))) / 2)) or x = (n -root ((p - ( sqrt ((p ^2 ) - (4 * q)))) / 2)) & y = ( - (n -root ((p + ( sqrt ((p ^2 ) - (4 * q)))) / 2))) or x = ( - (n -root ((p - ( sqrt ((p ^2 ) - (4 * q)))) / 2))) & y = ( - (n -root ((p + ( sqrt ((p ^2 ) - (4 * q)))) / 2)))

    proof

      assume

       A1: ((x |^ n) + (y |^ n)) = p & ((x |^ n) * (y |^ n)) = q;

      assume that

       A2: ((p ^2 ) - (4 * q)) >= 0 and

       A3: p > 0 and

       A4: q > 0 and

       A5: n is even & n >= 1;

      ( - ( - (4 * q))) > 0 by A4, XREAL_1: 129;

      then ( - (4 * q)) < 0 ;

      then ((p ^2 ) + ( - (4 * q))) < ((p ^2 ) + 0 ) by XREAL_1: 8;

      then ( sqrt ((p ^2 ) - (4 * q))) < ( sqrt (p ^2 )) by A2, SQUARE_1: 27;

      then ( sqrt ((p ^2 ) - (4 * q))) < p by A3, SQUARE_1: 22;

      then ( - ( sqrt ((p ^2 ) - (4 * q)))) > ( - p) by XREAL_1: 24;

      then (( - ( sqrt ((p ^2 ) - (4 * q)))) + p) > ((( - p) + 0 ) + p) by XREAL_1: 8;

      then

       A6: ((( 0 + p) - ( sqrt ((p ^2 ) - (4 * q)))) / 2) > 0 by XREAL_1: 139;

      

       A7: ( delta (1,( - p),q)) = ((( - p) ^2 ) - ((4 * 1) * q)) by QUIN_1:def 1

      .= ((p ^2 ) - (4 * q));

      then 0 <= ( sqrt ( delta (1,( - p),q))) by A2, SQUARE_1: 17, SQUARE_1: 26;

      then (( - ( - p)) + ( sqrt ( delta (1,( - p),q)))) > ( 0 + 0 ) by A3;

      then

       A8: ((( 0 + p) + ( sqrt ((p ^2 ) - (4 * q)))) / 2) > 0 by A7, XREAL_1: 139;

      now

        per cases by A1, A2, Th14;

          suppose (x |^ n) = ((p + ( sqrt ((p ^2 ) - (4 * q)))) / 2) & (y |^ n) = ((p - ( sqrt ((p ^2 ) - (4 * q)))) / 2);

          hence thesis by A5, A8, A6, Th4;

        end;

          suppose (x |^ n) = ((p - ( sqrt ((p ^2 ) - (4 * q)))) / 2) & (y |^ n) = ((p + ( sqrt ((p ^2 ) - (4 * q)))) / 2);

          hence thesis by A5, A8, A6, Th4;

        end;

      end;

      hence thesis;

    end;

    theorem :: POLYEQ_4:17

    ((x |^ n) + (y |^ n)) = a & ((x |^ n) - (y |^ n)) = b & n is even & n >= 1 & (a + b) > 0 & (a - b) > 0 implies x = (n -root ((a + b) / 2)) & y = (n -root ((a - b) / 2)) or x = (n -root ((a + b) / 2)) & y = ( - (n -root ((a - b) / 2))) or x = ( - (n -root ((a + b) / 2))) & y = (n -root ((a - b) / 2)) or x = ( - (n -root ((a + b) / 2))) & y = ( - (n -root ((a - b) / 2)))

    proof

      assume

       A1: ((x |^ n) + (y |^ n)) = a & ((x |^ n) - (y |^ n)) = b;

      assume that

       A2: n is even & n >= 1 and

       A3: (a + b) > 0 & (a - b) > 0 ;

      ((a + b) / 2) > 0 & ((a - b) / 2) > 0 by A3, XREAL_1: 139;

      hence thesis by A1, A2, Th4;

    end;

    theorem :: POLYEQ_4:18

    ((a * (x |^ n)) + (b * (y |^ n))) = p & (x * y) = 0 & n is odd & (a * b) <> 0 implies x = 0 & y = (n -root (p / b)) or x = (n -root (p / a)) & y = 0

    proof

      assume that

       A1: ((a * (x |^ n)) + (b * (y |^ n))) = p and

       A2: (x * y) = 0 and

       A3: n is odd and

       A4: (a * b) <> 0 ;

      consider m be Nat such that

       A5: n = ((2 * m) + 1) by A3, ABIAN: 9;

      

       A6: n > 0 by A5;

      now

        per cases by A2;

          suppose

           A7: x = 0 ;

          then ((a * ( 0 to_power n)) + (b * (y |^ n))) = p by A1;

          then ((a * 0 ) + (b * (y |^ n))) = p by A6, POWER:def 2;

          then (y |^ n) = (p / b) by A4, XCMPLX_1: 89;

          hence thesis by A3, A7, POWER: 4;

        end;

          suppose

           A8: y = 0 ;

          then ((a * (x |^ n)) + (b * ( 0 to_power n))) = p by A1;

          then ((a * (x |^ n)) + (b * 0 )) = p by A6, POWER:def 2;

          then (x |^ n) = (p / a) by A4, XCMPLX_1: 89;

          hence thesis by A3, A8, POWER: 4;

        end;

      end;

      hence thesis;

    end;

    theorem :: POLYEQ_4:19

    ((a * (x |^ n)) + (b * (y |^ n))) = p & (x * y) = 0 & n is even & n >= 1 & (p / b) > 0 & (p / a) > 0 & (a * b) <> 0 implies x = 0 & y = (n -root (p / b)) or x = 0 & y = ( - (n -root (p / b))) or x = (n -root (p / a)) & y = 0 or x = ( - (n -root (p / a))) & y = 0

    proof

      assume that

       A1: ((a * (x |^ n)) + (b * (y |^ n))) = p and

       A2: (x * y) = 0 and

       A3: n is even & n >= 1 and

       A4: (p / b) > 0 and

       A5: (p / a) > 0 and

       A6: (a * b) <> 0 ;

      n >= 1 by A3;

      then

       A7: n > 0 ;

      per cases by A2;

        suppose

         A8: x = 0 ;

        then ((a * ( 0 to_power n)) + (b * (y |^ n))) = p by A1;

        then ((a * 0 ) + (b * (y |^ n))) = p by A7, POWER:def 2;

        then (y |^ n) = (p / b) by A6, XCMPLX_1: 89;

        hence thesis by A3, A4, A8, Th4;

      end;

        suppose

         A9: y = 0 ;

        then ((a * (x |^ n)) + (b * ( 0 to_power n))) = p by A1;

        then ((a * (x |^ n)) + (b * 0 )) = p by A7, POWER:def 2;

        then (x |^ n) = (p / a) by A6, XCMPLX_1: 89;

        hence thesis by A3, A5, A9, Th4;

      end;

    end;

    theorem :: POLYEQ_4:20

    (a * (x |^ n)) = p & (x * y) = q & n is odd & (p * a) <> 0 implies x = (n -root (p / a)) & y = (q * (n -root (a / p)))

    proof

      assume that

       A1: (a * (x |^ n)) = p and

       A2: (x * y) = q and

       A3: n is odd and

       A4: (p * a) <> 0 ;

      consider m be Nat such that

       A5: n = ((2 * m) + 1) by A3, ABIAN: 9;

      

       A6: a <> 0 by A4;

      then

       A7: (x |^ n) = (p / a) by A1, XCMPLX_1: 89;

      then x = (n -root (p / a)) by A3, POWER: 4;

      then (y * ((n -root (p / a)) * (n -root (a / p)))) = (q * (n -root (a / p))) by A2;

      then (y * (n -root ((p / a) * (a / p)))) = (q * (n -root (a / p))) by A3, POWER: 11;

      then (y * (n -root ((p / a) * (a * (p " ))))) = (q * (n -root (a / p))) by XCMPLX_0:def 9;

      then (y * (n -root (((p / a) * a) * (p " )))) = (q * (n -root (a / p)));

      then (y * (n -root (p * (p " )))) = (q * (n -root (a / p))) by A6, XCMPLX_1: 87;

      then

       A8: (y * (n -root (p / p))) = (q * (n -root (a / p))) by XCMPLX_0:def 9;

      

       A9: ((2 * m) + 1) >= ( 0 + 1) by XREAL_1: 7;

      p <> 0 by A4;

      then (y * (n -root 1)) = (q * (n -root (a / p))) by A8, XCMPLX_1: 60;

      then (y * 1) = (q * (n -root (a / p))) by A5, A9, POWER: 6;

      hence thesis by A3, A7, POWER: 4;

    end;

    theorem :: POLYEQ_4:21

    (a * (x |^ n)) = p & (x * y) = q & n is even & n >= 1 & (p / a) > 0 & a <> 0 implies x = (n -root (p / a)) & y = (q * (n -root (a / p))) or x = ( - (n -root (p / a))) & y = ( - (q * (n -root (a / p))))

    proof

      assume that

       A1: (a * (x |^ n)) = p and

       A2: (x * y) = q and

       A3: n is even & n >= 1 and

       A4: (p / a) > 0 and

       A5: a <> 0 ;

      

       A6: (x |^ n) = (p / a) by A1, A5, XCMPLX_1: 89;

      ((p / a) " ) > 0 by A4;

      then (1 / (p / a)) > 0 by XCMPLX_1: 215;

      then

       A7: ((1 * a) / p) > 0 by XCMPLX_1: 77;

      

       A8: p <> 0 by A4;

      per cases by A3, A4, A6, Th4;

        suppose

         A9: x = (n -root (p / a));

        then (y * ((n -root (p / a)) * (n -root (a / p)))) = (q * (n -root (a / p))) by A2;

        then (y * (n -root ((p / a) * (a / p)))) = (q * (n -root (a / p))) by A4, A3, A7, POWER: 11;

        then (y * (n -root ((p / a) * (a * (p " ))))) = (q * (n -root (a / p))) by XCMPLX_0:def 9;

        then (y * (n -root (((p / a) * a) * (p " )))) = (q * (n -root (a / p)));

        then (y * (n -root (p * (p " )))) = (q * (n -root (a / p))) by A5, XCMPLX_1: 87;

        then (y * (n -root (p / p))) = (q * (n -root (a / p))) by XCMPLX_0:def 9;

        then (y * (n -root 1)) = (q * (n -root (a / p))) by A8, XCMPLX_1: 60;

        then (y * 1) = (q * (n -root (a / p))) by A3, POWER: 6;

        hence thesis by A9;

      end;

        suppose

         A10: x = ( - (n -root (p / a)));

        then (y * ((n -root (p / a)) * (n -root (a / p)))) = ( - (q * (n -root (a / p)))) by A2;

        then (y * (n -root ((p / a) * (a / p)))) = ( - (q * (n -root (a / p)))) by A4, A3, A7, POWER: 11;

        then (y * (n -root ((p / a) * (a * (p " ))))) = ( - (q * (n -root (a / p)))) by XCMPLX_0:def 9;

        then (y * (n -root (((p / a) * a) * (p " )))) = ( - (q * (n -root (a / p))));

        then (y * (n -root (p * (p " )))) = ( - (q * (n -root (a / p)))) by A5, XCMPLX_1: 87;

        then (y * (n -root (p / p))) = ( - (q * (n -root (a / p)))) by XCMPLX_0:def 9;

        then (y * (n -root 1)) = ( - (q * (n -root (a / p)))) by A8, XCMPLX_1: 60;

        then (y * 1) = ( - (q * (n -root (a / p)))) by A3, POWER: 6;

        hence thesis by A10;

      end;

    end;

    theorem :: POLYEQ_4:22

    for a,x be Real st a > 0 & a <> 1 & (a to_power x) = 1 holds x = 0

    proof

      let a,x be Real;

      assume that

       A1: a > 0 & a <> 1 and

       A2: (a to_power x) = 1;

      x = ( log (a,1)) by A1, A2, POWER:def 3;

      hence thesis by A1, POWER: 51;

    end;

    theorem :: POLYEQ_4:23

    for a,x be Real st a > 0 & a <> 1 & (a to_power x) = a holds x = 1

    proof

      let a,x be Real;

      assume that

       A1: a > 0 & a <> 1 and

       A2: (a to_power x) = a;

      x = ( log (a,a)) by A1, A2, POWER:def 3;

      hence thesis by A1, POWER: 52;

    end;

    theorem :: POLYEQ_4:24

    for a,b,x be Real st a > 0 & a <> 1 & x > 0 & ( log (a,x)) = 0 holds x = 1

    proof

      let a,b,x be Real;

      assume a > 0 & a <> 1 & x > 0 & ( log (a,x)) = 0 ;

      then (a to_power 0 ) = x by POWER:def 3;

      hence thesis by POWER: 24;

    end;

    theorem :: POLYEQ_4:25

    for a,b,x be Real st a > 0 & a <> 1 & x > 0 & ( log (a,x)) = 1 holds x = a

    proof

      let a,b,x be Real;

      assume a > 0 & a <> 1 & x > 0 & ( log (a,x)) = 1;

      then (a to_power 1) = x by POWER:def 3;

      hence thesis;

    end;