let a, b be positive Real; :: thesis: for n being Real holds
( (a + b) to_power n < (a to_power n) + (b to_power n) iff n < 1 )
let n be Real; :: thesis: ( (a + b) to_power n < (a to_power n) + (b to_power n) iff n < 1 )
( ( n is heavy & n is positive ) iff n > 1 ) by TA1;
then ( (a + b) to_power n <= (a to_power n) + (b to_power n) iff n <= 1 ) by LME;
hence ( (a + b) to_power n < (a to_power n) + (b to_power n) iff n < 1 ) by NE1, XXREAL_0:1; :: thesis: verum