let a, b be real positive number ; :: thesis: for n, k being Element of 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 Element of NAT ; :: thesis: ( n >= 1 & k >= 1 implies ((a |^ k) + (b |^ k)) * ((a |^ n) + (b |^ n)) <= 2 * ((a |^ (k + n)) + (b |^ (k + n))) )
assume A1: ( n >= 1 & k >= 1 ) ; :: thesis: ((a |^ k) + (b |^ k)) * ((a |^ n) + (b |^ n)) <= 2 * ((a |^ (k + n)) + (b |^ (k + n)))
A2: (((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:13
.= (((((a |^ (k + n)) + ((a |^ k) * (b |^ n))) + ((b |^ k) * (a |^ n))) + (b |^ (k + n))) - (2 * (a |^ (k + n)))) - (2 * (b |^ (k + n))) by NEWTON:13
.= ((((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:13
.= ((((a |^ k) * (b |^ n)) + ((b |^ k) * (a |^ n))) - ((a |^ k) * (a |^ n))) - ((b |^ k) * (b |^ n)) by NEWTON:13
.= ((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 (a - b) + b > 0 + b by XREAL_1:10;
then A3: ( a |^ n > b |^ n & a |^ k > b |^ k ) by A1, PREPOWER:18;
then A4: (a |^ n) - (b |^ n) > 0 by XREAL_1:52;
(b |^ k) - (a |^ k) < 0 by A3, XREAL_1:51;
then (((a |^ k) + (b |^ k)) * ((a |^ n) + (b |^ n))) - (2 * ((a |^ (k + n)) + (b |^ (k + n)))) < 0 by A2, A4;
hence ((a |^ k) + (b |^ k)) * ((a |^ n) + (b |^ n)) <= 2 * ((a |^ (k + n)) + (b |^ (k + n))) by XREAL_1:50; :: 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 & a |^ k = b |^ k ) ;
hence ((a |^ k) + (b |^ k)) * ((a |^ n) + (b |^ n)) <= 2 * ((a |^ (k + n)) + (b |^ (k + n))) by A2; :: 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 - b) + b < 0 + b by XREAL_1:10;
then A5: ( a |^ n < b |^ n & a |^ k < b |^ k ) by A1, PREPOWER:18;
then A6: (a |^ n) - (b |^ n) < 0 by XREAL_1:51;
(b |^ k) - (a |^ k) > 0 by A5, XREAL_1:52;
then (((a |^ k) + (b |^ k)) * ((a |^ n) + (b |^ n))) - (2 * ((a |^ (k + n)) + (b |^ (k + n)))) < 0 by A2, A6;
hence ((a |^ k) + (b |^ k)) * ((a |^ n) + (b |^ n)) <= 2 * ((a |^ (k + n)) + (b |^ (k + n))) by XREAL_1:50; :: thesis: verum

end;

end;