let z, a0, a1, a2, a3, x, q, r, p be Complex; ( 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 implies ( ((((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 ) )
assume A1:
z = x - (a3 / 4)
; ( not p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 or not q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 or not r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 or ( ((((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 ) )
then A2:
4 * z = (4 * x) - a3
;
A3: 16 * (z |^ 2) =
(4 * 4) * (z |^ 2)
.=
(4 |^ 2) * (z |^ 2)
by Th1
.=
(4 * z) |^ 2
by NEWTON:7
.=
(((4 * x) |^ 2) - ((2 * (4 * x)) * a3)) + (a3 |^ 2)
by A2, Th4
.=
(((4 * x) * (4 * x)) - ((2 * (4 * x)) * a3)) + (a3 |^ 2)
by Th1
.=
((16 * (x * x)) - ((8 * x) * a3)) + (a3 |^ 2)
.=
((16 * (x |^ 2)) - ((8 * x) * a3)) + (a3 |^ 2)
by Th1
;
A4: (4 * x) |^ 3 =
(4 |^ 3) * (x |^ 3)
by NEWTON:7
.=
((4 * 4) * 4) * (x |^ 3)
by Th2
.=
64 * (x |^ 3)
;
A5: (4 * x) |^ 2 =
(4 |^ 2) * (x |^ 2)
by NEWTON:7
.=
(4 * 4) * (x |^ 2)
by Th1
.=
16 * (x |^ 2)
;
A6: (4 * a3) * (64 * (z |^ 3)) =
(4 * a3) * (((4 * 4) * 4) * (z |^ 3))
.=
(4 * a3) * ((4 |^ 3) * (z |^ 3))
by Th2
.=
(4 * a3) * (((4 * x) - a3) |^ 3)
by A2, NEWTON:7
.=
(4 * a3) * ((((64 * (x |^ 3)) - ((3 * (16 * (x |^ 2))) * a3)) + ((3 * (a3 |^ 2)) * (4 * x))) - (a3 |^ 3))
by A4, A5, Th5
.=
((((256 * a3) * (x |^ 3)) - ((192 * (a3 * a3)) * (x |^ 2))) + ((48 * ((a3 |^ 2) * a3)) * x)) - (4 * ((a3 |^ 3) * a3))
.=
((((256 * a3) * (x |^ 3)) - ((192 * (a3 |^ 2)) * (x |^ 2))) + ((48 * ((a3 |^ 2) * a3)) * x)) - (4 * ((a3 |^ 3) * a3))
by Th1
.=
((((256 * a3) * (x |^ 3)) - ((192 * (a3 |^ 2)) * (x |^ 2))) + ((48 * (a3 |^ (2 + 1))) * x)) - (4 * ((a3 |^ 3) * a3))
by NEWTON:6
.=
((((256 * a3) * (x |^ 3)) - ((192 * (a3 |^ 2)) * (x |^ 2))) + ((48 * (a3 |^ 3)) * x)) - (4 * (a3 |^ (3 + 1)))
by NEWTON:6
.=
((((256 * a3) * (x |^ 3)) - ((192 * (a3 |^ 2)) * (x |^ 2))) + ((48 * (a3 |^ 3)) * x)) - (4 * (a3 |^ 4))
;
A7: (4 * x) |^ 4 =
(4 |^ 4) * (x |^ 4)
by NEWTON:7
.=
(((4 * 4) * 4) * 4) * (x |^ 4)
by Th3
.=
256 * (x |^ 4)
;
A8: 256 * (z |^ 4) =
(((4 * 4) * 4) * 4) * (z |^ 4)
.=
(4 |^ 4) * (z |^ 4)
by Th3
.=
((4 * x) - a3) |^ 4
by A2, NEWTON:7
.=
((((256 * (x |^ 4)) - ((4 * (64 * (x |^ 3))) * a3)) + ((6 * (16 * (x |^ 2))) * (a3 |^ 2))) - ((4 * (a3 |^ 3)) * (4 * x))) + (a3 |^ 4)
by A7, A4, A5, Th6
.=
((((256 * (x |^ 4)) - ((256 * (x |^ 3)) * a3)) + ((96 * (x |^ 2)) * (a3 |^ 2))) - ((16 * (a3 |^ 3)) * x)) + (a3 |^ 4)
;
assume A9:
( 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 )
; ( ((((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 )
256 * (((((z |^ 4) + (a3 * (z |^ 3))) + (a2 * (z |^ 2))) + (a1 * z)) + a0) =
((((256 * (z |^ 4)) + ((4 * a3) * (64 * (z |^ 3)))) + ((16 * a2) * (16 * (z |^ 2)))) + ((64 * a1) * (4 * z))) + (256 * a0)
.=
((((((((256 * (x |^ 4)) - ((256 * (x |^ 3)) * a3)) + ((96 * (x |^ 2)) * (a3 |^ 2))) - ((16 * (a3 |^ 3)) * x)) + (a3 |^ 4)) + (((((256 * a3) * (x |^ 3)) - ((192 * (a3 |^ 2)) * (x |^ 2))) + ((48 * (a3 |^ 3)) * x)) - (4 * (a3 |^ 4)))) + ((16 * a2) * (((16 * (x |^ 2)) - ((8 * x) * a3)) + (a3 |^ 2)))) + ((64 * a1) * ((4 * x) - a3))) + (256 * a0)
by A1, A8, A6, A3
.=
256 * ((((x |^ 4) + ((4 * p) * (x |^ 2))) + ((8 * q) * x)) + (4 * r))
by A9
;
hence
( ((((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 )
; verum