let n be Nat; :: thesis: for r being Real st 0 <= 1 - r & 1 - r <= 1 holds
(1 - r) |^ n >= 1 - (n * r)
let r be Real; :: thesis: ( 0 <= 1 - r & 1 - r <= 1 implies (1 - r) |^ n >= 1 - (n * r) )
defpred S1[ Nat] means ( 1 - ($1 * r) >= 0 implies (1 - r) |^ $1 >= 1 - ($1 * r) );
assume A1: ( 0 <= 1 - r & 1 - r <= 1 ) ; :: thesis: (1 - r) |^ n >= 1 - (n * r)
1 - 0 = 1 ;
then A2: r >= 0 by A1, XREAL_1:10;
A3: S1[ 0 ] by NEWTON:4;
A4: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A5: S1[k] ; :: thesis: S1[k + 1]
A6: (1 - r) |^ (k + 1) = (1 - r) * ((1 - r) |^ k) by NEWTON:6;
assume 1 - ((k + 1) * r) >= 0 ; :: thesis: (1 - r) |^ (k + 1) >= 1 - ((k + 1) * r)
then ((1 - (k * r)) - r) + r >= 0 + r by XREAL_1:6;
then 1 - (k * r) >= 0 ;
then A7: (1 - r) |^ (k + 1) >= (1 - r) * (1 - (k * r)) by A5, A6, A1, XREAL_1:66;
((1 - (k * r)) - r) + ((r * r) * k) >= ((1 - (k * r)) - r) + 0 by A2, XREAL_1:7;
hence (1 - r) |^ (k + 1) >= 1 - ((k + 1) * r) by A7, XXREAL_0:2; :: thesis: verum
end;
A8: for k being Nat holds S1[k] from NAT_1:sch 2(A3, A4);
 ( 1 - (n * r) >= 0 or 1 - (n * r) < 0 ) ;
hence (1 - r) |^ n >= 1 - (n * r) by A8, A1; :: thesis: verum