let a, b, c be Nat; ( not (a |^ 3) + (b |^ 3) = c |^ 3 or 7 divides a or 7 divides b or 7 divides c )
assume A1:
(a |^ 3) + (b |^ 3) = c |^ 3
; ( 7 divides a or 7 divides b or 7 divides c )
A1a:
( (a |^ 3) + ((b |^ 3) - 1) = (c |^ 3) - 1 & ((a |^ 3) - 2) + ((b |^ 3) + 1) = (c |^ 3) - 1 )
by A1;
A1b:
( (a |^ 3) + ((b |^ 3) + 1) = (c |^ 3) + 1 & ((a |^ 3) + 2) + ((b |^ 3) - 1) = (c |^ 3) + 1 )
by A1;
A2:
(2 * 3) + 1 = 7
;