defpred S₁[ Nat] means (2 * $1) + 3 < 2 to_power $1;
A1: 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
A2: k >= 4 and
A3: (2 * k) + 3 < 2 to_power k ; :: thesis: S₁[k + 1]
k > 1 by A2, XXREAL_0:2;
then 2 to_power k > 2 to_power 1 by POWER:39;
then 2 to_power k > 2 by POWER:25;
then A4: (2 to_power k) + (2 to_power k) > 2 + (2 to_power k) by XREAL_1:6;
(2 * (k + 1)) + 3 = 2 + ((2 * k) + 3) ;
then (2 * (k + 1)) + 3 < 2 + (2 to_power k) by A3, XREAL_1:6;
then (2 * (k + 1)) + 3 < 2 * (2 to_power k) by A4, XXREAL_0:2;
then (2 * (k + 1)) + 3 < (2 to_power 1) * (2 to_power k) by POWER:25;
hence S₁[k + 1] by POWER:27; :: thesis: verum

end;

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