let a, b be positive Real; :: thesis: for n, k being Nat st n >= 1 & k >= 1 holds
((a |^ k) + (b |^ k)) * ((a |^ n) + (b |^ n)) <= 2 * ((a |^ (k + n)) + (b |^ (k + n)))
let n, k be Nat; :: thesis: ( n >= 1 & k >= 1 implies ((a |^ k) + (b |^ k)) * ((a |^ n) + (b |^ n)) <= 2 * ((a |^ (k + n)) + (b |^ (k + n))) )
assume that
A1: n >= 1 and
A2: k >= 1 ; :: thesis: ((a |^ k) + (b |^ k)) * ((a |^ n) + (b |^ n)) <= 2 * ((a |^ (k + n)) + (b |^ (k + n)))
A3: (((a |^ k) + (b |^ k)) * ((a |^ n) + (b |^ n))) - (2 * ((a |^ (k + n)) + (b |^ (k + n)))) = ((((((a |^ k) * (a |^ n)) + ((a |^ k) * (b |^ n))) + ((b |^ k) * (a |^ n))) + ((b |^ k) * (b |^ n))) - (2 * (a |^ (k + n)))) - (2 * (b |^ (k + n)))
.= (((((a |^ (k + n)) + ((a |^ k) * (b |^ n))) + ((b |^ k) * (a |^ n))) + ((b |^ k) * (b |^ n))) - (2 * (a |^ (k + n)))) - (2 * (b |^ (k + n))) by NEWTON:8
.= (((((a |^ (k + n)) + ((a |^ k) * (b |^ n))) + ((b |^ k) * (a |^ n))) + (b |^ (k + n))) - (2 * (a |^ (k + n)))) - (2 * (b |^ (k + n))) by NEWTON:8
.= ((((a |^ k) * (b |^ n)) + ((b |^ k) * (a |^ n))) - (a |^ (k + n))) - (b |^ (k + n))
.= ((((a |^ k) * (b |^ n)) + ((b |^ k) * (a |^ n))) - ((a |^ k) * (a |^ n))) - (b |^ (k + n)) by NEWTON:8
.= ((((a |^ k) * (b |^ n)) + ((b |^ k) * (a |^ n))) - ((a |^ k) * (a |^ n))) - ((b |^ k) * (b |^ n)) by NEWTON:8
.= ((a |^ n) - (b |^ n)) * ((b |^ k) - (a |^ k)) ;

per cases ( a - b > 0 or a - b = 0 or a - b < 0 ) ;

suppose a - b > 0 ; :: thesis: ((a |^ k) + (b |^ k)) * ((a |^ n) + (b |^ n)) <= 2 * ((a |^ (k + n)) + (b |^ (k + n)))

then A4: (a - b) + b > 0 + b by XREAL_1:8;
then a |^ k > b |^ k by A2, PREPOWER:10;
then A5: (b |^ k) - (a |^ k) < 0 by XREAL_1:49;
a |^ n > b |^ n by A1, A4, PREPOWER:10;
then (a |^ n) - (b |^ n) > 0 by XREAL_1:50;
hence ((a |^ k) + (b |^ k)) * ((a |^ n) + (b |^ n)) <= 2 * ((a |^ (k + n)) + (b |^ (k + n))) by A3, A5, XREAL_1:48; :: thesis: verum

end;

suppose a - b = 0 ; :: thesis: ((a |^ k) + (b |^ k)) * ((a |^ n) + (b |^ n)) <= 2 * ((a |^ (k + n)) + (b |^ (k + n)))

then a |^ n = b |^ n ;
hence ((a |^ k) + (b |^ k)) * ((a |^ n) + (b |^ n)) <= 2 * ((a |^ (k + n)) + (b |^ (k + n))) by A3; :: thesis: verum

end;

suppose a - b < 0 ; :: thesis: ((a |^ k) + (b |^ k)) * ((a |^ n) + (b |^ n)) <= 2 * ((a |^ (k + n)) + (b |^ (k + n)))

then A6: (a - b) + b < 0 + b by XREAL_1:8;
then a |^ k < b |^ k by A2, PREPOWER:10;
then A7: (b |^ k) - (a |^ k) > 0 by XREAL_1:50;
a |^ n < b |^ n by A1, A6, PREPOWER:10;
then (a |^ n) - (b |^ n) < 0 by XREAL_1:49;
hence ((a |^ k) + (b |^ k)) * ((a |^ n) + (b |^ n)) <= 2 * ((a |^ (k + n)) + (b |^ (k + n))) by A3, A7, XREAL_1:48; :: thesis: verum

end;

end;