deffunc H₁( Nat) -> object = (1 + (1 / ($1 + 1))) to_power ($1 + 1);
let n be Element of NAT ; :: thesis: ( n >= 1 implies ((n + 1) / n) to_power n <= ((n + 2) / (n + 1)) to_power (n + 1) )
consider seq being Real_Sequence such that
A1: for n being Nat holds seq . n = H₁(n) from SEQ_1:sch 1();
assume A2: n >= 1 ; :: thesis: ((n + 1) / n) to_power n <= ((n + 2) / (n + 1)) to_power (n + 1)
then reconsider m = n - 1 as Element of NAT by INT_1:3;
seq is non-decreasing by A1, Lm41;
then seq . m <= seq . (m + 1) ;
then (1 + (1 / (m + 1))) to_power (m + 1) <= seq . (m + 1) by A1;
then (1 + (1 / n)) to_power n <= (1 + (1 / (n + 1))) to_power (n + 1) by A1;
then ((n / n) + (1 / n)) to_power n <= (1 + (1 / (n + 1))) to_power (n + 1) by A2, XCMPLX_1:60;
then ((n + 1) / n) to_power n <= (((n + 1) / (n + 1)) + (1 / (n + 1))) to_power (n + 1) by XCMPLX_1:60;
hence ((n + 1) / n) to_power n <= ((n + 2) / (n + 1)) to_power (n + 1) ; :: thesis: verum