avewright/proofwiki-math huggingface dataset:
Theorem: Complex Roots of Polynomial with Real Coefficients occur in Conjugate Pairs

Let $\map f z = a_n z^n + a_{n - 1} z^{n - 1} + \cdots + a_1 z + a_0$ be a polynomial over complex numbers where $a_0, \ldots, a_n$ are real numbers.
Let $\alpha \in \C$ be a root of $f$.
Then $\overline \alpha$ is also a root of $f$, where $\overline \alpha$ denotes the complex conjugate of $\alpha$.
That is, all complex roots of $f$ appear as conjugate pairs.

Proof:
Let $\alpha = p + q i$.
Let $p + q i$ be expressed in exponential form as $\alpha = r e^{i \theta}$.
As $\alpha = r e^{i \theta}$ satisfies $\map f \alpha = 0$, it follows that:
:$a_n r^n e^{n i \theta} + a_{n - 1} r^{n - 1} e^{\paren {n - 1} i \theta} + \dotsb + a_1 r e^{i \theta} + a_0 = 0$
Taking the conjugate of both sides:
:$a_n r^n e^{-n i \theta} + a_{n - 1} r^{n - 1} e^{-\paren {n - 1} i \theta} + \dotsb + a_1 r e^{-i \theta} + a_0 = 0$
it follows that $\overline \alpha = p - q i$ is also a root of $f$.
If any of the $a_k$ are complex, then the conjugate of $f$ is not the same polynomial as $f$.
Therefore the result holds only for real coefficients.
{{qed}}
Theorem: Sum of Squares of Complex Moduli of Sum and Differences of Complex Numbers

Let $\alpha, \beta \in \C$ be complex numbers.
Then:
:$\cmod {\alpha + \beta}^2 + \cmod {\alpha - \beta}^2 = 2 \cmod \alpha^2 + 2 \cmod \beta^2$

Proof:
Let:
:$\alpha = x_1 + i y_1$
:$\beta = x_2 + i y_2$
Then:
{{begin-eqn}}
{{eqn | o = 
      | r = \cmod {\alpha + \beta}^2 + \cmod {\alpha - \beta}^2
      | c = 
}}
{{eqn | r = \cmod {\paren {x_1 + i y_1} + \paren {x_2 + i y_2} }^2 + \cmod {\paren {x_1 + i y_1} - \paren {x_2 + i y_2} }^2
      | c = Definition of $\alpha$ and $\beta$
}}
{{eqn | r = \cmod {\paren {x_1 + x_2} + i \paren {y_1 + y_2} }^2 + \cmod {\paren {x_1 - x_2} + i \paren {y_1 - y_2} }^2
      | c = {{Defof|Complex Addition}}, {{Defof|Complex Subtraction}}
}}
{{eqn | r = \paren {x_1 + x_2}^2 + \paren {y_1 + y_2}^2 + \paren {x_1 - x_2}^2 + \paren {y_1 - y_2}^2
      | c = {{Defof|Complex Modulus}}
}}
{{eqn | r = {x_1}^2 + 2 x_1 x_2 + {x_2}^2 + {y_1}^2 + 2 y_1 y_2 + {y_2}^2 + {x_1}^2 - 2 x_1 x_2 + {x_2}^2 + {y_1}^2 - 2 y_1 y_2 + {y_2}^2
      | c = Square of Sum, Square of Difference
}}
{{eqn | r = 2 {x_1}^2 + 2 {x_2}^2 + 2 {y_1}^2 + 2 {y_2}^2
      | c = simplifying
}}
{{eqn | r = 2 \paren { {x_1}^2 + {y_1}^2} + 2 \paren { {x_2}^2 + {y_2}^2}
      | c = simplifying
}}
{{eqn | r = 2 \cmod {x_1 + i y_1}^2 + 2 \cmod {x_2 + i y_2}^2
      | c = {{Defof|Complex Modulus}}
}}
{{eqn | r = 2 \cmod \alpha^2 + 2 \cmod \beta^2
      | c = Definition of $\alpha$ and $\beta$
}}
{{end-eqn}}
{{qed}}
Theorem: Equation of Circle in Complex Plane/Formulation 1

Let $\C$ be the complex plane.
Let $C$ be a circle in $\C$ whose radius is $r \in \R_{>0}$ and whose center is $\alpha \in \C$.
Then $C$ may be written as:
:$\cmod {z - \alpha} = r$
where $\cmod {\, \cdot \,}$ denotes complex modulus.

Proof:
Let $z = x + i y$.
Let $\alpha = a + i b$.
Thus:
{{begin-eqn}}
{{eqn | l = \cmod {z - \alpha}
      | r = r
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \cmod {x + i y - a + i b}
      | r = r
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \cmod {\paren {x - a} + i \paren {y - b} }
      | r = r
      | c = {{Defof|Complex Subtraction}}
}}
{{eqn | ll= \leadsto
      | l = \sqrt {\paren {x - a}^2 + \paren {y - b}^2}
      | r = r
      | c = {{Defof|Complex Modulus}}
}}
{{eqn | ll= \leadsto
      | l = \paren {x - a}^2 + \paren {y - b}^2
      | r = r^2
      | c = squaring both sides
}}
{{end-eqn}}
The result follows from Equation of Circle.
{{qed}}
Theorem: Equation of Circle in Complex Plane/Formulation 1/Interior

The points in $\C$ which correspond to the interior of $C$ can be defined by:
:$\cmod {z - \alpha} < r$

Proof:
From Equation of Circle in Complex Plane, the circle $C$ itself is given by:
:$\cmod {z - \alpha} = r$
{{ProofWanted|This needs to be put into the rigorous context of Jordan curves, so as to define what is actually meant by "interior".  At the moment, the understanding is intuitive.}}
Theorem: Equation of Circle in Complex Plane/Formulation 1/Exterior

The points in $\C$ which correspond to the exterior of $C$ can be defined by:
:$\left\lvert{z - \alpha}\right\rvert > r$

Proof:
From Equation of Circle in Complex Plane, the circle $C$ itself is given by:
:$\left\lvert{z - \alpha}\right\rvert = r$
{{ProofWanted|This needs to be put into the rigorous context of Jordan curves, so as to define what is actually meant by "exterior".  At the moment, the understanding is intuitive.}}
Theorem: Equation of Imaginary Axis in Complex Plane

Let $\C$ be the complex plane.
Let $z \in \C$ be subject to the condition:
:$\cmod {z - 1} = \cmod {z + 1}$
where $\cmod {\, \cdot \,}$ denotes complex modulus.
Then the locus of $z$ is the imaginary axis.

Proof:
{{begin-eqn}}
{{eqn | l = \cmod {z - 1}
      | r = \cmod {z + 1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \cmod {z - 1}^2
      | r = \cmod {z + 1}^2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {z - 1} \paren {\overline {z - 1} }
      | r = \paren {z + 1} \paren {\overline {z + 1} }
      | c = Modulus in Terms of Conjugate
}}
{{eqn | ll= \leadsto
      | l = z \overline z - z - \overline z + 1
      | r = z \overline z + z + \overline z + 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 2 \paren {z + \overline z}
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 4 \map \Re z
      | r = 0
      | c = Sum of Complex Number with Conjugate
}}
{{eqn | ll= \leadsto
      | l = \map \Re z
      | r = 0
      | c = 
}}
{{end-eqn}}
The result follows by definition of imaginary axis.
{{qed}}
Theorem: Equation of Line in Complex Plane/Formulation 2

Let $\C$ be the complex plane.
Let $L$ be the infinite straight line in $\C$ which is the locus of the equation:
:$l x + m y = 1$
Then $L$ may be written as:
:$\map \Re {a z} = 1$
where $a$ is the point in $\C$ defined as:
:$a = l - i m$

Proof:
Let $z = x + i y$.
Let $a = l - i m$.
Then:
{{begin-eqn}}
{{eqn | l = \map \Re {a z}
      | r = 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\paren {a z + \overline {a z} } } 2
      | r = 1
      | c = Sum of Complex Number with Conjugate
}}
{{eqn | ll= \leadsto
      | l = a z + \overline a \cdot \overline z
      | r = 2
      | c = Complex Modulus of Product of Complex Numbers
}}
{{eqn | ll= \leadsto
      | l = \paren {l - i m} \paren {x + i y} + \paren {l + i m} \paren {x - i y}
      | r = 2
      | c = {{Defof|Complex Conjugate}}
}}
{{eqn | ll= \leadsto
      | l = \paren {\paren {l x + m y} + i \paren {l y - m x} } + \paren {\paren {l x + m y} - i \paren {l y - m x} }
      | r = 2
      | c = {{Defof|Complex Multiplication}}
}}
{{eqn | ll= \leadsto
      | l = l x + m y
      | r = 1
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Conversion between Cartesian and Polar Coordinates in Plane

Let $S$ be the plane.
Let a Cartesian plane $\CC$ be applied to $S$.
Let a polar coordinate plane $\PP$ be superimposed upon $\CC$ such that:
:$(1): \quad$ The origin of $\CC$ coincides with the pole of $\PP$.
:$(2): \quad$ The $x$-axis of $\CC$ coincides with the polar axis of $\PP$.
Let $p$ be a point in $S$.
Let $p$ be specified as $p = \polar {r, \theta}$ expressed in the polar coordinates of $\PP$.
Then $p$ is expressed as $\tuple {r \cos \theta, r \sin \theta}$ in $\CC$.
Contrariwise, let $p$ be expressed as $\tuple {x, y}$ in the cartesian coordinates of $\CC$.
Then $p$ is expressed in $\PP$ as:
:$p = \polar {\sqrt {x^2 + y^2}, \arctan \dfrac y x + \pi \sqbrk {x < 0 \text{ or } y < 0} + \pi \sqbrk {x > 0 \text{ and } y < 0} }$
where:
:$\sqbrk {\, \cdot \,}$ is Iverson's convention.
:$\arctan$ denotes the arctangent function.

Proof:
Let $P$ be a point in the plane expressed:
:in Cartesian coordinates as $\tuple {x, y}$
:in polar coordinates as $\polar {r, \theta}$.
:330px
As specified, we identify:
:the origins of both coordinate systems with a distinguished point $O$
:the $x$-axis of $C$ with the polar axis of $P$.
Let a perpendicular $PM$ be dropped from $P$ to the $x$-axis.
The triangle $OMP$ is a right triangle:
:whose hypotenuse is $OP$, whose length is $r$
:whose legs are $OM$ and $MP$
:whose angle $POM$ is $\theta$.
By definition of sine and cosine
:$x = r \cos \theta$
:$y = r \sin \theta$
The result follows.
{{qed}}
Theorem: Polar Form of Reciprocal of Complex Number

Let $z := r \paren {\cos \theta + i \sin \theta} \in \C$ be a complex number expressed in polar form.
Then:
:$\dfrac 1 z = \dfrac {\cos \theta - i \sin \theta} r$

Proof:
{{begin-eqn}}
{{eqn | l = \dfrac 1 z
      | r = \dfrac {\overline z} {z \overline z}
      | c = Inverse for Complex Multiplication
}}
{{eqn | r = \dfrac {r \paren {\cos \theta - i \sin \theta} } {r \paren {\cos \theta + i \sin \theta} r \paren {\cos \theta - i \sin \theta} }
      | c = Polar Form of Complex Conjugate
}}
{{eqn | r = \dfrac {\paren {\cos \theta - i \sin \theta} } {r \paren {\cos^2 \theta - i^2 \sin^2 \theta} }
      | c = simplifying
}}
{{eqn | r = \dfrac {\paren {\cos \theta - i \sin \theta} } {r \paren {\cos^2 \theta + \sin^2 \theta} }
      | c = {{Defof|Imaginary Unit}}
}}
{{eqn | r = \dfrac {\cos \theta - i \sin \theta} r
      | c = Sum of Squares of Sine and Cosine
}}
{{end-eqn}}
{{qed}}
Theorem: Argument of Complex Conjugate equals Argument of Reciprocal

Let $z \in \C$ be a complex number.
Then:
:$\arg {\overline z} = \arg \dfrac 1 z$
where:
:$\arg$ denotes the argument of a complex number
:$\overline z$ denotes the complex conjugate of $z$.

Proof:
Let $z$ be expressed in polar form:
:$z := r \paren {\cos \theta + i \sin \theta}$
Then:
{{begin-eqn}}
{{eqn | l = \dfrac 1 z
      | r = \dfrac 1 r \paren {\cos \theta - i \sin \theta}
      | c = Polar Form of Reciprocal of Complex Number
}}
{{eqn | r = \dfrac 1 r \paren {\map \cos {-\theta} + i \map \sin {-\theta} }
      | c = Cosine Function is Even, Sine Function is Odd
}}
{{end-eqn}}
The result follows by definition of the argument of a complex number
{{qed}}
Theorem: Multiplication by Imaginary Unit is Equivalent to Rotation through Right Angle

Let $z \in \C$ be a complex number.
Let $z$ be interpreted as a vector in the complex plane.
Let $w \in \C$ be the complex number defined as $z$ multiplied by the imaginary unit $i$:
:$w = i z$
Then $w$ can be interpreted as the vector $z$ after being rotated through a right angle in an anticlockwise direction.

Proof:
:600px
Let $z$ be expressed in polar form as:
:$z = r \left({\cos \theta + i \sin \theta}\right)$
From Polar Form of Complex Number: $i$:
:$i = \cos \dfrac \pi 2 + i \sin \dfrac \pi 2$
and so:
: the modulus of $i$ is $1$
: the argument of $i$ is $\dfrac \pi 2$.
By Product of Complex Numbers in Polar Form:
: the modulus of $i z$ is $r$
: the argument of $i$ is $\theta + \dfrac \pi 2$.
That is, the result of multiplying $z$ by $i$ is the same as rotating $z$ through $\dfrac \pi 2$, which is a right angle.
{{qed}}
Theorem: Multiplication of Complex Number by -1 is Equivalent to Rotation through Two Right Angles

Let $z \in \C$ be a complex number.
Let $z$ be interpreted as a vector in the complex plane.
Let $w \in \C$ be the complex number defined as $z$ multiplied by $-1$:
:$w = \left({-1}\right) z$
Then $w$ can be interpreted as the vector $z$ after being rotated through two right angles.
The direction of rotation is usually interpreted as being anticlockwise, but a rotated through two right angles is the same whichever direction the rotation is performed.

Proof:
:600px
By definition of the imaginary unit:
:$-1 = i^2$
and so:
:$-1 \times z = i \paren {i z}$
From Multiplication by Imaginary Unit is Equivalent to Rotation through Right Angle, multiplication by $i$ is equivalent to rotation through a right angle, in an anticlockwise direction.
So multiplying by $i^2$ is equivalent to rotation through two right angles in an anticlockwise direction.
{{qed}}
Theorem: Diagonals of Rhombus Intersect at Right Angles

Let $ABCD$ be a rhombus.
The diagonals $AC$ and $BD$ of $ABCD$ intersect each other at right angles.

Proof:
:400px
{{WLOG}}, let $ABCD$ be embedded in the complex plane so that vertex $A$ coincides with the origin $0 + 0 i$.
Let $AB$ and $AD$ be represented by the complex numbers $a$ and $b$ respectively, expressed as vectors $\mathbf a$ and $\mathbf b$ respectively.
By Geometrical Interpretation of Complex Addition, the diagonal $AC$ is represented by the complex number $a + b$, expressed as a vector $\mathbf a + \mathbf b$.
By Geometrical Interpretation of Complex Subtraction, the diagonal $BD$ is represented by the complex number $a - b$, expressed as a vector $\mathbf a - \mathbf b$.
Let $a - b = w \paren {a + b}$ for some complex number $w \in \C$.
For $A \perp BD$, it is necessary and sufficient  from Complex Multiplication as Geometrical Transformation for the argument of $w$ to be $\dfrac \pi 2$.
That is, for $w$ to be wholly imaginary.
From Complex Number equals Negative of Conjugate iff Wholly Imaginary, that is for $w + \overline w = 0$.
It remains to demonstrate this.
So:
{{begin-eqn}}
{{eqn | l = w + \overline w
      | r = \dfrac {a - b} {a + b} + \dfrac {\overline a - \overline b} {\overline a + \overline b}
      | c = 
}}
{{eqn | r = \dfrac {2 a \overline a - 2 b \overline b} {\left({a + b}\right) \left({\overline a + \overline b}\right)}
      | c = 
}}
{{eqn | r = \dfrac {2 \cmod a^2 - 2 \cmod b^2} {\left({a + b}\right) \left({\overline a + \overline b}\right)}
      | c = Modulus in Terms of Conjugate
}}
{{eqn | r = 0
      | c = as $\cmod a = \cmod b$
}}
{{end-eqn}}
The result follows.
{{qed}}
Theorem: Geometrical Interpretation of Complex Addition

Let $a, b \in \C$ be complex numbers expressed as vectors $\mathbf a$ and $\mathbf b$ respectively.
Let $OA$ and $OB$ be two adjacent sides of the parallelogram $OACB$ such that $OA$ corresponds to $\mathbf a$ and $OB$ corresponds to $\mathbf b$.
Then the diagonal $OC$ of $OACB$ corresponds to $\mathbf a + \mathbf b$, the sum of $a$ and $b$ expressed as a vector.

Proof:
:400px
Let $a = a_x + i a_y$ and $b = b_x + i b_y$.
Then by definition of complex addition:
:$a + b = \paren {a_x + b_x} + i \paren {a_y + b_y}$
Thus $\mathbf a + \mathbf b$ is the vector whose components are $a_x + b_x$ and $a_y + b_y$.
Similarly, we have:
:$b + a = \paren {b_x + a_x} + i \paren {b_y + a_y}$
Thus $\mathbf b + \mathbf a$ is the vector whose components are $b_x + a_x$ and $b_y + a_y$.
It follows that both $\mathbf a + \mathbf b$ and $\mathbf b + \mathbf a$ both correspond to the diagonal $OC$ of $OACB$.
{{qed}}
Theorem: Geometrical Interpretation of Complex Subtraction

Let $a, b \in \C$ be complex numbers expressed as vectors $\mathbf a$ and $\mathbf b$ respectively.
Let $OA$ and $OB$ be two adjacent sides of the parallelogram $OACB$ such that $OA$ corresponds to $\mathbf a$ and $OB$ corresponds to $\mathbf b$.
Then the diagonal $BA$ of $OACB$ corresponds to $\mathbf a - \mathbf b$, the difference of $a$ and $b$ expressed as a vector.

Proof:
:400px
By definition of vector addition:
:$OB + BA = OA$
That is:
:$\mathbf b + \vec {BA} = \mathbf a$
which leads directly to:
:$\vec {BA} = \mathbf a - \mathbf b$
{{qed}}
Theorem: Condition for Collinearity of Points in Complex Plane/Formulation 1

Let $z_1$, $z_2$ and $z_3$ be points in the complex plane.
Then $z_1$, $z_2$ and $z_3$ are collinear {{iff}}:
:$\dfrac {z_1 - z_3} {z_3 - z_2} = \lambda$
where $\lambda \in \R$ is a real number.
If this is the case, then $z_3$ divides the line segment in the ratio $\lambda$.
If $\lambda > 0$ then $z_3$ is between $z_1$ and $z_2$, and if $\lambda < 0$ then $z_3$ is outside the line segment joining $z_1$ to $z_2$.

Proof:
By Geometrical Interpretation of Complex Subtraction:
:$z_1 - z_3$ can be represented as the line segment from $z_3$ to $z_1$
:$z_3 - z_2$ can be represented as the line segment from $z_2$ to $z_3$.
Thus we have that $z_1$, $z_2$ and $z_3$ are collinear {{iff}} $z_1 - z_3$ is parallel to $z_3 - z_2$, when expressed as line segments.
Let $\dfrac {z_1 - z_3} {z_3 - z_2} = \lambda$ for $\lambda \in \C$.
That is:
:$z_1 - z_3 = \lambda \paren {z_3 - z_2}$
By Complex Multiplication as Geometrical Transformation:
:$\map \arg {z_1 - z_3} = \map \arg {z_3 - z_2} \iff \map \arg {z_3 - z_2} \arg \lambda \in \R_{>0}$
and:
:$\map \arg {z_1 - z_3} = -\map \arg {z_3 - z_2} \iff \map \arg {z_3 - z_2} \arg \lambda \in \R_{<0}$
where $\arg$ denotes the argument of a complex number.
Also by Complex Multiplication as Geometrical Transformation, $z_1 - z_3$ is $\lambda$ the length of $z_3 - z_2$.
The result follows.
{{Qed}}
Theorem: Equation of Circular Arc in Complex Plane

Let $a, b \in \C$ be complex constants representing the points $A$ and $B$ respectively in the complex plane.
Let $z \in \C$ be a complex variable representing the point $Z$ in the complex plane.
Let $\lambda \in \R$ be a real constant such that $-\pi < \lambda < \pi$.
Then the equation:
:$\arg \dfrac {z - b} {z - a} = \lambda$
represents the arc of a circle with $AB$ as a chord subtending an angle $\lambda$ at $Z$ on the circumference.

Proof:
:420px
By Geometrical Interpretation of Complex Subtraction:
:$z - a$ represents the line from $A$ to $Z$
:$z - b$ represents the line from $B$ to $Z$
{{begin-eqn}}
{{eqn | l = \arg \dfrac {z - b} {z - a}
      | r = \lambda
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \arg {z - b} - \map \arg {z - a}
      | r = \lambda
      | c = Argument of Quotient equals Difference of Arguments
}}
{{end-eqn}}
Thus:
:$\arg \dfrac {z - b} {z - a} = \lambda$
represents the statement that the angle between $AZ$ and $BZ$ is constant:
:$\angle AZB = \lambda$
That is, the angle subtended by $AB$ at $Z$ is $\lambda$.
The result follows from the Inscribed Angle Theorem.
{{qed}}
Theorem: Equivalence of Definitions of Real Exponential Function/Inverse of Natural Logarithm implies Limit of Sequence

The following definition of the concept of the real exponential function:

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 {{RHS}} 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:
{{begin-eqn}}
{{eqn | l = \map \ln {\paren {1 + \frac x n}^n}
      | r = n \, \map \ln {1 + x n^{-1} }
      | c = Logarithms of Powers
}}
{{eqn | r = x \frac {\map \ln {1 + x n^{-1} } } {x n^{-1} }
      | c = multiplying by $1 = \dfrac {x n^{-1} } {x n^{-1} }$
}}
{{end-eqn}}
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$.
{{qed}}
Theorem: Equivalence of Definitions of Real Exponential Function/Limit of Sequence implies Extension of Rational Exponential

The following definition of the concept of the real exponential function:

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$:
{{begin-eqn}}
{{eqn | l = \exp \restriction_\Q \paren 0
      | r = \lim_{n \mathop \to +\infty} \paren {1 + \frac 0 n}^n
}}
{{eqn | r = 1
}}
{{eqn | r = e^0
}}
{{end-eqn}}
For $x \ne 0$:
{{begin-eqn}}
{{eqn | l = \map {\exp \restriction_\Q} x
      | r = \lim_{n \mathop \to +\infty} \paren {1 + \frac x n}^n
      | c = 
}}
{{eqn | r = \lim_{\paren {n / x} \mathop \to +\infty} \paren {\paren {1 + \frac 1 {\paren {n / x} } }^{\paren {n / x} } }^x
      | c = Exponent Combination Laws
}}
{{eqn | r = e^x
}}
{{end-eqn}}
where the continuity in the last step follows {{afortiori}} 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.
{{qed}}
Theorem: Equivalence of Definitions of Real Exponential Function/Extension of Rational Exponential implies Differential Equation

The following definition of the concept of the real exponential function:

Proof:
Let $\exp x$ be the real function defined as the extension of rational exponential.
Then we have:
{{begin-eqn}}
{{eqn | l = \map {D_x} {\exp x}
      | r = \lim_{h \mathop \to 0} \frac {\map \exp {x + h} - \exp x} h
      | c = {{Defof|Derivative}}
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {\exp x \cdot \exp h - \exp x} h
      | c = Exponential of Sum
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {\exp x \paren {\exp h - 1} } h
}}
{{eqn | r = \exp x \paren {\lim_{h \mathop \to 0} \frac {\exp h - 1} h}
      | c = Multiple Rule for Limits of Real Functions, as $\exp x$ is constant
}}
{{eqn | r = \exp x
      | c = Derivative of Exponential at Zero: Proof 2
}}
{{end-eqn}}
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$.
{{qed|lemma}}
{{begin-eqn}}
{{eqn | l = \exp 0
      | r = \lim_{n \mathop \to +\infty} \paren {1 + \frac 0 n}^n
}}
{{eqn | r = 1
}}
{{end-eqn}}
{{qed}}
Theorem: Euler's Number as Limit of 1 + Reciprocal of n to nth Power

:$\ds \lim_{n \mathop \to \infty} \paren {1 + \frac 1 n}^n = e$
where $e$ denotes Euler's number.

Proof:
By definition of the real exponential function as the limit of a sequence:
:$(1): \quad \exp x := \ds \lim_{n \mathop \to \infty} \paren {1 + \frac x n}^n$
By definition of Euler's number:
:$e = e^1 = \exp 1$
The result follows by setting $x = 1$ in $(1)$.
{{qed}}
Theorem: Exponential of Sum/Complex Numbers/General Result

Let $m \in \N_{>0}$ be a natural number.
Let $z_1, z_2, \ldots, z_m \in \C$ be complex numbers.
Let $\exp z$ be the exponential of $z$.
Then:
:$\ds \map \exp {\sum_{j \mathop = 1}^m z_j} = \prod_{j \mathop = 1}^m \paren {\exp z_j}$

Proof:
The proof proceeds by induction.
For all $m \in \N_{>0}$, let $\map P m$ be the proposition:
:$\ds \map \exp {\sum_{j \mathop = 1}^m z_j} = \prod_{j \mathop = 1}^m \paren {\exp z_j}$
$\map P 1$ is the case:
{{begin-eqn}}
{{eqn | l = \map \exp {\sum_{j \mathop = 1}^1 z_j}
      | r = \exp z_j
      | c = 
}}
{{eqn | r = \prod_{j \mathop = 1}^1 \paren {\exp z_j}
      | c = 
}}
{{end-eqn}}
Thus $\map P 1$ is seen to hold.
Theorem: Exponential of Sum/Complex Numbers/General Result/Corollary

Let $m \in \Z_{>0}$ be a positive integer.
Let $z \in \C$ be a complex number.
Let $\exp z$ be the exponential of $z$.
Then:
: $\ds \exp \paren {m z} = \paren {\exp z}^m$

Proof:
From Exponential of Sum: Complex Numbers: General Result:
:$\ds \exp \paren {\sum_{j \mathop = 1}^m z_j} = \prod_{j \mathop = 1}^m \paren {\exp z_j}$
for complex numberst $z_1, z_2, \ldots, z_m \in \C$.
The result follows by setting $z = z_1 = z_2 = \cdots = z_m$.
{{qed}}
Theorem: Exponential of Complex Number plus 2 pi i

:$\map \exp {z + 2 \pi i} = \map \exp z$

Proof:
{{begin-eqn}}
{{eqn | l = \map \exp {z + 2 \pi i}
      | r = \map \exp z \, \map \exp {2 \pi i}
      | c = Exponential of Sum: Complex Numbers
}}
{{eqn | r = \map \exp z \times 1
      | c = Euler's Formula Example: $e^{2 i \pi}$
}}
{{eqn | r = \map \exp z
}}
{{end-eqn}}
{{qed}}