let a, b, c be Nat; ( 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
; ( 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
;