let a, b be positive Real; :: thesis: for n being non positive Real holds (a to_power n) + (b to_power n) > (a + b) to_power n
let n be non positive Real; :: thesis: (a to_power n) + (b to_power n) > (a + b) to_power n
reconsider k = a / b as positive Real ;
k + 1 = (a / b) + (b / b) by XCMPLX_1:60
.= (a + b) / b ;
then A1: ( (k + 1) * b = a + b & k * b = a ) by XCMPLX_1:87;
A2: ( ((k + 1) to_power n) * (b to_power n) = ((k + 1) * b) to_power n & (k to_power n) * (b to_power n) = (k * b) to_power n ) by POWER:30;
((k + 1) to_power n) * (b to_power n) < ((k to_power n) + 1) * (b to_power n) by XREAL_1:68, LMN;
hence (a to_power n) + (b to_power n) > (a + b) to_power n by A1, A2; :: thesis: verum