let n be Nat; :: thesis: ( n >= 1 implies (1 + (1 / (n + 1))) |^ n < (1 + (1 / n)) |^ (n + 1) )
assume A1: n >= 1 ; :: thesis: (1 + (1 / (n + 1))) |^ n < (1 + (1 / n)) |^ (n + 1)
n + 1 > n + 0 by XREAL_1:8;
then 1 / (n + 1) < 1 / n by A1, XREAL_1:76;
then (1 / (n + 1)) + 1 < (1 / n) + 1 by XREAL_1:8;
then A2: (1 + (1 / (n + 1))) |^ n < (1 + (1 / n)) |^ n by A1, PREPOWER:10;
A3: (1 + (1 / n)) |^ n > 0 by PREPOWER:6;
((1 + (1 / n)) |^ (n + 1)) - ((1 + (1 / n)) |^ n) = (((1 + (1 / n)) |^ n) * (1 + (1 / n))) - ((1 + (1 / n)) |^ n) by NEWTON:6
.= ((1 + (1 / n)) |^ n) * (1 / n) ;
then (((1 + (1 / n)) |^ (n + 1)) - ((1 + (1 / n)) |^ n)) + ((1 + (1 / n)) |^ n) > 0 + ((1 + (1 / n)) |^ n) by A1, A3, XREAL_1:8;
hence (1 + (1 / (n + 1))) |^ n < (1 + (1 / n)) |^ (n + 1) by A2, XXREAL_0:2; :: thesis: verum