:: Solution of Cubic and Quartic Equations :: by Marco Riccardi :: :: Received March 3, 2009 :: Copyright (c) 2009-2012 Association of Mizar Users begin theorem Th1: :: POLYEQ_5:1 for a being complex number holds a * a = a |^ 2 proofend; theorem Th2: :: POLYEQ_5:2 for a being complex number holds (a * a) * a = a |^ 3 proofend; theorem Th3: :: POLYEQ_5:3 for a being complex number holds ((a * a) * a) * a = a |^ 4 proofend; theorem Th4: :: POLYEQ_5:4 for a, b being complex number holds (a - b) |^ 2 = ((a |^ 2) - ((2 * a) * b)) + (b |^ 2) proofend; :: like SERIES_4:5 theorem Th5: :: POLYEQ_5:5 for a, b being complex number holds (a - b) |^ 3 = (((a |^ 3) - ((3 * (a |^ 2)) * b)) + ((3 * (b |^ 2)) * a)) - (b |^ 3) proofend; theorem Th6: :: POLYEQ_5:6 for a, b being complex number holds (a - b) |^ 4 = ((((a |^ 4) - ((4 * (a |^ 3)) * b)) + ((6 * (a |^ 2)) * (b |^ 2))) - ((4 * (b |^ 3)) * a)) + (b |^ 4) proofend; notation let n be Nat; let r be real number ; synonym n -real-root r for n -root r; end; :: principal root definition let n be non zero Nat; let z be complex number ; funcn -root z -> complex number equals :: POLYEQ_5:def 1 (n -real-root |.z.|) * ((cos ((Arg z) / n)) + ((sin ((Arg z) / n)) * )); correctness coherence (n -real-root |.z.|) * ((cos ((Arg z) / n)) + ((sin ((Arg z) / n)) * )) is complex number ; ; end; :: deftheorem defines -root POLYEQ_5:def_1_:_ for n being non zero Nat for z being complex number holds n -root z = (n -real-root |.z.|) * ((cos ((Arg z) / n)) + ((sin ((Arg z) / n)) * )); theorem Th7: :: POLYEQ_5:7 for z being complex number for n0 being non zero Nat holds (n0 -root z) |^ n0 = z proofend; theorem Th8: :: POLYEQ_5:8 for n0 being non zero Nat for r being real number st r >= 0 holds n0 -root r = n0 -real-root r proofend; theorem Th9: :: POLYEQ_5:9 for z being complex number for n0 being non zero Nat for r being real number st r > 0 holds n0 -root (z / r) = (n0 -root z) / (n0 -root r) proofend; theorem Th10: :: POLYEQ_5:10 for a, z being complex number holds ( z |^ 2 = a iff ( z = 2 -root a or z = - (2 -root a) ) ) proofend; begin theorem Th11: :: POLYEQ_5:11 for z, a1, s1, s2, a0 being complex number st a1 = - (s1 + s2) & a0 = s1 * s2 holds ( ((z |^ 2) + (a1 * z)) + a0 = 0 iff ( z = s1 or z = s2 ) ) proofend; theorem Th12: :: POLYEQ_5:12 for z, a2, a1, a0 being complex number st a2 <> 0 holds ( ((a2 * (z |^ 2)) + (a1 * z)) + a0 = 0 iff ( z = (- (a1 / (2 * a2))) + ((2 -root (delta (a0,a1,a2))) / (2 * a2)) or z = (- (a1 / (2 * a2))) - ((2 -root (delta (a0,a1,a2))) / (2 * a2)) ) ) proofend; begin theorem Th13: :: POLYEQ_5:13 for z, a2, a1, a0, x, q, r being complex number st z = x - (a2 / 3) & q = ((3 * a1) - (a2 |^ 2)) / 9 & r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 holds ( (((z |^ 3) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ((x |^ 3) + ((3 * q) * x)) - (2 * r) = 0 ) proofend; theorem Th14: :: POLYEQ_5:14 for z, a2, s1, s2, a1, a0, s3 being complex number st a2 = - ((s1 + s2) + s3) & a1 = ((s1 * s2) + (s1 * s3)) + (s2 * s3) & a0 = - ((s1 * s2) * s3) holds ( (((z |^ 3) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ( z = s1 or z = s2 or z = s3 ) ) proofend; :: Cardan's Solution :: Mathematical Handbook for Scientists and Engineers (Korn) p.23 :: roots of cubic (I) theorem :: POLYEQ_5:15 for z, a1, a2, a0, s1, s2, q, r, s being complex number st q = ((3 * a1) - (a2 |^ 2)) / 9 & q <> 0 & r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s = 2 -root ((q |^ 3) + (r |^ 2)) & s1 = 3 -root (r + s) & s2 = - (q / s1) holds ( (((z |^ 3) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ( z = (s1 + s2) - (a2 / 3) or z = ((- ((s1 + s2) / 2)) - (a2 / 3)) + ((((s1 - s2) * (2 -root 3)) * ) / 2) or z = ((- ((s1 + s2) / 2)) - (a2 / 3)) - ((((s1 - s2) * (2 -root 3)) * ) / 2) ) ) proofend; :: roots of cubic (II) theorem :: POLYEQ_5:16 for z, a1, a2, a0, s1, q, r being complex number st q = ((3 * a1) - (a2 |^ 2)) / 9 & q = 0 & r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s1 = 3 -root (2 * r) holds ( (((z |^ 3) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ( z = s1 - (a2 / 3) or z = ((- (s1 / 2)) - (a2 / 3)) + (((s1 * (2 -root 3)) * ) / 2) or z = ((- (s1 / 2)) - (a2 / 3)) - (((s1 * (2 -root 3)) * ) / 2) ) ) proofend; definition let a0, a1, a2 be complex number ; func 1_root_of_cubic (a0,a1,a2) -> complex number means :Def2: :: POLYEQ_5:def 2 ex r, s1 being complex number st ( r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s1 = 3 -root (2 * r) & it = s1 - (a2 / 3) ) if (3 * a1) - (a2 |^ 2) = 0 otherwise ex q, r, s, s1, s2 being complex number st ( q = ((3 * a1) - (a2 |^ 2)) / 9 & r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s = 2 -root ((q |^ 3) + (r |^ 2)) & s1 = 3 -root (r + s) & s2 = - (q / s1) & it = (s1 + s2) - (a2 / 3) ); existence ( ( (3 * a1) - (a2 |^ 2) = 0 implies ex b1, r, s1 being complex number st ( r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s1 = 3 -root (2 * r) & b1 = s1 - (a2 / 3) ) ) & ( not (3 * a1) - (a2 |^ 2) = 0 implies ex b1, q, r, s, s1, s2 being complex number st ( q = ((3 * a1) - (a2 |^ 2)) / 9 & r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s = 2 -root ((q |^ 3) + (r |^ 2)) & s1 = 3 -root (r + s) & s2 = - (q / s1) & b1 = (s1 + s2) - (a2 / 3) ) ) ) proofend; uniqueness for b1, b2 being complex number holds ( ( (3 * a1) - (a2 |^ 2) = 0 & ex r, s1 being complex number st ( r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s1 = 3 -root (2 * r) & b1 = s1 - (a2 / 3) ) & ex r, s1 being complex number st ( r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s1 = 3 -root (2 * r) & b2 = s1 - (a2 / 3) ) implies b1 = b2 ) & ( not (3 * a1) - (a2 |^ 2) = 0 & ex q, r, s, s1, s2 being complex number st ( q = ((3 * a1) - (a2 |^ 2)) / 9 & r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s = 2 -root ((q |^ 3) + (r |^ 2)) & s1 = 3 -root (r + s) & s2 = - (q / s1) & b1 = (s1 + s2) - (a2 / 3) ) & ex q, r, s, s1, s2 being complex number st ( q = ((3 * a1) - (a2 |^ 2)) / 9 & r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s = 2 -root ((q |^ 3) + (r |^ 2)) & s1 = 3 -root (r + s) & s2 = - (q / s1) & b2 = (s1 + s2) - (a2 / 3) ) implies b1 = b2 ) ) ; correctness consistency for b1 being complex number holds verum; ; func 2_root_of_cubic (a0,a1,a2) -> complex number means :Def3: :: POLYEQ_5:def 3 ex r, s1 being complex number st ( r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s1 = 3 -root (2 * r) & it = ((- (s1 / 2)) - (a2 / 3)) + (((s1 * (2 -root 3)) * ) / 2) ) if (3 * a1) - (a2 |^ 2) = 0 otherwise ex q, r, s, s1, s2 being complex number st ( q = ((3 * a1) - (a2 |^ 2)) / 9 & r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s = 2 -root ((q |^ 3) + (r |^ 2)) & s1 = 3 -root (r + s) & s2 = - (q / s1) & it = ((- ((s1 + s2) / 2)) - (a2 / 3)) + ((((s1 - s2) * (2 -root 3)) * ) / 2) ); existence ( ( (3 * a1) - (a2 |^ 2) = 0 implies ex b1, r, s1 being complex number st ( r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s1 = 3 -root (2 * r) & b1 = ((- (s1 / 2)) - (a2 / 3)) + (((s1 * (2 -root 3)) * ) / 2) ) ) & ( not (3 * a1) - (a2 |^ 2) = 0 implies ex b1, q, r, s, s1, s2 being complex number st ( q = ((3 * a1) - (a2 |^ 2)) / 9 & r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s = 2 -root ((q |^ 3) + (r |^ 2)) & s1 = 3 -root (r + s) & s2 = - (q / s1) & b1 = ((- ((s1 + s2) / 2)) - (a2 / 3)) + ((((s1 - s2) * (2 -root 3)) * ) / 2) ) ) ) proofend; uniqueness for b1, b2 being complex number holds ( ( (3 * a1) - (a2 |^ 2) = 0 & ex r, s1 being complex number st ( r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s1 = 3 -root (2 * r) & b1 = ((- (s1 / 2)) - (a2 / 3)) + (((s1 * (2 -root 3)) * ) / 2) ) & ex r, s1 being complex number st ( r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s1 = 3 -root (2 * r) & b2 = ((- (s1 / 2)) - (a2 / 3)) + (((s1 * (2 -root 3)) * ) / 2) ) implies b1 = b2 ) & ( not (3 * a1) - (a2 |^ 2) = 0 & ex q, r, s, s1, s2 being complex number st ( q = ((3 * a1) - (a2 |^ 2)) / 9 & r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s = 2 -root ((q |^ 3) + (r |^ 2)) & s1 = 3 -root (r + s) & s2 = - (q / s1) & b1 = ((- ((s1 + s2) / 2)) - (a2 / 3)) + ((((s1 - s2) * (2 -root 3)) * ) / 2) ) & ex q, r, s, s1, s2 being complex number st ( q = ((3 * a1) - (a2 |^ 2)) / 9 & r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s = 2 -root ((q |^ 3) + (r |^ 2)) & s1 = 3 -root (r + s) & s2 = - (q / s1) & b2 = ((- ((s1 + s2) / 2)) - (a2 / 3)) + ((((s1 - s2) * (2 -root 3)) * ) / 2) ) implies b1 = b2 ) ) ; correctness consistency for b1 being complex number holds verum; ; func 3_root_of_cubic (a0,a1,a2) -> complex number means :Def4: :: POLYEQ_5:def 4 ex r, s1 being complex number st ( r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s1 = 3 -root (2 * r) & it = ((- (s1 / 2)) - (a2 / 3)) - (((s1 * (2 -root 3)) * ) / 2) ) if (3 * a1) - (a2 |^ 2) = 0 otherwise ex q, r, s, s1, s2 being complex number st ( q = ((3 * a1) - (a2 |^ 2)) / 9 & r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s = 2 -root ((q |^ 3) + (r |^ 2)) & s1 = 3 -root (r + s) & s2 = - (q / s1) & it = ((- ((s1 + s2) / 2)) - (a2 / 3)) - ((((s1 - s2) * (2 -root 3)) * ) / 2) ); existence ( ( (3 * a1) - (a2 |^ 2) = 0 implies ex b1, r, s1 being complex number st ( r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s1 = 3 -root (2 * r) & b1 = ((- (s1 / 2)) - (a2 / 3)) - (((s1 * (2 -root 3)) * ) / 2) ) ) & ( not (3 * a1) - (a2 |^ 2) = 0 implies ex b1, q, r, s, s1, s2 being complex number st ( q = ((3 * a1) - (a2 |^ 2)) / 9 & r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s = 2 -root ((q |^ 3) + (r |^ 2)) & s1 = 3 -root (r + s) & s2 = - (q / s1) & b1 = ((- ((s1 + s2) / 2)) - (a2 / 3)) - ((((s1 - s2) * (2 -root 3)) * ) / 2) ) ) ) proofend; uniqueness for b1, b2 being complex number holds ( ( (3 * a1) - (a2 |^ 2) = 0 & ex r, s1 being complex number st ( r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s1 = 3 -root (2 * r) & b1 = ((- (s1 / 2)) - (a2 / 3)) - (((s1 * (2 -root 3)) * ) / 2) ) & ex r, s1 being complex number st ( r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s1 = 3 -root (2 * r) & b2 = ((- (s1 / 2)) - (a2 / 3)) - (((s1 * (2 -root 3)) * ) / 2) ) implies b1 = b2 ) & ( not (3 * a1) - (a2 |^ 2) = 0 & ex q, r, s, s1, s2 being complex number st ( q = ((3 * a1) - (a2 |^ 2)) / 9 & r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s = 2 -root ((q |^ 3) + (r |^ 2)) & s1 = 3 -root (r + s) & s2 = - (q / s1) & b1 = ((- ((s1 + s2) / 2)) - (a2 / 3)) - ((((s1 - s2) * (2 -root 3)) * ) / 2) ) & ex q, r, s, s1, s2 being complex number st ( q = ((3 * a1) - (a2 |^ 2)) / 9 & r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s = 2 -root ((q |^ 3) + (r |^ 2)) & s1 = 3 -root (r + s) & s2 = - (q / s1) & b2 = ((- ((s1 + s2) / 2)) - (a2 / 3)) - ((((s1 - s2) * (2 -root 3)) * ) / 2) ) implies b1 = b2 ) ) ; correctness consistency for b1 being complex number holds verum; ; end; :: deftheorem Def2 defines 1_root_of_cubic POLYEQ_5:def_2_:_ for a0, a1, a2, b4 being complex number holds ( ( (3 * a1) - (a2 |^ 2) = 0 implies ( b4 = 1_root_of_cubic (a0,a1,a2) iff ex r, s1 being complex number st ( r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s1 = 3 -root (2 * r) & b4 = s1 - (a2 / 3) ) ) ) & ( not (3 * a1) - (a2 |^ 2) = 0 implies ( b4 = 1_root_of_cubic (a0,a1,a2) iff ex q, r, s, s1, s2 being complex number st ( q = ((3 * a1) - (a2 |^ 2)) / 9 & r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s = 2 -root ((q |^ 3) + (r |^ 2)) & s1 = 3 -root (r + s) & s2 = - (q / s1) & b4 = (s1 + s2) - (a2 / 3) ) ) ) ); :: deftheorem Def3 defines 2_root_of_cubic POLYEQ_5:def_3_:_ for a0, a1, a2, b4 being complex number holds ( ( (3 * a1) - (a2 |^ 2) = 0 implies ( b4 = 2_root_of_cubic (a0,a1,a2) iff ex r, s1 being complex number st ( r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s1 = 3 -root (2 * r) & b4 = ((- (s1 / 2)) - (a2 / 3)) + (((s1 * (2 -root 3)) * ) / 2) ) ) ) & ( not (3 * a1) - (a2 |^ 2) = 0 implies ( b4 = 2_root_of_cubic (a0,a1,a2) iff ex q, r, s, s1, s2 being complex number st ( q = ((3 * a1) - (a2 |^ 2)) / 9 & r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s = 2 -root ((q |^ 3) + (r |^ 2)) & s1 = 3 -root (r + s) & s2 = - (q / s1) & b4 = ((- ((s1 + s2) / 2)) - (a2 / 3)) + ((((s1 - s2) * (2 -root 3)) * ) / 2) ) ) ) ); :: deftheorem Def4 defines 3_root_of_cubic POLYEQ_5:def_4_:_ for a0, a1, a2, b4 being complex number holds ( ( (3 * a1) - (a2 |^ 2) = 0 implies ( b4 = 3_root_of_cubic (a0,a1,a2) iff ex r, s1 being complex number st ( r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s1 = 3 -root (2 * r) & b4 = ((- (s1 / 2)) - (a2 / 3)) - (((s1 * (2 -root 3)) * ) / 2) ) ) ) & ( not (3 * a1) - (a2 |^ 2) = 0 implies ( b4 = 3_root_of_cubic (a0,a1,a2) iff ex q, r, s, s1, s2 being complex number st ( q = ((3 * a1) - (a2 |^ 2)) / 9 & r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s = 2 -root ((q |^ 3) + (r |^ 2)) & s1 = 3 -root (r + s) & s2 = - (q / s1) & b4 = ((- ((s1 + s2) / 2)) - (a2 / 3)) - ((((s1 - s2) * (2 -root 3)) * ) / 2) ) ) ) ); theorem Th17: :: POLYEQ_5:17 for a0, a1, a2 being complex number holds ((1_root_of_cubic (a0,a1,a2)) + (2_root_of_cubic (a0,a1,a2))) + (3_root_of_cubic (a0,a1,a2)) = - a2 proofend; theorem Th18: :: POLYEQ_5:18 for a0, a1, a2 being complex number holds (((1_root_of_cubic (a0,a1,a2)) * (2_root_of_cubic (a0,a1,a2))) + ((1_root_of_cubic (a0,a1,a2)) * (3_root_of_cubic (a0,a1,a2)))) + ((2_root_of_cubic (a0,a1,a2)) * (3_root_of_cubic (a0,a1,a2))) = a1 proofend; theorem Th19: :: POLYEQ_5:19 for a0, a1, a2 being complex number holds ((1_root_of_cubic (a0,a1,a2)) * (2_root_of_cubic (a0,a1,a2))) * (3_root_of_cubic (a0,a1,a2)) = - a0 proofend; theorem :: POLYEQ_5:20 for z, a2, a1, a0, a3 being complex number st a3 <> 0 holds ( (((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)) ) ) proofend; begin theorem Th21: :: POLYEQ_5:21 for z, a2, a1, a0, x, a3, q, r, p being complex number st z = x - (a3 / 4) & p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 holds ( ((((z |^ 4) + (a3 * (z |^ 3))) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff (((x |^ 4) + ((4 * p) * (x |^ 2))) + ((8 * q) * x)) + (4 * r) = 0 ) proofend; theorem Th22: :: POLYEQ_5:22 for z, s1, s2, a2, a1, a0, a3, s3, s4 being complex number st a3 = - (((s1 + s2) + s3) + s4) & a2 = (((((s1 * s2) + (s1 * s3)) + (s1 * s4)) + (s2 * s3)) + (s2 * s4)) + (s3 * s4) & a1 = - (((((s1 * s2) * s3) + ((s1 * s2) * s4)) + ((s1 * s3) * s4)) + ((s2 * s3) * s4)) & a0 = ((s1 * s2) * s3) * s4 holds ( ((((z |^ 4) + (a3 * (z |^ 3))) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ( z = s1 or z = s2 or z = s3 or z = s4 ) ) proofend; :: Descartes-Euler Solution :: Mathematical Handbook for Scientists and Engineers (Korn) p.24 theorem Th23: :: POLYEQ_5:23 for z, s1, s2, q, r, s3, p being complex number st q <> 0 & s1 = 2 -root (1_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s2 = 2 -root (2_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s3 = - (q / (s1 * s2)) holds ( (((z |^ 4) + ((4 * p) * (z |^ 2))) + ((8 * q) * z)) + (4 * r) = 0 iff ( z = (s1 + s2) + s3 or z = (s1 - s2) - s3 or z = ((- s1) + s2) - s3 or z = ((- s1) - s2) + s3 ) ) proofend; :: roots of quartic (I) theorem :: POLYEQ_5:24 for z, a2, a1, a0, s1, s2, a3, q, r, s3, p being complex number st p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 & q <> 0 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root (1_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s2 = 2 -root (2_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s3 = - (q / (s1 * s2)) holds ( ((((z |^ 4) + (a3 * (z |^ 3))) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ( z = ((s1 + s2) + s3) - (a3 / 4) or z = ((s1 - s2) - s3) - (a3 / 4) or z = (((- s1) + s2) - s3) - (a3 / 4) or z = (((- s1) - s2) + s3) - (a3 / 4) ) ) proofend; :: roots of quartic (II) theorem :: POLYEQ_5:25 for z, a2, a1, a0, s1, a3, q, r, p being complex number st p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 & q = 0 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root ((p |^ 2) - r) holds ( ((((z |^ 4) + (a3 * (z |^ 3))) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ( z = (2 -root (- (2 * (p - s1)))) - (a3 / 4) or z = (- (2 -root (- (2 * (p - s1))))) - (a3 / 4) or z = (2 -root (- (2 * (p + s1)))) - (a3 / 4) or z = (- (2 -root (- (2 * (p + s1))))) - (a3 / 4) ) ) proofend; definition let a0, a1, a2, a3 be complex number ; func 1_root_of_quartic (a0,a1,a2,a3) -> complex number means :Def5: :: POLYEQ_5:def 5 ex p, r, s1 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root ((p |^ 2) - r) & it = (2 -root (- (2 * (p - s1)))) - (a3 / 4) ) if ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 otherwise ex p, q, r, s1, s2, s3 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root (1_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s2 = 2 -root (2_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s3 = - (q / (s1 * s2)) & it = ((s1 + s2) + s3) - (a3 / 4) ); existence ( ( ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 implies ex b1, p, r, s1 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root ((p |^ 2) - r) & b1 = (2 -root (- (2 * (p - s1)))) - (a3 / 4) ) ) & ( not ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 implies ex b1, p, q, r, s1, s2, s3 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root (1_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s2 = 2 -root (2_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s3 = - (q / (s1 * s2)) & b1 = ((s1 + s2) + s3) - (a3 / 4) ) ) ) proofend; uniqueness for b1, b2 being complex number holds ( ( ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 & ex p, r, s1 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root ((p |^ 2) - r) & b1 = (2 -root (- (2 * (p - s1)))) - (a3 / 4) ) & ex p, r, s1 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root ((p |^ 2) - r) & b2 = (2 -root (- (2 * (p - s1)))) - (a3 / 4) ) implies b1 = b2 ) & ( not ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 & ex p, q, r, s1, s2, s3 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root (1_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s2 = 2 -root (2_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s3 = - (q / (s1 * s2)) & b1 = ((s1 + s2) + s3) - (a3 / 4) ) & ex p, q, r, s1, s2, s3 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root (1_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s2 = 2 -root (2_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s3 = - (q / (s1 * s2)) & b2 = ((s1 + s2) + s3) - (a3 / 4) ) implies b1 = b2 ) ) ; correctness consistency for b1 being complex number holds verum; ; func 2_root_of_quartic (a0,a1,a2,a3) -> complex number means :Def6: :: POLYEQ_5:def 6 ex p, r, s1 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root ((p |^ 2) - r) & it = (- (2 -root (- (2 * (p - s1))))) - (a3 / 4) ) if ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 otherwise ex p, q, r, s1, s2, s3 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root (1_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s2 = 2 -root (2_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s3 = - (q / (s1 * s2)) & it = (((- s1) - s2) + s3) - (a3 / 4) ); existence ( ( ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 implies ex b1, p, r, s1 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root ((p |^ 2) - r) & b1 = (- (2 -root (- (2 * (p - s1))))) - (a3 / 4) ) ) & ( not ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 implies ex b1, p, q, r, s1, s2, s3 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root (1_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s2 = 2 -root (2_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s3 = - (q / (s1 * s2)) & b1 = (((- s1) - s2) + s3) - (a3 / 4) ) ) ) proofend; uniqueness for b1, b2 being complex number holds ( ( ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 & ex p, r, s1 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root ((p |^ 2) - r) & b1 = (- (2 -root (- (2 * (p - s1))))) - (a3 / 4) ) & ex p, r, s1 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root ((p |^ 2) - r) & b2 = (- (2 -root (- (2 * (p - s1))))) - (a3 / 4) ) implies b1 = b2 ) & ( not ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 & ex p, q, r, s1, s2, s3 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root (1_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s2 = 2 -root (2_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s3 = - (q / (s1 * s2)) & b1 = (((- s1) - s2) + s3) - (a3 / 4) ) & ex p, q, r, s1, s2, s3 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root (1_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s2 = 2 -root (2_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s3 = - (q / (s1 * s2)) & b2 = (((- s1) - s2) + s3) - (a3 / 4) ) implies b1 = b2 ) ) ; correctness consistency for b1 being complex number holds verum; ; func 3_root_of_quartic (a0,a1,a2,a3) -> complex number means :Def7: :: POLYEQ_5:def 7 ex p, r, s1 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root ((p |^ 2) - r) & it = (2 -root (- (2 * (p + s1)))) - (a3 / 4) ) if ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 otherwise ex p, q, r, s1, s2, s3 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root (1_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s2 = 2 -root (2_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s3 = - (q / (s1 * s2)) & it = (((- s1) + s2) - s3) - (a3 / 4) ); existence ( ( ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 implies ex b1, p, r, s1 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root ((p |^ 2) - r) & b1 = (2 -root (- (2 * (p + s1)))) - (a3 / 4) ) ) & ( not ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 implies ex b1, p, q, r, s1, s2, s3 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root (1_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s2 = 2 -root (2_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s3 = - (q / (s1 * s2)) & b1 = (((- s1) + s2) - s3) - (a3 / 4) ) ) ) proofend; uniqueness for b1, b2 being complex number holds ( ( ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 & ex p, r, s1 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root ((p |^ 2) - r) & b1 = (2 -root (- (2 * (p + s1)))) - (a3 / 4) ) & ex p, r, s1 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root ((p |^ 2) - r) & b2 = (2 -root (- (2 * (p + s1)))) - (a3 / 4) ) implies b1 = b2 ) & ( not ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 & ex p, q, r, s1, s2, s3 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root (1_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s2 = 2 -root (2_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s3 = - (q / (s1 * s2)) & b1 = (((- s1) + s2) - s3) - (a3 / 4) ) & ex p, q, r, s1, s2, s3 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root (1_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s2 = 2 -root (2_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s3 = - (q / (s1 * s2)) & b2 = (((- s1) + s2) - s3) - (a3 / 4) ) implies b1 = b2 ) ) ; correctness consistency for b1 being complex number holds verum; ; func 4_root_of_quartic (a0,a1,a2,a3) -> complex number means :Def8: :: POLYEQ_5:def 8 ex p, r, s1 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root ((p |^ 2) - r) & it = (- (2 -root (- (2 * (p + s1))))) - (a3 / 4) ) if ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 otherwise ex p, q, r, s1, s2, s3 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root (1_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s2 = 2 -root (2_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s3 = - (q / (s1 * s2)) & it = ((s1 - s2) - s3) - (a3 / 4) ); existence ( ( ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 implies ex b1, p, r, s1 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root ((p |^ 2) - r) & b1 = (- (2 -root (- (2 * (p + s1))))) - (a3 / 4) ) ) & ( not ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 implies ex b1, p, q, r, s1, s2, s3 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root (1_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s2 = 2 -root (2_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s3 = - (q / (s1 * s2)) & b1 = ((s1 - s2) - s3) - (a3 / 4) ) ) ) proofend; uniqueness for b1, b2 being complex number holds ( ( ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 & ex p, r, s1 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root ((p |^ 2) - r) & b1 = (- (2 -root (- (2 * (p + s1))))) - (a3 / 4) ) & ex p, r, s1 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root ((p |^ 2) - r) & b2 = (- (2 -root (- (2 * (p + s1))))) - (a3 / 4) ) implies b1 = b2 ) & ( not ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 & ex p, q, r, s1, s2, s3 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root (1_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s2 = 2 -root (2_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s3 = - (q / (s1 * s2)) & b1 = ((s1 - s2) - s3) - (a3 / 4) ) & ex p, q, r, s1, s2, s3 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root (1_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s2 = 2 -root (2_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s3 = - (q / (s1 * s2)) & b2 = ((s1 - s2) - s3) - (a3 / 4) ) implies b1 = b2 ) ) ; correctness consistency for b1 being complex number holds verum; ; end; :: deftheorem Def5 defines 1_root_of_quartic POLYEQ_5:def_5_:_ for a0, a1, a2, a3, b5 being complex number holds ( ( ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 implies ( b5 = 1_root_of_quartic (a0,a1,a2,a3) iff ex p, r, s1 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root ((p |^ 2) - r) & b5 = (2 -root (- (2 * (p - s1)))) - (a3 / 4) ) ) ) & ( not ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 implies ( b5 = 1_root_of_quartic (a0,a1,a2,a3) iff ex p, q, r, s1, s2, s3 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root (1_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s2 = 2 -root (2_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s3 = - (q / (s1 * s2)) & b5 = ((s1 + s2) + s3) - (a3 / 4) ) ) ) ); :: deftheorem Def6 defines 2_root_of_quartic POLYEQ_5:def_6_:_ for a0, a1, a2, a3, b5 being complex number holds ( ( ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 implies ( b5 = 2_root_of_quartic (a0,a1,a2,a3) iff ex p, r, s1 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root ((p |^ 2) - r) & b5 = (- (2 -root (- (2 * (p - s1))))) - (a3 / 4) ) ) ) & ( not ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 implies ( b5 = 2_root_of_quartic (a0,a1,a2,a3) iff ex p, q, r, s1, s2, s3 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root (1_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s2 = 2 -root (2_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s3 = - (q / (s1 * s2)) & b5 = (((- s1) - s2) + s3) - (a3 / 4) ) ) ) ); :: deftheorem Def7 defines 3_root_of_quartic POLYEQ_5:def_7_:_ for a0, a1, a2, a3, b5 being complex number holds ( ( ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 implies ( b5 = 3_root_of_quartic (a0,a1,a2,a3) iff ex p, r, s1 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root ((p |^ 2) - r) & b5 = (2 -root (- (2 * (p + s1)))) - (a3 / 4) ) ) ) & ( not ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 implies ( b5 = 3_root_of_quartic (a0,a1,a2,a3) iff ex p, q, r, s1, s2, s3 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root (1_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s2 = 2 -root (2_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s3 = - (q / (s1 * s2)) & b5 = (((- s1) + s2) - s3) - (a3 / 4) ) ) ) ); :: deftheorem Def8 defines 4_root_of_quartic POLYEQ_5:def_8_:_ for a0, a1, a2, a3, b5 being complex number holds ( ( ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 implies ( b5 = 4_root_of_quartic (a0,a1,a2,a3) iff ex p, r, s1 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root ((p |^ 2) - r) & b5 = (- (2 -root (- (2 * (p + s1))))) - (a3 / 4) ) ) ) & ( not ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 implies ( b5 = 4_root_of_quartic (a0,a1,a2,a3) iff ex p, q, r, s1, s2, s3 being complex number st ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root (1_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s2 = 2 -root (2_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s3 = - (q / (s1 * s2)) & b5 = ((s1 - s2) - s3) - (a3 / 4) ) ) ) ); theorem Th26: :: POLYEQ_5:26 for a0, a1, a2, a3 being complex number holds (((1_root_of_quartic (a0,a1,a2,a3)) + (2_root_of_quartic (a0,a1,a2,a3))) + (3_root_of_quartic (a0,a1,a2,a3))) + (4_root_of_quartic (a0,a1,a2,a3)) = - a3 proofend; theorem Th27: :: POLYEQ_5:27 for a0, a1, a2, a3 being complex number holds ((((((1_root_of_quartic (a0,a1,a2,a3)) * (2_root_of_quartic (a0,a1,a2,a3))) + ((1_root_of_quartic (a0,a1,a2,a3)) * (3_root_of_quartic (a0,a1,a2,a3)))) + ((1_root_of_quartic (a0,a1,a2,a3)) * (4_root_of_quartic (a0,a1,a2,a3)))) + ((2_root_of_quartic (a0,a1,a2,a3)) * (3_root_of_quartic (a0,a1,a2,a3)))) + ((2_root_of_quartic (a0,a1,a2,a3)) * (4_root_of_quartic (a0,a1,a2,a3)))) + ((3_root_of_quartic (a0,a1,a2,a3)) * (4_root_of_quartic (a0,a1,a2,a3))) = a2 proofend; theorem Th28: :: POLYEQ_5:28 for a0, a1, a2, a3 being complex number holds (((((1_root_of_quartic (a0,a1,a2,a3)) * (2_root_of_quartic (a0,a1,a2,a3))) * (3_root_of_quartic (a0,a1,a2,a3))) + (((1_root_of_quartic (a0,a1,a2,a3)) * (2_root_of_quartic (a0,a1,a2,a3))) * (4_root_of_quartic (a0,a1,a2,a3)))) + (((1_root_of_quartic (a0,a1,a2,a3)) * (3_root_of_quartic (a0,a1,a2,a3))) * (4_root_of_quartic (a0,a1,a2,a3)))) + (((2_root_of_quartic (a0,a1,a2,a3)) * (3_root_of_quartic (a0,a1,a2,a3))) * (4_root_of_quartic (a0,a1,a2,a3))) = - a1 proofend; theorem Th29: :: POLYEQ_5:29 for a0, a1, a2, a3 being complex number holds (((1_root_of_quartic (a0,a1,a2,a3)) * (2_root_of_quartic (a0,a1,a2,a3))) * (3_root_of_quartic (a0,a1,a2,a3))) * (4_root_of_quartic (a0,a1,a2,a3)) = a0 proofend; :: [WP: ] The_Solution_of_the_General_Quartic_Equation theorem :: POLYEQ_5:30 for z, a2, a1, a0, a3, a4 being complex number st a4 <> 0 holds ( ((((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)) ) ) proofend;