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 S1[ 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 S1[m] holds
S1[m + 1]
proof
A4: (- 1) + 1 < 1 + a by ;
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume (1 + a) |^ m >= 1 + (m * a) ; :: thesis: S1[m + 1]
then ((1 + a) |^ m) * (1 + a) >= (1 + (m * a)) * (1 + a) by ;
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 S1[m + 1] by ; :: thesis: verum
end;
(1 + a) |^ 0 = ((1 + a) GeoSeq) . 0 by Def1
.= 1 by Th3 ;
then A6: S1[ 0 ] ;
for m being Nat holds S1[m] from NAT_1:sch 2(A6, A3);
hence (1 + a) |^ n >= 1 + (n * a) by A1; :: thesis: verum