theorem :: COMPLEX3:63

for a, b being positive Real
for m being non positive Real
for n being negative Real st (a to_power m) + (b to_power m) <= 1 holds
(a to_power (m + n)) + (b to_power (m + n)) < 1