let a be real number ; :: thesis: for n being natural number st - 1 < a holds
(1 + a) |^ n >= 1 + (n * a)
let n be natural number ; :: thesis: ( - 1 < a implies (1 + a) |^ n >= 1 + (n * a) )
defpred S₁[ natural number ] means (1 + a) |^ $1 >= 1 + ($1 * a);
assume A1: - 1 < a ; :: thesis: (1 + a) |^ n >= 1 + (n * a)
A2: for m being natural number st S₁[m] holds
S₁[m + 1]

proof

A3: (- 1) + 1 < 1 + a by A1, XREAL_1:8;
let m be natural number ; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume (1 + a) |^ m >= 1 + (m * a) ; :: thesis: S₁[m + 1]
then ((1 + a) |^ m) * (1 + a) >= (1 + (m * a)) * (1 + a) by A3, XREAL_1:66;
then A4: (1 + a) |^ (m + 1) >= ((1 + (1 * a)) + (m * a)) + ((m * a) * a) by NEWTON:11;
0 <= a * a by XREAL_1:65;
then (1 + ((m + 1) * a)) + 0 <= (1 + ((m + 1) * a)) + (m * (a * a)) by XREAL_1:9;
hence S₁[m + 1] by A4, XXREAL_0:2; :: thesis: verum

end;

(1 + a) |^ 0 = ((1 + a) GeoSeq ) . 0 by Def1
.= 1 by Th4 ;
then A5: S₁[ 0 ] ;
for m being natural number holds S₁[m] from NAT_1:sch 2(A5, A2);
hence (1 + a) |^ n >= 1 + (n * a) ; :: thesis: verum