theorem :: SERIES_5:43

for a, b being positive Real
for n being Nat st n >= 1 holds
(a |^ (n + 1)) + (b |^ (n + 1)) >= ((a |^ n) * b) + (a * (b |^ n))