let a, b be positive Real; :: thesis:
let n be Real; :: thesis:
( ( 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:
then n <= 1 by TA1;

per cases by XXREAL_0:1;

suppose n = 1 ; :: thesis:

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

end;

suppose B1: n < 1 ; :: thesis:

per cases ;

suppose n is positive ; :: thesis:

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:

end;

suppose not n is positive ; :: thesis:

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

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: