let a, b, c be Nat; :: thesis: ( 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 ; :: thesis: ( 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 ;
per cases then ( 7 divides c or 7 divides (c |^ 3) - 1 or 7 divides (c |^ 3) + 1 ) by ;
suppose 7 divides c ; :: thesis: ( 7 divides a or 7 divides b or 7 divides c )
hence ( 7 divides a or 7 divides b or 7 divides c ) ; :: thesis: verum
end;
suppose B1: 7 divides (c |^ 3) - 1 ; :: thesis: ( 7 divides a or 7 divides b or 7 divides c )
per cases ( 7 divides b or 7 divides (b |^ 3) - 1 or 7 divides (b |^ 3) + 1 ) by ;
suppose 7 divides b ; :: thesis: ( 7 divides a or 7 divides b or 7 divides c )
hence ( 7 divides a or 7 divides b or 7 divides c ) ; :: thesis: verum
end;
suppose 7 divides (b |^ 3) - 1 ; :: thesis: ( 7 divides a or 7 divides b or 7 divides c )
then 7 divides a |^ 3 by ;
hence ( 7 divides a or 7 divides b or 7 divides c ) by ; :: thesis: verum
end;
suppose 7 divides (b |^ 3) + 1 ; :: thesis: ( 7 divides a or 7 divides b or 7 divides c )
hence ( 7 divides a or 7 divides b or 7 divides c ) by ; :: thesis: verum
end;
end;
end;
suppose B2: 7 divides (c |^ 3) + 1 ; :: thesis: ( 7 divides a or 7 divides b or 7 divides c )
per cases ( 7 divides b or 7 divides (b |^ 3) + 1 or 7 divides (b |^ 3) - 1 ) by ;
suppose 7 divides b ; :: thesis: ( 7 divides a or 7 divides b or 7 divides c )
hence ( 7 divides a or 7 divides b or 7 divides c ) ; :: thesis: verum
end;
suppose 7 divides (b |^ 3) + 1 ; :: thesis: ( 7 divides a or 7 divides b or 7 divides c )
then 7 divides a |^ 3 by ;
hence ( 7 divides a or 7 divides b or 7 divides c ) by ; :: thesis: verum
end;
suppose 7 divides (b |^ 3) - 1 ; :: thesis: ( 7 divides a or 7 divides b or 7 divides c )
hence ( 7 divides a or 7 divides b or 7 divides c ) by ; :: thesis: verum
end;
end;
end;
end;