let a, c, x be real number ; :: thesis: ( a <> 0 & c / a < 0 & Polynom a,0 ,c,0 ,x = 0 & not x = 0 & not x = sqrt (- (c / a)) implies x = - (sqrt (- (c / a))) )
assume that
A1: a <> 0 and
A2: c / a < 0 ; :: thesis: ( not Polynom a,0 ,c,0 ,x = 0 or x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) )
x |^ 3 = x |^ (2 + 1) ;
then x |^ 3 = (x |^ (1 + 1)) * x by NEWTON:11;
then A3: x |^ 3 = ((x |^ 1) * x) * x by NEWTON:11;
x |^ 1 = x to_power 1 by POWER:46;
then A4: x |^ 3 = (x ^2 ) * x by A3, POWER:30;
assume Polynom a,0 ,c,0 ,x = 0 ; :: thesis: ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) )
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 ( x > 0 or x < 0 or x = 0 ) by XXREAL_0:1;

case A6: x > 0 ; :: thesis: ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) )

x |^ 2 = x |^ (1 + 1) ;
then x |^ 2 = (x |^ 1) * x by NEWTON:11;
then x |^ 2 = (x to_power 1) * x by POWER:46;
then A7: x |^ 2 = x * x by POWER:30;
A8: - (c / a) > 0 by A2, XREAL_1:60;
x ^2 = (- c) / a by A1, A5, A6, XCMPLX_1:90;
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 3;
hence ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) ) by A8, PREPOWER:41; :: thesis: verum

end;

case A9: x < 0 ; :: thesis: ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) )

(- x) |^ 2 = (- x) |^ (1 + 1) ;
then (- x) |^ 2 = ((- x) |^ 1) * (- x) by NEWTON:11;
then (- x) |^ 2 = ((- x) to_power 1) * (- x) by POWER:46;
then A10: (- x) |^ 2 = (- x) * (- x) by POWER:30;
x ^2 = (- c) / a by A1, A5, A9, XCMPLX_1:90;
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:60;
- x > 0 by A9, XREAL_1:60;
then - x = 2 -Root (- (c / a)) by A11, A12, A10, PREPOWER:def 3;
then - x = sqrt (- (c / a)) by A12, PREPOWER:41;
hence ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) ) ; :: thesis: verum

end;

case x = 0 ; :: thesis: ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) )

hence ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) ) ; :: thesis: verum

end;

end;

end;

hence ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) ) ; :: thesis: verum