let a, b be positive Real; :: thesis: for n being positive heavy Real holds (((2 * a) + b) to_power n) + (b to_power n) < (2 * (a + b)) to_power n
let n be positive heavy Real; :: thesis: (((2 * a) + b) to_power n) + (b to_power n) < (2 * (a + b)) to_power n
(((2 * a) + b) to_power n) + (b to_power n) < (((2 * a) + b) + b) to_power n by APB;
hence (((2 * a) + b) to_power n) + (b to_power n) < (2 * (a + b)) to_power n ; :: thesis: verum