let a be Real; :: thesis: for n being natural Number st 0 < a & a < 1 holds

(1 + a) |^ n <= 1 + ((3 |^ n) * a)

let n be natural Number ; :: thesis: ( 0 < a & a < 1 implies (1 + a) |^ n <= 1 + ((3 |^ n) * a) )

A1: n is Nat by TARSKI:1;

assume that

A2: 0 < a and

A3: a < 1 ; :: thesis: (1 + a) |^ n <= 1 + ((3 |^ n) * a)

A4: 1 + 0 < 1 + a by A2, XREAL_1:6;

defpred S_{1}[ Nat] means (1 + a) |^ $1 <= 1 + ((3 |^ $1) * a);

A5: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]

.= 1 + (1 * a) by Th3

.= 1 + a ;

(1 + a) |^ 0 = ((1 + a) GeoSeq) . 0 by Def1

.= 1 by Th3 ;

then A13: S_{1}[ 0 ]
by A12, A4;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A13, A5);

hence (1 + a) |^ n <= 1 + ((3 |^ n) * a) by A1; :: thesis: verum

(1 + a) |^ n <= 1 + ((3 |^ n) * a)

let n be natural Number ; :: thesis: ( 0 < a & a < 1 implies (1 + a) |^ n <= 1 + ((3 |^ n) * a) )

A1: n is Nat by TARSKI:1;

assume that

A2: 0 < a and

A3: a < 1 ; :: thesis: (1 + a) |^ n <= 1 + ((3 |^ n) * a)

A4: 1 + 0 < 1 + a by A2, XREAL_1:6;

defpred S

A5: for n being Nat st S

S

proof

A12: 1 + ((3 |^ 0) * a) =
1 + (((3 GeoSeq) . 0) * a)
by Def1
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume (1 + a) |^ n <= 1 + ((3 |^ n) * a) ; :: thesis: S_{1}[n + 1]

then A6: ((1 + a) |^ n) * (1 + a) <= (1 + ((3 |^ n) * a)) * (1 + a) by A2, XREAL_1:64;

A7: (1 + ((3 |^ n) * a)) + (((3 |^ n) + (3 |^ n)) * a) = 1 + (((3 |^ n) * (1 + 2)) * a)

.= 1 + ((3 |^ (n + 1)) * a) by NEWTON:6 ;

A8: 1 <= 3 |^ n then 1 * a <= (3 |^ n) * a by A2, XREAL_1:64;

then A10: 1 + a <= 1 + ((3 |^ n) * a) by XREAL_1:7;

a * a < 1 * a by A2, A3, XREAL_1:68;

then (3 |^ n) * (a * a) < (3 |^ n) * a by A8, XREAL_1:68;

then A11: ((3 |^ n) * a) + ((3 |^ n) * (a * a)) < ((3 |^ n) * a) + ((3 |^ n) * a) by XREAL_1:6;

(1 + ((3 |^ n) * a)) * (1 + a) = (1 + a) + (((3 |^ n) * a) + ((3 |^ n) * (a * a))) ;

then (1 + ((3 |^ n) * a)) * (1 + a) < 1 + ((3 |^ (n + 1)) * a) by A10, A7, A11, XREAL_1:8;

then ((1 + a) |^ n) * (1 + a) <= 1 + ((3 |^ (n + 1)) * a) by A6, XXREAL_0:2;

hence S_{1}[n + 1]
by NEWTON:6; :: thesis: verum

end;assume (1 + a) |^ n <= 1 + ((3 |^ n) * a) ; :: thesis: S

then A6: ((1 + a) |^ n) * (1 + a) <= (1 + ((3 |^ n) * a)) * (1 + a) by A2, XREAL_1:64;

A7: (1 + ((3 |^ n) * a)) + (((3 |^ n) + (3 |^ n)) * a) = 1 + (((3 |^ n) * (1 + 2)) * a)

.= 1 + ((3 |^ (n + 1)) * a) by NEWTON:6 ;

A8: 1 <= 3 |^ n then 1 * a <= (3 |^ n) * a by A2, XREAL_1:64;

then A10: 1 + a <= 1 + ((3 |^ n) * a) by XREAL_1:7;

a * a < 1 * a by A2, A3, XREAL_1:68;

then (3 |^ n) * (a * a) < (3 |^ n) * a by A8, XREAL_1:68;

then A11: ((3 |^ n) * a) + ((3 |^ n) * (a * a)) < ((3 |^ n) * a) + ((3 |^ n) * a) by XREAL_1:6;

(1 + ((3 |^ n) * a)) * (1 + a) = (1 + a) + (((3 |^ n) * a) + ((3 |^ n) * (a * a))) ;

then (1 + ((3 |^ n) * a)) * (1 + a) < 1 + ((3 |^ (n + 1)) * a) by A10, A7, A11, XREAL_1:8;

then ((1 + a) |^ n) * (1 + a) <= 1 + ((3 |^ (n + 1)) * a) by A6, XXREAL_0:2;

hence S

.= 1 + (1 * a) by Th3

.= 1 + a ;

(1 + a) |^ 0 = ((1 + a) GeoSeq) . 0 by Def1

.= 1 by Th3 ;

then A13: S

for n being Nat holds S

hence (1 + a) |^ n <= 1 + ((3 |^ n) * a) by A1; :: thesis: verum