theorem :: COMPLEX3:86

for a being positive light Real
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 )