defpred S1[ Nat] means ($1 + 1) ^2 < 2 to_power $1;
A1: for k being Nat st k >= 6 & S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( k >= 6 & S1[k] implies S1[k + 1] )
assume that
A2: k >= 6 and
A3: (k + 1) ^2 < 2 to_power k ; :: thesis: S1[k + 1]
k >= 4 by A2, XXREAL_0:2;
then (2 * k) + 3 < 2 to_power k by Lm7;
then A4: ((k + 1) ^2) + ((2 * k) + 3) < ((k + 1) ^2) + (2 to_power k) by XREAL_1:6;
((k + 1) ^2) + (2 to_power k) < (2 to_power k) + (2 to_power k) by A3, XREAL_1:6;
then ((k + 1) + 1) ^2 < 2 * (2 to_power k) by A4, XXREAL_0:2;
then ((k + 1) + 1) ^2 < (2 to_power 1) * (2 to_power k) by POWER:25;
hence S1[k + 1] by POWER:27; :: thesis: verum
end;
A5: S1[6] by POWER:64;
for n being Nat st n >= 6 holds
S1[n] from NAT_1:sch 8(A5, A1);
 hence for n being Element of NAT st n >= 6 holds
(n + 1) ^2 < 2 to_power n ; :: thesis: verum