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_{1}[ 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_{1}[m] holds

S_{1}[m + 1]

.= 1 by Th3 ;

then A6: S_{1}[ 0 ]
;

for m being Nat holds S_{1}[m]
from NAT_1:sch 2(A6, A3);

hence (1 + a) |^ n >= 1 + (n * a) by A1; :: thesis: verum

(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

assume A2: - 1 < a ; :: thesis: (1 + a) |^ n >= 1 + (n * a)

A3: for m being Nat st S

S

proof

(1 + a) |^ 0 =
((1 + a) GeoSeq) . 0
by Def1
A4:
(- 1) + 1 < 1 + a
by A2, XREAL_1:6;

let m be Nat; :: thesis: ( S_{1}[m] implies S_{1}[m + 1] )

assume (1 + a) |^ m >= 1 + (m * a) ; :: thesis: S_{1}[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_{1}[m + 1]
by A5, XXREAL_0:2; :: thesis: verum

end;let m be Nat; :: thesis: ( S

assume (1 + a) |^ m >= 1 + (m * a) ; :: thesis: S

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

.= 1 by Th3 ;

then A6: S

for m being Nat holds S

hence (1 + a) |^ n >= 1 + (n * a) by A1; :: thesis: verum