defpred S₁[ Nat] means 2 to_power $1 > $1 to_power 6;
A1: for n being Nat st n >= 30 & S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( n >= 30 & S₁[n] implies S₁[n + 1] )
assume that
A2: n >= 30 and
A3: 2 to_power n > n to_power 6 ; :: thesis: S₁[n + 1]
n >= 9 by A2, XXREAL_0:2;
then A4: (n + 1) to_power 6 < 2 * (n to_power 6) by Lm29;
A5: 2 to_power (n + 1) = (2 to_power n) * (2 to_power 1) by POWER:27
.= (2 to_power n) * 2 by POWER:25 ;
(2 to_power n) * 2 > (n to_power 6) * 2 by A3, XREAL_1:68;
hence S₁[n + 1] by A5, A4, XXREAL_0:2; :: thesis: verum

end;

2 to_power 30 = 2 to_power (5 * 6)
.= 32 to_power 6 by POWER:33, POWER:63 ;
then A6: S₁[30] by POWER:37;
for n being Nat st n >= 30 holds
S₁[n] from NAT_1:sch 8(A6, A1);
hence for n being Element of NAT st n >= 30 holds
2 to_power n > n to_power 6 ; :: thesis: verum