theorem :: COMPLEX3:84

for a, b being positive Real
for n being positive heavy Real holds (((2 * a) + b) to_power n) + (b to_power n) < (2 * (a + b)) to_power n