let k be Nat; :: thesis: for r being Real st 0 < r & r < 1 / 2 holds
(1 + r) |^ k < 1 + (r * (2 |^ k))
let r be Real; :: thesis: ( 0 < r & r < 1 / 2 implies (1 + r) |^ k < 1 + (r * (2 |^ k)) )
assume A1: ( 0 < r & r < 1 / 2 ) ; :: thesis: (1 + r) |^ k < 1 + (r * (2 |^ k))
defpred S₁[ Nat] means (1 + r) |^ $1 < 1 + (r * (2 |^ $1));

per cases ( k = 0 or k >= 1 ) by NAT_1:14;

suppose A2: k = 0 ; :: thesis: (1 + r) |^ k < 1 + (r * (2 |^ k))

( (1 + r) |^ 0 = 1 & 2 |^ 0 = 1 & 1 + 0 < 1 + r ) by NEWTON:4, A1, XREAL_1:8;
hence (1 + r) |^ k < 1 + (r * (2 |^ k)) by A2; :: thesis: verum

end;

suppose A3: k >= 1 ; :: thesis: (1 + r) |^ k < 1 + (r * (2 |^ k))

(1 + r) + 0 < (1 + r) + r by A1, XREAL_1:8;
then A4: S₁[1] ;
A5: for k being Nat st 1 <= k & S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( 1 <= k & S₁[k] implies S₁[k + 1] )
assume that
A6: 1 <= k and
A7: S₁[k] ; :: thesis: S₁[k + 1]
set k1 = k + 1;
2 |^ k >= 2 by A6, PREPOWER:12;
then A8: (2 |^ k) * (1 / 2) >= 2 * (1 / 2) by XREAL_1:64;
r * (2 |^ k) < (1 / 2) * (2 |^ k) by A1, XREAL_1:68;
then 1 + (r * (2 |^ k)) < ((1 / 2) * (2 |^ k)) + ((1 / 2) * (2 |^ k)) by A8, XREAL_1:8;
then A9: (2 |^ k) + (1 + (r * (2 |^ k))) < (2 |^ k) + (2 |^ k) by XREAL_1:8;
2 |^ (k + 1) = 2 * (2 |^ k) by NEWTON:6;
then r * (((2 |^ k) + 1) + (r * (2 |^ k))) < r * (2 |^ (k + 1)) by A9, A1, XREAL_1:68;
then A10: 1 + (r * (((2 |^ k) + 1) + (r * (2 |^ k)))) < 1 + (r * (2 |^ (k + 1))) by XREAL_1:8;
A11: (1 + r) |^ (k + 1) = ((1 + r) |^ k) * (1 + r) by NEWTON:6;
(1 + r) |^ (k + 1) < (1 + (r * (2 |^ k))) * (1 + r) by A7, A1, A11, XREAL_1:68;
hence S₁[k + 1] by A10, XXREAL_0:2; :: thesis: verum

end;

for k being Nat st 1 <= k holds
S₁[k] from NAT_1:sch 8(A4, A5);
hence (1 + r) |^ k < 1 + (r * (2 |^ k)) by A3; :: thesis: verum

end;

end;