let z, a0, a1, a2, x, q, r be Complex; ( z = x - (a2 / 3) & q = ((3 * a1) - (a2 |^ 2)) / 9 & r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 implies ( (((z |^ 3) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ((x |^ 3) + ((3 * q) * x)) - (2 * r) = 0 ) )
assume A1:
z = x - (a2 / 3)
; ( not q = ((3 * a1) - (a2 |^ 2)) / 9 or not r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 or ( (((z |^ 3) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ((x |^ 3) + ((3 * q) * x)) - (2 * r) = 0 ) )
then A2:
3 * z = (3 * x) - a2
;
A3: (3 * x) |^ 2 =
(3 |^ 2) * (x |^ 2)
by NEWTON:7
.=
(3 * 3) * (x |^ 2)
by Th1
.=
9 * (x |^ 2)
;
A4: (3 * x) |^ 3 =
(3 |^ 3) * (x |^ 3)
by NEWTON:7
.=
((3 * 3) * 3) * (x |^ 3)
by Th2
.=
27 * (x |^ 3)
;
A5: 27 * (z |^ 3) =
((3 * 3) * 3) * (z |^ 3)
.=
(3 |^ 3) * (z |^ 3)
by Th2
.=
((3 * x) - a2) |^ 3
by A2, NEWTON:7
.=
(((27 * (x |^ 3)) - ((3 * (9 * (x |^ 2))) * a2)) + ((3 * (a2 |^ 2)) * (3 * x))) - (a2 |^ 3)
by A4, A3, Th5
.=
(((27 * (x |^ 3)) - ((27 * a2) * (x |^ 2))) + ((9 * (a2 |^ 2)) * x)) - (a2 |^ 3)
;
assume A6:
( q = ((3 * a1) - (a2 |^ 2)) / 9 & r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 )
; ( (((z |^ 3) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ((x |^ 3) + ((3 * q) * x)) - (2 * r) = 0 )
A7:
(27 * a1) * z = ((27 * a1) * x) - ((9 * a2) * a1)
by A1;
((27 * 1) * a2) * (z |^ 2) =
(((3 * a2) * (3 * 3)) * (1 * 1)) * (z |^ 2)
.=
((3 * a2) * (3 |^ 2)) * (z |^ 2)
by Th1
.=
(3 * a2) * ((3 |^ 2) * (z |^ 2))
.=
(3 * a2) * ((3 * z) |^ 2)
by NEWTON:7
.=
(3 * a2) * ((((3 * x) |^ 2) - ((2 * (3 * x)) * a2)) + (a2 |^ 2))
by A2, Th4
.=
(3 * a2) * ((((3 * x) * (3 * x)) - ((2 * (3 * x)) * a2)) + (a2 |^ 2))
by Th1
.=
((((27 * a2) * x) * x) - (((2 * (3 * x)) * a2) * (3 * a2))) + ((a2 |^ 2) * (3 * a2))
.=
(((27 * a2) * (x * x)) - ((18 * (a2 * a2)) * x)) + ((3 * a2) * (a2 * a2))
by Th1
.=
(((27 * a2) * (x |^ 2)) - ((18 * (a2 * a2)) * x)) + (((3 * a2) * a2) * a2)
by Th1
.=
(((27 * a2) * (x |^ 2)) - ((18 * (a2 |^ 2)) * x)) + (3 * ((a2 * a2) * a2))
by Th1
.=
(((27 * a2) * (x |^ 2)) - ((18 * (a2 |^ 2)) * x)) + (3 * (a2 |^ 3))
by Th2
;
then 27 * ((((z |^ 3) + (a2 * (z |^ 2))) + (a1 * z)) + a0) =
((27 * (x |^ 3)) + (((- (9 * (a2 |^ 2))) + (27 * a1)) * x)) + (((2 * (a2 |^ 3)) - ((9 * a2) * a1)) + (27 * a0))
by A5, A7
.=
27 * (((x |^ 3) + ((3 * q) * x)) - (2 * r))
by A6
;
hence
( (((z |^ 3) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ((x |^ 3) + ((3 * q) * x)) - (2 * r) = 0 )
; verum