let n be Nat; :: thesis: ((((n + 1) |^ 3) + ((n + 2) |^ 3)) + ((n + 3) |^ 3)) + ((n + 4) |^ 3) <> (n + 5) |^ 3
assume A1: ((((n + 1) |^ 3) + ((n + 2) |^ 3)) + ((n + 3) |^ 3)) + ((n + 4) |^ 3) = (n + 5) |^ 3 ; :: thesis: contradiction
( (n + 1) |^ 3 = ((n + 1) * (n + 1)) * (n + 1) & (n + 2) |^ 3 = ((n + 2) * (n + 2)) * (n + 2) & (n + 3) |^ 3 = ((n + 3) * (n + 3)) * (n + 3) & (n + 4) |^ 3 = ((n + 4) * (n + 4)) * (n + 4) & (n + 5) |^ 3 = ((n + 5) * (n + 5)) * (n + 5) ) by POLYEQ_5:2;
then A2: 3 * ((((n * n) * n) + ((5 * n) * n)) + (5 * n)) = 25 by A1;
not 3 divides (3 * 8) + 1 by NAT_4:9;
hence contradiction by A2; :: thesis: verum