let a0, a1, a2, a3 be Complex; (((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
per cases
( ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 or ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) <> 0 )
;
suppose A1:
((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0
;
(((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)) = - a3then A2:
( 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) &
3_root_of_quartic (
a0,
a1,
a2,
a3)
= (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) &
4_root_of_quartic (
a0,
a1,
a2,
a3)
= (- (2 -root (- (2 * (p + s1))))) - (a3 / 4) ) )
by Def7, Def8;
( 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) &
1_root_of_quartic (
a0,
a1,
a2,
a3)
= (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) &
2_root_of_quartic (
a0,
a1,
a2,
a3)
= (- (2 -root (- (2 * (p - s1))))) - (a3 / 4) ) )
by A1, Def5, Def6;
hence
(((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
by A2;
verum end; suppose A3:
((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) <> 0
;
(((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)) = - a3then A4:
( 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)) &
3_root_of_quartic (
a0,
a1,
a2,
a3)
= (((- 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)) &
4_root_of_quartic (
a0,
a1,
a2,
a3)
= ((s1 - s2) - s3) - (a3 / 4) ) )
by Def7, Def8;
( 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)) &
1_root_of_quartic (
a0,
a1,
a2,
a3)
= ((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)) &
2_root_of_quartic (
a0,
a1,
a2,
a3)
= (((- s1) - s2) + s3) - (a3 / 4) ) )
by A3, Def5, Def6;
hence
(((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
by A4;
verum end; end;