let n be Nat; :: thesis: 2 |^ (n + 1) < (2 |^ (n + 2)) - 1
defpred S₁[ Nat] means 2 |^ ($1 + 1) < (2 |^ ($1 + 2)) - 1;
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then (2 |^ (k + 1)) * 2 < ((2 |^ (k + 2)) - 1) * 2 by XREAL_1:68;
then 2 |^ ((k + 1) + 1) < ((2 |^ (k + 2)) * 2) - (1 * 2) by NEWTON:6;
then A2: 2 |^ ((k + 1) + 1) < (2 |^ ((k + 2) + 1)) - 2 by NEWTON:6;
(- 2) + (2 |^ ((k + 1) + 2)) < (- 1) + (2 |^ ((k + 1) + 2)) by XREAL_1:8;
hence S₁[k + 1] by A2, XXREAL_0:2; :: thesis: verum

end;

2 |^ 1 < ((2 |^ 1) * 2) - 1 ;
then 2 |^ 1 < (2 |^ (1 + 1)) - 1 by NEWTON:6;
then A3: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A1);
hence 2 |^ (n + 1) < (2 |^ (n + 2)) - 1 ; :: thesis: verum