defpred S₁[ Nat] means 2 to_power ($1 - 1) > (2 * $1) ^2 ;
A1: for n being Nat st n >= 10 & S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( n >= 10 & S₁[n] implies S₁[n + 1] )
assume that
A2: n >= 10 and
A3: 2 to_power (n - 1) > (2 * n) ^2 ; :: thesis: S₁[n + 1]

A4: now :: thesis: not ((2 * n) ^2) * 2 <= (2 * 2) * (((n * n) + (2 * n)) + 1)

assume ((2 * n) ^2) * 2 <= (2 * 2) * (((n * n) + (2 * n)) + 1) ; :: thesis: contradiction
then ((2 * 2) * (n * n)) * 2 <= ((2 * 2) * (n * n)) + ((2 * 2) * ((2 * n) + 1)) ;
then (((2 * 2) * (n * n)) * 2) - ((2 * 2) * (n * n)) <= (2 * 2) * ((2 * n) + 1) by XREAL_1:20;
then ((2 * 2) ") * ((2 * 2) * (n * n)) <= ((2 * 2) ") * ((2 * 2) * ((2 * n) + 1)) by XREAL_1:64;
then A5: n ^2 <= (2 * n) + 1 ;
n >= 3 by A2, XXREAL_0:2;
hence contradiction by A5, Lm27; :: thesis: verum

end;

2 to_power ((n + 1) - 1) = 2 to_power ((n + (- 1)) + 1)
.= (2 to_power (n - 1)) * (2 to_power 1) by POWER:27
.= (2 to_power (n - 1)) * 2 by POWER:25 ;
then 2 to_power ((n + 1) - 1) > ((2 * n) ^2) * 2 by A3, XREAL_1:68;
hence 2 to_power ((n + 1) - 1) > (2 * (n + 1)) ^2 by A4, XXREAL_0:2; :: thesis: verum

end;

2 to_power (10 - 1) = 2 to_power (6 + 3)
.= 64 * (2 to_power (2 + 1)) by POWER:27, POWER:64
.= 64 * ((2 to_power 2) * (2 to_power 1)) by POWER:27
.= 64 * ((2 to_power (1 + 1)) * 2) by POWER:25
.= 64 * (((2 to_power 1) * (2 to_power 1)) * 2) by POWER:27
.= 64 * ((2 * (2 to_power 1)) * 2) by POWER:25
.= 64 * ((2 * 2) * 2) by POWER:25
.= 512 ;
then A6: S₁[10] ;
for n being Nat st n >= 10 holds
S₁[n] from NAT_1:sch 8(A6, A1);
hence for n being Element of NAT st n >= 10 holds
2 to_power (n - 1) > (2 * n) ^2 ; :: thesis: verum