let n be Element of NAT ; :: thesis: ( n >= 1 implies (2 to_power (n + 1)) - (2 to_power n) > 1 )
assume A1: n >= 1 ; :: thesis: (2 to_power (n + 1)) - (2 to_power n) > 1
2 to_power n >= 2 to_power 1 by A1, PRE_FF:10;
then (2 to_power n) * 1 >= 2 by POWER:30;
then ((2 to_power n) * 2) - ((2 to_power n) * 1) > 1 by XXREAL_0:2;
then ((2 to_power n) * (2 to_power 1)) - (2 to_power n) > 1 by POWER:30;
hence (2 to_power (n + 1)) - (2 to_power n) > 1 by POWER:32; :: thesis: verum