defpred S₁[ Nat] means (2 * $1) + 3 < 2 to_power $1;
A1: S₁[4] by Lm9;
A2: for k being Nat st k >= 4 & S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( k >= 4 & S₁[k] implies S₁[k + 1] )
assume that
A3: k >= 4 and
A4: (2 * k) + 3 < 2 to_power k ; :: thesis: S₁[k + 1]
(2 * (k + 1)) + 3 = 2 + ((2 * k) + 3) ;
then A5: (2 * (k + 1)) + 3 < 2 + (2 to_power k) by A4, XREAL_1:8;
k > 1 by A3, XXREAL_0:2;
then 2 to_power k > 2 to_power 1 by POWER:44;
then 2 to_power k > 2 by POWER:30;
then (2 to_power k) + (2 to_power k) > 2 + (2 to_power k) by XREAL_1:8;
then (2 * (k + 1)) + 3 < 2 * (2 to_power k) by A5, XXREAL_0:2;
then (2 * (k + 1)) + 3 < (2 to_power 1) * (2 to_power k) by POWER:30;
hence S₁[k + 1] by POWER:32; :: thesis: verum

end;

for n being Nat st n >= 4 holds
S₁[n] from NAT_1:sch 8(A1, A2);
hence for n being Nat st n >= 4 holds
(2 * n) + 3 < 2 to_power n ; :: thesis: verum