let a, b be positive Real; :: thesis: for n being Nat st n >= 1 holds
(a |^ (n + 1)) + (b |^ (n + 1)) >= ((a |^ n) * b) + (a * (b |^ n))
let n be Nat; :: thesis: ( n >= 1 implies (a |^ (n + 1)) + (b |^ (n + 1)) >= ((a |^ n) * b) + (a * (b |^ n)) )
assume A1: n >= 1 ; :: thesis: (a |^ (n + 1)) + (b |^ (n + 1)) >= ((a |^ n) * b) + (a * (b |^ n))

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

suppose A2: a - b > 0 ; :: thesis: (a |^ (n + 1)) + (b |^ (n + 1)) >= ((a |^ n) * b) + (a * (b |^ n))

then (a - b) + b > 0 + b by XREAL_1:8;
then a |^ n > b |^ n by A1, PREPOWER:10;
then (a |^ n) - (b |^ n) > 0 by XREAL_1:50;
then (a - b) * ((a |^ n) - (b |^ n)) > 0 by A2;
then (((a * (a |^ n)) - (a * (b |^ n))) - (b * (a |^ n))) + (b * (b |^ n)) > 0 ;
then (((a |^ (n + 1)) - (a * (b |^ n))) - (b * (a |^ n))) + (b * (b |^ n)) > 0 by NEWTON:6;
then (((a |^ (n + 1)) - (a * (b |^ n))) - (b * (a |^ n))) + (b |^ (n + 1)) > 0 by NEWTON:6;
then ((((a |^ (n + 1)) + (b |^ (n + 1))) - (a * (b |^ n))) - (b * (a |^ n))) + ((a * (b |^ n)) + (b * (a |^ n))) > 0 + ((a * (b |^ n)) + (b * (a |^ n))) by XREAL_1:8;
hence (a |^ (n + 1)) + (b |^ (n + 1)) >= ((a |^ n) * b) + (a * (b |^ n)) ; :: thesis: verum

end;

suppose A3: a - b = 0 ; :: thesis: (a |^ (n + 1)) + (b |^ (n + 1)) >= ((a |^ n) * b) + (a * (b |^ n))

then ((a |^ n) * b) + (a * (b |^ n)) = (a |^ (n + 1)) + ((a |^ n) * a) by NEWTON:6
.= (a |^ (n + 1)) + (a |^ (n + 1)) by NEWTON:6
.= 2 * (a |^ (n + 1)) ;
hence (a |^ (n + 1)) + (b |^ (n + 1)) >= ((a |^ n) * b) + (a * (b |^ n)) by A3; :: thesis: verum

end;

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

then (a - b) + b < 0 + b by XREAL_1:8;
then a |^ n < b |^ n by A1, PREPOWER:10;
then (a |^ n) - (b |^ n) < 0 by XREAL_1:49;
then (a - b) * ((a |^ n) - (b |^ n)) > 0 by A4;
then (((a * (a |^ n)) - (a * (b |^ n))) - (b * (a |^ n))) + (b * (b |^ n)) > 0 ;
then (((a |^ (n + 1)) - (a * (b |^ n))) - (b * (a |^ n))) + (b * (b |^ n)) > 0 by NEWTON:6;
then (((a |^ (n + 1)) - (a * (b |^ n))) - (b * (a |^ n))) + (b |^ (n + 1)) > 0 by NEWTON:6;
then ((((a |^ (n + 1)) + (b |^ (n + 1))) - (a * (b |^ n))) - (b * (a |^ n))) + ((a * (b |^ n)) + (b * (a |^ n))) > 0 + ((a * (b |^ n)) + (b * (a |^ n))) by XREAL_1:8;
hence (a |^ (n + 1)) + (b |^ (n + 1)) >= ((a |^ n) * b) + (a * (b |^ n)) ; :: thesis: verum

end;

end;