theorem :: NEWTON02:184

for a, b, c being Nat holds
( not (a |^ 2) + (b |^ 2) = c |^ 2 or 5 divides a or 5 divides b or 5 divides c )