let a, b, c, d be Real; for z being Element of COMPLEX st a <> 0 & Polynom a,b,c,d,z = 0 & Im z = 0 holds
for u, v, x1 being Real st x1 = (Re z) + (b / (3 * a)) & Re z = (u + v) - (b / (3 * a)) & ((3 * u) * v) + ((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) = 0 & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) holds
z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> )
let z be Element of COMPLEX ; ( a <> 0 & Polynom a,b,c,d,z = 0 & Im z = 0 implies for u, v, x1 being Real st x1 = (Re z) + (b / (3 * a)) & Re z = (u + v) - (b / (3 * a)) & ((3 * u) * v) + ((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) = 0 & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) holds
z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) )
assume A1:
a <> 0
; ( not Polynom a,b,c,d,z = 0 or not Im z = 0 or for u, v, x1 being Real st x1 = (Re z) + (b / (3 * a)) & Re z = (u + v) - (b / (3 * a)) & ((3 * u) * v) + ((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) = 0 & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) holds
z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) )
set p = (((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ));
set b9 = c / a;
A2:
a = a + (0 * <i> )
;
set q = (2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )));
set c9 = d / a;
set a9 = b / a;
set y = Im z;
set x = Re z;
assume that
A3:
Polynom a,b,c,d,z = 0
and
A4:
Im z = 0
; for u, v, x1 being Real st x1 = (Re z) + (b / (3 * a)) & Re z = (u + v) - (b / (3 * a)) & ((3 * u) * v) + ((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) = 0 & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) holds
z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> )
A5:
z = (Re z) + ((Im z) * <i> )
by COMPLEX1:29;
0 =
(((a * ((Re (z ^3 )) + ((Im (z ^3 )) * <i> ))) + (b * (z ^2 ))) + (c * z)) + d
by A3, COMPLEX1:29
.=
(((a * ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) + ((Im (z ^3 )) * <i> ))) + (b * (z ^2 ))) + (c * z)) + d
by Th11
.=
(((a * ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z))) * <i> ))) + (b * (z ^2 ))) + (c * z)) + d
by Th11
.=
((((a + (0 * <i> )) * ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z))) * <i> ))) + (b * (z ^2 ))) + (c * ((Re z) + ((Im z) * <i> )))) + d
by COMPLEX1:29
.=
((((((Re a) * (Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z))) * <i> )))) - ((Im a) * (Im ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z))) * <i> ))))) + ((((Re a) * (Im ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z))) * <i> )))) + ((Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z))) * <i> ))) * (Im a))) * <i> )) + (b * (z ^2 ))) + (c * ((Re z) + ((Im z) * <i> )))) + d
by COMPLEX1:def 10
.=
((((((Re a) * (Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z))) * <i> )))) - (0 * (Im ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z))) * <i> ))))) + ((((Re a) * (Im ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z))) * <i> )))) + ((Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z))) * <i> ))) * (Im a))) * <i> )) + (b * (z ^2 ))) + (c * ((Re z) + ((Im z) * <i> )))) + d
by A2, COMPLEX1:28
.=
((((((Re a) * (Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z))) * <i> )))) - 0 ) + ((((Re a) * (Im ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z))) * <i> )))) + ((Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z))) * <i> ))) * 0 )) * <i> )) + (b * (z ^2 ))) + (c * ((Re z) + ((Im z) * <i> )))) + d
by A2, COMPLEX1:28
.=
((((((Re a) * (Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z))) * <i> )))) - 0 ) + ((((Re a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z)))) + 0 ) * <i> )) + (b * (z ^2 ))) + (c * ((Re z) + ((Im z) * <i> )))) + d
by COMPLEX1:28
.=
((((((Re a) * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 )))) - 0 ) + (((Re a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z)))) * <i> )) + (b * (z ^2 ))) + (c * ((Re z) + ((Im z) * <i> )))) + d
by COMPLEX1:28
.=
(((((a * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 )))) - 0 ) + (((Re a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z)))) * <i> )) + (b * (z ^2 ))) + (c * ((Re z) + ((Im z) * <i> )))) + d
by A2, COMPLEX1:28
.=
((((a * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 )))) + ((a * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z)))) * <i> )) + (b * ((((Re z) ^2 ) - ((Im z) ^2 )) + (((2 * (Re z)) * (Im z)) * <i> )))) + ((c * (Re z)) + ((c * (Im z)) * <i> ))) + d
by A2, A5, COMPLEX1:28
;
then 0 =
((((a * (((Re z) |^ 3) - ((3 * (Re z)) * 0 ))) + (b * (((Re z) ^2 ) - 0 ))) + (c * (Re z))) + d) + ((((a * ((- (0 |^ 3)) + 0 )) + (b * 0 )) + 0 ) * <i> )
by A4
.=
((((a * ((Re z) |^ 3)) + (b * ((Re z) ^2 ))) + (c * (Re z))) + d) + (((a * 0 ) + 0 ) * <i> )
by NEWTON:16
;
then A6:
Polynom a,b,c,d,(Re z) = 0
;
A7:
d / a = d / a
;
((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) / 3 = (1 / 3) * ((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 )))
;
then A8:
((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) / 3 = (((3 * a) * c) - (b ^2 )) / (((a ^2 ) * 3) * 3)
by XCMPLX_1:104;
A9: - (((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) / 2) =
- (((b / (3 * a)) |^ 3) + ((1 / 2) * ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))))
.=
- (((b / (3 * a)) |^ 3) + ((((3 * a) * d) - (b * c)) / (((a ^2 ) * 3) * 2)))
by XCMPLX_1:104
.=
(- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))
;
let u, v, x1 be Real; ( x1 = (Re z) + (b / (3 * a)) & Re z = (u + v) - (b / (3 * a)) & ((3 * u) * v) + ((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) = 0 & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) implies z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) )
assume that
A10:
( x1 = (Re z) + (b / (3 * a)) & Re z = (u + v) - (b / (3 * a)) )
and
A11:
((3 * u) * v) + ((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) = 0
; ( z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) or z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) or z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) )
( b / a = b / a & c / a = c / a )
;
then
Polynom 1,0 ,((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))),((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))),x1 = 0
by A1, A10, A6, A7, POLYEQ_1:16;
then
( x1 = (3 -root ((- (((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) / 2)) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + ((((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) / 3) |^ 3))))) + (3 -root ((- (((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) / 2)) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + ((((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) / 3) |^ 3))))) or x1 = (3 -root ((- (((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) / 2)) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + ((((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) / 3) |^ 3))))) + (3 -root ((- (((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) / 2)) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + ((((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) / 3) |^ 3))))) or x1 = (3 -root ((- (((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) / 2)) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + ((((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) / 3) |^ 3))))) + (3 -root ((- (((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) / 2)) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + ((((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) / 3) |^ 3))))) )
by A10, A11, POLYEQ_1:19;
hence
( z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) or z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) or z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) )
by A4, A10, A8, A9, COMPLEX1:29; verum
set h = - (b / (3 * a));