let a, b be positive Real; :: thesis: for n being positive Real holds
( 2 * ((a + b) to_power n) > ((a + b) to_power n) + (a to_power n) & ((a + b) to_power n) + (a to_power n) > 2 * (a to_power n) )
let n be positive Real; :: thesis: ( 2 * ((a + b) to_power n) > ((a + b) to_power n) + (a to_power n) & ((a + b) to_power n) + (a to_power n) > 2 * (a to_power n) )
a + b > a + 0 by XREAL_1:6;
then (a + b) to_power n > a to_power n by POWER:37;
then ( ((a + b) to_power n) + ((a + b) to_power n) > ((a + b) to_power n) + (a to_power n) & ((a + b) to_power n) + (a to_power n) > (a to_power n) + (a to_power n) ) by XREAL_1:6;
hence ( 2 * ((a + b) to_power n) > ((a + b) to_power n) + (a to_power n) & ((a + b) to_power n) + (a to_power n) > 2 * (a to_power n) ) ; :: thesis: verum