let p, q, y be Real; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( (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; :: thesis: (u |^ 3) * (v |^ 3) = (- (p / 3)) |^ 3
3 * (v * u) = - p by A3;
hence (u |^ 3) * (v |^ 3) = (- (p / 3)) |^ 3 by NEWTON:7; :: thesis: verum