let a, b, c, m be Nat; ( c |^ m >= (a |^ m) + (b |^ m) & a > 0 & b > 0 implies c |^ (m + 1) > (a |^ (m + 1)) + (b |^ (m + 1)) )
assume A0:
( c |^ m >= (a |^ m) + (b |^ m) & a > 0 & b > 0 )
; c |^ (m + 1) > (a |^ (m + 1)) + (b |^ (m + 1))
consider x being Nat such that
A0b:
c = a + x
by A0, Th6, NAT_1:10;
A1:
( (a + x) |^ m >= (a |^ m) + (b |^ m) & a > 0 & x > 0 )
by A0, A0b, Lm5d;
A2a:
a |^ m > 0
by A0, PREPOWER:6;
then A3:
(a + x) |^ m > b |^ m
by A0, A0b, XREAL_1:39;
A4:
a + x > b
by A3, Lm3a;
A5:
((a + x) |^ m) * (a + x) >= ((a |^ m) + (b |^ m)) * (a + x)
by A0, A0b, XREAL_1:66;
A7:
b |^ m > 0
by A0, PREPOWER:6;
A8:
(a |^ m) * (a + x) > (a |^ m) * a
by A1, NAT_1:16, A2a, XREAL_1:68;
(b |^ m) * (a + x) > (b |^ m) * b
by A4, A7, XREAL_1:68;
then
((a |^ m) * (a + x)) + ((b |^ m) * (a + x)) > ((a |^ m) * a) + ((b |^ m) * b)
by A8, XREAL_1:8;
then A12:
((a + x) |^ m) * (a + x) > ((a |^ m) * a) + ((b |^ m) * b)
by A5, XXREAL_0:2;
( (a |^ m) * a = a |^ (m + 1) & (b |^ m) * b = b |^ (m + 1) )
by NEWTON:6;
hence
c |^ (m + 1) > (a |^ (m + 1)) + (b |^ (m + 1))
by A0b, A12, NEWTON:6; verum