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 is heavy & n is positive ) )
let n be Real; :: thesis: ( (a + b) to_power n > (a to_power n) + (b to_power n) iff ( n is heavy & n is positive ) )
( ( not n is heavy or not n is positive ) implies (a + b) to_power n <= (a to_power n) + (b to_power n) )

proof

assume ( not n is heavy or not n is positive ) ; :: thesis: (a + b) to_power n <= (a to_power n) + (b to_power n)
then n <= 1 by TA1;

per cases then ( n = 1 or n < 1 ) by XXREAL_0:1;

suppose n = 1 ; :: thesis: (a + b) to_power n <= (a to_power n) + (b to_power n)

hence (a + b) to_power n <= (a to_power n) + (b to_power n) ; :: thesis: verum

end;

suppose B1: n < 1 ; :: thesis: (a + b) to_power n <= (a to_power n) + (b to_power n)

per cases ( n is positive or not n is positive ) ;

suppose n is positive ; :: thesis: (a + b) to_power n <= (a to_power n) + (b to_power n)

then ( n is light & n is positive ) by B1, TA1;
hence (a + b) to_power n <= (a to_power n) + (b to_power n) by BPA; :: thesis: verum

end;

suppose not n is positive ; :: thesis: (a + b) to_power n <= (a to_power n) + (b to_power n)

hence (a + b) to_power n <= (a to_power n) + (b to_power n) by BPC; :: thesis: verum

end;

end;

end;

end;

end;

hence ( (a + b) to_power n > (a to_power n) + (b to_power n) iff ( n is heavy & n is positive ) ) by APB; :: thesis: verum