let a, c, x be Real; :: 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: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 ; :: 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 :: thesis: ( ( x > 0 & ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) ) ) or ( x < 0 & ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) ) ) or ( x = 0 & ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) ) ) )
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: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 ;
x ^2 = (- c) / a by ;
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 ;
hence ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) ) by ; :: 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: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 ;
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 ;
- x > 0 by ;
then - x = 2 -Root (- (c / a)) by ;
then - x = sqrt (- (c / a)) by ;
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