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_{1}[ Nat] means (1 + r) |^ $1 < 1 + (r * (2 |^ $1));

(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

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

end;

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;hence (1 + r) |^ k < 1 + (r * (2 |^ k)) by A2; :: thesis: verum

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}[1]
;

A5: for k being Nat st 1 <= k & S_{1}[k] holds

S_{1}[k + 1]

S_{1}[k]
from NAT_1:sch 8(A4, A5);

hence (1 + r) |^ k < 1 + (r * (2 |^ k)) by A3; :: thesis: verum

end;then A4: S

A5: for k being Nat st 1 <= k & S

S

proof

for k being Nat st 1 <= k holds
let k be Nat; :: thesis: ( 1 <= k & S_{1}[k] implies S_{1}[k + 1] )

assume that

A6: 1 <= k and

A7: S_{1}[k]
; :: thesis: S_{1}[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_{1}[k + 1]
by A10, XXREAL_0:2; :: thesis: verum

end;assume that

A6: 1 <= k and

A7: S

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

S

hence (1 + r) |^ k < 1 + (r * (2 |^ k)) by A3; :: thesis: verum