theorem BPC: :: COMPLEX3:70

for a, b being positive Real
for n being non positive Real holds (a to_power n) + (b to_power n) > (a + b) to_power n