let z, a0, a1, a2, a3 be Complex; ( a3 <> 0 implies ( (((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)) ) ) )
assume A1:
a3 <> 0
; ( (((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)) ) )
set s3 = 3_root_of_cubic ((a0 / a3),(a1 / a3),(a2 / a3));
set s2 = 2_root_of_cubic ((a0 / a3),(a1 / a3),(a2 / a3));
set s1 = 1_root_of_cubic ((a0 / a3),(a1 / a3),(a2 / a3));
- (a2 / a3) = ((1_root_of_cubic ((a0 / a3),(a1 / a3),(a2 / a3))) + (2_root_of_cubic ((a0 / a3),(a1 / a3),(a2 / a3)))) + (3_root_of_cubic ((a0 / a3),(a1 / a3),(a2 / a3)))
by Th17;
then A2:
a2 / a3 = - (((1_root_of_cubic ((a0 / a3),(a1 / a3),(a2 / a3))) + (2_root_of_cubic ((a0 / a3),(a1 / a3),(a2 / a3)))) + (3_root_of_cubic ((a0 / a3),(a1 / a3),(a2 / a3))))
;
- (a0 / a3) = ((1_root_of_cubic ((a0 / a3),(a1 / a3),(a2 / a3))) * (2_root_of_cubic ((a0 / a3),(a1 / a3),(a2 / a3)))) * (3_root_of_cubic ((a0 / a3),(a1 / a3),(a2 / a3)))
by Th19;
then A3:
a0 / a3 = - (((1_root_of_cubic ((a0 / a3),(a1 / a3),(a2 / a3))) * (2_root_of_cubic ((a0 / a3),(a1 / a3),(a2 / a3)))) * (3_root_of_cubic ((a0 / a3),(a1 / a3),(a2 / a3))))
;
((((z |^ 3) + ((a2 / a3) * (z |^ 2))) + ((a1 / a3) * z)) + (a0 / a3)) * a3 =
(((a3 * (z |^ 3)) + (((a2 / a3) * a3) * (z |^ 2))) + (((a1 / a3) * a3) * z)) + ((a0 / a3) * a3)
.=
(((a3 * (z |^ 3)) + (((a2 / a3) * a3) * (z |^ 2))) + (((a1 / a3) * a3) * z)) + a0
by A1, XCMPLX_1:87
.=
(((a3 * (z |^ 3)) + (((a2 / a3) * a3) * (z |^ 2))) + (a1 * z)) + a0
by A1, XCMPLX_1:87
.=
(((a3 * (z |^ 3)) + (a2 * (z |^ 2))) + (a1 * z)) + a0
by A1, XCMPLX_1:87
;
then A4:
( (((z |^ 3) + ((a2 / a3) * (z |^ 2))) + ((a1 / a3) * z)) + (a0 / a3) = 0 iff (((a3 * (z |^ 3)) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 )
by A1;
a1 / a3 = (((1_root_of_cubic ((a0 / a3),(a1 / a3),(a2 / a3))) * (2_root_of_cubic ((a0 / a3),(a1 / a3),(a2 / a3)))) + ((1_root_of_cubic ((a0 / a3),(a1 / a3),(a2 / a3))) * (3_root_of_cubic ((a0 / a3),(a1 / a3),(a2 / a3))))) + ((2_root_of_cubic ((a0 / a3),(a1 / a3),(a2 / a3))) * (3_root_of_cubic ((a0 / a3),(a1 / a3),(a2 / a3))))
by Th18;
hence
( (((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)) ) )
by A4, A2, A3, Th14; verum