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