theorem :: COMPLEX3:88

for a, b, n being positive Real holds
( 2 * ((a + b) to_power n) > ((a + b) to_power n) + (a to_power n) & ((a + b) to_power n) + (a to_power n) > 2 * (a to_power n) )