let a be Real; :: 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) )
A1: n is Nat by TARSKI:1;
defpred S₁[ Nat] means (1 + a) |^ $1 >= 1 + ($1 * a);
assume A2: - 1 < a ; :: thesis: (1 + a) |^ n >= 1 + (n * a)
A3: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

A4: (- 1) + 1 < 1 + a by A2, XREAL_1:6;
let m be Nat; :: 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 A4, XREAL_1:64;
then A5: (1 + a) |^ (m + 1) >= ((1 + (1 * a)) + (m * a)) + ((m * a) * a) by NEWTON:6;
0 <= a * a by XREAL_1:63;
then (1 + ((m + 1) * a)) + 0 <= (1 + ((m + 1) * a)) + (m * (a * a)) by XREAL_1:7;
hence S₁[m + 1] by A5, XXREAL_0:2; :: thesis: verum

end;

(1 + a) |^ 0 = ((1 + a) GeoSeq) . 0 by Def1
.= 1 by Th3 ;
then A6: S₁[ 0 ] ;
for m being Nat holds S₁[m] from NAT_1:sch 2(A6, A3);
hence (1 + a) |^ n >= 1 + (n * a) by A1; :: thesis: verum