Domain of Real Natural Logarithm

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\ln$ be the natural logarithm function on the real numbers.


Then the domain of $\ln$ is the set of strictly positive real numbers:

$\Dom \ln = \R_{>0}$


Proof

By definition of natural logarithm:

$\ln^{-1} = \exp$

From Exponential Tends to Zero and Infinity:

$\Dom \exp = \openint {-\infty} {+\infty}$
$\Img \exp = \openint 0 {+\infty}$

From Exponential is Strictly Increasing:

$\exp$ is strictly increasing.

From Strictly Monotone Real Function is Bijective, $\exp: \R \to \R_{>0}$ is a bijection.

Thus:

$\Dom \ln = \Img \exp$

and so $\Dom \ln = \R_{>0}$.

$\blacksquare$