let z, a0, a1, a2, s1, a3, q, r, p be Complex; ( 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) implies ( ((((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) ) ) )
assume A1:
p = ((8 * a2) - (3 * (a3 |^ 2))) / 32
; ( not q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 or not q = 0 or not r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 or not s1 = 2 -root ((p |^ 2) - r) or ( ((((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) ) ) )
set x = z + (a3 / 4);
assume that
A2:
q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64
and
A3:
q = 0
; ( not r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 or not s1 = 2 -root ((p |^ 2) - r) or ( ((((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) ) ) )
A4:
z = (z + (a3 / 4)) - (a3 / 4)
;
assume
r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024
; ( not s1 = 2 -root ((p |^ 2) - r) or ( ((((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) ) ) )
then A5:
( ((((z |^ 4) + (a3 * (z |^ 3))) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ((((z + (a3 / 4)) |^ 4) + ((4 * p) * ((z + (a3 / 4)) |^ 2))) + ((8 * q) * (z + (a3 / 4)))) + (4 * r) = 0 )
by A1, A2, A4, Th21;
assume A6:
s1 = 2 -root ((p |^ 2) - r)
; ( ((((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) ) )
set y = (z + (a3 / 4)) |^ 2;
A7: ((z + (a3 / 4)) |^ 2) |^ 2 =
(z + (a3 / 4)) |^ (2 * 2)
by NEWTON:9
.=
(z + (a3 / 4)) |^ 4
;
A8:
( (z + (a3 / 4)) |^ 2 = (- (2 * p)) + ((2 -root (delta ((4 * r),(4 * p),1))) / 2) iff ( z + (a3 / 4) = 2 -root ((- (2 * p)) + ((2 -root (delta ((4 * r),(4 * p),1))) / 2)) or z + (a3 / 4) = - (2 -root ((- (2 * p)) + ((2 -root (delta ((4 * r),(4 * p),1))) / 2))) ) )
by Th10;
A9:
( (z + (a3 / 4)) |^ 2 = (- (2 * p)) - ((2 -root (delta ((4 * r),(4 * p),1))) / 2) iff ( z + (a3 / 4) = 2 -root ((- (2 * p)) - ((2 -root (delta ((4 * r),(4 * p),1))) / 2)) or z + (a3 / 4) = - (2 -root ((- (2 * p)) - ((2 -root (delta ((4 * r),(4 * p),1))) / 2))) ) )
by Th10;
A10: 4 |^ 2 =
4 * 4
by Th1
.=
16
;
( ((1 * (((z + (a3 / 4)) |^ 2) |^ 2)) + ((4 * p) * ((z + (a3 / 4)) |^ 2))) + (4 * r) = 0 iff ( (z + (a3 / 4)) |^ 2 = (- ((4 * p) / (2 * 1))) + ((2 -root (delta ((4 * r),(4 * p),1))) / (2 * 1)) or (z + (a3 / 4)) |^ 2 = (- ((4 * p) / (2 * 1))) - ((2 -root (delta ((4 * r),(4 * p),1))) / (2 * 1)) ) )
by Th12;
then A11:
( ((1 * (((z + (a3 / 4)) |^ 2) |^ 2)) + ((4 * p) * ((z + (a3 / 4)) |^ 2))) + (4 * r) = 0 iff ( z = (2 -root ((- (2 * p)) + ((2 -root (delta ((4 * r),(4 * p),1))) / 2))) - (a3 / 4) or z = (- (2 -root ((- (2 * p)) + ((2 -root (delta ((4 * r),(4 * p),1))) / 2)))) - (a3 / 4) or z = (2 -root ((- (2 * p)) - ((2 -root (delta ((4 * r),(4 * p),1))) / 2))) - (a3 / 4) or z = (- (2 -root ((- (2 * p)) - ((2 -root (delta ((4 * r),(4 * p),1))) / 2)))) - (a3 / 4) ) )
by A8, A9;
2 -root 16 =
2 -real-root 16
by Th8
.=
2 -Root 16
by POWER:def 1
.=
4
by A10, PREPOWER:def 2
;
then (2 -root (delta ((4 * r),(4 * p),1))) / 4 =
2 -root ((16 * ((p * p) - r)) / 16)
by Th9
.=
s1
by A6, Th1
;
hence
( ((((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) ) )
by A3, A5, A7, A11; verum