avewright/proofwiki-math huggingface dataset:
Theorem: Power Rule for Derivatives/Real Number Index

Let $n \in \R$.
Let $f: \R \to \R$ be the real function defined as $\map f x = x^n$.
Then:
:$\map {f'} x = n x^{n-1}$
everywhere that $\map f x = x^n$ is defined.
When $x = 0$ and $n = 0$, $\map {f'} x$ is undefined.

Proof:
We are going to prove that $\map {f'} x = n x^{n - 1}$ holds for all real $n$.
To do this, we compute the limit $\ds \lim_{h \mathop \to 0} \frac {\paren {x + h}^n - x^n} h$:
{{begin-eqn}}
{{eqn | l = \frac {\paren {x + h}^n - x^n} h
      | r = \frac {x^n} h \paren {\paren {1 + \frac h x}^n - 1}
      | c = 
}}
{{eqn | r = \frac{x^n} h \paren {e^{n \map \ln {1 + \frac h x} } - 1}
      | c = 
}}
{{eqn | r = x^n \cdot \frac {e^{n \map \ln {1 + \frac h x} } - 1} {n \map \ln {1 + \frac h x} } \cdot \frac {n \map \ln {1 + \frac h x} } {\frac h x} \cdot \frac 1 x
      | c = 
}}
{{end-eqn}}
Now we use the following results:
:$\ds \lim_{x \mathop \to 0} \frac {\exp x - 1} x = 1$ from Derivative of Exponential at Zero
:$\ds \lim_{x \mathop \to 0} \frac {\map \ln {1 + x} } x = 1$ from Derivative of Logarithm at One
to obtain:
:$x^n \cdot \dfrac {e^{n \map \ln {1 + \frac h x} } - 1} {n \map \ln {1 + \dfrac h x} } \cdot \dfrac {n \map \ln {1 + \dfrac h x}} {\dfrac h x} \cdot \dfrac 1 x \to n x^{n - 1}$ as $h \to 0$
Hence the result.
{{qed}}
Theorem: Power Rule for Derivatives/Real Number Index

Let $n \in \R$.
Let $f: \R \to \R$ be the real function defined as $\map f x = x^n$.
Then:
:$\map {f'} x = n x^{n-1}$
everywhere that $\map f x = x^n$ is defined.
When $x = 0$ and $n = 0$, $\map {f'} x$ is undefined.

Proof:
Note this proof does not hold for $x = 0$.
Let $y$ = $\map f x$.
Then $y = x^n$.
Then:
{{begin-eqn}}
{{eqn | l = y
      | r = x^n
}}
{{eqn | ll= \leadsto
      | l = \size y
      | r = \size {x^n}
      | c = taking the absolute value of both sides
}}
{{eqn | r = \size x^n
      | c = Absolute Value of Power
}}
{{eqn | ll= \leadsto
      | l = \ln \size y
      | r = \map \ln {\size x^n}
      | c = taking the natural logarithm of both sides
}}
{{eqn | r = n \ln \size x
      | c = Logarithm of Power
}}
{{end-eqn}}
Using:
* Derivative of Composite Function
* Derivative of Constant Multiple
* {{Corollary|Primitive of Reciprocal|2}}
and taking the derivative of both sides with respect to $x$ gives:
:$\dfrac 1 y \dfrac {\d y} {\d x} = n \dfrac 1 x$
Multiplying both sides of the equation by $y$ yields:
:$\dfrac {\d y} {\d x} = n \dfrac y x$
Substituting $x^n$ for $y$:
:$\dfrac {\d y} {\d x} = n \dfrac {x^n} x$
From Quotient of Powers:
:$\dfrac {\d y} {\d x} = n x^{n - 1}$
{{qed}}
Theorem: Well-Ordering Minimal Elements are Unique

Let $\struct {S,\preceq}$ be a well-ordered set.
Then every non-empty subset of $S$ has a unique minimal element.

Proof:
The proof consists of a uniqueness and an existence part.
Let $S'$ be a non-empty subset of $S$.
Theorem: Fundamental Theorem of Calculus/First Part

Let $f$ be a real function which is continuous on the closed interval $\closedint a b$.
Let $F$ be a real function which is defined on $\closedint a b$ by:
:$\ds \map F x = \int_a^x \map f t \rd t$
Then $F$ is a primitive of $f$ on $\closedint a b$.

Proof:
To show that $F$ is a primitive of $f$ on $\closedint a b$, we need to establish the following:
:$F$ is continuous on $\closedint a b$
:$F$ is differentiable on the open interval $\openint a b$
:$\forall x \in \closedint a b: \map {F'} x = \map f x$.
=== Proof that $F$ is Continuous ===
We have that $f$ is continuous on $\closedint a b$.
It follows from Continuous Image of Closed Real Interval is Closed Real Interval that $f$ is bounded on $\closedint a b$.
Suppose that:
:$\forall t \in \closedint a b: \size {\map f t} < \kappa$
Let $x, \xi \in \closedint a b$.
From Sum of Integrals on Adjacent Intervals for Continuous Functions, we have that:
:$\ds \int_a^x \map f t \rd t + \int_x^\xi \map f t \rd t = \int_a^\xi \map f t \rd t$
That is:
:$\ds \map F x + \int_x^\xi \map f t \rd t = \map F \xi$
So:
:$\ds \map F x - \map F \xi = -\int_x^\xi \map f t \rd t = \int_\xi^x \map f t \rd t$
From {{Corollary|Darboux's Theorem|1}}:
:$\size {\map F x - \map F \xi} < \kappa \size {x - \xi}$
Thus it follows that $F$ is continuous on $\closedint a b$.
{{qed|lemma}}
=== Proof that $F$ is Differentiable and $f$ is its Derivative ===
It is now to be shown that that $F$ is differentiable on $\openint a b$ and that:
:$\forall x \in \closedint a b: \map {F'} x = \map f x$
Let $x, \xi \in \closedint a b$ such that $x \ne \xi$.
Then:
{{begin-eqn}}
{{eqn | l = \frac {\map F x - \map F \xi} {x - \xi} - \map f \xi
      | r = \frac 1 {x - \xi} \paren {\map F x - \map F \xi - \paren {x - \xi} \map f \xi}
      | c = 
}}
{{eqn | r = \frac 1 {x - \xi} \paren {\int_\xi^x \map f t \rd t - \paren {x - \xi} \map f \xi}
      | c = 
}}
{{eqn | r = \frac 1 {x - \xi} \int_\xi^x \paren {\map f t - \map f \xi} \rd t
      | c = Definite Integral of Function plus Constant, putting $c = \map f \xi$
}}
{{end-eqn}}
Now, let $\epsilon > 0$.
If $\xi \in \openint a b$, then $f$ is continuous at $\xi$.
So for some $\delta > 0$:
:$\size {\map f t - \map f \xi} < \epsilon$
provided $\size {t - \xi} < \delta$.
So provided $\size {x - \xi} < \delta$ it follows that:
:$\size {\map f t - \map f \xi} < \epsilon$
for any $t$ in an interval whose endpoints are $x$ and $\xi$.
So from {{Corollary|Darboux's Theorem|1}}:
{{begin-eqn}}
{{eqn | l = \size {\frac {\map F x - \map F \xi} {x - \xi} - \map f \xi}
      | r = \frac 1 {\size {x - \xi} } \size {\int_\xi^x \paren {\map f t - \map f \xi} \rd t}
      | c = 
}}
{{eqn | o = <
      | r = \frac 1 {\size {x - \xi} } \epsilon \size {x - \xi}
      | c = 
}}
{{eqn | r = \epsilon
      | c = 
}}
{{end-eqn}}
provided $0 < \size {x - \xi} < \delta$.
But that is what this means:
:$\dfrac {\map F x - \map F \xi} {x - \xi} \to \map f \xi$ as $x \to \xi$
So $F$ is differentiable on $\openint a b$, and:
:$\forall x \in \closedint a b: \map {F'} x = \map f x$
{{qed}}
Theorem: Fundamental Theorem of Calculus/First Part

Let $f$ be a real function which is continuous on the closed interval $\closedint a b$.
Let $F$ be a real function which is defined on $\closedint a b$ by:
:$\ds \map F x = \int_a^x \map f t \rd t$
Then $F$ is a primitive of $f$ on $\closedint a b$.

Proof:
{{begin-eqn}}
{{eqn | l = \dfrac \d {\d x} \map F x
      | r = \lim_{\Delta x \mathop \to 0} \frac 1 {\Delta x} \paren {\int_a^{x + \Delta x} \map f t \rd t - \int_a^x \map f t \rd t}
      | c = {{Defof|Derivative of Real Function at Point}}
}}
{{eqn | r = \lim_{\Delta x \mathop \to 0} \frac 1 {\Delta x} \paren {\int_x^a \map f t \rd t + \int_a^{x + \Delta x} \map f t \rd t}
      | c = because $\ds \int_a^b \map f x \rd x = -\int_b^a \map f x \rd x$
}}
{{eqn | r = \lim_{\Delta x \mathop \to 0} \frac 1 {\Delta x} \paren {\int_x^{x + \Delta x} \map f t \rd t}
      | c = Sum of Integrals on Adjacent Intervals for Continuous Functions
}}
{{end-eqn}}
Suppose $\Delta x > 0$ and both $x$ and $x + \Delta x$ are in the closed interval $\closedint a b$.
By hypothesis, $f$ is continuous on the closed interval $\closedint a b$
Thus it is also continuous on the closed interval $\closedint x {x + \Delta x}$.
Thus the conditions of the Mean Value Theorem for Integrals are fulfilled.
So, by the Mean Value Theorem for Integrals, there exists some $k \in \closedint x {x + \Delta x}$ such that:
:$\ds \int_x^{x + \Delta x} \map f x \rd x = \map f k \paren {x + \Delta x - x} = \map f k \Delta x$
Then:
{{begin-eqn}}
{{eqn | l = \lim_{\Delta x \mathop \to 0} \frac 1 {\Delta x} \paren {\int_x^{x + \Delta x} \map f t \rd t}
      | r = \lim_{\Delta x \mathop \to 0} \frac 1 {\Delta x} \map f k \Delta x
}}
{{eqn | r = \lim_{\Delta x \mathop \to 0} \map f k
}}
{{end-eqn}}
By the definition of $k$:
:$x \le k \le x + \Delta x$
which means that $k \to x$ as $\Delta x \to 0$.
So:
{{begin-eqn}}
{{eqn | l = \lim_{\Delta x \mathop \to 0} \map f k
      | r = \lim_{k \mathop \to x} \map f k
}}
{{eqn | r = \map f x
      | c = because $f$ is continuous
}}
{{end-eqn}}
For $\Delta x < 0$, consider $k \in \closedint {x + \Delta x} x$, and the argument is similar.
Hence the result, by the definition of primitive.
{{qed}}
Theorem: Fundamental Theorem of Calculus/First Part

Let $f$ be a real function which is continuous on the closed interval $\closedint a b$.
Let $F$ be a real function which is defined on $\closedint a b$ by:
:$\ds \map F x = \int_a^x \map f t \rd t$
Then $F$ is a primitive of $f$ on $\closedint a b$.

Proof:
By Topological Manifold/Examples/Real Cartesian Space, the closed real interval is a manifold. 
We have that $F$ is a smooth $0$-form with compact support on a smooth $1$-dimensional oriented manifold $\closedint a b$.
We have that the boundary of $\closedint a b$ is $\partial \closedint a b$.
We denote $\d F$ to be the exterior derivative of $F$.
Hence, by the General Stokes' Theorem:
:$\ds \int_{\closedint a b} \rd F = \int_{\partial {\closedint a b} } = \map F b - \map F a$
{{finish|How to use the choice of orientation from the oriented manifold}}
{{qed}}
Theorem: Fundamental Theorem of Calculus/Second Part

Let $f$ be a real function which is continuous on the closed interval $\closedint a b$.
Then:
:$(1): \quad f$ has a primitive on $\closedint a b$
:$(2): \quad$ If $F$ is any primitive of $f$ on $\closedint a b$, then:
:::$\ds \int_a^b \map f t \rd t = \map F b - \map F a = \bigintlimits {\map F t} a b$

Proof:
Let $G$ be defined on $\closedint a b$ by:
:$\ds \map G x = \int_a^x \map f t \rd t$
We have:
:$\ds \map G a = \int_a^a \map f t \rd t = 0$ from Integral on Zero Interval
:$\ds \map G b = \int_a^b \map f t \rd t$ from the definition of $G$ above.
Therefore, we can compute:
{{begin-eqn}}
{{eqn | l = \int_a^b \map f t \rd t
      | r = \int_a^a \map f t \rd t + \int_a^b \map f t \rd t
      | c = Sum of Integrals on Adjacent Intervals for Continuous Functions
}}
{{eqn | r = \map G a + \map G b
      | c = From the definition of $G$
}}
{{eqn | r = \map G b - \map G a
      | c = $\map G a = 0$
}}
{{end-eqn}}
By the first part of the theorem, $G$ is a primitive of $f$ on $\closedint a b$.
By Primitives which Differ by Constant, we have that any primitive $F$ of $f$ on $\closedint a b$ satisfies $\map F x = \map G x + c$, where $c$ is a constant.
Thus we conclude:
{{begin-eqn}}
{{eqn | l = \int_a^b \map f t \rd t
      | r = \paren {\map G b + c} - \paren {\map G a + c}
}}
{{eqn | r = \map F b - \map F a
}}
{{end-eqn}}
{{qed}}
Theorem: Fundamental Theorem of Calculus/Second Part

Let $f$ be a real function which is continuous on the closed interval $\closedint a b$.
Then:
:$(1): \quad f$ has a primitive on $\closedint a b$
:$(2): \quad$ If $F$ is any primitive of $f$ on $\closedint a b$, then:
:::$\ds \int_a^b \map f t \rd t = \map F b - \map F a = \bigintlimits {\map F t} a b$

Proof:
As $f$ is continuous, by the first part of the theorem, it has a primitive. Call it $F$.
$\closedint a b$ can be divided into any number of closed subintervals of the form $\closedint {x_{k - 1} } {x_k}$ where:
:$a = x_0 < x_1 \cdots < x_{k-1} < x_k = b$
Fix such a finite subdivision of the interval $\closedint a b$; call it $P$.
Next, we observe the following telescoping sum identity:
{{begin-eqn}}
{{eqn | n = 1
      | l = \sum_{i \mathop = 1}^k \paren {\map F {x_i} - \map F {x_{i - 1} } }
      | r = \map F b - \map F a
}}
{{end-eqn}}
Because $F' = f$, $F$ is differentiable.
By Differentiable Function is Continuous, $F$ is also continuous.
Therefore we can apply the Mean Value Theorem on $F$.
It follows that in every closed subinterval $I_i = \closedint {x_{i - 1} } {x_i}$ there is some $c_i$ such that:
:$\map {F'} {c_i} = \dfrac {\map F {x_i} - \map F {x_{i - 1} } } {x_i - x_{i - 1} }$ 
It follows that:
{{begin-eqn}}
{{eqn | l = \map F {x_i} - \map F {x_{i - 1} }
      | r = \map {F'} {c_i} \paren {x_i - x_{i - 1} }
}}
{{eqn | n = 2
      | l = \map F b - \map F z 
      | r = \sum_{i \mathop = 1}^k \map {F'} {c_i} \paren {x_i - x_{i - 1} }
      | c = from $(1)$
}}
{{eqn | r = \sum_{i \mathop = 1}^k \map f {c_i} \paren {x_i - x_{i - 1} }
      | c = because $F' = f$
}}
{{end-eqn}}
From the definitions of supremum and infimum, we have for all $i$ (recall $I_i = \closedint {x_{i - 1} } {x_i}$):
:$\displaystyle \inf_{x \mathop \in I_i} \map f x \le \map f {c_i} \le \sup_{x \mathop \in I_i} \map f x$
From the definitions of upper Darboux sum and lower Darboux sum, we conclude for any finite subdivision $P$:
:$\displaystyle \map L P \le \sum_{i \mathop = 1}^k \map f {c_i} \paren {x_i - x_{i - 1} } \le \map U P$
Lastly, from the definition of a definite integral and from $(2)$, we conclude:
:$\displaystyle \map F b - \map F a = \int_a^b \map f t \rd t$
{{qed}}
Theorem: Natural Logarithm of 1 is 0

:$\ln 1 = 0$

Proof:
We use the definition of the natural logarithm as an integral:
:$\ds \ln x = \int_1^x \frac {\d t} t$
From Integral on Zero Interval:
:$\ds \ln 1 = \int_1^1 \frac {\d t} t = 0$
{{qed}}
Theorem: Natural Logarithm of 1 is 0

:$\ln 1 = 0$

Proof:
We use the definition of the natural logarithm as the inverse of the exponential:
:$\ln x = y \iff e^y = x$
Then:
{{begin-eqn}}
{{eqn | l = e^0
      | r = 1
      | c = Exponential of Zero
}}
{{eqn | ll= \leadstoandfrom
      | l = \ln 1
      | r = 0
}}
{{end-eqn}}
{{qed}}
Theorem: Natural Logarithm of 1 is 0

:$\ln 1 = 0$

Proof:
We use the definition of the natural logarithm as the limit of a sequence:
:$\ds \ln x = \lim_{n \mathop \to \infty} n \paren {\sqrt [n] x - 1}$
Then:
{{begin-eqn}}
{{eqn | l = \ln 1
      | r = \lim_{n \mathop \to \infty} n \paren {\sqrt [n] 1 - 1}
}}
{{eqn | r = \lim_{n \mathop \to \infty} n \times 0
}}
{{eqn | r = \lim_{n \mathop \to \infty} 0
}}
{{eqn | r = 0
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Natural Logarithm Function

Let $\ln x$ be the natural logarithm function.
Then:
:$\map {\dfrac \d {\d x} } {\ln x} = \dfrac 1 x$

Proof:
{{begin-eqn}}
{{eqn | l = \ln x
      | o = :=
      | r = \int_1^x \dfrac 1 t \rd t
      | c = {{Defof|Natural Logarithm|subdef = Positive Real|index = 1}}
}}
{{eqn | l = \frac \d {\d x} \ln x
      | r = \frac \d {\d x} \int_1^x \dfrac 1 t \rd t
}}
{{eqn | r = \frac 1 x
      | c = Fundamental Theorem of Calculus
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Natural Logarithm Function

Let $\ln x$ be the natural logarithm function.
Then:
:$\map {\dfrac \d {\d x} } {\ln x} = \dfrac 1 x$

Proof:
This proof assumes the definition of the natural logarithm as the inverse of the exponential function, where the exponential function is defined as the limit of a sequence:
:$e^x := \ds \lim_{n \mathop \to +\infty} \paren {1 + \frac x n}^n$
It also assumes the Laws of Logarithms.
{{begin-eqn}}
{{eqn | l = \map {\frac \d {\d x} } {\ln x}
      | r = \lim_{\Delta x \mathop \to 0} \frac {\map \ln {x + \Delta x} - \ln x} {\Delta x}
      | c = {{Defof|Derivative}}
}}
{{eqn | r = \lim_{\Delta x \mathop \to 0} \frac {\map \ln {\frac {x + \Delta x} x} } {\Delta x}
      | c = Difference of Logarithms
}}
{{eqn | r = \lim_{\Delta x \mathop \to 0} \paren {\frac 1 {\Delta x} \centerdot \map \ln {1 + \frac {\Delta x} x} }
}}
{{eqn | n = 1
      | r = \lim_{\Delta x \mathop \to 0} \paren {\map \ln {\paren {1 + \frac {\Delta x} x}^{1 / \Delta x} } }
      | c = Natural Logarithm of Power
}}
{{end-eqn}}
Define $u$ as:
{{begin-eqn}}
{{eqn | l = u
      | r = \dfrac {\Delta x} x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \Delta x
      | r = u x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac 1 {\Delta x}
      | r = \frac 1 x \cdot \frac 1 u
      | c = 
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | r = \lim_{u \mathop \to 0} \paren {\map \ln {\paren {1 + u}^{\frac 1 u \cdot \frac 1 x} } }
      | c = substituting $u x$ for $\Delta x$ in $(1)$
}}
{{eqn | r = \lim_{u \mathop \to 0} \paren {\frac 1 x \cdot \map \ln {1 + u}^{\frac 1 u} }
      | c = Natural Logarithm of Power
}}
{{eqn | r = \frac 1 x \cdot \lim_{u \mathop \to 0} \paren {\map \ln {1 + u}^{\frac 1 u} }
      | c = factoring out constants
}}
{{eqn | r = \frac 1 x \cdot \lim_{v \mathop \to +\infty} \paren {\map \ln {1 + \frac 1 v}^v}
      | c = substituting $\dfrac 1 v$ for $u$
}}
{{eqn | r = \frac 1 x \cdot \ln e^1
      | c = Limit of Composite Function, Limit definition of $e^x$, Real Natural Logarithm Function is Continuous
}}
{{eqn | r = \frac 1 x
      | c = Exponential of Natural Logarithm
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Natural Logarithm Function

Let $\ln x$ be the natural logarithm function.
Then:
:$\map {\dfrac \d {\d x} } {\ln x} = \dfrac 1 x$

Proof:
This proof assumes the definition of the natural logarithm as the inverse of the exponential function as defined by differential equation:
:$y = \dfrac {\d y} {\d x}$
:$y = e^x \iff \ln y = x$
{{begin-eqn}}
{{eqn | l = \frac {\d y} {\d x}
      | r = y
      | c = {{Defof|Exponential Function/Real|subdef = Differential Equation|Exponential Function}}
}}
{{eqn | l = \int \frac 1 y \rd y 
      | r = \int \rd x
      | c = Solution to Separable Differential Equation
}}
{{eqn | r = x + C_0
      | c = Integral of Constant where that constant is $1$
}}
{{eqn | r = \ln y + C_0
      | c = {{Defof|Natural Logarithm/Positive Real|index = 2|Natural Logarithm}}: $x = \ln y$
}}
{{end-eqn}}
The result follows from the definition of the antiderivative and the defined  initial condition:
:$\tuple {x_0, y_0} = \tuple {0, 1}$
{{qed}}
Theorem: Derivative of Natural Logarithm Function

Let $\ln x$ be the natural logarithm function.
Then:
:$\map {\dfrac \d {\d x} } {\ln x} = \dfrac 1 x$

Proof:
This proof assumes the definition of the natural logarithm as the limit of a sequence of real functions.
Let $\sequence {f_n}$ be the sequence of mappings $f_n: \R_{>0} \to \R$ defined as:
:$\map {f_n} x = n \paren {\sqrt [n] x - 1}$
Fix $x_0 \in \R_{>0}$.
Pick $k \in \N : x_0 \in J := \closedint {\dfrac 1 k} k$.
From definition of bounded interval, $J$ is bounded.
From Derivative of Nth Root and Combination Theorem for Sequences:
:$\forall n \in \N : \forall x \in J : D_x \map {f_n} x = \dfrac {\sqrt [n] x} x$
In particular:
:$\forall n: f_n$ is differentiable on $J$
From Defining Sequence of Natural Logarithm is Convergent, $\sequence {\map {f_n} {x_0} }$ is convergent.
=== Lemma ===
{{:Derivative of Natural Logarithm Function/Proof 4/Lemma}}{{qed|lemma}}
From the lemma, $\sequence { {f_n}'}$ converges uniformly to $\dfrac 1 x$ on $J$.
From Derivative of Uniformly Convergent Sequence of Differentiable Functions, $\map {f'} x = \dfrac 1 x$ on $J$
In particular:
:$\map {f'} {x_0} = \dfrac 1 {x_0}$
Hence the result.
{{qed}}
Theorem: Logarithm is Strictly Increasing

:$\ln x: x > 0$ is strictly increasing.

Proof:
From Derivative of Natural Logarithm Function $D \ln x = \dfrac 1 x$, which is strictly positive on $x > 0$.
From Derivative of Monotone Function it follows that $\ln x$ is strictly increasing on $x > 0$.
{{qed}}
Theorem: Logarithm Tends to Infinity

:$\ln x \to +\infty$ as $x \to +\infty$

Proof:
From Natural Logarithm of 2 is Greater than One Half:
:$\ln 2 \ge \dfrac 1 2$
From the definition of infinite limit at infinity, our assertion is:
:$\forall M \in \R_{>0} : \exists N > 0 : x > N \implies \ln x > M$.
As $x \to +\infty$, we will restrict our attention to sufficiently large $M$.
From Logarithm is Strictly Increasing:
:$\ln x$ is strictly increasing.
So, for sufficiently large $M$:
:$x > 2^{2 M} \implies \ln x > \ln 2^{2 M}$
From the Laws of Logarithms:
{{begin-eqn}}
{{eqn | l = \ln 2^{2 M}
      | r = 2 M \ln 2
}}
{{eqn | o = \ge 
      | r = 2 M \cdot \dfrac 1 2
}}
{{eqn | r = M
}}
{{end-eqn}}
Choosing $N = \ln 2^{2 M}$:
:$\forall M \ge a: \exists N > 0: x > N \implies \ln x > M$
for some $a \in \R$.
Hence the result, by the definition of infinite limit at infinity.
{{qed}}
Theorem: Logarithm Tends to Infinity

:$\ln x \to +\infty$ as $x \to +\infty$

Proof:
From the definition of the natural logarithm:
{{begin-eqn}}
{{eqn | l = \ln x
      | r = \int_1^x \dfrac 1 t \rd t
}}
{{end-eqn}}
The result follows from Integral of Reciprocal is Divergent.
{{qed}}
Theorem: Logarithm Tends to Negative Infinity

:$\ln x \to -\infty$ as $x \to 0^+$

Proof:
From the definition of natural logarithm:
{{begin-eqn}}
{{eqn | l = \ln x
      | r = \int_1^x \dfrac 1 t \ \mathrm dt
}}
{{end-eqn}}
The result follows from Integral of Reciprocal is Divergent.
{{qed}}
Theorem: Second Derivative of Natural Logarithm Function

Let $\ln x$ be the natural logarithm function.
Then:
:$\map {\dfrac {\d^2} {\d x^2} } {\ln x} = -\dfrac 1 {x^2}$

Proof:
From Derivative of Natural Logarithm Function:
:$\dfrac \d {\d x} \ln x = \dfrac 1 x$
From the Power Rule for Derivatives: Integer Index:
:$\dfrac {\d^2} {\d x^2} \ln x = \dfrac \d {\d x} \dfrac 1 x = -\dfrac 1 {x^2}$
{{qed}}
Theorem: Exponential is Strictly Increasing

:The function $\map f x = \exp x$ is strictly increasing.

Proof:
By definition, the exponential function is the inverse of the natural logarithm function.
From Logarithm is Strictly Increasing, $\ln x$ is strictly increasing.
The result follows from Inverse of Strictly Monotone Function.
{{qed}}
Theorem: Exponential is Strictly Increasing

:The function $\map f x = \exp x$ is strictly increasing.

Proof:
For all $x \in \R$:
{{begin-eqn}}
{{eqn | l = D_x \exp x
      | r = \exp x
      | c = Derivative of Exponential Function
}}
{{eqn | o = >
      | r = 0
      | c = Exponential of Real Number is Strictly Positive
}}
{{end-eqn}}
Hence the result, from Derivative of Monotone Function.
{{qed}}
Theorem: Exponential Tends to Zero and Infinity

:$\exp x \to +\infty$ as $x \to +\infty$
:$\exp x \to 0$ as $x \to -\infty$
Thus the exponential function has domain $\R$ and image $\openint 0 \infty$.

Proof:
=== The exponential function approaches positive infinity as x approaches positive infinity ===
Let $M$ be a strictly positive real number.
Let $N$ be $\ln M$.
$N$ is real because $M > 0$.
From Exponential is Strictly Increasing:
:$\forall x: x > N \implies \exp x > \exp N = M$
Therefore:
:$\forall M \in \R_{>0} : \exists N \in \R : \forall x > N : \exp x > M$
The result follows from the definition of infinite limit at infinity.
{{qed}}
Theorem: Exponential of Natural Logarithm

: $\forall x > 0: \map \exp {\ln x} = x$
: $\forall x \in \R: \map \ln {\exp x} = x$

Proof:
From the definition of the exponential function:
:$e^y = x \iff \ln x = y$
Raising both sides of the equation $\ln x = y$ to the power of $e$:
{{begin-eqn}}
{{eqn | l = e^{\ln x}
      | r = e^y
      | c = 
}}
{{eqn | r = x
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Exponential Function
Category:Natural Logarithms
lm9xjtrvp6hurqg1fig5wmpsd84gd5u
Theorem: Exponent Combination Laws/Product of Powers

:$a^x a^y = a^{x + y}$

Proof:
{{begin-eqn}}
{{eqn | l = a^{x + y}
      | r = \map \exp {\paren {x + y} \ln a}
      | c = {{Defof|Power to Real Number}}
}}
{{eqn | r = \map \exp {x \ln a + y \ln a}
      | c = 
}}
{{eqn | r = \map \exp {x \ln a} \, \map \exp {y \ln a}
      | c = Exponential of Sum
}}
{{eqn | r = a^x a^y
      | c = {{Defof|Power to Real Number}}
}}
{{end-eqn}}
{{qed}}
Theorem: Exponent Combination Laws/Product of Powers

:$a^x a^y = a^{x + y}$

Proof:
Let $x, y \in \R$.
From Rational Sequence Decreasing to Real Number, there exist rational sequences $\sequence {x_n}$ and $\sequence {y_n}$ converging to $x$ and $y$, respectively.
Then, since Power Function on Strictly Positive Base is Continuous: Real Power:
{{begin-eqn}}
{{eqn | l = a^{x + y}
      | r = a^{\ds \paren {\lim_{n \mathop \to \infty} x_n + \lim_{n \mathop \to \infty} y_n} }
}}
{{eqn | r = a^{\ds \paren {\lim_{n \mathop \to \infty} \paren {x_n + y_n} } }
      | c = Sum Rule for Real Sequences
}}
{{eqn | r = \lim_{n \mathop \to \infty} a^{x_n + y_n}
      | c = Sequential Continuity is Equivalent to Continuity in the Reals
}}
{{eqn | r = \lim_{n \mathop \to \infty} \paren {a^{x_n} a^{y_n} }
      | c = Sum of Indices of Real Number: Rational Numbers
}}
{{eqn | r = \paren {\lim_{n \mathop \to \infty} a^{x_n} } \paren {\lim_{n \mathop \to \infty} a^{y_n} }
      | c = Product Rule for Real Sequences
}}
{{eqn | r = a^x a^y
      | c = Sequential Continuity is Equivalent to Continuity in the Reals
}}
{{end-eqn}}
{{qed}}