let a be Real; :: thesis: for n being Nat st 0 < a & a < 1 holds
(1 + a) |^ n <= 1 + ((3 |^ n) * a)
let n be Nat; :: thesis: ( 0 < a & a < 1 implies (1 + a) |^ n <= 1 + ((3 |^ n) * a) )
assume that
A1: 0 < a and
A2: a < 1 ; :: thesis: (1 + a) |^ n <= 1 + ((3 |^ n) * a)
A3: 1 + 0 < 1 + a by A1, XREAL_1:6;
defpred S₁[ Nat] means (1 + a) |^ $1 <= 1 + ((3 |^ $1) * a);
A4: 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 A5: ((1 + a) |^ n) * (1 + a) <= (1 + ((3 |^ n) * a)) * (1 + a) by A1, XREAL_1:64;
A6: (1 + ((3 |^ n) * a)) + (((3 |^ n) + (3 |^ n)) * a) = 1 + (((3 |^ n) * (1 + 2)) * a)
.= 1 + ((3 |^ (n + 1)) * a) by NEWTON:6 ;
A7: 1 <= 3 |^ n

proof

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

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

3 |^ n = (3 GeoSeq) . n by Def1
.= 1 by A8, 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 by NEWTON:10; :: thesis: verum

end;

end;

end;

then 1 * a <= (3 |^ n) * a by A1, XREAL_1:64;
then A9: 1 + a <= 1 + ((3 |^ n) * a) by XREAL_1:7;
a * a < 1 * a by A1, A2, XREAL_1:68;
then (3 |^ n) * (a * a) < (3 |^ n) * a by A7, XREAL_1:68;
then A10: ((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 A9, A6, A10, XREAL_1:8;
then ((1 + a) |^ n) * (1 + a) <= 1 + ((3 |^ (n + 1)) * a) by A5, XXREAL_0:2;
hence S₁[n + 1] by NEWTON:6; :: thesis: verum

end;

A11: 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 A12: S₁[ 0 ] by A11, A3;
for n being Nat holds S₁[n] from NAT_1:sch 2(A12, A4);
hence (1 + a) |^ n <= 1 + ((3 |^ n) * a) ; :: thesis: verum