let a be positive light Real; :: thesis: for n being positive heavy Real holds
( 2 to_power n > ((1 + a) to_power n) - ((1 - a) to_power n) & ((1 + a) to_power n) - ((1 - a) to_power n) > (2 * a) to_power n )
let n be positive heavy Real; :: thesis: ( 2 to_power n > ((1 + a) to_power n) - ((1 - a) to_power n) & ((1 + a) to_power n) - ((1 - a) to_power n) > (2 * a) to_power n )
A1: ( a < 1 & n > 1 ) by TA1;
1 + a = (1 - a) + (2 * a) ;
then A2: ((1 + a) to_power n) - ((1 - a) to_power n) > (((1 - a) to_power n) + ((2 * a) to_power n)) - ((1 - a) to_power n) by APB, XREAL_1:9;
1 + 1 > 1 + a by A1, XREAL_1:6;
then 2 to_power n > (1 + a) to_power n by POWER:37;
then (2 to_power n) - 0 > ((1 + a) to_power n) - ((1 - a) to_power n) by XREAL_1:14;
hence ( 2 to_power n > ((1 + a) to_power n) - ((1 - a) to_power n) & ((1 + a) to_power n) - ((1 - a) to_power n) > (2 * a) to_power n ) by A2; :: thesis: verum