nyuuzyou/wikis huggingface dataset:
Equivalence of Definitions of Principal Ideal of Preordered Set

== Theorem ==
Let $\struct {S, \preceq}$ be a preordered set.
Let $I$ be an ideal in $S$.
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
=== Definition $1$ implies Definition $2$ ===
Assume that
:$\exists x \in I: x$ is upper bound for $I$
We will prove that
:$I \subseteq x^\preceq$
Let $y \in I$.
By definition of upper bound:
:$y \preceq x$
Thus by definition of lower closure of element:
:$y \in x^\preceq$
We will prove that
:$x^\preceq \subseteq I$
Let $y \in x^\preceq$.
By definition of lower closure of element:
:$y \preceq x$
Thus by definition of lower section:
:$y \in I$
Thus by definition of set equality:
:$\exists x \in S: I = x^\preceq$
=== Definition $2$ implies Definition $1$ ===
Assume that:
:$\exists x \in S: I = x^\preceq$
By definition of reflexivity:
:$x \preceq x$
Thus by definition of lower closure of element:
:$x \in I$
Let $y \in I$.
Thus by definition of lower closure of element:
:$y \preceq x$
== Sources ==
* 
Category:Principal Ideals of Preordered Sets
Equivalence of Definitions of Projective Module

== Theorem ==
Let $A$ be a ring.
Let $M$ be an $A$-module.
The following are equivalent:
:$(1): \quad$ $M$ is a projective module, that is, $M$ is a projective object in the category of left $A$-modules.
:$(2): \quad$ $M$ is a direct summand of a free module.
:$(3): \quad$ Every short exact sequence of the form:
::$\xymatrix{
0 \ar[r] & X \ar[r]^f & Y \ar[r]^g & M \ar[r] & 0
}$
splits, that is, there is a homomorphism $s : M \to Y$ with $g \circ s = \operatorname {id}_M$.
== Proof ==
=== $(1)$ implies $(2)$ ===
By Surjection by Free Module there is a free module $Y$ and a surjection $g : Y \to M$.
By Epimorphism of modules iff surjective $g$ is an epimorphism.
By Definition:Projective Object applied to $\operatorname {id}_M$, there is a homomorphism $s : M \to Y$ with $g \circ s = \operatorname {id}_M$.
We have $Y = \map {\operatorname {im} } s \oplus \map \ker g$.
=== $(2)$ implies $(1)$ ===
Assume that there is an $A$-module $Q$ such that $M \oplus Q$ is free.
Let $f : Y \to Z$ be an epimorphism.
Let $h : M \to Z$ be a homomorphism.
Let $S$ be a basis of $M \oplus Q$.
By Epimorphism of modules iff surjective $f$ is surjective.
Hence for all $s \in S$, there is some $y_s \in Y$ with $\map f {y_s} = \map h {\map {\pr_1} s}$, where $\pr_1: M \oplus Q \to M$ denotes projection to $M$.
By Universal Property of Free Modules there is a unique homomorphism $t : M \oplus Q \to Y$, such that $f \circ t = h \circ \pr_1$.
We have $f \circ (t \circ i_1) = h \circ \pr_1 \circ i_1 = h$, where $i_1 : M \to M \oplus Q$ is the inclusion of the first summand.
It follows, that $t \circ i_1$ is the desired lift of $f$.
=== $(2)$ implies $(3)$ ===
Assume that there is an $A$-module $Q$ such that $M \oplus Q$ is free.
Consider a short exact sequence $\xymatrix{
0 \ar[r] & X \ar[r]^f & Y \ar[r]^g & M \ar[r] & 0
}$.
Let $M \oplus Q \xrightarrow r M$ be the canonical projection.
We will construct a lift of $r$ across $g$.
Let $\set {e_i}_{i \mathop \in I}$ be a basis of $M \oplus Q$.
Let $m_i = \map r {e_i}$ and choose a $b_i \in \map {g^{-1}} {m_i}$ for each $i \in I$.
By the Universal Property of Free Module on Set, there exists a morphism $\phi: M \oplus Q \to B$ such that $\map \phi {e_i} = b_i$ for all $i \in I$.
For all $i \in I$, the image of $e_i$ under $M \oplus Q \xrightarrow \phi B \xrightarrow g M$ is, by construction, $m_i$.
Likewise for $M \oplus Q \xrightarrow r M$.
Therefore, by the Universal Property of Free Module on Set, $r = g \circ \phi$.
Now restrict along the canonical inclusion $M \xrightarrow s M \oplus Q$, which is a section of $r$.
We obtain $1_P = r \circ s = g \circ \phi \circ s$.
Therefore $\phi s$ is a section of $g$.
=== $(3)$ implies $(2)$ ===
By Surjection by Free Module there is a free module $Y$ and a surjection $g : Y \to M$.
There is a short exact sequence:
$\xymatrix{
0 \ar[r] & \map \ker g \ar[r] & Y \ar[r]^g & M \ar[r] & 0
}$
By Structure of Split Exact Sequence there is an isomorphism $Y \cong M \oplus \map \ker g$.
Category:Projective Modules
Equivalence of Definitions of Quasi-Reflexive Relation

== Theorem ==
Let $\RR \subseteq S \times S$ be a relation in $S$.
=== Definition 1 ===
=== Definition 2 ===
=== Definition 3 ===
== Proof ==
=== $(1)$ implies $(3)$ ===
Let $\RR$ be a quasi-reflexive relation by definition $1$.
Then by definition:
:$\forall x, y \in S: \tuple {x, y} \in \RR \implies \tuple {x, x} \in \RR \land \tuple {y, y} \in \RR$
That is:
:$\forall x, y \in S: \tuple {x, y} \in \RR \implies \tuple {x, x} \in \RR$
and:
:$\forall x, y \in S: \tuple {x, y} \in \RR \implies \tuple {y, y} \in \RR$
Hence:
:$\RR$ is a left quasi-reflexive relation by definition
and:
:$\RR$ is a right quasi-reflexive relation by definition.
Thus $\RR$ is a quasi-reflexive relation by definition $3$.
=== $(3)$ implies $(2)$ ===
Let $\RR$ be a quasi-reflexive relation by definition $3$.
Then by definition:
:$\RR$ is a left quasi-reflexive relation
and:
:$\RR$ is a right quasi-reflexive relation.
Hence by definition of left quasi-reflexive relation:
:$\forall x \in \Dom \RR: \tuple {x, x} \in \RR$
and by definition of right quasi-reflexive relation:
:$\forall x \in \Img \RR: \tuple {x, x} \in \RR$
Let $x \in \Field \RR$ be arbitrary.
Then by definition of field of relation:
:$x \in \Dom \RR \cup \Img \RR$
That is, either:
:$x \in \Dom \RR$, in which case $\tuple {x, x} \in \RR$
or:
:$x \in \Img \RR$, in which case $\tuple {x, x} \in \RR$.
In both cases $\tuple {x, x} \in \RR$.
As $x \in \Field \RR$ is arbitrary:
:$\forall x \in \Field \RR: \tuple {x, x} \in \RR$
Thus $\RR$ is a quasi-reflexive relation by definition $2$.
=== $(2)$ implies $(1)$ ===
Let $\RR$ be a quasi-reflexive relation by definition $2$.
:$\forall x \in \Field \RR: \tuple {x, x} \in \RR$
Let $\tuple {x, y} \in \RR$ be arbitrary.
By definition of domain of mapping:
:$x \in \Dom \RR$
and so by definition of field of relation:
:$x \in \Field \RR$
Thus :
:$\tuple {x, x} \in \RR$
Simlarly, by definition of image set of mapping:
:$y \in \Img \RR$
and so by definition of field of relation:
:$y \in \Field \RR$
Thus :
:$\tuple {y, y} \in \RR$
That is:
:$\tuple {x, x} \in \RR \land \tuple {y, y} \in \RR$
As $\tuple {x, y} \in \RR$ is arbitrary:
:$\forall \tuple {x, y} \in \RR: \tuple {x, x} \in \RR \land \tuple {y, y} \in \RR$
Thus $\RR$ is a quasi-reflexive relation by definition $1$.
Category:Quasi-Reflexive Relations
Equivalence of Definitions of Quasiamicable Numbers

== Theorem ==
Let $m \in \Z_{>0}$ and $n \in \Z_{>0}$ be (strictly) positive integers.
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
Let $\map s n$ denote the sum of the proper divisors of (strictly) positive integer $n$.
The sum of all the divisors of a (strictly) positive integer $n$ is $\map {\sigma_1} n$, where $\sigma_1$ is the divisor sum function.
The proper divisors of $n$ are the divisors $n$ with $1$ and $n$ excluded.
Thus:
:$\map s n = \map {\sigma_1} n - n - 1$
Suppose:
:$\map s n = m$
and:
:$\map s m = n$
Then:
Similarly:
Thus:
:$\map s n = \map s m = m + n + 1$
The argument reverses.
Category:Quasiamicable Numbers
Equivalence of Definitions of Quasiperfect Number

== Theorem ==
The following definitions of a quasiperfect number are equivalent:
=== Definition 1 ===
=== Definition 2 ===
=== Definition 3 ===
== Proof ==
By definition of abundance:
:$\map A n = \map {\sigma_1} n - 2 n$
By definition of divisor sum function:
:$\map {\sigma_1} n$ is the sum of all the divisors of $n$.
Thus $\map {\sigma_1} n - n$ is the sum of the aliquot parts of $n$.
Hence the result.
Category:Quasiperfect Numbers
Equivalence of Definitions of Quaternion Modulus

== Theorem ==
Let $\mathbf x = a \mathbf 1 + b \mathbf i + c \mathbf j + d \mathbf k$ be a quaternion, where $a, b, c, d \in \R$.
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
Let $\mathbf x = \begin{bmatrix} a + b i & c + d i \\ -c + d i & a - b i \end{bmatrix}$ be the matrix form of quaternion $\mathbf x$.
Category:Quaternion Modulus
Equivalence of Definitions of Reachable

== Theorem ==
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
Let $G = \struct {V, A}$ be a digraph.
Let $u, v \in V$.
Let $\RR$ be the reachability relation for $G$, defined as the transitive closure of $A$.
=== Definition 1 implies Definition 2 ===
Suppose that $v$ is reachable from $u$ by definition 1.
Then there exists a directed walk $\tuple {u = x_0, \dots, x_n = v}$ from $u$ to $v$.
Then by the definition of directed walk:
:$x_0 \mathrel \RR x_1 \mathrel \RR \cdots \mathrel \RR x_n$
Then by the definition of transitive closure:
:$u \mathrel \RR v$
Thus $v$ is reachable from $u$ by definition 2.
=== Definition 2 implies Definition 1 ===
Suppose that $v$ is reachable from $u$ by definition 2.
That is:
:$u \mathrel \RR v$
Thus by the definition of transitive closure:
:$\exists x_0, \ldots, x_n \in V: x_0 \mathrel \RR x_1 \mathrel \RR \cdots \mathrel \RR x_n$
Then $\tuple {x_0 \mathrel \RR x_1 \mathrel \RR \cdots \mathrel \RR x_n}$ is a directed walk from $u$ to $v$.
Therefore, $v$ is reachable from $u$ by definition 1.
Category:Digraphs
Equivalence of Definitions of Real Area Hyperbolic Cosecant

== Theorem ==
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
=== Definition 1 implies Definition 2 ===
If $x \ge 0$, then:
If $x < 0$, then:
That is:
:$y = \map \ln {\dfrac 1 x + \dfrac {\sqrt {1 + x^2} } {\size x} }$
=== Definition 2 implies Definition 1 ===
Therefore:
== Also see ==
* Equivalence of Definitions of Real Area Hyperbolic Sine
* Equivalence of Definitions of Real Area Hyperbolic Cosine
* Equivalence of Definitions of Real Area Hyperbolic Tangent
* Equivalence of Definitions of Real Area Hyperbolic Cotangent
* Equivalence of Definitions of Real Area Hyperbolic Secant
Category:Inverse Hyperbolic Cosecant
Equivalence of Definitions of Real Area Hyperbolic Cosine

== Theorem ==
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
=== Definition 1 implies Definition 2 ===
Let $x = \cosh y$, where $y > 0$.
Let $z = e^y$.
Then:
Also, from Minimum of Real Hyperbolic Cosine Function:
:$x = \cosh y \ge 1$
Also:
Thus $x - \sqrt {x^2 - 1}$ is (strictly) positive.
 $x - \sqrt {x^2 - 1} > 1$.
Then:
and a contradiction is deduced.
Therefore:
:$x - \sqrt {x^2 - 1} < 1$
From Logarithm is Strictly Increasing:
:$y = \map \ln {x - \sqrt {x^2 - 1} } < \ln 1 = 0$
Since $y$ is (strictly) positive from the first definition of real inverse hyperbolic cosine:
:$y = \map \ln {x + \sqrt {x^2 - 1} }$
=== Definition 2 implies Definition 1 ===
Let $z = x + \sqrt {x^2 - 1}$.
Then:
:$y = \ln z$
If $-1 < x < 1$, $z$ is not defined.
If $x \le -1$:
If $x \ge 1$, $z \ge 1$.
Therefore, $y = \ln z \ge \ln 1 = 0$.
Therefore:
== Also see ==
* Equivalence of Definitions of Real Area Hyperbolic Sine
* Equivalence of Definitions of Real Area Hyperbolic Tangent
* Equivalence of Definitions of Real Area Hyperbolic Cosecant
* Equivalence of Definitions of Real Area Hyperbolic Secant
* Equivalence of Definitions of Real Area Hyperbolic Cotangent
Category:Inverse Hyperbolic Cosine
Equivalence of Definitions of Real Area Hyperbolic Cotangent

== Theorem ==
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
=== Definition 1 implies Definition 2 ===
=== Definition 2 implies Definition 1 ===
Therefore:
== Also see ==
* Equivalence of Definitions of Real Area Hyperbolic Sine
* Equivalence of Definitions of Real Area Hyperbolic Cosine
* Equivalence of Definitions of Real Area Hyperbolic Tangent
* Equivalence of Definitions of Real Area Hyperbolic Secant
* Equivalence of Definitions of Real Area Hyperbolic Cosecant
Category:Inverse Hyperbolic Cotangent
Equivalence of Definitions of Real Area Hyperbolic Secant

== Theorem ==
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
=== Definition 1 implies Definition 2 ===
=== Definition 2 implies Definition 1 ===
Therefore:
== Also see ==
* Equivalence of Definitions of Real Area Hyperbolic Sine
* Equivalence of Definitions of Real Area Hyperbolic Cosine
* Equivalence of Definitions of Real Area Hyperbolic Tangent
* Equivalence of Definitions of Real Area Hyperbolic Cotangent
* Equivalence of Definitions of Real Area Hyperbolic Cosecant
Category:Inverse Hyperbolic Secant
Equivalence of Definitions of Real Area Hyperbolic Sine

== Theorem ==
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
=== Definition 1 implies Definition 2 ===
Let $x = \sinh y$.
Let $z = e^y$.
Then:
If $x \ge 0$, then:
If $x < 0$, then:
Since the natural logarithm of a negative number is not defined:
:$y = \map \ln {x + \sqrt {x^2 + 1} }$
=== Definition 2 implies Definition 1 ===
Let $y = x + \sqrt {x^2 + 1}$.
Therefore:
== Also see ==
* Equivalence of Definitions of Real Area Hyperbolic Cosine
* Equivalence of Definitions of Real Area Hyperbolic Tangent
* Equivalence of Definitions of Real Area Hyperbolic Cosecant
* Equivalence of Definitions of Real Area Hyperbolic Secant
* Equivalence of Definitions of Real Area Hyperbolic Cotangent
Category:Inverse Hyperbolic Sine
Equivalence of Definitions of Real Area Hyperbolic Tangent

== Theorem ==
Let $S$ denote the open real interval:
:$S := \openint {-1} 1$
=== Definition 1 ===
=== Definition 2 ===
== Proof ==
=== Definition 1 implies Definition 2 ===
Let $x = \tanh y$.
Then:
=== Definition 2 implies Definition 1 ===
Let $y = \dfrac {1 + x} {1 - x}$.
Therefore:
== Also see ==
* Equivalence of Definitions of Real Area Hyperbolic Sine
* Equivalence of Definitions of Real Area Hyperbolic Cosine
* Equivalence of Definitions of Real Area Hyperbolic Cosecant
* Equivalence of Definitions of Real Area Hyperbolic Secant
* Equivalence of Definitions of Real Area Hyperbolic Cotangent
Category:Inverse Hyperbolic Tangent
Equivalence of Definitions of Real Exponential Function

== Theorem ==
=== As a Power Series Expansion ===
=== As a Limit of a Sequence ===
=== As an Extension of the Rational Exponential ===
=== As the Inverse of the Natural Logarithm ===
=== As the Solution of a Differential Equation ===
== Proof ==
=== Inverse of Natural Logarithm implies Limit of Sequence ===
=== Limit of Sequence implies Power Series Expansion ===
=== Limit of Sequence implies Extension of Rational Exponential ===
=== Extension of Rational Exponential implies Solution of Differential Equation ===
=== Power Series Expansion equivalent to Solution of Differential Equation ===
=== Inverse of Natural Logarithm equivalent to Solution of Differential Equation ===
== Also see ==
* Equivalence of Definitions of Complex Exponential Function
* Equivalence of Definitions of Euler's Number
* Equivalence of Definitions of Real Natural Logarithm
Category:Exponential Function
Category:Equivalence of Definitions of Exponential Function
Equivalence of Definitions of Real Exponential Function/Extension of Rational Exponential implies Differential Equation

== Theorem ==
The following definition of the concept of the real exponential function:
=== As an Extension of the Rational Exponential ===
implies the following definition:
=== As the Solution of a Differential Equation ===
== Proof ==
Let $\exp x$ be the real function defined as the extension of rational exponential.
Then we have:
The application of Derivative of Exponential at Zero is not circular as the referenced proof does not depend on $D_x \exp x = \exp x$.
Category:Equivalence of Definitions of Exponential Function
Equivalence of Definitions of Real Exponential Function/Inverse of Natural Logarithm equivalent to Differential Equation

== Theorem ==
=== As the Inverse of the Natural Logarithm ===
=== As the Solution of a Differential Equation ===
== Proof ==
==== Inverse of Natural Logarithm implies Solution of Differential Equation ====
Let $\exp x$ be the real function defined as the inverse of the natural logarithm:
:$y = \exp x \iff x = \ln y$
Then:
This proves that $y$ is a solution of the differential equation.
It remains to be proven that $y$ fulfills the initial condition: 
That is:
$\exp x$ is the particular solution of the differential equation:
:$\dfrac {\d y} {\d x} = y$
satisfying the initial condition $\map f 0 = 1$.
==== Solution of Differential Equation implies Inverse of Natural Logarithm ====
Let $\exp x$ be the real function defined as the particular solution of the differential equation:
:$\dfrac {\d y} {\d x} = y$
satisfying the initial condition $\map f = 1$.
Thus:
To solve for $C$, put $\tuple {x_0, y_0} = \tuple {0, 1}$:
That is:
:$y = \exp x \iff x = \ln y$
Category:Equivalence of Definitions of Exponential Function
Equivalence of Definitions of Real Exponential Function/Inverse of Natural Logarithm implies Limit of Sequence

== Theorem ==
The following definition of the concept of the real exponential function:
=== As the Inverse of the Natural Logarithm ===
implies the following definition:
=== As the Limit of a Sequence ===
== Proof ==
Let $\exp x$ be the real function defined as the inverse of the natural logarithm:
:$y = \exp x \iff x = \ln y$
Let $\left \langle {x_n} \right \rangle$ be the sequence in $\R$ defined as:
:$x_n = \paren {1 + \dfrac x n}^n$
First it needs to be noted that $\sequence {x_n}$ does indeed converge to a limit.
From Equivalence of Definitions of Real Exponential Function: Limit of Sequence implies Power Series Expansion, we have:
:$\ds \lim_{n \mathop \to \infty} \paren {1 + \dfrac x n}^n = \sum_{n \mathop = 0}^\infty \frac {x^n} {n!}$
From Series of Power over Factorial Converges, the is indeed shown to converge to a limit.
It will next be shown that:
:$\ds \map \ln {\lim_{n \mathop \to \infty} \sequence {x_n} } = x$
We have:
From Limit of Sequence is Limit of Real Function, we can consider the differentiable analogue of the sequence.
From Derivative of Logarithm at One we have:
:$\ds \lim_{x \mathop \to 0} \frac {\map \ln {1 + x} } x = 1$
But $x n^{-1} \to 0$ as $n \to \infty$ from Sequence of Powers of Reciprocals is Null Sequence.
Thus:
:$\ds x \frac {\map \ln {1 + x n^{-1} } } {x n^{-1} } \to x$
as $n \to \infty$.
From Exponential Function is Continuous:
:$\paren {1 + \dfrac x n}^n = \exp \paren {n \map \ln {1 + \dfrac x n} } \to \exp x = e^x$
as $n \to \infty$.
== Sources ==
* : $\S 14.7 \ (3)$
Category:Equivalence of Definitions of Exponential Function
Equivalence of Definitions of Real Exponential Function/Limit of Sequence implies Extension of Rational Exponential

== Theorem ==
The following definition of the concept of the real exponential function:
=== As the Limit of a Sequence ===
implies the following definition:
=== As an Extension of the Rational Exponential ===
== Proof ==
Let the restriction of the exponential function to the rationals be defined as:
:$\ds \exp \restriction_\Q: x \mapsto \lim_{n \mathop \to +\infty} \paren {1 + \frac x n}^n$
Thus, let $e$ be Euler's Number defined as:
:$e = \ds \lim_{n \mathop \to +\infty} \paren {1 + \frac 1 n}^n$
For $x = 0$:
For $x \ne 0$:
where the continuity in the last step follows from Power Function to Rational Power permits Unique Continuous Extension.
For $x \in \R \setminus \Q$, we invoke Power Function to Rational Power permits Unique Continuous Extension.
== Sources ==
* : $\S 5.5$
Category:Equivalence of Definitions of Exponential Function
Equivalence of Definitions of Real Exponential Function/Limit of Sequence implies Power Series Expansion

== Theorem ==
The following definition of the concept of the real exponential function:
=== As the Limit of a Sequence ===
implies the following definition:
=== As a Power Series Expansion ===
== Proof ==
Let $\exp x$ be the real function defined as the limit of the sequence:
:$\exp x := \ds \lim_{n \mathop \to \infty} \paren {1 + \frac x n}^n$
From the General Binomial Theorem:
From Power over Factorial, this converges to:
:$\exp x - \paren {\dfrac {x^0} {0!} + \dfrac {x^1} {1!} + \dfrac {x^2} {2!} + \dfrac {x^3} {3!} + \cdots} = 0$
as $n \to +\infty$.
Category:Equivalence of Definitions of Exponential Function
Equivalence of Definitions of Real Exponential Function/Power Series Expansion equivalent to Differential Equation

== Theorem ==
=== As a Power Series Expansion ===
=== As the Solution of a Differential Equation ===
== Proof ==
==== Power Series Expansion implies Solution of Differential Equation ====
Let $\exp x$ be the real function defined as the sum of the power series:
:$\exp x := \ds \sum_{n \mathop = 0}^\infty \frac {x^n} {n!}$
Let $y = \ds \sum_{n \mathop = 0}^\infty \frac {x^n} {n!}$.
Then:
Setting $x = 0$ we find:
That is:
$\exp x$ is the particular solution of the differential equation:
:$\dfrac {\d y} {\d x} = y$
satisfying the initial condition $\map f 0 = 1$.
==== Solution of Differential Equation implies Power Series Expansion ====
Let $\exp x$ be the real function defined as the particular solution of the differential equation:
:$\dfrac {\d y} {\d x} = y$
satisfying the initial condition $\map f 0 = 1$.
We have Taylor Series Expansion for Exponential Function:
Category:Equivalence of Definitions of Exponential Function
Equivalence of Definitions of Real Exponential Function/Proof 2

== Theorem ==
The following definitions of the exponential function are equivalent.
=== As a Power Series Expansion ===
=== As a Limit of a Sequence ===
=== As an Extension of a Rational Exponential ===
=== As the Inverse of the Natural Logarithm ===
=== As the Solution of a Differential Equation ===
== Proof ==
From Derivative of Exponential Function and Exponential of Zero, each definition of $\exp$ satisfies the following:
:$(1): \quad D_x \exp = \exp$
:$(2): \quad \map \exp 0 = 1$
on $\R$.
From Exponential Function is Well-Defined, such a solution is unique.
Thus they all are all equivalent.
Category:Equivalence of Definitions of Exponential Function
Equivalence of Definitions of Real Interval

== Theorem ==
=== Definition 1 ===
=== Definition 2 ===
== Outline of proof ==
That an interval according to the second definition is an interval according to the first, follows by the Ordering Properties of Real Numbers.
To prove the other direction, we distinguish according to if the subset is bounded on the left or on the right, and use the Continuum Property.
== Proof ==
=== 1 implies 2 ===
Let $I \subset \R$ be a subset such that:
:$\forall x, y \in I : \forall z \in \R : \paren {x \le z \le y \implies z \in I}$
Let:
:$a = \map \inf I$ (or $a = -\infty$ if $I$ is not bounded below)
:$b = \map \sup I$ (or $b = +\infty$ if $I$ is not bounded above).
We will prove that:
:$\openint a b \subseteq I \subseteq \closedint a b$
In order not to need to provide a long list of cases, the temporary convention is used:
:A square bracket "$[$" or "$]$" next to $\pm \infty$ means the same as a round bracket "$($" or "$)$"
:$\openint a b$ means $\O$ $a = b$.
Let $z \in \openint a b$.
Then $z \ge a$, so $\exists x \in I: x \le z$ by definition of $a$.
Similarly $z \le b$, so $\exists y \in S: z \le y$ by definition of $b$.
Hence by hypothesis $z \in I$.
This proves that $\openint a b \subseteq I$.
From the definitions of $a$ and $b$ it follows that $I \subseteq \closedint a b$.
But if $\openint a b \subseteq I \subseteq \closedint a b$, then $I$ must be one of the various types of real interval.
=== 2 implies 1 ===
If $I$ is a real interval of any of the various kinds, then it clearly has this property by definition.
== Sources ==
* : $6.2$: Connectedness: Lemma $6.2.6$
* : $\S 2$: Continuum Property: $\S 2.9$: Intervals
Category:Real Intervals
Equivalence of Definitions of Real Natural Logarithm/Proof 1

== Theorem ==
== Proof ==
=== Definition 1 implies Definition 2 ===
Let $\map F x$ be $\ds \int_1^x \frac {\d t} t$.
Let $\map f t$ be $\ds \int \frac {\d t} t$.
Then:
:$\dfrac {\d t} t = \dfrac 1 t$
Or:
:$\dfrac {\d x} x = \dfrac 1 x$
Also:
:$\map F x = \map f x - \map f 1$
Therefore:
Furthermore:
:$\map F 1 = \map f 1 - \map f 1 = 0$
The result follows from the fifth definition of the exponential function:
:$\map F x \equiv e^x$
=== Definition 2 implies Definition 1 ===
Let $\map f t$ be $\ds \int \frac 1 t \rd t$.
Then:
:$\map F x = \map f x + C$
When $\map F x = 0$:
:$x = e^{\map F x} = 1$
:$\map F 1 = \map f 1 + C = 0 \implies \map f 1 = - C$
Therefore:
:$\map F x = \map f x - \map f 1$
Therefore:
:$\ds \map F x = \int_1^x \frac {\d t} t$
Therefore:
Category:Natural Logarithms