Equivalence of Definitions of Real Natural Logarithm
If you are fairly certain that there are none, please remove {{proofread}} from the code.
Theorem
The following definitions of the concept of Real Natural Logarithm are equivalent:
Definition 1
Let $x \in \R$ be a real number such that $x > 0$.
The (natural) logarithm of $x$ is defined as:
- $\displaystyle \ln x := \int_1^x \frac {\d t} t$
Definition 2
Let $x \in \R$ be a real number such that $x > 0$.
The (natural) logarithm of $x$ is defined as:
- $\ln x := y \in \R: e^y = x$
where $e$ is Euler's number.
Definition 3
Let $x \in \R$ be a real number such that $x > 0$.
The (natural) logarithm of $x$ is defined as:
- $ \displaystyle \ln x := \lim_{n \mathop \to \infty} n \paren {\sqrt [n] x - 1}$
Proof
Definition 1 implies Definition 2
Let $F \left({x}\right)$ be $\displaystyle \int_1^x \frac {\d t} t$.
Let $f \left({t}\right)$ be $\displaystyle \int \frac {\d t} t$.
Then:
- $\dfrac {\d t} t = \dfrac 1 t$
Or:
- $\dfrac {\d x} x = \dfrac 1 x$
Also:
- $F \left({x}\right) = f \left({x}\right) - f \left({1}\right)$
Therefore:
| \(\ds \frac {\d F \left({x}\right)} {\d x}\) | \(=\) | \(\ds \frac {\d f \left({x}\right)} {\d x} - \frac {\d F \left({1}\right)} {\d x}\) | ||||||||||||
| \(\ds \) | \(=\) | \(\ds \frac {\d f \left({x}\right)} {\d x}\) | Derivative of Constant | |||||||||||
| \(\ds \) | \(=\) | \(\ds \frac 1 x\) | ||||||||||||
| \(\ds \leadsto \ \ \) | \(\ds \frac {\d x} {\d F \left({x}\right)}\) | \(=\) | \(\ds x\) | Derivative of Inverse Function |
Furthermore:
- $F \left({1}\right) = f \left({1}\right) - f \left({1}\right) = 0$
Why is the reverse of $F \left({x}\right)$ a function?
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by explaining it. To discuss this point in more detail, feel free to use the talk page.
If you are able to explain it, then when you have done so you can remove this instance of {{Explain}} from the code.
The result follows from the fifth definition of the exponential function:
- $F \left({x}\right) \equiv e^x$
$\Box$
Definition 2 implies Definition 1
| \(\ds e^{F \left({x}\right)}\) | \(=\) | \(\ds x\) | ||||||||||||
| \(\ds \leadsto \ \ \) | \(\ds \frac {\d x} {\d F \left({x}\right)}\) | \(=\) | \(\ds x\) | |||||||||||
| \(\ds \leadsto \ \ \) | \(\ds \frac {\d F \left({x}\right)} {\d x}\) | \(=\) | \(\ds \frac 1 x\) | Derivative of Inverse Function |
Let $f \left({t}\right)$ be $\displaystyle \int \frac 1 t \rd t$.
Then:
- $F \left({x}\right) = f \left({x}\right) + C$
When $F \left({x}\right) = 0$:
- $x = e^{F \left({x}\right)} = 1$
- $F \left({1}\right) = f \left({1}\right) + C = 0 \implies f \left({1}\right) = - C$
Therefore:
- $F \left({x}\right) = f \left({x}\right) - f \left({1}\right)$
Therefore:
- $\displaystyle F \left({x}\right) = \int_1^x \frac {\d t} t$
$\Box$
Therefore:
| \(\ds y = \int_1^x \frac {\d t} t\) | \(\leadsto\) | \(\ds e^y = x\) | Definition 1 implies Definition 2 | |||||||||||
| \(\ds e^y = x\) | \(\leadsto\) | \(\ds y = \int_1^x \frac {\d t} t\) | Definition 2 implies Definition 1 | |||||||||||
| \(\ds \leadsto \ \ \) | \(\ds y = \int_1^x \frac {\d t} t\) | \(\iff\) | \(\ds e^y = x\) |
$\blacksquare$
Add definition 3
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by crafting such a proof.
When this page/section has been completed, {{ProofWanted}} should be removed from the code.
If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page (see the proofread template for usage).