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