let a, b be positive Real; :: thesis: for n being non trivial Nat holds (a + b) |^ n > (a |^ n) + (b |^ n)
let n be non trivial Nat; :: thesis: (a + b) |^ n > (a |^ n) + (b |^ n)
reconsider m = n - 1 as non zero Nat ;
reconsider c = max (a,b), d = min (a,b) as positive Real ;
A1: ( c * (c |^ m) = c |^ (m + 1) & d * (d |^ m) = d |^ (m + 1) & (c + d) * ((c + d) |^ m) = (c + d) |^ (m + 1) ) by NEWTON:6;
A2: ( c |^ n = max ((a |^ n),(b |^ n)) & d |^ n = min ((a |^ n),(b |^ n)) ) by MM1;
( c + d > c + 0 & c + d > 0 + d ) by XREAL_1:6;
then ( (c + d) |^ m > c |^ m & (c + d) |^ m > d |^ m ) by NEWTON02:40;
then ( c * ((c + d) |^ m) > c * (c |^ m) & d * ((c + d) |^ m) > d * (d |^ m) ) by XREAL_1:68;
then ( c * ((c + d) |^ m) > c |^ (m + 1) & d * ((c + d) |^ m) > d |^ (m + 1) ) by NEWTON:6;
then A3: (c * ((c + d) |^ m)) + (d * ((c + d) |^ m)) > (c |^ (m + 1)) + (d |^ (m + 1)) by XREAL_1:8;
(a + b) |^ (m + 1) = (c * ((c + d) |^ m)) + (d * ((c + d) |^ m)) by A1, MinMax;
hence (a + b) |^ n > (a |^ n) + (b |^ n) by A2, A3, MinMax; :: thesis: verum