let p, q, y be real number ; :: thesis: ( Polynom 1,0 ,p,q,y = 0 implies for u, v being real number 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 number 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 number ; :: thesis: ( y = u + v & ((3 * v) * u) + p = 0 implies ( (u |^ 3) + (v |^ 3) = - q & (u |^ 3) * (v |^ 3) = (- (p / 3)) |^ 3 ) )
assume A2: ( y = u + v & ((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 A3: 0 = (((u |^ 3) + (v |^ 3)) + ((((3 * v) * u) + p) * (u + v))) + q by A1, A2;
A4: 3 * (v * u) = - p by A2;
thus (u |^ 3) + (v |^ 3) = - q by A2, A3; :: thesis: (u |^ 3) * (v |^ 3) = (- (p / 3)) |^ 3
thus (u |^ 3) * (v |^ 3) = (- (p / 3)) |^ 3 by A4, NEWTON:12; :: thesis: verum