let z, a2, a1, a0, a3, a4 be complex number ; :: thesis: ( 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 ; :: thesis: ( ((((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 s1 = 1_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 s3 = 3_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);
(((((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 A2: ( ((((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;
( - (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 Th27, Th29;
then ( 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))) & 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))) & 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)))) & 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 Th28, Th30;
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 A2, Th23; :: thesis: verum