Theorem: Upper Bound of Natural Logarithm

Let $\ln x$ be the natural logarithm of $x$ where $x \in \R_{>0}$.
Then:
:$\ln x \le x - 1$

Proof:
Let $\sequence {f_n}$ denote the sequence of mappings $f_n: \R_{>0} \to \R$ defined as:
:$\map {f_n} x = n \paren {\sqrt [n] x - 1}$
Fix $x \in \R_{>0}$.
We first show that
$\forall n \in \N : n \paren {\sqrt [n] x - 1} < x - 1 $
=== Case 1: $0 < x < 1$ ===
Suppose $0 < x < 1$.
Then:
{{begin-eqn}}
{{eqn | l = 0
      | o = <
      | m = x
      | mo= <
      | r = 1
}}
{{eqn | ll= \leadsto
      | l = 0
      | o = <
      | m = \sqrt [n] x^{n - k}
      | mo= <
      | r = 1
      | c = Power Function on Base between Zero and One is Strictly Decreasing/Rational Number
      | cc= $\forall k \in \set {0, 1, \ldots, n - 1}$
}}
{{eqn | ll= \leadsto
      | l = 0
      | o = <
      | m = \sum_{k \mathop = 0}^{n - 1} \sqrt [n] x^{n - k}
      | mo= <
      | r = n
      | c = Real Number Ordering is Compatible with Addition
}}
{{eqn | ll= \leadsto
      | o = 
      | m = \frac 1 n
      | mo= <
      | r = \frac 1 {1 + \sqrt [n] x + \cdots + \sqrt [n] x^{n - 1} }
      | c = Ordering of Reciprocals
}}
{{eqn | ll= \leadsto
      | o = 
      | m = 1
      | mo= <
      | r = \frac n {1 + \sqrt [n] x + \cdots + \sqrt [n] x^{n - 1} }
      | c = multiplying both sides by $n$
}}
{{eqn | ll= \leadsto
      | o = 
      | m = x - 1
      | mo= >
      | r = \frac {n \paren {x - 1} } {1 + \sqrt [n] x + \cdots + \sqrt [n] x^{n - 1} }
      | c = multiplying both sides by $x - 1 < 0$
}}
{{eqn | ll= \leadsto
      | o = 
      | m = y^n - 1
      | mo= >
      | r = \frac {\paren {y^n - 1} } {1 + y + \cdots + y^{n - 1} }
      | c = substituting $y = \sqrt [n] x$
}}
{{eqn | ll= \leadsto
      | o = 
      | m = y^n - 1
      | mo= >
      | r = n \paren {y - 1}
      | c = Sum of Geometric Sequence
}}
{{eqn | ll= \leadsto
      | o = 
      | m = x - 1
      | mo= >
      | r = n \paren {\sqrt [n] x - 1}
      | c = substituting $\sqrt [n] x = y$
}}
{{end-eqn}}
{{qed|lemma}}
=== Case 2: $x = 1$ ===
Suppose $x = 1$.
Then:
{{begin-eqn}}
{{eqn | l = \map \ln x
      | r = \map \ln 1
}}
{{eqn | r = 0
      | c = Natural Logarithm of 1 is 0/Proof 3
}}
{{eqn | r = 1 - 1
}}
{{eqn | r = x - 1
}}
{{end-eqn}}
{{qed|lemma}}
=== Case 3: $x > 1$ ===
Suppose $x > 1$.
Then:
{{begin-eqn}}
{{eqn | l = x
      | o = >
      | r = 1
}}
{{eqn | ll= \leadsto
      | l = \sqrt [n] x^{n - k}
      | o = >
      | r = 1
      | c = Power Function on Base Greater than One is Strictly Increasing/Rational Number
      | cc = $\forall k \in \set { 0, 1, \ldots, n - 1}$
}}
{{eqn | ll= \leadsto
      | l = \sum_{k \mathop = 0}^{n - 1} \sqrt [n] x^{n - k}
      | o = >
      | r = n
      | c = Real Number Ordering is Compatible with Addition
}}
{{eqn | ll= \leadsto
      | l = \frac 1 n
      | o = > 
      | r = \frac 1 {1 + \sqrt [n] x + \cdots + \sqrt [n] x^{n - 1} }
      | c = Ordering of Reciprocals
}}
{{eqn | ll= \leadsto
      | l = 1
      | o = > 
      | r = \frac n {1 + \sqrt [n] x + \cdots + \sqrt [n] x^{n - 1} }
      | c = Multiply both sides by $n$
}}
{{eqn | ll= \leadsto
      | l = x - 1
      | o = >
      | r = \frac {n \paren {x - 1} } {1 + \sqrt [n] x + \cdots + \sqrt [n] x^{n - 1} }
      | c = multiplying both sides by $x - 1 > 1$
}}
{{eqn | ll= \leadsto
      | l = y^n - 1
      | o = >
      | r = \frac {n \paren {y^n - 1} } {1 + y + \cdots + y^{n - 1} }
      | c = substituting $y = \sqrt [n] x$
}}
{{eqn | ll= \leadsto
      | l = y^n - 1
      | o = >
      | r = n \paren {y - 1}
      | c = Sum of Geometric Sequence
}}
{{eqn | ll= \leadsto
      | l = x - 1
      | o = >
      | r = n \paren {\sqrt [n] x - 1}
      | c = Substitute $\sqrt [n] x = y$
}}
{{end-eqn}}
{{qed|lemma}}
Thus:
:$\forall n \in \N: n \paren {\sqrt [n] x - 1} \le x - 1$
by Proof by Cases.
Thus:
:$\ds \lim_{n \mathop \to \infty} \paren {\sqrt [n] x - 1 } \le x - 1$
from Limit of Bounded Convergent Sequence is Bounded.
Hence the result, from the definition of $\ln$.
{{qed}}