let a, c, d be Real; :: thesis: for z being Element of COMPLEX st a <> 0 & Im z <> 0 & Polynom a,0 ,c,d,z = 0 holds
for u, v being Real st Re z = u + v & ((3 * v) * u) + (c / (4 * a)) = 0 & c / a >= 0 & not z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) & not z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) & not z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) & not z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) & not z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) holds
z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> )
let z be Element of COMPLEX ; :: thesis: ( a <> 0 & Im z <> 0 & Polynom a,0 ,c,d,z = 0 implies for u, v being Real st Re z = u + v & ((3 * v) * u) + (c / (4 * a)) = 0 & c / a >= 0 & not z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) & not z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) & not z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) & not z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) & not z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) holds
z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) )
assume A1:
a <> 0
; :: thesis: ( not Im z <> 0 or not Polynom a,0 ,c,d,z = 0 or for u, v being Real st Re z = u + v & ((3 * v) * u) + (c / (4 * a)) = 0 & c / a >= 0 & not z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) & not z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) & not z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) & not z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) & not z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) holds
z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) )
assume A2:
( Im z <> 0 & Polynom a,0 ,c,d,z = 0 )
; :: thesis: for u, v being Real st Re z = u + v & ((3 * v) * u) + (c / (4 * a)) = 0 & c / a >= 0 & not z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) & not z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) & not z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) & not z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) & not z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) holds
z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> )
let u, v be Real; :: thesis: ( Re z = u + v & ((3 * v) * u) + (c / (4 * a)) = 0 & c / a >= 0 & not z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) & not z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) & not z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) & not z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) & not z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) implies z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) )
assume A3:
( Re z = u + v & ((3 * v) * u) + (c / (4 * a)) = 0 & c / a >= 0 )
; :: thesis: ( z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) or z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) or z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) or z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) or z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) or z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) )
set x = Re z;
set y = Im z;
A5:
a = a + (0 * <i> )
;
A7:
z = (Re z) + ((Im z) * <i> )
by COMPLEX1:29;
A8: 0 =
(((a * ((Re (z ^3 )) + ((Im (z ^3 )) * <i> ))) + (0 * (z ^2 ))) + (c * z)) + d
by A2, COMPLEX1:29
.=
((a * ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) + ((Im (z ^3 )) * <i> ))) + (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> ))) + (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> ))) + (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> )) + (c * ((Re z) + ((Im z) * <i> )))) + d
by COMPLEX1:def 10
.=
(((((Re a) * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 )))) - ((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> )) + (c * ((Re z) + ((Im z) * <i> )))) + d
by COMPLEX1:28
.=
(((((Re a) * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 )))) - ((Im a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z))))) + ((((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> )) + (c * ((Re z) + ((Im z) * <i> )))) + d
by COMPLEX1:28
.=
(((((Re a) * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 )))) - ((Im a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z))))) + ((((Re a) * (Im ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z))) * <i> )))) + ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) * (Im a))) * <i> )) + (c * ((Re z) + ((Im z) * <i> )))) + d
by COMPLEX1:28
.=
(((((Re a) * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 )))) - ((Im a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z))))) + ((((Re a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z)))) + ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) * (Im a))) * <i> )) + (c * ((Re z) + ((Im z) * <i> )))) + d
by COMPLEX1:28
.=
((((a * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 )))) - ((Im a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z))))) + ((((Re a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z)))) + ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) * (Im a))) * <i> )) + (c * ((Re z) + ((Im z) * <i> )))) + d
by A5, COMPLEX1:28
.=
((((a * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 )))) - (0 * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z))))) + ((((Re a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z)))) + ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) * (Im a))) * <i> )) + (c * ((Re z) + ((Im z) * <i> )))) + d
by A5, COMPLEX1:28
.=
((((a * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 )))) - 0 ) + (((a * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z)))) + ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) * (Im a))) * <i> )) + (c * ((Re z) + ((Im z) * <i> )))) + d
by A5, COMPLEX1:28
.=
((((a * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 )))) - 0 ) + (((a * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z)))) + ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) * 0 )) * <i> )) + (c * ((Re z) + ((Im z) * <i> )))) + d
by A5, COMPLEX1:28
.=
(((a * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 )))) + (c * (Re z))) + d) + ((((a * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z)))) + (c * (Im z))) + 0 ) * <i> )
;
then A9:
((a * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z)))) + (c * (Im z))) + 0 = 0
by COMPLEX1:12, COMPLEX1:28;
(a * ((- ((Im z) |^ (2 + 1))) + ((3 * ((Re z) ^2 )) * (Im z)))) + (c * (Im z)) = 0
by A8, COMPLEX1:12, COMPLEX1:28;
then
(a * ((- (((Im z) |^ 2) * (Im z))) + ((3 * ((Re z) ^2 )) * (Im z)))) + (c * (Im z)) = 0
by NEWTON:11;
then
(((a * ((- ((Im z) |^ 2)) + (3 * ((Re z) ^2 )))) + c) + 0 ) * (Im z) = 0
;
then
(a * ((Im z) |^ 2)) + ((- (a * ((Im z) |^ 2))) + ((a * (3 * ((Re z) ^2 ))) + c)) = (a * ((Im z) |^ 2)) + 0
by A2, XCMPLX_1:6;
then
(Im z) |^ (1 + 1) = ((a * (3 * ((Re z) ^2 ))) + c) / a
by A1, XCMPLX_1:90;
then
((Im z) |^ 1) * (Im z) = ((a * (3 * ((Re z) ^2 ))) + c) / a
by NEWTON:11;
then A10:
(Im z) ^2 = ((((3 * ((Re z) ^2 )) * a) / a) + (c / a)) + (0 / a)
by NEWTON:10;
then A11:
(Im z) ^2 = ((3 * ((Re z) ^2 )) + (c / a)) + (0 * (a " ))
by A1, XCMPLX_1:90;
((a * ((((Re z) |^ 3) - ((3 * (Re z)) * ((3 * ((Re z) ^2 )) + (c / a)))) + 0 )) + (c * (Re z))) + d = 0
by A1, A8, A9, A10, XCMPLX_1:90;
then 0 =
(((a * ((Re z) |^ 3)) - (a * ((9 * ((Re z) * ((Re z) ^2 ))) + ((3 * (Re z)) * (c / a))))) + (c * (Re z))) + d
.=
(((a * ((Re z) |^ 3)) - (a * ((9 * ((((Re z) |^ 1) * (Re z)) * (Re z))) + ((3 * (Re z)) * (c / a))))) + (c * (Re z))) + d
by NEWTON:10
.=
(((a * ((Re z) |^ 3)) - (a * ((9 * (((Re z) |^ (1 + 1)) * (Re z))) + ((3 * (Re z)) * (c / a))))) + (c * (Re z))) + d
by NEWTON:11
.=
(((a * ((Re z) |^ 3)) - (a * (((9 * ((Re z) |^ (2 + 1))) + ((3 * (Re z)) * (c / a))) + 0 ))) + (c * (Re z))) + d
by NEWTON:11
.=
(((a * ((Re z) |^ 3)) - ((a * (9 * ((Re z) |^ 3))) + ((3 * (Re z)) * (c * (a / a))))) + (c * (Re z))) + d
.=
(((a * ((Re z) |^ 3)) - ((a * (9 * ((Re z) |^ 3))) + ((3 * (Re z)) * c))) + (c * (Re z))) + d
by A1, XCMPLX_1:89
.=
(((- (8 * a)) * ((Re z) |^ 3)) + ((- (2 * c)) * (Re z))) + d
;
then
(- 1) * 0 = (((8 * a) * ((Re z) |^ 3)) + ((2 * c) * (Re z))) + (- d)
;
then A12:
0 = ((((Re z) |^ 3) * ((8 * a) / (8 * a))) + (((8 * a) " ) * ((2 * c) * (Re z)))) + (((8 * a) " ) * (- d))
;
0 = (((1 * ((Re z) |^ 3)) + (0 * ((Re z) ^2 ))) + (((2 * c) / (8 * a)) * (Re z))) + (((8 * a) " ) * (- d))
by A12, XCMPLX_1:89, A1;
then
0 = (((1 * ((Re z) |^ 3)) + (0 * ((Re z) ^2 ))) + ((((2 / 8) * c) / a) * (Re z))) + ((- d) / (8 * a))
by XCMPLX_1:84;
then
0 = (((1 * ((Re z) |^ 3)) + (0 * ((Re z) ^2 ))) + (((1 / a) * (c / 4)) * (Re z))) + ((- d) / (8 * a))
;
then A13:
Polynom 1,0 ,(c / (4 * a)),(- (d / (8 * a))),(Re z) = 0
by XCMPLX_1:104;
set pp = c / (4 * a);
set q = - (d / (8 * a));
- ((- (d / (8 * a))) / 2) = (1 / 2) * (d / (8 * a))
;
then A14:
- ((- (d / (8 * a))) / 2) = d / ((a * 8) * 2)
by XCMPLX_1:104;
A15:
((- (d / (8 * a))) ^2 ) / 4 = ((1 / 2) * (d / (8 * a))) ^2
;
A16:
( Re z = (3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2 ) / 4) + (((c / (4 * a)) / 3) |^ 3))))) + (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2 ) / 4) + (((c / (4 * a)) / 3) |^ 3))))) or Re z = (3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2 ) / 4) + (((c / (4 * a)) / 3) |^ 3))))) + (3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2 ) / 4) + (((c / (4 * a)) / 3) |^ 3))))) or Re z = (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2 ) / 4) + (((c / (4 * a)) / 3) |^ 3))))) + (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2 ) / 4) + (((c / (4 * a)) / 3) |^ 3))))) )
by A3, A13, POLYEQ_1:19;
set m = 3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2 ) / 4) + (((c / (4 * a)) / 3) |^ 3))));
set n = 3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2 ) / 4) + (((c / (4 * a)) / 3) |^ 3))));
A17:
( z = ((3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2 ) / 4) + (((c / (4 * a)) / 3) |^ 3))))) + (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2 ) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) + ((sqrt ((3 * (((3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2 ) / 4) + (((c / (4 * a)) / 3) |^ 3))))) + (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2 ) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) ^2 )) + (c / a))) * <i> ) or z = ((3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2 ) / 4) + (((c / (4 * a)) / 3) |^ 3))))) + (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2 ) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) - ((sqrt ((3 * (((3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2 ) / 4) + (((c / (4 * a)) / 3) |^ 3))))) + (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2 ) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) ^2 )) + (c / a))) * <i> ) or z = (2 * (3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2 ) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2 ) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) ^2 )) + (c / a))) * <i> ) or z = (2 * (3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2 ) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2 ) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) ^2 )) + (c / a))) * <i> ) or z = (2 * (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2 ) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2 ) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) ^2 )) + (c / a))) * <i> ) or z = (2 * (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2 ) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2 ) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) ^2 )) + (c / a))) * <i> ) )
(c / (4 * a)) / 3 =
(1 / 3) * (c / (4 * a))
.=
c / ((a * 4) * 3)
by XCMPLX_1:104
.=
c / (a * (4 * 3))
;
hence
( z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) or z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) or z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) or z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) or z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) or z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2 ) + ((c / (12 * a)) |^ 3)))))) ^2 )) + (c / a))) * <i> ) )
by A14, A15, A17; :: thesis: verum