let z, a0, a1, a2, a3, a4 be Complex; ( a4 <> 0 implies ( ((((a4 * (z |^ 4)) + (a3 * (z |^ 3))) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ( z = 1_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4)) or z = 2_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4)) or z = 3_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4)) or z = 4_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4)) ) ) )
assume A1:
a4 <> 0
; ( ((((a4 * (z |^ 4)) + (a3 * (z |^ 3))) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ( z = 1_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4)) or z = 2_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4)) or z = 3_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4)) or z = 4_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4)) ) )
set s4 = 4_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4));
set s3 = 3_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4));
set s2 = 2_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4));
set s1 = 1_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4));
- (a3 / a4) = (((1_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4))) + (2_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4)))) + (3_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4)))) + (4_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4)))
by Th26;
then A2:
a3 / a4 = - ((((1_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4))) + (2_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4)))) + (3_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4)))) + (4_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4))))
;
- (a1 / a4) = (((((1_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4))) * (2_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4)))) * (3_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4)))) + (((1_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4))) * (2_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4)))) * (4_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4))))) + (((1_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4))) * (3_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4)))) * (4_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4))))) + (((2_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4))) * (3_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4)))) * (4_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4))))
by Th28;
then A3:
a1 / a4 = - ((((((1_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4))) * (2_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4)))) * (3_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4)))) + (((1_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4))) * (2_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4)))) * (4_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4))))) + (((1_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4))) * (3_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4)))) * (4_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4))))) + (((2_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4))) * (3_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4)))) * (4_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4)))))
;
(((((z |^ 4) + ((a3 / a4) * (z |^ 3))) + ((a2 / a4) * (z |^ 2))) + ((a1 / a4) * z)) + (a0 / a4)) * a4 =
((((a4 * (z |^ 4)) + (((a3 / a4) * a4) * (z |^ 3))) + (((a2 / a4) * a4) * (z |^ 2))) + (((a1 / a4) * a4) * z)) + ((a0 / a4) * a4)
.=
((((a4 * (z |^ 4)) + (((a3 / a4) * a4) * (z |^ 3))) + (((a2 / a4) * a4) * (z |^ 2))) + (((a1 / a4) * a4) * z)) + a0
by A1, XCMPLX_1:87
.=
((((a4 * (z |^ 4)) + (((a3 / a4) * a4) * (z |^ 3))) + (((a2 / a4) * a4) * (z |^ 2))) + (a1 * z)) + a0
by A1, XCMPLX_1:87
.=
((((a4 * (z |^ 4)) + (((a3 / a4) * a4) * (z |^ 3))) + (a2 * (z |^ 2))) + (a1 * z)) + a0
by A1, XCMPLX_1:87
.=
((((a4 * (z |^ 4)) + (a3 * (z |^ 3))) + (a2 * (z |^ 2))) + (a1 * z)) + a0
by A1, XCMPLX_1:87
;
then A4:
( ((((z |^ 4) + ((a3 / a4) * (z |^ 3))) + ((a2 / a4) * (z |^ 2))) + ((a1 / a4) * z)) + (a0 / a4) = 0 iff ((((a4 * (z |^ 4)) + (a3 * (z |^ 3))) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 )
by A1;
( a2 / a4 = ((((((1_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4))) * (2_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4)))) + ((1_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4))) * (3_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4))))) + ((1_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4))) * (4_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4))))) + ((2_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4))) * (3_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4))))) + ((2_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4))) * (4_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4))))) + ((3_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4))) * (4_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4)))) & a0 / a4 = (((1_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4))) * (2_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4)))) * (3_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4)))) * (4_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4))) )
by Th27, Th29;
hence
( ((((a4 * (z |^ 4)) + (a3 * (z |^ 3))) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ( z = 1_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4)) or z = 2_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4)) or z = 3_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4)) or z = 4_root_of_quartic ((a0 / a4),(a1 / a4),(a2 / a4),(a3 / a4)) ) )
by A4, A2, A3, Th22; verum