let x be Real; :: thesis: ( ((((x + 1) |^ 3) + ((x + 2) |^ 3)) + ((x + 3) |^ 3)) + ((x + 4) |^ 3) = (x + 10) |^ 3 iff x = 10 )
A1: (x + 1) |^ 3 = ((x + 1) * (x + 1)) * (x + 1) by POLYEQ_5:2;
A2: (x + 2) |^ 3 = ((x + 2) * (x + 2)) * (x + 2) by POLYEQ_5:2;
A3: (x + 3) |^ 3 = ((x + 3) * (x + 3)) * (x + 3) by POLYEQ_5:2;
A4: (x + 4) |^ 3 = ((x + 4) * (x + 4)) * (x + 4) by POLYEQ_5:2;
A5: (x + 10) |^ 3 = ((x + 10) * (x + 10)) * (x + 10) by POLYEQ_5:2;
thus ( ((((x + 1) |^ 3) + ((x + 2) |^ 3)) + ((x + 3) |^ 3)) + ((x + 4) |^ 3) = (x + 10) |^ 3 implies x = 10 ) :: thesis: ( x = 10 implies ((((x + 1) |^ 3) + ((x + 2) |^ 3)) + ((x + 3) |^ 3)) + ((x + 4) |^ 3) = (x + 10) |^ 3 )

proof

set t = x - 10;
assume ((((x + 1) |^ 3) + ((x + 2) |^ 3)) + ((x + 3) |^ 3)) + ((x + 4) |^ 3) = (x + 10) |^ 3 ; :: thesis: x = 10
then (x - 10) * ((((x - 10) * (x - 10)) + (30 * (x - 10))) + 230) = 0 by A1, A2, A3, A4, A5;
then A6: ( x - 10 = 0 or ((1 * ((x - 10) ^2)) + (30 * (x - 10))) + 230 = 0 ) ;
delta (1,30,230) = - 20 ;
hence x = 10 by A6, QUIN_1:3; :: thesis: verum

end;

thus ( x = 10 implies ((((x + 1) |^ 3) + ((x + 2) |^ 3)) + ((x + 3) |^ 3)) + ((x + 4) |^ 3) = (x + 10) |^ 3 ) by A1, A2, A3, A4, A5; :: thesis: verum