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₁[ Nat] means (1 + a) |^ $1 <= 1 + ((3 |^ $1) * a);
A5: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume (1 + a) |^ n <= 1 + ((3 |^ n) * a) ; :: thesis: S₁[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

proof

per cases ( 0 = n or 0 <> n ) ;

suppose A9: 0 = n ; :: thesis: 1 <= 3 |^ n

3 |^ n = (3 GeoSeq) . n by Def1
.= 1 by A9, Th3 ;
hence 1 <= 3 |^ n ; :: thesis: verum

end;

suppose 0 <> n ; :: thesis: 1 <= 3 |^ n

then 0 + 1 <= n by NAT_1:13;
then 1 |^ n < 3 |^ n by Lm1;
hence 1 <= 3 |^ n ; :: thesis: verum

end;

end;

end;

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₁[n + 1] by NEWTON:6; :: thesis: verum

end;

A12: 1 + ((3 |^ 0) * a) = 1 + (((3 GeoSeq) . 0) * a) by Def1
.= 1 + (1 * a) by Th3
.= 1 + a ;
(1 + a) |^ 0 = ((1 + a) GeoSeq) . 0 by Def1
.= 1 by Th3 ;
then A13: S₁[ 0 ] by A12, A4;
for n being Nat holds S₁[n] from NAT_1:sch 2(A13, A5);
hence (1 + a) |^ n <= 1 + ((3 |^ n) * a) by A1; :: thesis: verum