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

per cases then ( 5 divides c or 5 divides (c |^ 2) - 1 or 5 divides (c |^ 2) + 1 ) by Th70, PEPIN:59;

suppose 5 divides c ; :: thesis: ( 5 divides a or 5 divides b or 5 divides c )

hence ( 5 divides a or 5 divides b or 5 divides c ) ; :: thesis: verum

end;

suppose B1: 5 divides (c |^ 2) - 1 ; :: thesis: ( 5 divides a or 5 divides b or 5 divides c )

per cases ( 5 divides b or 5 divides (b |^ 2) - 1 or 5 divides (b |^ 2) + 1 ) by A2, Th70, PEPIN:59;

suppose 5 divides b ; :: thesis: ( 5 divides a or 5 divides b or 5 divides c )

hence ( 5 divides a or 5 divides b or 5 divides c ) ; :: thesis: verum

end;

suppose 5 divides (b |^ 2) - 1 ; :: thesis: ( 5 divides a or 5 divides b or 5 divides c )

then 5 divides a |^ 2 by A1a, B1, INT_2:1;
hence ( 5 divides a or 5 divides b or 5 divides c ) by NAT_3:5, PEPIN:59; :: thesis: verum

end;

suppose 5 divides (b |^ 2) + 1 ; :: thesis: ( 5 divides a or 5 divides b or 5 divides c )

hence ( 5 divides a or 5 divides b or 5 divides c ) by A1a, B1, INT_2:1, Th85; :: thesis: verum

end;

end;

end;

suppose B2: 5 divides (c |^ 2) + 1 ; :: thesis: ( 5 divides a or 5 divides b or 5 divides c )

per cases ( 5 divides b or 5 divides (b |^ 2) + 1 or 5 divides (b |^ 2) - 1 ) by A2, Th70, PEPIN:59;

suppose 5 divides b ; :: thesis: ( 5 divides a or 5 divides b or 5 divides c )

hence ( 5 divides a or 5 divides b or 5 divides c ) ; :: thesis: verum

end;

suppose 5 divides (b |^ 2) + 1 ; :: thesis: ( 5 divides a or 5 divides b or 5 divides c )

then 5 divides a |^ 2 by A1b, B2, INT_2:1;
hence ( 5 divides a or 5 divides b or 5 divides c ) by NAT_3:5, PEPIN:59; :: thesis: verum

end;

suppose 5 divides (b |^ 2) - 1 ; :: thesis: ( 5 divides a or 5 divides b or 5 divides c )

hence ( 5 divides a or 5 divides b or 5 divides c ) by A1b, B2, INT_2:1, Th85; :: thesis: verum

end;

end;

end;

end;