let p, q, y be Real; ( Polynom (1,0,p,q,y) = 0 implies for u, v being Real st y = u + v & ((3 * v) * u) + p = 0 holds
( (u |^ 3) + (v |^ 3) = - q & (u |^ 3) * (v |^ 3) = (- (p / 3)) |^ 3 ) )
assume A1:
Polynom (1,0,p,q,y) = 0
; for u, v being Real st y = u + v & ((3 * v) * u) + p = 0 holds
( (u |^ 3) + (v |^ 3) = - q & (u |^ 3) * (v |^ 3) = (- (p / 3)) |^ 3 )
let u, v be Real; ( y = u + v & ((3 * v) * u) + p = 0 implies ( (u |^ 3) + (v |^ 3) = - q & (u |^ 3) * (v |^ 3) = (- (p / 3)) |^ 3 ) )
assume that
A2:
y = u + v
and
A3:
((3 * v) * u) + p = 0
; ( (u |^ 3) + (v |^ 3) = - q & (u |^ 3) * (v |^ 3) = (- (p / 3)) |^ 3 )
(u + v) |^ 3 =
((u |^ 3) + (((3 * v) * (u ^2)) + ((3 * (v ^2)) * u))) + (v |^ 3)
by Th14
.=
((u |^ 3) + (((3 * v) * u) * (u + v))) + (v |^ 3)
;
then
0 = (((u |^ 3) + (v |^ 3)) + ((((3 * v) * u) + p) * (u + v))) + q
by A1, A2;
hence
(u |^ 3) + (v |^ 3) = - q
by A3; (u |^ 3) * (v |^ 3) = (- (p / 3)) |^ 3
3 * (v * u) = - p
by A3;
hence
(u |^ 3) * (v |^ 3) = (- (p / 3)) |^ 3
by NEWTON:7; verum