let r be Real; :: thesis: ( ((r |^ 3) + ((r + 1) |^ 3)) + ((r + 2) |^ 3) = (r + 3) |^ 3 iff r = 3 )
A1: ( r |^ 3 = (r * r) * r & (r + 1) |^ 3 = ((r + 1) * (r + 1)) * (r + 1) & (r + 2) |^ 3 = ((r + 2) * (r + 2)) * (r + 2) & (r + 3) |^ 3 = ((r + 3) * (r + 3)) * (r + 3) ) by POLYEQ_5:2;
thus ( ((r |^ 3) + ((r + 1) |^ 3)) + ((r + 2) |^ 3) = (r + 3) |^ 3 implies r = 3 ) :: thesis: ( r = 3 implies ((r |^ 3) + ((r + 1) |^ 3)) + ((r + 2) |^ 3) = (r + 3) |^ 3 )

proof

set t = r - 3;
assume ((r |^ 3) + ((r + 1) |^ 3)) + ((r + 2) |^ 3) = (r + 3) |^ 3 ; :: thesis: r = 3
then A2: (2 * (r - 3)) * ((((r - 3) * (r - 3)) + (9 * (r - 3))) + 21) = 0 by A1;
delta (1,9,21) < 0 ;
then ((1 * ((r - 3) ^2)) + (9 * (r - 3))) + 21 > 0 by QUIN_1:3;
then 2 * (r - 3) = 0 by A2;
hence r = 3 ; :: thesis: verum

end;

thus ( r = 3 implies ((r |^ 3) + ((r + 1) |^ 3)) + ((r + 2) |^ 3) = (r + 3) |^ 3 ) by A1; :: thesis: verum