theorem :: COMPLEX3:52

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