:: Solution of Cubic and Quartic Equations
:: by Marco Riccardi
::
:: Received March 3, 2009
:: Copyright (c) 2009-2021 Association of Mizar Users


theorem Th1: :: POLYEQ_5:1
for a being Complex holds a * a = a |^ 2
proof end;

theorem Th2: :: POLYEQ_5:2
for a being Complex holds (a * a) * a = a |^ 3
proof end;

theorem Th3: :: POLYEQ_5:3
for a being Complex holds ((a * a) * a) * a = a |^ 4
proof end;

theorem Th4: :: POLYEQ_5:4
for a, b being Complex holds (a - b) |^ 2 = ((a |^ 2) - ((2 * a) * b)) + (b |^ 2)
proof end;

:: like SERIES_4:5
theorem Th5: :: POLYEQ_5:5
for a, b being Complex holds (a - b) |^ 3 = (((a |^ 3) - ((3 * (a |^ 2)) * b)) + ((3 * (b |^ 2)) * a)) - (b |^ 3)
proof end;

theorem Th6: :: POLYEQ_5:6
for a, b being Complex holds (a - b) |^ 4 = ((((a |^ 4) - ((4 * (a |^ 3)) * b)) + ((6 * (a |^ 2)) * (b |^ 2))) - ((4 * (b |^ 3)) * a)) + (b |^ 4)
proof end;

notation
let n be Nat;
let r be Real;
synonym n -real-root r for n -root r;
end;

:: principal root
definition
let n be non zero Nat;
let z be Complex;
func n -root z -> Complex equals :: POLYEQ_5:def 1
(n -real-root |.z.|) * ((cos ((Arg z) / n)) + ((sin ((Arg z) / n)) * <i>));
correctness
coherence
(n -real-root |.z.|) * ((cos ((Arg z) / n)) + ((sin ((Arg z) / n)) * <i>)) is Complex;
;
end;

:: deftheorem defines -root POLYEQ_5:def 1 :
for n being non zero Nat
for z being Complex holds n -root z = (n -real-root |.z.|) * ((cos ((Arg z) / n)) + ((sin ((Arg z) / n)) * <i>));

theorem Th7: :: POLYEQ_5:7
for z being Complex
for n0 being non zero Nat holds (n0 -root z) |^ n0 = z
proof end;

theorem Th8: :: POLYEQ_5:8
for n0 being non zero Nat
for r being Real st r >= 0 holds
n0 -root r = n0 -real-root r
proof end;

theorem Th9: :: POLYEQ_5:9
for z being Complex
for n0 being non zero Nat
for r being Real st r > 0 holds
n0 -root (z / r) = (n0 -root z) / (n0 -root r)
proof end;

theorem Th10: :: POLYEQ_5:10
for a, z being Complex holds
( z |^ 2 = a iff ( z = 2 -root a or z = - (2 -root a) ) )
proof end;

theorem Th11: :: POLYEQ_5:11
for z, a0, a1, s1, s2 being Complex st a1 = - (s1 + s2) & a0 = s1 * s2 holds
( ((z |^ 2) + (a1 * z)) + a0 = 0 iff ( z = s1 or z = s2 ) )
proof end;

theorem Th12: :: POLYEQ_5:12
for z, a0, a1, a2 being Complex 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)) ) )
proof end;

theorem Th13: :: POLYEQ_5:13
for z, a0, a1, a2, x, q, r being Complex 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 )
proof end;

theorem Th14: :: POLYEQ_5:14
for z, a0, a1, a2, s1, s2, s3 being Complex 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 ) )
proof end;

:: Cardan's Solution
:: Mathematical Handbook for Scientists and Engineers (Korn) p.23
:: roots of cubic (I)
theorem :: POLYEQ_5:15
for z, a0, a1, a2, s1, s2, q, r, s being Complex 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)) * <i>) / 2) or z = ((- ((s1 + s2) / 2)) - (a2 / 3)) - ((((s1 - s2) * (2 -root 3)) * <i>) / 2) ) )
proof end;

:: roots of cubic (II)
theorem :: POLYEQ_5:16
for z, a0, a1, a2, s1, q, r being Complex 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)) * <i>) / 2) or z = ((- (s1 / 2)) - (a2 / 3)) - (((s1 * (2 -root 3)) * <i>) / 2) ) )
proof end;

definition
let a0, a1, a2 be Complex;
func 1_root_of_cubic (a0,a1,a2) -> Complex means :Def2: :: POLYEQ_5:def 2
 ex r, s1 being Complex 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 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 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 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) ) ) )
proof end;
uniqueness
for b1, b2 being Complex holds
( ( (3 * a1) - (a2 |^ 2) = 0 & ex r, s1 being Complex 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 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 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 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 holds verum;
;
func 2_root_of_cubic (a0,a1,a2) -> Complex means :Def3: :: POLYEQ_5:def 3
 ex r, s1 being Complex 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)) * <i>) / 2) ) if (3 * a1) - (a2 |^ 2) = 0
otherwise ex q, r, s, s1, s2 being Complex 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)) * <i>) / 2) );
existence
( ( (3 * a1) - (a2 |^ 2) = 0 implies ex b1, r, s1 being Complex 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)) * <i>) / 2) ) ) & ( not (3 * a1) - (a2 |^ 2) = 0 implies ex b1, q, r, s, s1, s2 being Complex 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)) * <i>) / 2) ) ) )
proof end;
uniqueness
for b1, b2 being Complex holds
( ( (3 * a1) - (a2 |^ 2) = 0 & ex r, s1 being Complex 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)) * <i>) / 2) ) & ex r, s1 being Complex 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)) * <i>) / 2) ) implies b1 = b2 ) & ( not (3 * a1) - (a2 |^ 2) = 0 & ex q, r, s, s1, s2 being Complex 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)) * <i>) / 2) ) & ex q, r, s, s1, s2 being Complex 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)) * <i>) / 2) ) implies b1 = b2 ) ) ;
correctness
consistency
for b1 being Complex holds verum;
;
func 3_root_of_cubic (a0,a1,a2) -> Complex means :Def4: :: POLYEQ_5:def 4
 ex r, s1 being Complex 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)) * <i>) / 2) ) if (3 * a1) - (a2 |^ 2) = 0
otherwise ex q, r, s, s1, s2 being Complex 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)) * <i>) / 2) );
existence
( ( (3 * a1) - (a2 |^ 2) = 0 implies ex b1, r, s1 being Complex 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)) * <i>) / 2) ) ) & ( not (3 * a1) - (a2 |^ 2) = 0 implies ex b1, q, r, s, s1, s2 being Complex 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)) * <i>) / 2) ) ) )
proof end;
uniqueness
for b1, b2 being Complex holds
( ( (3 * a1) - (a2 |^ 2) = 0 & ex r, s1 being Complex 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)) * <i>) / 2) ) & ex r, s1 being Complex 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)) * <i>) / 2) ) implies b1 = b2 ) & ( not (3 * a1) - (a2 |^ 2) = 0 & ex q, r, s, s1, s2 being Complex 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)) * <i>) / 2) ) & ex q, r, s, s1, s2 being Complex 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)) * <i>) / 2) ) implies b1 = b2 ) ) ;
correctness
consistency
for b1 being Complex holds verum;
;
end;

:: deftheorem Def2 defines 1_root_of_cubic POLYEQ_5:def 2 :
for a0, a1, a2, b4 being Complex holds
( ( (3 * a1) - (a2 |^ 2) = 0 implies ( b4 = 1_root_of_cubic (a0,a1,a2) iff ex r, s1 being Complex 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 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 holds
( ( (3 * a1) - (a2 |^ 2) = 0 implies ( b4 = 2_root_of_cubic (a0,a1,a2) iff ex r, s1 being Complex 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)) * <i>) / 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 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)) * <i>) / 2) ) ) ) );

:: deftheorem Def4 defines 3_root_of_cubic POLYEQ_5:def 4 :
for a0, a1, a2, b4 being Complex holds
( ( (3 * a1) - (a2 |^ 2) = 0 implies ( b4 = 3_root_of_cubic (a0,a1,a2) iff ex r, s1 being Complex 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)) * <i>) / 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 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)) * <i>) / 2) ) ) ) );

theorem Th17: :: POLYEQ_5:17
for a0, a1, a2 being Complex holds ((1_root_of_cubic (a0,a1,a2)) + (2_root_of_cubic (a0,a1,a2))) + (3_root_of_cubic (a0,a1,a2)) = - a2
proof end;

theorem Th18: :: POLYEQ_5:18
for a0, a1, a2 being Complex 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
proof end;

theorem Th19: :: POLYEQ_5:19
for a0, a1, a2 being Complex holds ((1_root_of_cubic (a0,a1,a2)) * (2_root_of_cubic (a0,a1,a2))) * (3_root_of_cubic (a0,a1,a2)) = - a0
proof end;

theorem :: POLYEQ_5:20
for z, a0, a1, a2, a3 being Complex 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)) ) )
proof end;

theorem Th21: :: POLYEQ_5:21
for z, a0, a1, a2, a3, x, q, r, p being Complex 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 )
proof end;

theorem Th22: :: POLYEQ_5:22
for z, a0, a1, a2, s1, s2, a3, s3, s4 being Complex 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 ) )
proof end;

:: 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 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 ) )
proof end;

:: roots of quartic (I)
theorem :: POLYEQ_5:24
for z, a0, a1, a2, s1, s2, a3, q, r, s3, p being Complex 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) ) )
proof end;

:: roots of quartic (II)
theorem :: POLYEQ_5:25
for z, a0, a1, a2, s1, a3, q, r, p being Complex 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) ) )
proof end;

definition
let a0, a1, a2, a3 be Complex;
func 1_root_of_quartic (a0,a1,a2,a3) -> Complex means :Def5: :: POLYEQ_5:def 5
 ex p, r, s1 being Complex 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 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 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 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) ) ) )
proof end;
uniqueness
for b1, b2 being Complex holds
( ( ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 & ex p, r, s1 being Complex 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 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 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 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 holds verum;
;
func 2_root_of_quartic (a0,a1,a2,a3) -> Complex means :Def6: :: POLYEQ_5:def 6
 ex p, r, s1 being Complex 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 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 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 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) ) ) )
proof end;
uniqueness
for b1, b2 being Complex holds
( ( ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 & ex p, r, s1 being Complex 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 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 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 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 holds verum;
;
func 3_root_of_quartic (a0,a1,a2,a3) -> Complex means :Def7: :: POLYEQ_5:def 7
 ex p, r, s1 being Complex 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 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 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 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) ) ) )
proof end;
uniqueness
for b1, b2 being Complex holds
( ( ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 & ex p, r, s1 being Complex 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 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 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 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 holds verum;
;
func 4_root_of_quartic (a0,a1,a2,a3) -> Complex means :Def8: :: POLYEQ_5:def 8
 ex p, r, s1 being Complex 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 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 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 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) ) ) )
proof end;
uniqueness
for b1, b2 being Complex holds
( ( ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 & ex p, r, s1 being Complex 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 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 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 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 holds verum;
;
end;

:: deftheorem Def5 defines 1_root_of_quartic POLYEQ_5:def 5 :
for a0, a1, a2, a3, b5 being Complex 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 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 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 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 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 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 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 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 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 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 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 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 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
proof end;

theorem Th27: :: POLYEQ_5:27
for a0, a1, a2, a3 being Complex 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
proof end;

theorem Th28: :: POLYEQ_5:28
for a0, a1, a2, a3 being Complex 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
proof end;

theorem Th29: :: POLYEQ_5:29
for a0, a1, a2, a3 being Complex 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
proof end;

:: WP: The Solution of the General Quartic Equation
theorem :: POLYEQ_5:30
for z, a0, a1, a2, a3, a4 being Complex 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)) ) )
proof end;