polyeq_1.miz



    begin

    reserve a,a9,a1,a2,a3,b,b9,c,c9,d,d9,h,p,q,x,x1,x2,x3,u,v,y,z for Real;

    definition

      let a,b,x be Complex;

      :: POLYEQ_1:def1

      func Polynom (a,b,x) -> number equals ((a * x) + b);

      coherence ;

    end

    registration

      let a,b,x be Complex;

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

      coherence ;

    end

    registration

      let a,b,x be Real;

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

      coherence ;

    end

    theorem :: POLYEQ_1:1

    for a,b,x be Complex holds a <> 0 & ( Polynom (a,b,x)) = 0 implies x = ( - (b / a))

    proof

      let a,b,x be Complex;

      assume that

       A1: a <> 0 and

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

      ((a " ) * ( - b)) = ((a " ) * (a * x)) by A2

      .= (((a " ) * a) * x);

      then (1 * x) = ((a " ) * ( - b)) by A1, XCMPLX_0:def 7;

      then x = ( - ((a " ) * b));

      hence thesis by XCMPLX_0:def 9;

    end;

    theorem :: POLYEQ_1:2

    for x be Complex holds ( Polynom ( 0 , 0 ,x)) = 0 ;

    theorem :: POLYEQ_1:3

    for b be Complex holds b <> 0 implies not ex x be Complex st ( Polynom ( 0 ,b,x)) = 0 ;

    definition

      let a,b,c,x be Complex;

      :: POLYEQ_1:def2

      func Polynom (a,b,c,x) -> number equals (((a * (x ^2 )) + (b * x)) + c);

      coherence ;

    end

    registration

      let a,b,c,x be Real;

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

      coherence ;

    end

    registration

      let a,b,c,x be Complex;

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

      coherence ;

    end

    theorem :: POLYEQ_1:4

    

     Th4: for a,b,c,a9,b9,c9 be Complex holds (for x be Real holds ( Polynom (a,b,c,x)) = ( Polynom (a9,b9,c9,x))) implies a = a9 & b = b9 & c = c9

    proof

      let a,b,c,a9,b9,c9 be Complex;

      assume

       A1: for x be Real holds ( Polynom (a,b,c,x)) = ( Polynom (a9,b9,c9,x));

      then

       A2: ( Polynom (a,b,c,( - 1))) = ( Polynom (a9,b9,c9,( - 1)));

      ( Polynom (a,b,c, 0 )) = ( Polynom (a9,b9,c9, 0 )) & ( Polynom (a,b,c,1)) = ( Polynom (a9,b9,c9,1)) by A1;

      hence thesis by A2;

    end;

    theorem :: POLYEQ_1:5

    

     Th5: a <> 0 & ( delta (a,b,c)) >= 0 implies for x holds ( Polynom (a,b,c,x)) = 0 implies x = ((( - b) + ( sqrt ( delta (a,b,c)))) / (2 * a)) or x = ((( - b) - ( sqrt ( delta (a,b,c)))) / (2 * a))

    proof

      assume that

       A1: a <> 0 and

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

      now

        set e = (a * c);

        let y;

        set t = (((a ^2 ) * (y ^2 )) + ((a * b) * y));

        assume ( Polynom (a,b,c,y)) = 0 ;

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

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

        then

         A3: ((t + ((b ^2 ) / 4)) - ((b ^2 ) * (4 " ))) = ( - ((4 * e) * (4 " )));

        

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

         A5:

        now

          assume (((a * y) + (b / 2)) - ( sqrt (((b ^2 ) - (4 * (a * c))) / 4))) = 0 ;

          then ((a * y) + (b / 2)) = (( sqrt ((b ^2 ) - (4 * (a * c)))) / 2) by A2, A4, SQUARE_1: 20, SQUARE_1: 30;

          

          then (a * y) = ( - ((b * (2 " )) - (( sqrt ((b ^2 ) - (4 * (a * c)))) * (2 " ))))

          .= ((( - b) * (2 " )) + (( sqrt ( delta (a,b,c))) * (2 " ))) by A4;

          

          then y = (((( - b) * (2 " )) + (( sqrt ( delta (a,b,c))) * (2 " ))) / a) by A1, XCMPLX_1: 89

          .= (((( - b) * (2 " )) + (( sqrt ( delta (a,b,c))) * (2 " ))) * (a " )) by XCMPLX_0:def 9

          .= ((( - b) + ( sqrt ( delta (a,b,c)))) * ((2 " ) * (a " )))

          .= ((( - b) + ( sqrt ( delta (a,b,c)))) * ((2 * a) " )) by XCMPLX_1: 204;

          hence y = ((( - b) + ( sqrt ( delta (a,b,c)))) / (2 * a)) by XCMPLX_0:def 9;

        end;

         A6:

        now

          assume (((a * y) + (b / 2)) + ( sqrt (((b ^2 ) - (4 * (a * c))) / 4))) = 0 ;

          then ((a * y) + (b / 2)) = ( - ( sqrt (((b ^2 ) - (4 * (a * c))) / 4)));

          then ((a * y) + (b / 2)) = ( - (( sqrt ((b ^2 ) - (4 * (a * c)))) / 2)) by A2, A4, SQUARE_1: 20, SQUARE_1: 30;

          

          then (a * y) = ( - ((b * (2 " )) + (( sqrt ((b ^2 ) - (4 * (a * c)))) * (2 " ))))

          .= ((( - b) * (2 " )) - (( sqrt ( delta (a,b,c))) * (2 " ))) by A4;

          

          then y = (((( - b) * (2 " )) - (( sqrt ( delta (a,b,c))) * (2 " ))) / a) by A1, XCMPLX_1: 89

          .= (((( - b) * (2 " )) - (( sqrt ( delta (a,b,c))) * (2 " ))) * (a " )) by XCMPLX_0:def 9

          .= ((( - b) - ( sqrt ( delta (a,b,c)))) * ((2 " ) * (a " )))

          .= ((( - b) - ( sqrt ( delta (a,b,c)))) * ((2 * a) " )) by XCMPLX_1: 204;

          hence y = ((( - b) - ( sqrt ( delta (a,b,c)))) / (2 * a)) by XCMPLX_0:def 9;

        end;

        (((b ^2 ) - (4 * (a * c))) / 4) >= ( 0 / 4) by A2, A4, XREAL_1: 72;

        then (((a * y) + (b / 2)) ^2 ) = (( sqrt (((b ^2 ) - (4 * (a * c))) / 4)) ^2 ) by A3, SQUARE_1:def 2;

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

        hence y = ((( - b) + ( sqrt ( delta (a,b,c)))) / (2 * a)) or y = ((( - b) - ( sqrt ( delta (a,b,c)))) / (2 * a)) by A5, A6, XCMPLX_1: 6;

      end;

      hence thesis;

    end;

    theorem :: POLYEQ_1:6

    for a,b,c,x be Complex holds a <> 0 & ( delta (a,b,c)) = 0 & ( Polynom (a,b,c,x)) = 0 implies x = ( - (b / (2 * a)))

    proof

      let a,b,c,x be Complex;

      assume that

       A1: a <> 0 and

       A2: ( delta (a,b,c)) = 0 ;

      set y = x;

      set t = (((a ^2 ) * (y ^2 )) + ((a * b) * y));

      

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

      assume ( Polynom (a,b,c,y)) = 0 ;

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

      then (t + (a * c)) = 0 ;

      then ((((a * y) ^2 ) + (2 * (((a * y) * b) * (2 " )))) + ((b / 2) ^2 )) = 0 by A2, A3;

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

      then ((a * y) + (b / 2)) = 0 by XCMPLX_1: 6;

      

      then y = (( - (b * (2 " ))) / a) by A1, XCMPLX_1: 89

      .= ((( - 1) * (b * (2 " ))) * (a " )) by XCMPLX_0:def 9

      .= ( - ((b * ((2 " ) * (a " ))) * 1))

      .= ( - (b * ((2 * a) " ))) by XCMPLX_1: 204;

      hence thesis by XCMPLX_0:def 9;

    end;

    theorem :: POLYEQ_1:7

    ( delta (a,b,c)) < 0 implies not ex x st ( Polynom (a,b,c,x)) = 0

    proof

      set e = (a * c);

      assume ( delta (a,b,c)) < 0 ;

      then ((b ^2 ) - ((4 * a) * c)) < 0 by QUIN_1:def 1;

      then

       A1: (((b ^2 ) - (4 * (a * c))) * (4 " )) < 0 by XREAL_1: 132;

      given y such that

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

      set t = (((a ^2 ) * (y ^2 )) + ((a * b) * y));

      (a * (((a * (y ^2 )) + (b * y)) + c)) = (a * 0 ) by A2;

      then ((t + ((b ^2 ) / 4)) - (((b ^2 ) * (4 " )) - ((4 * e) * (4 " )))) = 0 ;

      then

       A3: (((a * y) + (b / 2)) ^2 ) = (((b ^2 ) - (4 * (a * c))) * (4 " ));

      then ((a * y) + (b / 2)) > 0 by A1, XREAL_1: 133;

      hence contradiction by A3, A1, XREAL_1: 133;

    end;

    theorem :: POLYEQ_1:8

    for b,c be Complex holds b <> 0 & (for x be Real holds ( Polynom ( 0 ,b,c,x)) = 0 ) implies x = ( - (c / b))

    proof

      let b,c be Complex;

      assume

       A1: b <> 0 ;

      set y = x;

      assume for x be Real holds ( Polynom ( 0 ,b,c,x)) = 0 ;

      then ( Polynom ( 0 ,b,c,y)) = 0 ;

      

      then y = (( - c) / b) by A1, XCMPLX_1: 89

      .= ((( - 1) * c) * (b " )) by XCMPLX_0:def 9

      .= (( - 1) * (c * (b " )))

      .= (( - 1) * (c / b)) by XCMPLX_0:def 9;

      hence thesis;

    end;

    theorem :: POLYEQ_1:9

    for x be Complex holds ( Polynom ( 0 , 0 , 0 ,x)) = 0 ;

    theorem :: POLYEQ_1:10

    for c be Complex holds c <> 0 implies not ex x be Complex st ( Polynom ( 0 , 0 ,c,x)) = 0 ;

    definition

      let a,x,x1,x2 be Complex;

      :: POLYEQ_1:def3

      func Quard (a,x1,x2,x) -> number equals (a * ((x - x1) * (x - x2)));

      coherence ;

    end

    registration

      let a,x,x1,x2 be Real;

      cluster ( Quard (a,x1,x2,x)) -> real;

      coherence ;

    end

    theorem :: POLYEQ_1:11

    for a,b,c be Complex holds a <> 0 & (for x be Real holds ( Polynom (a,b,c,x)) = ( Quard (a,x1,x2,x))) implies (b / a) = ( - (x1 + x2)) & (c / a) = (x1 * x2)

    proof

      let a,b,c be Complex;

      assume

       A1: a <> 0 ;

      assume

       A2: for x be Real holds ( Polynom (a,b,c,x)) = ( Quard (a,x1,x2,x));

      now

        let z be Real;

        set h = (z - x1), t = (z - x2);

        set e = ((h * t) - (z ^2 ));

        ( Polynom (a,b,c,z)) = ( Quard (a,x1,x2,z)) by A2;

        then (a * ((h * t) - (z ^2 ))) = ((b * z) + c);

        

        then e = (((b * z) + c) / a) by A1, XCMPLX_1: 89

        .= ((a " ) * ((b * z) + c)) by XCMPLX_0:def 9

        .= (((a " ) * (b * z)) + ((a " ) * c));

        then ((((z * z) - (z * x2)) - (x1 * z)) + (x1 * x2)) = (((z ^2 ) + (((a " ) * b) * z)) + ((a " ) * c));

        

        then (((z ^2 ) - ((x1 + x2) * z)) + (x1 * x2)) = (((z ^2 ) + ((b / a) * z)) + ((a " ) * c)) by XCMPLX_0:def 9

        .= (((z ^2 ) + ((b / a) * z)) + (c / a)) by XCMPLX_0:def 9;

        hence ( Polynom (1,( - (x1 + x2)),(x1 * x2),z)) = ( Polynom (1,(b / a),(c / a),z));

      end;

      hence thesis by Th4;

    end;

    begin

    definition

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

      :: POLYEQ_1:def4

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

      coherence ;

    end

    registration

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

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

      coherence ;

    end

    registration

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

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

      coherence ;

    end

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

    then

     Lm1: 3 is odd by ABIAN: 1;

    theorem :: POLYEQ_1:12

    

     Th12: (for x holds ( Polynom (a,b,c,d,x)) = ( Polynom (a9,b9,c9,d9,x))) implies a = a9 & b = b9 & c = c9 & d = d9

    proof

      (( - 1) |^ 3) = ( - (1 |^ (2 + 1))) by Lm1, POWER: 2

      .= ( - ((1 |^ 2) * 1));

      then

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

      

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

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

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

      .= ((2 |^ 1) * (2 * 2));

      assume

       A3: for x holds ( Polynom (a,b,c,d,x)) = ( Polynom (a9,b9,c9,d9,x));

      then

       A4: ( Polynom (a,b,c,d,2)) = ( Polynom (a9,b9,c9,d9,2));

      ( Polynom (a,b,c,d,1)) = ( Polynom (a9,b9,c9,d9,1)) by A3;

      then ((((a * 1) + (b * 1)) + (c * 1)) + d) = ( Polynom (a9,b9,c9,d9,1));

      

      then

       A5: (((a + b) + c) + d) = ((((a9 * 1) + (b9 * 1)) + (c9 * 1)) + d9)

      .= (((a9 + b9) + c9) + d9);

      ( Polynom (a,b,c,d, 0 )) = ( Polynom (a9,b9,c9,d9, 0 )) & ( Polynom (a,b,c,d,( - 1))) = ( Polynom (a9,b9,c9,d9,( - 1))) by A3;

      hence thesis by A5, A1, A4, A2;

    end;

    definition

      let a,x,x1,x2,x3 be Complex;

      :: POLYEQ_1:def5

      func Tri (a,x1,x2,x3,x) -> number equals (a * (((x - x1) * (x - x2)) * (x - x3)));

      coherence ;

    end

    registration

      let a,x,x1,x2,x3 be Real;

      cluster ( Tri (a,x1,x2,x3,x)) -> real;

      coherence ;

    end

    theorem :: POLYEQ_1:13

    a <> 0 & (for x holds ( Polynom (a,b,c,d,x)) = ( Tri (a,x1,x2,x3,x))) implies (b / a) = ( - ((x1 + x2) + x3)) & (c / a) = (((x1 * x2) + (x2 * x3)) + (x1 * x3)) & (d / a) = ( - ((x1 * x2) * x3))

    proof

      assume

       A1: a <> 0 ;

      set t3 = (d / a);

      set t2 = (c / a);

      set t1 = (b / a);

      set d9 = ( - ((x1 * x2) * x3));

      set c9 = (((x1 * x2) + (x2 * x3)) + (x1 * x3));

      set b9 = ( - ((x1 + x2) + x3));

      assume

       A2: for x holds ( Polynom (a,b,c,d,x)) = ( Tri (a,x1,x2,x3,x));

      now

        let x;

        set t = ((((a * (x |^ 3)) + (b * (x ^2 ))) + (c * x)) + d);

        set r8 = (((x - x1) * (x - x2)) * (x - x3));

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

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

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

        then

         A3: (x |^ 3) = ((x * x) * x);

        ( Polynom (a,b,c,d,x)) = ( Tri (a,x1,x2,x3,x)) by A2;

        then

         A4: (t / a) = r8 by A1, XCMPLX_1: 89;

        ((a " ) * t) = (((((a " ) * a) * (x |^ 3)) + (((a " ) * b) * (x ^2 ))) + ((a " ) * ((c * x) + d)))

        .= (((1 * (x |^ 3)) + (((a " ) * b) * (x ^2 ))) + ((((a " ) * c) * x) + ((a " ) * d))) by A1, XCMPLX_0:def 7

        .= (((1 * (x |^ 3)) + (t1 * (x ^2 ))) + ((((a " ) * c) * x) + ((a " ) * d))) by XCMPLX_0:def 9

        .= (((1 * (x |^ 3)) + (t1 * (x ^2 ))) + ((t2 * x) + ((a " ) * d))) by XCMPLX_0:def 9

        .= (((1 * (x |^ 3)) + (t1 * (x ^2 ))) + ((t2 * x) + t3)) by XCMPLX_0:def 9

        .= ( Polynom (1,t1,t2,t3,x));

        hence ( Polynom (1,t1,t2,t3,x)) = ( Polynom (1,b9,c9,d9,x)) by A4, A3, XCMPLX_0:def 9;

      end;

      hence thesis by Th12;

    end;

    theorem :: POLYEQ_1:14

    

     Th14: ((y + h) |^ 3) = (((y |^ 3) + (((3 * h) * (y ^2 )) + ((3 * (h ^2 )) * y))) + (h |^ 3))

    proof

      ((y + h) |^ 3) = ((y + h) |^ (2 + 1));

      

      then

       A1: ((y + h) |^ 3) = (((y + h) |^ (1 + 1)) * (y + h)) by NEWTON: 6

      .= ((((y + h) |^ 1) * (y + h)) * (y + h)) by NEWTON: 6

      .= (((y + h) |^ 1) * ((y + h) ^2 ))

      .= (((y + h) to_power 1) * (((y ^2 ) + ((2 * y) * h)) + (h ^2 ))) by POWER: 41

      .= ((y + h) * (((y ^2 ) + ((2 * y) * h)) + (h ^2 ))) by POWER: 25

      .= (((y * (y ^2 )) + (((3 * h) * (y ^2 )) + (((2 + 1) * (h ^2 )) * y))) + (h * (h ^2 )));

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

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

      .= (((y |^ 1) * y) * y) by NEWTON: 6

      .= ((y |^ 1) * (y ^2 ));

      then

       A2: (y |^ 3) = ((y to_power 1) * (y ^2 )) by POWER: 41;

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

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

      .= (((h |^ 1) * h) * h) by NEWTON: 6

      .= ((h |^ 1) * (h ^2 ))

      .= ((h to_power 1) * (h ^2 )) by POWER: 41

      .= (h * (h ^2 )) by POWER: 25;

      hence thesis by A1, A2, POWER: 25;

    end;

    theorem :: POLYEQ_1:15

    

     Th15: a <> 0 & ( Polynom (a,b,c,d,x)) = 0 implies for a1, a2, a3, h, y st y = (x + (b / (3 * a))) & h = ( - (b / (3 * a))) & a1 = (b / a) & a2 = (c / a) & a3 = (d / a) holds (((y |^ 3) + ((((3 * h) + a1) * (y ^2 )) + ((((3 * (h ^2 )) + (2 * (a1 * h))) + a2) * y))) + (((h |^ 3) + (a1 * (h ^2 ))) + ((a2 * h) + a3))) = 0

    proof

      assume

       A1: a <> 0 ;

      assume

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

      let a1, a2, a3, h, y;

      assume that

       A3: y = (x + (b / (3 * a))) & h = ( - (b / (3 * a))) and

       A4: a1 = (b / a) & a2 = (c / a) & a3 = (d / a);

       0 = ((a " ) * (((a * (x |^ 3)) + (b * (x ^2 ))) + ((c * x) + d))) by A2

      .= (((((a " ) * a) * (x |^ 3)) + ((a " ) * (b * (x ^2 )))) + ((a " ) * ((c * x) + d)))

      .= (((1 * (x |^ 3)) + ((a " ) * (b * (x ^2 )))) + ((a " ) * ((c * x) + d))) by A1, XCMPLX_0:def 7

      .= ((((x |^ 3) + (((a " ) * b) * (x ^2 ))) + (((a " ) * c) * x)) + ((a " ) * d))

      .= ((((x |^ 3) + ((b / a) * (x ^2 ))) + (((a " ) * c) * x)) + ((a " ) * d)) by XCMPLX_0:def 9

      .= ((((x |^ 3) + ((b / a) * (x ^2 ))) + ((c / a) * x)) + ((a " ) * d)) by XCMPLX_0:def 9

      .= ((((x |^ 3) + (a1 * (x ^2 ))) + (a2 * x)) + a3) by A4, XCMPLX_0:def 9;

      

      then 0 = ((((((y |^ 3) + (((3 * h) * (y ^2 )) + ((3 * (h ^2 )) * y))) + (h |^ 3)) + (((a1 * (y ^2 )) + ((2 * (a1 * h)) * y)) + (a1 * (h ^2 )))) + (a2 * (y + h))) + a3) by A3, Th14

      .= ((((y |^ 3) + (((3 * h) * (y ^2 )) + ((3 * (h ^2 )) * y))) + (((2 * (a1 * h)) * y) + (a1 * (y ^2 )))) + ((a2 * y) + (((h |^ 3) + (a1 * (h ^2 ))) + ((a2 * h) + a3))));

      hence thesis;

    end;

    theorem :: POLYEQ_1:16

    a <> 0 & ( Polynom (a,b,c,d,x)) = 0 implies for a1, a2, a3, h, y st y = (x + (b / (3 * a))) & h = ( - (b / (3 * a))) & a1 = (b / a) & a2 = (c / a) & a3 = (d / a) holds ((((y |^ 3) + ( 0 * (y ^2 ))) + (((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) * y)) + ((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 ))))) = 0

    proof

      assume

       A1: a <> 0 ;

      then

       A2: (3 * a) <> 0 ;

      assume

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

      let a1, a2, a3, h, y;

      assume that

       A4: y = (x + (b / (3 * a))) and

       A5: h = ( - (b / (3 * a))) and

       A6: a1 = (b / a) and

       A7: a2 = (c / a) and

       A8: a3 = (d / a);

      set p0 = ((3 * h) + a1);

      

       A9: p0 = (( - (3 * (b / (3 * a)))) + a1) by A5

      .= (( - (3 * (((3 * a) " ) * b))) + a1) by XCMPLX_0:def 9

      .= (( - (3 * (((3 " ) * (a " )) * b))) + a1) by XCMPLX_1: 204

      .= (( - (((3 * (3 " )) * (a " )) * b)) + a1)

      .= (( - (b / a)) + a1) by XCMPLX_0:def 9;

      set q2 = (((h |^ 3) + (a1 * (h ^2 ))) + ((a2 * h) + a3));

      

       A10: q2 = ((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 ))))

      proof

        set t = (3 * a);

        set a6 = (b / t);

        

         A11: (b / a) = ((3 * b) / t) by XCMPLX_1: 91;

        

         A12: (a6 |^ 3) = (a6 |^ (2 + 1))

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

        .= (((a6 |^ 1) * a6) * a6) by NEWTON: 6

        .= ((a6 |^ 1) * (a6 ^2 ))

        .= ((a6 to_power 1) * (a6 ^2 )) by POWER: 41;

        q2 = (((( - (b / t)) |^ 3) + ((b / a) * (( - (b / t)) ^2 ))) + (( - ((c / a) * (b / t))) + (d / a))) by A5, A6, A7, A8

        .= (((( - (b / t)) |^ 3) + ((b / a) * (( - (b / t)) ^2 ))) + (( - ((b * c) / (t * a))) + (d / a))) by XCMPLX_1: 76

        .= (((( - (b / t)) |^ 3) + ((b / a) * (( - (b / t)) ^2 ))) + (( - ((b * c) / (3 * (a ^2 )))) + (1 * (d / a))))

        .= (((( - (b / t)) |^ 3) + ((b / a) * (( - (b / t)) ^2 ))) + (( - ((b * c) / (3 * (a ^2 )))) + ((t / t) * (d / a)))) by A2, XCMPLX_1: 60

        .= ((((( - (b / t)) |^ 3) + ((b / a) * (( - (b / t)) ^2 ))) + ((t / t) * (d / a))) - ((b * c) / (3 * (a ^2 ))))

        .= ((((( - (b / t)) |^ 3) + ((b / a) * (( - (b / t)) ^2 ))) + ((t * d) / (t * a))) - ((b * c) / (3 * (a ^2 )))) by XCMPLX_1: 76

        .= ((((( - (b / t)) |^ 3) + ((b / a) * (( - (b / t)) ^2 ))) + ((t * d) * ((3 * (a ^2 )) " ))) - ((b * c) / (3 * (a ^2 )))) by XCMPLX_0:def 9

        .= ((((( - (b / t)) |^ 3) + ((b / a) * (( - (b / t)) ^2 ))) + ((t * d) * ((3 * (a ^2 )) " ))) - ((b * c) * ((3 * (a ^2 )) " ))) by XCMPLX_0:def 9

        .= (((( - (b / t)) |^ 3) + ((b / a) * (( - (b / t)) ^2 ))) + (((t * d) - (b * c)) * ((3 * (a ^2 )) " )))

        .= (((( - (b / t)) |^ (2 + 1)) + ((b / a) * ((b / t) ^2 ))) + (((t * d) - (b * c)) / (3 * (a ^2 )))) by XCMPLX_0:def 9

        .= ((((( - (b / t)) |^ (1 + 1)) * ( - (b / t))) + ((b / a) * ((b / t) ^2 ))) + (((t * d) - (b * c)) / (3 * (a ^2 )))) by NEWTON: 6

        .= (((((( - (b / t)) |^ 1) * ( - (b / t))) * ( - (b / t))) + ((b / a) * ((b / t) ^2 ))) + (((t * d) - (b * c)) / (3 * (a ^2 )))) by NEWTON: 6

        .= ((((( - (b / t)) |^ 1) * (( - (b / t)) ^2 )) + ((b / a) * ((b / t) ^2 ))) + (((t * d) - (b * c)) / (3 * (a ^2 ))))

        .= ((((( - (b / t)) to_power 1) * (( - (b / t)) ^2 )) + ((b / a) * ((b / t) ^2 ))) + (((t * d) - (b * c)) / (3 * (a ^2 )))) by POWER: 41

        .= (((( - (b / t)) * ((b / t) ^2 )) + ((b / a) * ((b / t) ^2 ))) + (((t * d) - (b * c)) / (3 * (a ^2 )))) by POWER: 25

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

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

        .= ((((b / a) - (b / t)) * ((b ^2 ) / (t ^2 ))) + (((t * d) - (b * c)) / (3 * (a ^2 ))))

        .= (((((3 * b) * (t " )) - ((1 * b) / t)) * ((b ^2 ) / (t ^2 ))) + (((t * d) - (b * c)) / (3 * (a ^2 )))) by A11, XCMPLX_0:def 9

        .= (((((3 * b) * (t " )) - ((1 * b) * (t " ))) * ((b ^2 ) / (t ^2 ))) + (((t * d) - (b * c)) / (3 * (a ^2 )))) by XCMPLX_0:def 9

        .= ((2 * ((b * (t " )) * ((b ^2 ) / (t ^2 )))) + (((t * d) - (b * c)) / (3 * (a ^2 ))))

        .= ((2 * ((b / t) * ((b ^2 ) / (t ^2 )))) + (((t * d) - (b * c)) / (3 * (a ^2 )))) by XCMPLX_0:def 9

        .= ((2 * ((b / t) * ((b / t) ^2 ))) + (((t * d) - (b * c)) / (3 * (a ^2 )))) by XCMPLX_1: 76;

        hence thesis by A12, POWER: 25;

      end;

      set p2 = (((3 * (h ^2 )) + (2 * (a1 * h))) + a2);

      

       A13: p2 = ((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 )))

      proof

        set t = (((3 * a) " ) * b);

        

         A14: ((3 * a) / (3 * a)) = 1 by A2, XCMPLX_1: 60;

        p2 = (((3 * ((b / (3 * a)) ^2 )) + (2 * (a1 * ( - (b / (3 * a)))))) + a2) by A5

        .= (((3 * ((((3 * a) " ) * b) ^2 )) + (2 * (a1 * ( - (b / (3 * a)))))) + a2) by XCMPLX_0:def 9

        .= (((((3 * ((3 * a) " )) * b) * t) + (2 * (a1 * ( - (b / (3 * a)))))) + a2)

        .= (((((3 * ((3 " ) * (a " ))) * b) * t) + (2 * (a1 * ( - (b / (3 * a)))))) + a2) by XCMPLX_1: 204

        .= ((((b / a) * (((3 * a) " ) * b)) + (2 * (a1 * ( - (b / (3 * a)))))) + a2) by XCMPLX_0:def 9

        .= ((((b / a) * (b / (3 * a))) + (2 * (a1 * ( - (b / (3 * a)))))) + a2) by XCMPLX_0:def 9

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

        .= ((((b ^2 ) / (3 * (a ^2 ))) - (2 * ((b / a) * (b / (3 * a))))) + (c / a)) by A6, A7

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

        .= (( - ((b ^2 ) / (3 * (a ^2 )))) + (((3 * a) / (3 * a)) * (c / a))) by A14

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

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

        .= ((((3 * a) * c) * ((3 * (a ^2 )) " )) - ((b ^2 ) / (3 * (a ^2 )))) by XCMPLX_0:def 9

        .= ((((3 * a) * c) * ((3 * (a ^2 )) " )) - ((b ^2 ) * ((3 * (a ^2 )) " ))) by XCMPLX_0:def 9

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

        hence thesis by XCMPLX_0:def 9;

      end;

      (((y |^ 3) + ((p0 * (y ^2 )) + (p2 * y))) + q2) = 0 by A1, A3, A4, A5, A6, A7, A8, Th15;

      hence thesis by A6, A9, A13, A10;

    end;

    theorem :: POLYEQ_1:17

    ((((y |^ 3) + ( 0 * (y ^2 ))) + (((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) * y)) + ((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 ))))) = 0 implies for p, q st p = ((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) & q = ((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) holds ( Polynom (1, 0 ,p,q,y)) = 0 ;

    theorem :: POLYEQ_1:18

    

     Th18: ( Polynom (1, 0 ,p,q,y)) = 0 implies for u, v st y = (u + v) & (((3 * v) * u) + p) = 0 holds ((u |^ 3) + (v |^ 3)) = ( - q) & ((u |^ 3) * (v |^ 3)) = (( - (p / 3)) |^ 3)

    proof

      assume

       A1: ( Polynom (1, 0 ,p,q,y)) = 0 ;

      let u, v;

      assume that

       A2: y = (u + v) and

       A3: (((3 * v) * u) + p) = 0 ;

      ((u + v) |^ 3) = (((u |^ 3) + (((3 * v) * (u ^2 )) + ((3 * (v ^2 )) * u))) + (v |^ 3)) by Th14

      .= (((u |^ 3) + (((3 * v) * u) * (u + v))) + (v |^ 3));

      then 0 = ((((u |^ 3) + (v |^ 3)) + ((((3 * v) * u) + p) * (u + v))) + q) by A1, A2;

      hence ((u |^ 3) + (v |^ 3)) = ( - q) by A3;

      (3 * (v * u)) = ( - p) by A3;

      hence thesis by NEWTON: 7;

    end;

    theorem :: POLYEQ_1:19

    

     Th19: ( Polynom (1, 0 ,p,q,y)) = 0 implies for u, v st y = (u + v) & (((3 * v) * u) + p) = 0 holds y = ((3 -root (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) + (3 -root (( - (q / 2)) - ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))))) or y = ((3 -root (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) + (3 -root (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))))) or y = ((3 -root (( - (q / 2)) - ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) + (3 -root (( - (q / 2)) - ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))))

    proof

      set e1 = 1;

      assume

       A1: ( Polynom (1, 0 ,p,q,y)) = 0 ;

      set e3 = (( - (p / 3)) |^ 3);

      set e2 = q;

      let u, v;

      assume that

       A2: y = (u + v) and

       A3: (((3 * v) * u) + p) = 0 ;

      set z2 = (v |^ 3);

      set z1 = (u |^ 3);

       A4:

      now

        let z;

        

        thus ((z - z1) * (z - z2)) = (((z ^2 ) - ((z1 + z2) * z)) + (z1 * z2))

        .= (((z ^2 ) - (( - q) * z)) + (z1 * z2)) by A1, A2, A3, Th18

        .= (((z ^2 ) + (q * z)) + (( - (p / 3)) |^ 3)) by A1, A2, A3, Th18;

      end;

      

       A5: (z1 + z2) = ( - q) by A1, A2, A3, Th18;

      then (e2 ^2 ) = ((z1 + z2) ^2 ) by SQUARE_1: 3;

      

      then

       A6: ((e2 ^2 ) - ((4 * e1) * e3)) = (( - ( - (((z1 ^2 ) + ((2 * z1) * z2)) + (z2 ^2 )))) - (4 * (z1 * z2))) by A1, A2, A3, Th18

      .= ((z1 - z2) ^2 );

      then

       A7: ((e2 ^2 ) - ((4 * e1) * e3)) >= 0 by XREAL_1: 63;

      then

       A8: ( delta (e1,e2,e3)) >= 0 by QUIN_1:def 1;

      ((z1 - z1) * (z1 - z2)) = ( 0 * (z1 - z2));

      then

       A9: ( Polynom (e1,e2,e3,z1)) = 0 by A4;

      ((z2 - z1) * (z2 - z2)) = ((z2 - z1) * 0 );

      then

       A10: ( Polynom (e1,e2,e3,z2)) = 0 by A4;

      

       A11: (z2 * z1) = (( - (p / 3)) |^ 3) by A1, A2, A3, Th18;

      now

        per cases by A9, A8, Th5;

          case

           A12: z1 = ((( - e2) + ( sqrt ( delta (e1,e2,e3)))) / (2 * e1));

          

           A13: ((p / 3) |^ 3) = ((p / 3) |^ (2 + 1))

          .= (((p / 3) |^ (1 + 1)) * (p / 3)) by NEWTON: 6

          .= ((((p / 3) |^ 1) * (p / 3)) * (p / 3)) by NEWTON: 6

          .= (((p / 3) |^ 1) * ((p / 3) ^2 ))

          .= (((p / 3) to_power 1) * ((p / 3) ^2 )) by POWER: 41

          .= ((p / 3) * ((p / 3) ^2 )) by POWER: 25;

          

           A14: ((q ^2 ) - (4 * (( - (p / 3)) |^ 3))) >= 0 by A6, XREAL_1: 63;

          

           A15: (( - (p / 3)) |^ 3) = (( - (p / 3)) |^ (2 + 1))

          .= ((( - (p / 3)) |^ (1 + 1)) * ( - (p / 3))) by NEWTON: 6

          .= (((( - (p / 3)) |^ 1) * ( - (p / 3))) * ( - (p / 3))) by NEWTON: 6

          .= ((( - (p / 3)) |^ 1) * (( - (p / 3)) ^2 ));

          

          then

           A16: (( - (p / 3)) |^ 3) = ((( - (p / 3)) to_power 1) * (( - (p / 3)) ^2 )) by POWER: 41

          .= (( - (p / 3)) * ((p / 3) ^2 )) by POWER: 25

          .= ( - ((p / 3) * ((p / 3) ^2 )));

          

           A17: z1 = ((( - e2) + ( sqrt ((e2 ^2 ) - ((4 * e1) * e3)))) / (2 * e1)) by A12, QUIN_1:def 1

          .= ((( - q) / 2) + (( sqrt ((q ^2 ) - (4 * (( - (p / 3)) |^ 3)))) / ( sqrt 4))) by SQUARE_1: 20, XCMPLX_1: 62

          .= ((( - q) / 2) + ( sqrt (((q ^2 ) - (4 * (( - (p / 3)) |^ 3))) / 4))) by A14, SQUARE_1: 30

          .= ((( - q) / 2) + ( sqrt (((q ^2 ) / 4) - (1 * (( - (p / 3)) |^ 3)))));

           A18:

          now

            per cases by XXREAL_0: 1;

              case

               A19: u > 0 ;

              then

               A20: (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) > 0 by A17, A16, A13, PREPOWER: 6;

              then u = (3 -Root (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A17, A16, A13, A19, PREPOWER:def 2;

              hence u = (3 -root (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A20, POWER:def 1;

            end;

              case

               A21: u = 0 ;

              then

               A22: (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) = 0 by A17, A16, A13, NEWTON: 11;

              then (3 -Root (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) = 0 by PREPOWER:def 2;

              hence u = (3 -root (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A21, A22, POWER:def 1;

            end;

              case u < 0 ;

              then

               A23: ( - u) > 0 by XREAL_1: 58;

              set r = (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))));

              

               A24: (3 -root ( - 1)) = ( - 1) by Lm1, POWER: 8;

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

              .= ((( - u) |^ (1 + 1)) * ( - u)) by NEWTON: 6

              .= (((( - u) |^ 1) * ( - u)) * ( - u)) by NEWTON: 6

              .= ((( - u) |^ 1) * (( - u) ^2 ));

              then (( - u) |^ 3) = ((( - u) to_power 1) * (( - u) ^2 )) by POWER: 41;

              

              then

               A25: (( - u) |^ 3) = (( - u) * (u ^2 )) by POWER: 25

              .= ( - (u * (u ^2 )));

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

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

              .= (((u |^ 1) * u) * u) by NEWTON: 6

              .= ((u |^ 1) * (u * u));

              then

               A26: (u |^ 3) = ((u to_power 1) * (u ^2 )) by POWER: 41;

              then

               A27: (( - u) |^ 3) = ( - (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A17, A16, A13, A25, POWER: 25;

              

               A28: (( - u) |^ 3) = ( - (u |^ 3)) by A25, A26, POWER: 25;

              then

               A29: ( - (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) > 0 by A17, A16, A13, A23, PREPOWER: 6;

              ( - (u |^ 3)) > 0 by A23, A28, PREPOWER: 6;

              then ( - u) = (3 -Root ( - (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))))) by A17, A16, A13, A23, A27, PREPOWER:def 2;

              then ( - u) = (3 -root (( - 1) * r)) by A29, POWER:def 1;

              then ( - u) = ((3 -root ( - 1)) * (3 -root r)) by Lm1, POWER: 11;

              hence u = (3 -root (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A24;

            end;

          end;

          now

            per cases by A8, A10, Th5;

              case z2 = ((( - e2) + ( sqrt ( delta (e1,e2,e3)))) / (2 * e1));

              then z2 = ((( - e2) + ( sqrt ((e2 ^2 ) - ((4 * e1) * e3)))) / (2 * e1)) by QUIN_1:def 1;

              then z2 = ((( - q) / 2) + (( sqrt ((q ^2 ) - (4 * (( - (p / 3)) |^ 3)))) / ( sqrt 4))) by SQUARE_1: 20, XCMPLX_1: 62;

              

              then

               A30: z2 = ((( - q) / 2) + ( sqrt (((q ^2 ) - (4 * (( - (p / 3)) |^ 3))) / 4))) by A7, SQUARE_1: 30

              .= ((( - q) / 2) + ( sqrt (((q ^2 ) / 4) - (1 * (( - (p / 3)) |^ 3)))));

              

               A31: (( - (p / 3)) |^ 3) = ((( - (p / 3)) to_power 1) * (( - (p / 3)) ^2 )) by A15, POWER: 41

              .= (( - (p / 3)) * ((p / 3) ^2 )) by POWER: 25;

              now

                per cases by XXREAL_0: 1;

                  case

                   A32: v > 0 ;

                  then

                   A33: (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) > 0 by A13, A30, A31, PREPOWER: 6;

                  then v = (3 -Root (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A13, A30, A31, A32, PREPOWER:def 2;

                  hence v = (3 -root (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A33, POWER:def 1;

                end;

                  case

                   A34: v = 0 ;

                  then (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) = 0 by A13, A30, A31, NEWTON: 11;

                  hence v = (3 -root (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A34, POWER: 5;

                end;

                  case v < 0 ;

                  then

                   A35: ( - v) > 0 by XREAL_1: 58;

                  then

                   A36: (( - v) |^ 3) > 0 by PREPOWER: 6;

                  (( - v) |^ 3) = (( - v) |^ (2 + 1));

                  then (( - v) |^ 3) = ((( - v) |^ (1 + 1)) * ( - v)) by NEWTON: 6;

                  then (( - v) |^ 3) = (((( - v) |^ 1) * ( - v)) * ( - v)) by NEWTON: 6;

                  then (( - v) |^ 3) = ((( - v) |^ 1) * (( - v) * ( - v)));

                  then (( - v) |^ 3) = ((( - v) to_power 1) * (( - v) ^2 )) by POWER: 41;

                  then (( - v) |^ 3) = (( - v) * (( - v) ^2 )) by POWER: 25;

                  then

                   A37: (( - v) |^ 3) = ( - (v * (v ^2 )));

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

                  then (v |^ 3) = ((v |^ (1 + 1)) * v) by NEWTON: 6;

                  then (v |^ 3) = (((v |^ 1) * v) * v) by NEWTON: 6;

                  then (v |^ 3) = ((v |^ 1) * (v * v));

                  then

                   A38: (v |^ 3) = ((v to_power 1) * (v ^2 )) by POWER: 41;

                  then (( - v) |^ 3) = ( - (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A13, A30, A31, A37, POWER: 25;

                  then

                   A39: ( - v) = (3 -Root ( - (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))))) by A35, A36, PREPOWER:def 2;

                  set r = (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))));

                  

                   A40: (3 -root ( - 1)) = ( - 1) by Lm1, POWER: 8;

                  ( - (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) > 0 by A13, A30, A31, A36, A37, A38, POWER: 25;

                  then ( - v) = (3 -root (( - 1) * r)) by A39, POWER:def 1;

                  then ( - v) = ((3 -root ( - 1)) * (3 -root r)) by Lm1, POWER: 11;

                  hence v = (3 -root (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A40;

                end;

              end;

              hence thesis by A2, A18;

            end;

              case z2 = ((( - e2) - ( sqrt ( delta (e1,e2,e3)))) / (2 * e1));

              then z2 = ((( - e2) - ( sqrt ((e2 ^2 ) - ((4 * e1) * e3)))) / (2 * e1)) by QUIN_1:def 1;

              then z2 = ((( - q) / 2) - (( sqrt ((q ^2 ) - (4 * (( - (p / 3)) |^ 3)))) / 2));

              

              then

               A41: z2 = (( - (q / 2)) - ( sqrt (((q ^2 ) - (4 * (( - (p / 3)) |^ 3))) / 4))) by A7, SQUARE_1: 20, SQUARE_1: 30

              .= (( - (q / 2)) - ( sqrt (((q ^2 ) / 4) - (1 * (( - (p / 3)) |^ 3)))));

              now

                per cases by XXREAL_0: 1;

                  case

                   A42: v > 0 ;

                  then (( - (q / 2)) - ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) > 0 by A16, A13, A41, PREPOWER: 6;

                  then

                   A43: v = (3 -Root (( - (q / 2)) - ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A16, A13, A41, A42, PREPOWER:def 2;

                  (( - (q / 2)) - ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) > 0 by A16, A13, A41, A42, PREPOWER: 6;

                  hence v = (3 -root (( - (q / 2)) - ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A43, POWER:def 1;

                end;

                  case

                   A44: v = 0 ;

                  then

                   A45: (( - (q / 2)) - ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) = 0 by A16, A13, A41, NEWTON: 11;

                  hence v = (3 -Root (( - (q / 2)) - ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A44, PREPOWER:def 2;

                  hence v = (3 -root (( - (q / 2)) - ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A45, POWER:def 1;

                end;

                  case v < 0 ;

                  then

                   A46: ( - v) > 0 by XREAL_1: 58;

                  set r = (( - (q / 2)) - ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))));

                  

                   A47: (3 -root ( - 1)) = ( - 1) by Lm1, POWER: 8;

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

                  then (v |^ 3) = ((v |^ (1 + 1)) * v) by NEWTON: 6;

                  then

                   A48: (v |^ 3) = (((v |^ 1) * v) * v) by NEWTON: 6;

                  (( - v) |^ 3) = (( - v) |^ (2 + 1));

                  then (( - v) |^ 3) = ((( - v) |^ (1 + 1)) * ( - v)) by NEWTON: 6;

                  then (( - v) |^ 3) = (((( - v) |^ 1) * ( - v)) * ( - v)) by NEWTON: 6;

                  then (( - v) |^ 3) = ((( - v) |^ 1) * (( - v) * ( - v)));

                  

                  then

                   A49: (( - v) |^ 3) = ((( - v) to_power 1) * (( - v) ^2 )) by POWER: 41

                  .= (( - v) * (v ^2 )) by POWER: 25

                  .= ( - (v * (v ^2 )));

                  (( - v) |^ 3) = ( - (v |^ 3)) by A49, A48;

                  then

                   A50: ( - (( - (q / 2)) - ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) > 0 by A16, A13, A41, A46, PREPOWER: 6;

                  (( - v) |^ 3) = ( - (( - (q / 2)) - ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A16, A13, A41, A49, A48;

                  then ( - v) = (3 -Root ( - (( - (q / 2)) - ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))))) by A46, A50, PREPOWER:def 2;

                  then ( - v) = (3 -root (( - 1) * r)) by A50, POWER:def 1;

                  then ( - v) = ((3 -root ( - 1)) * (3 -root r)) by Lm1, POWER: 11;

                  hence v = (3 -root (( - (q / 2)) - ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A47;

                end;

              end;

              hence thesis by A2, A18;

            end;

          end;

          hence thesis;

        end;

          case

           A51: z1 = ((( - e2) - ( sqrt ( delta (e1,e2,e3)))) / (2 * e1));

          (( - (p / 3)) |^ 3) = (( - (p / 3)) |^ (2 + 1));

          then (( - (p / 3)) |^ 3) = ((( - (p / 3)) |^ (1 + 1)) * ( - (p / 3))) by NEWTON: 6;

          then (( - (p / 3)) |^ 3) = (((( - (p / 3)) |^ 1) * ( - (p / 3))) * ( - (p / 3))) by NEWTON: 6;

          then (( - (p / 3)) |^ 3) = ((( - (p / 3)) |^ 1) * (( - (p / 3)) * ( - (p / 3))));

          then (( - (p / 3)) |^ 3) = ((( - (p / 3)) to_power 1) * (( - (p / 3)) ^2 )) by POWER: 41;

          then (( - (p / 3)) |^ 3) = (( - (p / 3)) * (( - (p / 3)) ^2 )) by POWER: 25;

          then

           A52: (( - (p / 3)) |^ 3) = ( - ((p / 3) * ((p / 3) ^2 )));

          z1 = ((( - e2) - ( sqrt ((e2 ^2 ) - ((4 * e1) * e3)))) / (2 * e1)) by A51, QUIN_1:def 1;

          

          then

           A53: z1 = ((( - q) * (2 " )) - (( sqrt ((q ^2 ) - (4 * (( - (p / 3)) |^ 3)))) / 2))

          .= (( - (q / 2)) - ( sqrt (((q ^2 ) - (4 * (( - (p / 3)) |^ 3))) / 4))) by A7, SQUARE_1: 20, SQUARE_1: 30

          .= (( - (q / 2)) - ( sqrt (((q ^2 ) / 4) - (1 * (( - (p / 3)) |^ 3)))));

          hence z1 = (( - (q / 2)) - ( sqrt (((q ^2 ) / 4) - (( - (p / 3)) |^ 3))));

          ((p / 3) |^ 3) = ((p / 3) |^ (2 + 1));

          then ((p / 3) |^ 3) = (((p / 3) |^ (1 + 1)) * (p / 3)) by NEWTON: 6;

          then ((p / 3) |^ 3) = ((((p / 3) |^ 1) * (p / 3)) * (p / 3)) by NEWTON: 6;

          then ((p / 3) |^ 3) = (((p / 3) |^ 1) * ((p / 3) * (p / 3)));

          then ((p / 3) |^ 3) = (((p / 3) to_power 1) * ((p / 3) ^2 )) by POWER: 41;

          then

           A54: (( - (p / 3)) |^ 3) = ( - ((p / 3) |^ 3)) by A52, POWER: 25;

           A55:

          now

            per cases by XXREAL_0: 1;

              case

               A56: u > 0 ;

              then (( - (q / 2)) - ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) > 0 by A53, A54, PREPOWER: 6;

              then

               A57: u = (3 -Root (( - (q / 2)) - ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A53, A54, A56, PREPOWER:def 2;

              (( - (q / 2)) - ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) > 0 by A53, A54, A56, PREPOWER: 6;

              hence u = (3 -root (( - (q / 2)) - ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A57, POWER:def 1;

            end;

              case

               A58: u = 0 ;

              then (( - (q / 2)) - ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) = 0 by A53, A54, NEWTON: 11;

              hence u = (3 -root (( - (q / 2)) - ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A58, POWER: 5;

            end;

              case u < 0 ;

              then

               A59: ( - u) > 0 by XREAL_1: 58;

              then

               A60: (( - u) |^ 3) > 0 by PREPOWER: 6;

              (( - u) |^ 3) = (( - u) |^ (2 + 1));

              then (( - u) |^ 3) = ((( - u) |^ (1 + 1)) * ( - u)) by NEWTON: 6;

              then (( - u) |^ 3) = (((( - u) |^ 1) * ( - u)) * ( - u)) by NEWTON: 6;

              then (( - u) |^ 3) = ((( - u) |^ 1) * (( - u) * ( - u)));

              then (( - u) |^ 3) = ((( - u) to_power 1) * (( - u) ^2 )) by POWER: 41;

              then (( - u) |^ 3) = (( - u) * (( - u) ^2 )) by POWER: 25;

              then

               A61: (( - u) |^ 3) = ( - (u * (u ^2 )));

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

              then (u |^ 3) = ((u |^ (1 + 1)) * u) by NEWTON: 6;

              then (u |^ 3) = (((u |^ 1) * u) * u) by NEWTON: 6;

              then (u |^ 3) = ((u |^ 1) * (u * u));

              then

               A62: (u |^ 3) = ((u to_power 1) * (u ^2 )) by POWER: 41;

              then ( - (( - (q / 2)) - ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) > 0 by A53, A54, A60, A61, POWER: 25;

              then

               A63: (3 -Root ( - (( - (q / 2)) - ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))))) = (3 -root ( - (( - (q / 2)) - ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))))) by POWER:def 1;

              set r = (( - (q / 2)) - ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))));

              (( - u) |^ 3) = ( - (( - (q / 2)) - ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A53, A54, A61, A62, POWER: 25;

              then ( - u) = (3 -root (( - 1) * r)) by A59, A60, A63, PREPOWER:def 2;

              then

               A64: ( - u) = ((3 -root ( - 1)) * (3 -root r)) by Lm1, POWER: 11;

              (3 -root ( - 1)) = ( - 1) by Lm1, POWER: 8;

              hence u = (3 -root (( - (q / 2)) - ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A64;

            end;

          end;

          now

            per cases by A8, A10, Th5;

              case

               A65: z2 = ((( - e2) + ( sqrt ( delta (e1,e2,e3)))) / (2 * e1));

              (( - (p / 3)) |^ 3) = (( - (p / 3)) |^ (2 + 1));

              then (( - (p / 3)) |^ 3) = ((( - (p / 3)) |^ (1 + 1)) * ( - (p / 3))) by NEWTON: 6;

              then (( - (p / 3)) |^ 3) = (((( - (p / 3)) |^ 1) * ( - (p / 3))) * ( - (p / 3))) by NEWTON: 6;

              then (( - (p / 3)) |^ 3) = ((( - (p / 3)) |^ 1) * (( - (p / 3)) * ( - (p / 3))));

              then (( - (p / 3)) |^ 3) = ((( - (p / 3)) to_power 1) * (( - (p / 3)) ^2 )) by POWER: 41;

              then (( - (p / 3)) |^ 3) = (( - (p / 3)) * (( - (p / 3)) ^2 )) by POWER: 25;

              then

               A66: (( - (p / 3)) |^ 3) = ( - ((p / 3) * ((p / 3) ^2 )));

              ((p / 3) |^ 3) = ((p / 3) |^ (2 + 1));

              then ((p / 3) |^ 3) = (((p / 3) |^ (1 + 1)) * (p / 3)) by NEWTON: 6;

              then ((p / 3) |^ 3) = ((((p / 3) |^ 1) * (p / 3)) * (p / 3)) by NEWTON: 6;

              then ((p / 3) |^ 3) = (((p / 3) |^ 1) * ((p / 3) * (p / 3)));

              then ((p / 3) |^ 3) = (((p / 3) to_power 1) * ((p / 3) ^2 )) by POWER: 41;

              then

               A67: (( - (p / 3)) |^ 3) = ( - ((p / 3) |^ 3)) by A66, POWER: 25;

              z2 = ((( - e2) + ( sqrt ((e2 ^2 ) - ((4 * e1) * e3)))) / (2 * e1)) by A65, QUIN_1:def 1;

              then z2 = ((( - q) / 2) + (( sqrt ((q ^2 ) - (4 * (( - (p / 3)) |^ 3)))) / ( sqrt 4))) by SQUARE_1: 20, XCMPLX_1: 62;

              

              then

               A68: z2 = ((( - q) / 2) + ( sqrt (((q ^2 ) - (4 * (( - (p / 3)) |^ 3))) / 4))) by A7, SQUARE_1: 30

              .= ((( - q) / 2) + ( sqrt (((q ^2 ) / 4) - (1 * (( - (p / 3)) |^ 3)))));

              now

                per cases by XXREAL_0: 1;

                  case

                   A69: v > 0 ;

                  then

                   A70: (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) > 0 by A68, A67, PREPOWER: 6;

                  then v = (3 -Root (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A68, A67, A69, PREPOWER:def 2;

                  hence v = (3 -root (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A70, POWER:def 1;

                end;

                  case

                   A71: v = 0 ;

                  then (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) = 0 by A68, A67, NEWTON: 11;

                  hence v = (3 -root (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A71, POWER: 5;

                end;

                  case v < 0 ;

                  then

                   A72: ( - v) > 0 by XREAL_1: 58;

                  then

                   A73: (( - v) |^ 3) > 0 by PREPOWER: 6;

                  (( - v) |^ 3) = (( - v) |^ (2 + 1));

                  then (( - v) |^ 3) = ((( - v) |^ (1 + 1)) * ( - v)) by NEWTON: 6;

                  then (( - v) |^ 3) = (((( - v) |^ 1) * ( - v)) * ( - v)) by NEWTON: 6;

                  then (( - v) |^ 3) = ((( - v) |^ 1) * (( - v) * ( - v)));

                  then (( - v) |^ 3) = ((( - v) to_power 1) * (( - v) ^2 )) by POWER: 41;

                  then (( - v) |^ 3) = (( - v) * (( - v) ^2 )) by POWER: 25;

                  then

                   A74: (( - v) |^ 3) = ( - (v * (v ^2 )));

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

                  then (v |^ 3) = ((v |^ (1 + 1)) * v) by NEWTON: 6;

                  then (v |^ 3) = (((v |^ 1) * v) * v) by NEWTON: 6;

                  then (v |^ 3) = ((v |^ 1) * (v * v));

                  then

                   A75: (v |^ 3) = ((v to_power 1) * (v ^2 )) by POWER: 41;

                  then

                   A76: ( - (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) > 0 by A68, A67, A73, A74, POWER: 25;

                  set r = (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))));

                  

                   A77: (3 -root ( - 1)) = ( - 1) by Lm1, POWER: 8;

                  (v |^ 3) = (v * (v ^2 )) by A75, POWER: 25;

                  then ( - v) = (3 -Root ( - (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))))) by A68, A67, A72, A73, A74, PREPOWER:def 2;

                  then ( - v) = (3 -root (( - 1) * r)) by A76, POWER:def 1;

                  then ( - v) = ((3 -root ( - 1)) * (3 -root r)) by Lm1, POWER: 11;

                  hence v = (3 -root (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A77;

                end;

              end;

              hence thesis by A2, A55;

            end;

              case

               A78: z2 = ((( - e2) - ( sqrt ( delta (e1,e2,e3)))) / (2 * e1));

              (e2 ^2 ) = ((z1 + z2) ^2 ) by A5, SQUARE_1: 3;

              then

               A79: ((e2 ^2 ) - ((4 * e1) * e3)) = ((z1 - z2) ^2 ) by A11;

              (( - (p / 3)) |^ 3) = (( - (p / 3)) |^ (2 + 1))

              .= ((( - (p / 3)) |^ (1 + 1)) * ( - (p / 3))) by NEWTON: 6

              .= (((( - (p / 3)) |^ 1) * ( - (p / 3))) * ( - (p / 3))) by NEWTON: 6

              .= ((( - (p / 3)) |^ 1) * (( - (p / 3)) * ( - (p / 3))));

              

              then (( - (p / 3)) |^ 3) = ((( - (p / 3)) to_power 1) * (( - (p / 3)) ^2 )) by POWER: 41

              .= (( - (p / 3)) * ((p / 3) ^2 )) by POWER: 25;

              then

               A80: (( - (p / 3)) |^ 3) = ( - ((p / 3) * ((p / 3) ^2 )));

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

              .= (((p / 3) |^ (1 + 1)) * (p / 3)) by NEWTON: 6

              .= ((((p / 3) |^ 1) * (p / 3)) * (p / 3)) by NEWTON: 6

              .= (((p / 3) |^ 1) * ((p / 3) ^2 ));

              then ((p / 3) |^ 3) = (((p / 3) to_power 1) * ((p / 3) ^2 )) by POWER: 41;

              then

               A81: (( - (p / 3)) |^ 3) = ( - ((p / 3) |^ 3)) by A80, POWER: 25;

              z2 = ((( - e2) - ( sqrt ((e2 ^2 ) - ((4 * e1) * e3)))) / (2 * e1)) by A78, QUIN_1:def 1;

              

              then

               A82: z2 = ((( - q) / 2) + ( sqrt (((q ^2 ) - (4 * (( - (p / 3)) |^ 3))) / 4))) by A51, A78, A79, SQUARE_1: 17

              .= ((( - q) / 2) + ( sqrt (((q ^2 ) / 4) - (1 * (( - (p / 3)) |^ 3)))));

              now

                per cases by XXREAL_0: 1;

                  case

                   A83: v > 0 ;

                  then

                   A84: (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) > 0 by A82, A81, PREPOWER: 6;

                  then v = (3 -Root (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A82, A81, A83, PREPOWER:def 2;

                  hence v = (3 -root (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A84, POWER:def 1;

                end;

                  case

                   A85: v = 0 ;

                  then (v |^ 3) = 0 by NEWTON: 11;

                  hence v = (3 -root (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A82, A81, A85, POWER: 5;

                end;

                  case v < 0 ;

                  then

                   A86: ( - v) > 0 by XREAL_1: 58;

                  then

                   A87: (( - v) |^ 3) > 0 by PREPOWER: 6;

                  set r = (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))));

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

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

                  .= (((v |^ 1) * v) * v) by NEWTON: 6

                  .= ((v |^ 1) * (v ^2 ));

                  then

                   A88: (v |^ 3) = ((v to_power 1) * (v ^2 )) by POWER: 41;

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

                  .= ((( - v) |^ (1 + 1)) * ( - v)) by NEWTON: 6

                  .= (((( - v) |^ 1) * ( - v)) * ( - v)) by NEWTON: 6

                  .= ((( - v) |^ 1) * (( - v) ^2 ))

                  .= ((( - v) to_power 1) * (( - v) ^2 )) by POWER: 41

                  .= (( - v) * (v ^2 )) by POWER: 25;

                  then

                   A89: (( - v) |^ 3) = ( - (v * (v ^2 )));

                  then

                   A90: ( - (v |^ 3)) > 0 by A87, A88, POWER: 25;

                  

                   A91: (3 -root ( - 1)) = ( - 1) by Lm1, POWER: 8;

                  (( - v) |^ 3) = ( - (v |^ 3)) by A89, A88, POWER: 25;

                  then ( - v) = (3 -Root ( - (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))))) by A82, A81, A86, A87, PREPOWER:def 2;

                  then ( - v) = (3 -root (( - 1) * r)) by A82, A81, A90, POWER:def 1;

                  then ( - v) = ((3 -root ( - 1)) * (3 -root r)) by Lm1, POWER: 11;

                  hence v = (3 -root (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A91;

                end;

              end;

              hence y = ((3 -root (( - (q / 2)) + ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) + (3 -root (( - (q / 2)) - ( sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))))) by A2, A55;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: POLYEQ_1:20

    b <> 0 & ( delta (b,c,d)) > 0 & ( Polynom ( 0 ,b,c,d,x)) = 0 implies x = ((( - c) + ( sqrt ( delta (b,c,d)))) / (2 * b)) or x = ((( - c) - ( sqrt ( delta (b,c,d)))) / (2 * b))

    proof

      assume

       A1: b <> 0 & ( delta (b,c,d)) > 0 ;

      assume ( Polynom ( 0 ,b,c,d,x)) = 0 ;

      then ( Polynom (b,c,d,x)) = 0 ;

      hence thesis by A1, Th5;

    end;

    theorem :: POLYEQ_1:21

    a <> 0 & p = (c / a) & q = (d / a) & ( Polynom (a, 0 ,c,d,x)) = 0 implies for u, v st x = (u + v) & (((3 * v) * u) + p) = 0 holds x = ((3 -root (( - (d / (2 * a))) + ( sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) + (3 -root (( - (d / (2 * a))) - ( sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3)))))) or x = ((3 -root (( - (d / (2 * a))) + ( sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) + (3 -root (( - (d / (2 * a))) + ( sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3)))))) or x = ((3 -root (( - (d / (2 * a))) - ( sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) + (3 -root (( - (d / (2 * a))) - ( sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))))

    proof

      assume that

       A1: a <> 0 and

       A2: p = (c / a) and

       A3: q = (d / a);

      

       A4: (p / 3) = (c / (3 * a)) & ( - (q / 2)) = ( - (d / (2 * a))) by A2, A3, XCMPLX_1: 78;

      assume ( Polynom (a, 0 ,c,d,x)) = 0 ;

      then ((a " ) * (((a * (x |^ 3)) + (c * x)) + d)) = 0 ;

      then ((((a " ) * a) * (x |^ 3)) + ((a " ) * ((c * x) + d))) = 0 ;

      then ((1 * (x |^ 3)) + ((a " ) * ((c * x) + d))) = 0 by A1, XCMPLX_0:def 7;

      then ((x |^ 3) + ((((a " ) * c) * x) + ((a " ) * d))) = 0 ;

      then ((x |^ 3) + (((c / a) * x) + ((a " ) * d))) = 0 by XCMPLX_0:def 9;

      then ((x |^ 3) + (((c / a) * x) + (d / a))) = 0 by XCMPLX_0:def 9;

      then

       A5: ( Polynom (1, 0 ,p,q,x)) = 0 by A2, A3;

      ((q ^2 ) / 4) = (((d ^2 ) / (a ^2 )) / 4) by A3, XCMPLX_1: 76;

      then

       A6: ((q ^2 ) / 4) = ((d ^2 ) / (4 * (a ^2 ))) by XCMPLX_1: 78;

      let u, v;

      assume x = (u + v) & (((3 * v) * u) + p) = 0 ;

      hence thesis by A5, A4, A6, Th19;

    end;

    theorem :: POLYEQ_1:22

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

    proof

      assume

       A1: a <> 0 & ( delta (a,b,c)) >= 0 ;

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

      then (x |^ 3) = ((x |^ (1 + 1)) * x) by NEWTON: 6;

      then

       A2: (x |^ 3) = (((x |^ 1) * x) * x) by NEWTON: 6;

      

       A3: (x |^ 3) = ((x ^2 ) * x) by A2;

      assume ( Polynom (a,b,c, 0 ,x)) = 0 ;

      then ((((a * (x ^2 )) + (b * x)) + c) * x) = 0 by A3;

      then x = 0 or ( Polynom (a,b,c,x)) = 0 by XCMPLX_1: 6;

      hence thesis by A1, Th5;

    end;

    theorem :: POLYEQ_1:23

    a <> 0 & (c / a) < 0 & ( Polynom (a, 0 ,c, 0 ,x)) = 0 implies x = 0 or x = ( sqrt ( - (c / a))) or x = ( - ( sqrt ( - (c / a))))

    proof

      assume that

       A1: a <> 0 and

       A2: (c / a) < 0 ;

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

      then (x |^ 3) = ((x |^ (1 + 1)) * x) by NEWTON: 6;

      then

       A3: (x |^ 3) = (((x |^ 1) * x) * x) by NEWTON: 6;

      

       A4: (x |^ 3) = ((x ^2 ) * x) by A3;

      assume ( Polynom (a, 0 ,c, 0 ,x)) = 0 ;

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

      then

       A5: x = 0 or ((a * (x ^2 )) + c) = 0 by XCMPLX_1: 6;

      now

        per cases by XXREAL_0: 1;

          case

           A6: x > 0 ;

          (x |^ 2) = (x |^ (1 + 1));

          then (x |^ 2) = ((x |^ 1) * x) by NEWTON: 6;

          then (x |^ 2) = ((x to_power 1) * x) by POWER: 41;

          then

           A7: (x |^ 2) = (x * x) by POWER: 25;

          

           A8: ( - (c / a)) > 0 by A2, XREAL_1: 58;

          (x ^2 ) = (( - c) / a) by A1, A5, A6, XCMPLX_1: 89;

          then (x ^2 ) = (( - c) * (a " )) by XCMPLX_0:def 9;

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

          then (x ^2 ) = ( - (c / a)) by XCMPLX_0:def 9;

          then x = (2 -Root ( - (c / a))) by A6, A8, A7, PREPOWER:def 2;

          hence thesis by A8, PREPOWER: 32;

        end;

          case

           A9: x < 0 ;

          (( - x) |^ 2) = (( - x) |^ (1 + 1));

          then (( - x) |^ 2) = ((( - x) |^ 1) * ( - x)) by NEWTON: 6;

          then (( - x) |^ 2) = ((( - x) to_power 1) * ( - x)) by POWER: 41;

          then

           A10: (( - x) |^ 2) = (( - x) * ( - x)) by POWER: 25;

          (x ^2 ) = (( - c) / a) by A1, A5, A9, XCMPLX_1: 89;

          then (x ^2 ) = (( - c) * (a " )) by XCMPLX_0:def 9;

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

          then

           A11: (( - x) ^2 ) = ( - (c / a)) by XCMPLX_0:def 9;

          

           A12: ( - (c / a)) > 0 by A2, XREAL_1: 58;

          ( - x) > 0 by A9, XREAL_1: 58;

          then ( - x) = (2 -Root ( - (c / a))) by A11, A12, A10, PREPOWER:def 2;

          then ( - x) = ( sqrt ( - (c / a))) by A12, PREPOWER: 32;

          hence thesis;

        end;

          case x = 0 ;

          hence thesis;

        end;

      end;

      hence thesis;

    end;