let z, a2, a1, a0, a3 be complex number ; ( 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:88
.=
(((a3 * (z |^ 3)) + (((a2 / a3) * a3) * (z |^ 2))) + (a1 * z)) + a0
by A1, XCMPLX_1:88
.=
(((a3 * (z |^ 3)) + (a2 * (z |^ 2))) + (a1 * z)) + a0
by A1, XCMPLX_1:88
;
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