theorem :: NEWTON01:12

for a, b, c, m being Nat st (a |^ m) + (b |^ m) <= c |^ m holds
ex x being Nat st (a |^ m) + (b |^ m) <= (a + x) |^ m