let a, b, c, m be Nat; :: thesis: ( (a |^ m) + (b |^ m) <= c |^ m implies a <= c )
assume A0: (a |^ m) + (b |^ m) <= c |^ m ; :: thesis: a <= c
( m = 0 implies (a |^ m) + (b |^ m) > c |^ m ) by Lm0;
then A2e: 0 + 1 <= m by A0, NAT_1:13;
(a |^ m) + (b |^ m) <= (c |^ m) + (b |^ m) by A0, NAT_1:12;
then ((a |^ m) + (b |^ m)) - (b |^ m) <= ((c |^ m) + (b |^ m)) - (b |^ m) by XREAL_1:9;
hence a <= c by A2e, PREPOWER:10; :: thesis: verum