theorem
for
z,
a0,
a1,
a2,
a3 being
Complex st
a3 <> 0 holds
(
(((a3 * (z |^ 3)) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff (
z = 1_root_of_cubic (
(a0 / a3),
(a1 / a3),
(a2 / a3)) or
z = 2_root_of_cubic (
(a0 / a3),
(a1 / a3),
(a2 / a3)) or
z = 3_root_of_cubic (
(a0 / a3),
(a1 / a3),
(a2 / a3)) ) )