let a, b, n be Nat; :: thesis: ( n > 0 & a <> b implies (2 * (a |^ n)) * (b |^ n) < (a |^ (2 * n)) + (b |^ (2 * n)) )
A0: ( (a |^ n) |^ 2 = a |^ (2 * n) & (b |^ n) |^ 2 = b |^ (2 * n) ) by NEWTON:9;
assume ( n > 0 & a <> b ) ; :: thesis: (2 * (a |^ n)) * (b |^ n) < (a |^ (2 * n)) + (b |^ (2 * n))
then ( n >= 1 & ( a > b or b > a ) ) by NAT_1:14, XXREAL_0:1;
then a |^ n <> b |^ n by PREPOWER:10;
hence (2 * (a |^ n)) * (b |^ n) < (a |^ (2 * n)) + (b |^ (2 * n)) by A0, Th55; :: thesis: verum