let n be Element of NAT ; :: thesis: ( n >= 1 implies ((n + 1) / n) to_power n <= ((n + 2) / (n + 1)) to_power (n + 1) )
assume A1:
n >= 1
; :: thesis: ((n + 1) / n) to_power n <= ((n + 2) / (n + 1)) to_power (n + 1)
deffunc H1( Element of NAT ) -> Element of REAL = (1 + (1 / ($1 + 1))) to_power ($1 + 1);
consider seq being Real_Sequence such that
A2:
for n being Element of NAT holds seq . n = H1(n)
from SEQ_1:sch 1();
A3:
seq is non-decreasing
by A2, Lm47;
n >= 0 + 1
by A1;
then
n - 1 >= 0
by XREAL_1:21;
then reconsider m = n - 1 as Element of NAT by INT_1:16;
seq . m <= seq . (m + 1)
by A3, SEQM_3:def 13;
then
(1 + (1 / (m + 1))) to_power (m + 1) <= seq . (m + 1)
by A2;
then
(1 + (1 / n)) to_power n <= (1 + (1 / (n + 1))) to_power (n + 1)
by A2;
then
((n / n) + (1 / n)) to_power n <= (1 + (1 / (n + 1))) to_power (n + 1)
by A1, XCMPLX_1:60;
then
((n + 1) / n) to_power n <= (1 + (1 / (n + 1))) to_power (n + 1)
;
then
((n + 1) / n) to_power n <= (((n + 1) / (n + 1)) + (1 / (n + 1))) to_power (n + 1)
by XCMPLX_1:60;
then
((n + 1) / n) to_power n <= (((n + 1) + 1) / (n + 1)) to_power (n + 1)
;
hence
((n + 1) / n) to_power n <= ((n + 2) / (n + 1)) to_power (n + 1)
; :: thesis: verum