let a be real number ; :: 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) )
assume A1: ( 0 < a & a < 1 ) ; :: thesis: (1 + a) |^ n <= 1 + ((3 |^ n) * a)
defpred S₁[ natural number ] means (1 + a) |^ $1 <= 1 + ((3 |^ $1) * a);
A2: S₁[ 0 ]

proof

A3: (1 + a) |^ 0 = ((1 + a) GeoSeq ) . 0 by Def1
.= 1 by Th4 ;
A4: 1 + ((3 |^ 0 ) * a) = 1 + (((3 GeoSeq ) . 0 ) * a) by Def1
.= 1 + (1 * a) by Th4
.= 1 + a ;
1 + 0 < 1 + a by A1, XREAL_1:8;
hence S₁[ 0 ] by A3, A4; :: thesis: verum

end;

A5: for n being natural number st S₁[n] holds
S₁[n + 1]

proof

let n be natural number ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A6: (1 + a) |^ n <= 1 + ((3 |^ n) * a) ; :: thesis: S₁[n + 1]
A7: 1 < 1 + a by A1, XREAL_1:31;
A8: 1 <= 3 |^ n

proof

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

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

n is Element of NAT by ORDINAL1:def 13;
then 3 |^ n = (3 GeoSeq ) . n by Def1
.= 1 by A9, Th4 ;
hence 1 <= 3 |^ n ; :: thesis: verum

end;

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

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

end;

end;

end;

then 1 * a <= (3 |^ n) * a by A1, XREAL_1:66;
then A10: 1 + a <= 1 + ((3 |^ n) * a) by XREAL_1:9;
A11: (1 + ((3 |^ n) * a)) * (1 + a) = (1 + a) + (((3 |^ n) * a) + ((3 |^ n) * (a * a))) ;
A12: (1 + ((3 |^ n) * a)) + (((3 |^ n) + (3 |^ n)) * a) = 1 + (((3 |^ n) * (1 + 2)) * a)
.= 1 + ((3 |^ (n + 1)) * a) by NEWTON:11 ;
a * a < 1 * a by A1, XREAL_1:70;
then (3 |^ n) * (a * a) < (3 |^ n) * a by A8, XREAL_1:70;
then ((3 |^ n) * a) + ((3 |^ n) * (a * a)) < ((3 |^ n) * a) + ((3 |^ n) * a) by XREAL_1:8;
then A13: (1 + ((3 |^ n) * a)) * (1 + a) < 1 + ((3 |^ (n + 1)) * a) by A10, A11, A12, XREAL_1:10;
((1 + a) |^ n) * (1 + a) <= (1 + ((3 |^ n) * a)) * (1 + a) by A6, A7, XREAL_1:66;
then ((1 + a) |^ n) * (1 + a) <= 1 + ((3 |^ (n + 1)) * a) by A13, XXREAL_0:2;
hence S₁[n + 1] by NEWTON:11; :: thesis: verum

end;

for n being natural number holds S₁[n] from NAT_1:sch 2(A2, A5);
hence (1 + a) |^ n <= 1 + ((3 |^ n) * a) ; :: thesis: verum