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 ;
defpred S1[ Nat] means (1 + a) |^ \$1 <= 1 + ((3 |^ \$1) * a);
A5: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume (1 + a) |^ n <= 1 + ((3 |^ n) * a) ; :: thesis: S1[n + 1]
then A6: ((1 + a) |^ n) * (1 + a) <= (1 + ((3 |^ n) * a)) * (1 + a) by ;
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 = () . n by Def1
.= 1 by ;
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 ;
then A10: 1 + a <= 1 + ((3 |^ n) * a) by XREAL_1:7;
a * a < 1 * a by ;
then (3 |^ n) * (a * a) < (3 |^ n) * a by ;
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 ;
then ((1 + a) |^ n) * (1 + a) <= 1 + ((3 |^ (n + 1)) * a) by ;
hence S1[n + 1] by NEWTON:6; :: thesis: verum
end;
A12: 1 + ((3 |^ 0) * a) = 1 + ((() . 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: S1[ 0 ] by ;
for n being Nat holds S1[n] from NAT_1:sch 2(A13, A5);
hence (1 + a) |^ n <= 1 + ((3 |^ n) * a) by A1; :: thesis: verum