avewright/proofwiki-math huggingface dataset:
Theorem: Measurable Image

Let $\mathfrak M$ be the set of measurable sets of $\R$.
For any extended real-valued function $f: \R \to \R \cup \set {-\infty, +\infty}$ whose domain is measurable, the following statements are equivalent:
:$(1): \quad \forall \alpha \in \R: \set {x: \map f x > \alpha} \in \mathfrak M$
:$(2): \quad \forall \alpha \in \R: \set {x: \map f x \ge \alpha} \in \mathfrak M$
:$(3): \quad \forall \alpha \in \R: \set {x: \map f x < \alpha} \in \mathfrak M$
:$(4): \quad \forall \alpha \in \R: \set {x: \map f x \le \alpha} \in \mathfrak M$
These statements imply:
:$(5): \quad \forall \alpha \in \R \cup \set {-\infty, +\infty}: \set {x: \map f x = \alpha} \in \mathfrak M$
{{proofread}}

Proof:
Let the domain of $f$ be $D$.
We have that Measurable Sets form Algebra of Sets.
First we note that, from Properties of Algebras of Sets, the difference of two measurable sets is measurable.
So:
:$\set {x: \map f x \le \alpha} = D - \set {x: \map f x > \alpha}$
and so $(1) \iff (4)$.
Similarly, $(2) \iff (3)$.
Next we note that, also from Properties of Algebras of Sets, the intersection of a sequence of measurable sets is measurable.
Now:
:$\ds \set {x: \map f x \ge \alpha} = \bigcap_{n \mathop = 1}^\infty \set {x: \map f x > \alpha -\dfrac 1 n}$
because if:
:$x \in \set {x: \map f x \ge \alpha}$
that is:
:$\map f x \ge \alpha$
and since:
:$\forall n \in \N: n > 0: \alpha > \alpha - \dfrac 1 n$
then:
:$\forall n \in \N: n > 0: \map f x > \alpha - \dfrac 1 n$
That is:
:$\forall n \in \N: n > 0: x \in \set {x: \map f x > \alpha - \dfrac 1 n}$
Hence:
:$\ds x \in \bigcap_{n \mathop = 1}^\infty \set {x: \map f x > \alpha - \dfrac 1 n}$
Conversely, suppose:
:$\ds x \in \bigcap_{n \mathop = 1}^\infty \set {x: \map f x > \alpha - \dfrac 1 n}$
that is:
:$\forall n \in \N: n > 0: x \in \set {x: \map f x > \alpha - \dfrac 1 n}$
Claim $\map f x \ge \alpha $.
Otherwise $\map f x < \alpha$, say for example $\map f x = \alpha - \size \epsilon$.
Choose $N = \ceiling {\dfrac 1 {\size \epsilon} } + 1 \in \N$.
Therefore:
:$N > \ceiling {\dfrac 1 {\size \epsilon} } \ge \dfrac 1 {\size \epsilon}$
and so:
:$\alpha - \dfrac 1 N > \alpha - \size \epsilon$
By hypothesis:
:$\forall N \in \N: \map f x > \alpha - \dfrac 1 N$
and therefore by the just previous:
:$\map f x > \alpha - \size \epsilon$
But we had $\map f x = \alpha - \size \epsilon$, a contradiction.
Therefore:
:$\map f x \ge \alpha $
that is:
$x \in \set {x: \map f x \ge \alpha}$
which was to be shown.
So $(1) \implies (2)$.
Similarly:
:$\ds \set {x: \map f x > \alpha} = \bigcup_{n \mathop = 1}^\infty \set {x: \map f x \ge \alpha + \dfrac 1 n}$
and so $(2) \implies (1)$.
This shows that $(1) \iff (2) \iff (3) \iff (4)$.
For the fifth statement, we have:
:$\set {x: \map f x = \alpha} = \set {x: \map f x \ge \alpha} \cap \set {x: \map f x \le \alpha}$
and so $(3) \land (4) \implies (5)$ for $\alpha \in \R$.
Since:
:$\ds \set {x: \map f x = +\infty} = \bigcap_{n \mathop = 1}^\infty \set {x: \map f x \ge n}$
we have that $(2) \implies (5)$ for $\alpha = +\infty$.
Similarly $(4) \implies (5)$ for $\alpha = - \infty$.
{{qed}}
Category:Measure Theory
cavv7wehfndo17ix3dfxyy1qih2irru
Theorem: Lebesgue Integral is Extension of Darboux Integral

Let $f: \closedint a b \to \R$ be a Darboux integrable function.
Then it is also Lebesgue integrable, and furthermore:
:$\ds R \int_a^b \map f x \rd x = \int_{\closedint a b} f \rd \lambda$
where $\ds R \int_a^b$ is the Darboux integral and $\ds \int_{\closedint a b}$ is the Lebesgue integral.

Proof:
Since every step function is also a simple function, we have
:$\ds \map L P \le \sup_{\phi \mathop \le f} \int_a^b \map \phi x \rd x \le \inf_{\psi \mathop \ge f} \int_a^b \map \psi x \rd x \le \map U P$
where $\map L P$ and $\map U P$ are the lower Darboux sum and upper Darboux sum as defined in the definition of definite integral.
Since $f$ is Darboux integrable, the inequalities are all equalities and $f$ is measurable by basic properties of measurable functions.
{{questionable|all reasoning is behind red links, and it's incomplete}}
{{ProofWanted}}
{{qed}}
Theorem: Euclidean Metric on Real Vector Space is Metric

The Euclidean metric on a real vector space $\R^n$ is a metric.

Proof:
The Euclidean metric on $\R^n$ is a special case of the $p$-product metric.
The result follows from $p$-Product Metric on Real Vector Space is Metric.
{{qed}}
Theorem: Euclidean Metric on Real Vector Space is Metric

The Euclidean metric on a real vector space $\R^n$ is a metric.

Proof:
Consider the Euclidean space $M = \struct {\R^n, d_2}$ where $d_2$ is the distance function given by:
:$\ds \map {d_2} {x, y} = \paren {\sum_{i \mathop = 1}^n \paren {x_i - y_i}^2}^{\frac 1 2}$
where $x = \tuple {x_1, x_2, \ldots, x_n}$ and $y = \tuple {y_1, y_2, \ldots, y_n}$.
=== Proof of {{Metric-space-axiom|1|nolink}} ===
{{begin-eqn}}
{{eqn | l = \map {d_2} {x, x}
      | r = \paren {\sum_{i \mathop = 1}^n \paren {x_i - x_i}^2}^{\frac 1 2}
      | c = Definition of $d_2$
}}
{{eqn | r = \paren {\sum_{i \mathop = 1}^n 0^2}^{\frac 1 2}
      | c = 
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
So {{Metric-space-axiom|1}} holds for $d_2$.
{{qed|lemma}}
=== {{Metric-space-axiom|2|nolink}} ===
It is required to be shown:
:$\map {d_2} {x, y} + \map {d_2} {y, z} \ge \map {d_2} {x, z}$
for all $x, y, z \in \R^n$.
Let:
:$(1): \quad z = \tuple {z_1, z_2, \ldots, z_n}$
:$(2): \quad$ all summations be over $i = 1, 2, \ldots, n$
:$(3): \quad x_i - y_i = r_i$
:$(4): \quad y_i - z_i = s_i$.
Thus we need to show that:
:$\ds \paren {\sum \paren {x_i - y_i}^2}^{\frac 1 2} + \paren {\sum \paren {y_i - z_i}^2}^{\frac 1 2} \ge \paren {\sum \paren {x_i - z_i}^2}^{\frac 1 2}$
We have:
{{begin-eqn}}
{{eqn | l = \map {d_2} {x, y} + \map {d_2} {y, z}
      | r = \paren {\sum \paren {x_i - y_i}^2}^{\frac 1 2} + \paren {\sum \paren {y_i - z_i}^2}^{\frac 1 2}
      | c = Definition of $d_2$
}}
{{eqn | r = \paren {\sum r_i^2}^{\frac 1 2} + \paren {\sum s_i^2}^{\frac 1 2}
      | c = 
}}
{{eqn | o = \ge
      | r = \paren {\sum \paren {r_i + s_i}^2}^{\frac 1 2}
      | c = Minkowski's Inequality for Sums: index $2$
}}
{{eqn | r = \paren {\sum \paren {x_i - y_i + y_i - z_i}^2}^{\frac 1 2}
      | c = Definition of $r_i$ and $s_i$
}}
{{eqn | r = \paren {\sum \paren {x_i - z_i}^2}^{\frac 1 2}
      | c = 
}}
{{eqn | r = \map {d_2} {x, z}
      | c = Definition of $d_2$
}}
{{end-eqn}}
So {{Metric-space-axiom|2}} holds for $d_2$.
{{qed|lemma}}
=== {{Metric-space-axiom|3|nolink}} ===
{{begin-eqn}}
{{eqn | l = \map {d_2} {x, y}
      | r = \paren {\sum \paren {x_i - y_i}^2}^{\frac 1 2}
      | c = Definition of $d_2$
}}
{{eqn | r = \paren {\sum \paren {y_i - x_i}^2}^{\frac 1 2}
      | c = 
}}
{{eqn | r = \map {d_2} {y, x}
      | c = Definition of $d_2$
}}
{{end-eqn}}
So {{Metric-space-axiom|3}} holds for $d_2$.
{{qed|lemma}}
=== {{Metric-space-axiom|4|nolink}} ===
{{begin-eqn}}
{{eqn | l = x
      | o = \ne
      | r = y
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists k \in \closedint 1 n
      | l = x_k
      | o = \ne
      | r = y_k
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x_k - y_k
      | o = \ne
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {\sum \paren {x_k - y_k}^2}^{\frac 1 2}
      | o = >
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {d_2} {x, y}
      | o = >
      | r = 0
      | c = Definition of $d_2$
}}
{{end-eqn}}
So {{Metric-space-axiom|4}} holds for $d_2$.
{{qed}}
Theorem: Metric Induces Topology

Let $M = \struct {A, d}$ be a metric space.
Then the topology $\tau$ induced by the metric $d$ is a topology on $M$.

Proof:
We examine each of the criteria for being a topology separately.
:$(1): \quad$ By Union of Open Sets of Metric Space is Open, the union of any collection of open sets of a metric space is open.
:$(2): \quad$ By Finite Intersection of Open Sets of Metric Space is Open, a finite intersection of open sets of a metric space is open.
:$(3): \quad$ By Open Sets in Metric Space, $\O \in \tau$ and $A \in \tau$.
Hence the result.
{{qed}}
Theorem: Countable Set has Measure Zero

Let $S$ be a countable set.
{{explain|Is it assumed that $S \subseteq \R$?}}
Then the measure of $S$ is $\map m S = 0$.

Proof:
Let $\ds \set {x_i}_{i \mathop = 1}^\infty$ be an enumeration of the elements of $S$.
For any (strictly) positive real number $\epsilon$, define $A_i$ as an open cover for $S$:
:$A_i = \paren {x_i - 2^{-i} \epsilon, x_i + 2^{-i} \epsilon}$
{{explain|What is the meaning of the above? Is it an open interval? If so, use the appropriate notation, then prove that the union of the open intervals is indeed a cover for $S$}}
Then:
:$\ds S \subseteq \bigcup_{i \mathop = 1}^\infty A_i$
and:
:$\ds \map m {\bigcup A_i} \le \sum_{i \mathop = 1}^\infty 2^{1 - i} \epsilon = 2 \epsilon$ From the infinite geometric series
Since our choice of $\epsilon$ was arbitrary, for any positive real $z$ we can construct a set $T$ such that $S \subseteq T$ and $\map m T \le z$.
Hence $X$ has zero measure.
{{qed}}
Category:Analysis
9nk32meu01kgv6gc4uyqzieuzi8gn7p
Theorem: Mean Value of Convex Real Function

Let $f$ be a real function which is continuous on the closed interval $\closedint a b$ and differentiable on the open interval $\openint a b$.
Let $f$ be convex on $\openint a b$.
Then:
:$\forall \xi \in \openint a b: \map f x - \map f \xi \ge \map {f'} \xi \paren {x - \xi}$

Proof:
By the Mean Value Theorem:
:$\exists \eta \in \openint x \xi: \map {f'} \eta = \dfrac {\map f x - \map f \xi} {x - \xi}$
From Real Function is Convex iff Derivative is Increasing, the derivative of $f$ is increasing.
Thus:
:$x > \xi \implies \map {f'} \eta \ge \map {f'} \xi$
:$x < \xi \implies \map {f'} \eta \le \map {f'} \xi$
Hence:
:$\map f x - \map f \xi \ge \map {f'} \xi \paren {x - \xi}$
{{qed}}
Theorem: Upper Bound of Natural Logarithm

Let $\ln x$ be the natural logarithm of $x$ where $x \in \R_{>0}$.
Then:
:$\ln x \le x - 1$

Proof:
From Logarithm is Strictly Concave:
:$\ln$ is (strictly) concave.
From Mean Value of Concave Real Function:
:$\ln x - \ln 1 \le \paren {\dfrac \d {\d x} \ln 1} \paren {x - 1}$
From Derivative of Natural Logarithm:
:$\dfrac \d {\d x} \ln 1 = \dfrac 1 1 = 1$
So:
:$\ln x - \ln 1 \le \paren {x - 1}$
But from Logarithm of 1 is 0:
:$\ln 1 = 0$
Hence the result.
{{qed}}
Theorem: Exponential of Sum/Real Numbers

Let $x, y \in \R$ be real numbers.
Let $\exp x$ be the exponential of $x$.
Then:
:$\map \exp {x + y} = \paren {\exp x} \paren {\exp y}$

Proof:
This proof assumes the definition of $\exp$ as:
:$\exp x = y \iff \ln y = x$
where:
:$\ln y = \ds \int_1^y \dfrac 1 t \rd t$
Let $X = \exp x$ and $Y = \exp y$.
From Sum of Logarithms, we have:
:$\ln X Y = \ln X + \ln Y = x + y$
From the Exponential of Natural Logarithm:
:$\map \exp {\ln x} = x$
Thus:
:$\map \exp {x + y} = \map \exp {\ln X Y} = X Y = \paren {\exp x} \paren {\exp y}$
{{qed}}
Theorem: Exponential of Sum/Real Numbers

Let $x, y \in \R$ be real numbers.
Let $\exp x$ be the exponential of $x$.
Then:
:$\map \exp {x + y} = \paren {\exp x} \paren {\exp y}$

Proof:
This proof assumes the definition of $\exp$ as defined by a limit of a sequence:
:$\exp x = \ds \lim_{n \mathop \to +\infty} \paren {1 + \frac x n}^n$
From Powers of Group Elements we can presuppose the Exponent Combination Laws for natural number indices.
First we introduce a lemma:
By definition:
{{begin-eqn}}
{{eqn | l = \paren {\exp x} \paren {\exp y}
      | r = \lim_{n \mathop \to +\infty} \paren {1 + \frac x n}^n \lim_{n \mathop \to +\infty} \paren {1 + \frac y n}^n
}}
{{eqn | r = \lim_{n \mathop \to +\infty} \paren {\paren {1 + \frac x n} \paren {1 + \frac y n} }^n
      | c = Combination Theorem for Sequences
}}
{{eqn | r = \lim_{n \mathop \to +\infty} \paren {1 + \frac {x + y} n + \frac {x y} {n^2} }^n
}}
{{eqn | r = \lim_{n \mathop \to +\infty} \paren {\paren {1 + \frac {x + y} n} \paren {1 + \frac {\paren {\frac {x y} {n + x + y} } } n} }^n
      | c = Lemma: {{WLOG}} let $n > - x - y$: therefore $n + x + y > 0$
}}
{{eqn | r = \lim_{n \mathop \to +\infty} \paren {1 + \frac {x + y} n}^n \lim_{n \mathop \to +\infty} \paren {1 + \frac {\paren {\frac {x y} {n + x + y} } } n}^n
      | c = Combination Theorem for Sequences
}}
{{eqn | r = \lim_{n \mathop \to +\infty} \paren {1 + \frac {x + y} n}^n
      | c = Null Sequence in Exponential Sequence
}}
{{eqn | r = \map \exp {x + y}
}}
{{end-eqn}}
{{qed}}
Theorem: Exponential of Sum/Real Numbers

Let $x, y \in \R$ be real numbers.
Let $\exp x$ be the exponential of $x$.
Then:
:$\map \exp {x + y} = \paren {\exp x} \paren {\exp y}$

Proof:
This proof assumes the definition of $\exp$ as defined by an initial value problem.
That is, suppose $\exp$ satisfies:
:$(1): \quad D_x \exp x = \exp x$
:$(2): \quad \exp 0 = 1$
on $\R$.
Consider the real function $f: \R \to \R$ defined by:
:$\map f x := \dfrac {\map \exp {x + y} } {\map \exp y}$
From Exponential of Real Number is Strictly Positive, $f$ is well-defined.
So:
{{begin-eqn}}
{{eqn | l = D_x \, \map f x
      | r = D_x \frac {\map \exp {x + y} } {\map \exp y}
}}
{{eqn | r = \frac 1 {\map \exp y} D_x \, \map \exp {x + y}
      | c = Derivative of Constant Multiple
}}
{{eqn | r = \frac {\map \exp {x + y} } {\map \exp y}
      | c = Chain Rule for Derivatives
}}
{{eqn | r = \map f x
}}
{{end-eqn}}
Thus $f$ satisfies $(1)$.
Further:
{{begin-eqn}}
{{eqn | l = \map f 0
      | r = \frac {\map \exp {0 + y} } {\map \exp y}
}}
{{eqn | r = \frac {\map \exp y} {\map \exp y}
}}
{{eqn | r = 1
}}
{{end-eqn}}
So $f$ satisfies $(2)$.
From Exponential Function is Well-Defined:
:$f = \exp$
That is:
{{begin-eqn}}
{{eqn | l = \frac {\map \exp {x + y} } {\map \exp y}
      | r = \map \exp x
}}
{{eqn | ll= \leadsto
      | l = \map \exp {x + y}
      | r = \map \exp x \, \map \exp y
}}
{{end-eqn}}
{{qed}}
Theorem: Exponential of Sum/Real Numbers

Let $x, y \in \R$ be real numbers.
Let $\exp x$ be the exponential of $x$.
Then:
:$\map \exp {x + y} = \paren {\exp x} \paren {\exp y}$

Proof:
This proof assumes the definition of $\exp$ as a series.
Then:
{{begin-eqn}}
{{eqn | l = \map \exp {x + y}
      | r = \sum_{n \mathop = 0}^\infty \frac 1 {n!} \paren {x + y}^n
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \frac 1 {n!} \sum_{k \mathop = 0}^n \frac {n!} {k! \paren {n - k}!} x^k y^{n - k}
      | c = Binomial Theorem
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \sum_{k \mathop = 0}^n \paren {\frac 1 {k!} x^k} \paren {\frac 1 {\paren {n - k}!} y^{n - k} }
}}
{{eqn | r = \paren {\sum_{n \mathop = 0}^\infty \frac {x^n} {n!} } \paren {\sum_{n \mathop = 0}^\infty \frac {y^n} {n!} }
      | c = {{Defof|Cauchy Product}}
}}
{{eqn | r = \map \exp x \, \map \exp y
}}
{{end-eqn}}
{{qed}}
Theorem: Exponential of Sum/Real Numbers

Let $x, y \in \R$ be real numbers.
Let $\exp x$ be the exponential of $x$.
Then:
:$\map \exp {x + y} = \paren {\exp x} \paren {\exp y}$

Proof:
Fix $a \in \R$ and define the function $f_a : \R \to \R$ by: 
:$\map {f_a} x = \map \exp {a - x} \exp x$
for all $x \in \R$.
We aim to establish that: 
:$\map {f_a} x = \map \exp {a - x} \exp x = \exp a$
for all $a, x \in \R$. 
Then, we can fix $x, y \in \R$ and set $a = x + y$ to obtain: 
:$\map {f_a} x = \exp y \exp x = \map \exp {x + y}$
which is the claim.
Note that $f_a$ is differentiable and we have: 
{{begin-eqn}}
{{eqn | l = \map {f_a'} x
      | r = \map {\frac \d {\d x} } {\map \exp {a - x} } \exp x + \map {\frac \d {\d x} } {\exp x} \map \exp {a - x}
      | c = Product Rule for Derivatives
}}
{{eqn | r = -\map \exp {a - x} \exp x + \exp x \map \exp {a - x}
      | c = Chain Rule for Derivatives, Derivative of Exponential Function
}}
{{eqn | r = 0
}}
{{end-eqn}}
From Zero Derivative implies Constant Function, $f_a$ is constant.
That is, there exists $C \in \R$ such that: 
:$\map {f_a} x = C$
for all $x \in \R$.
We have: 
{{begin-eqn}}
{{eqn | l = \map {f_a} a
      | r = \map \exp {a - a} \exp a
}}
{{eqn | r = \exp 0 \exp a
}}
{{eqn | r = \exp a
	  | c = Exponential of Zero
}}
{{end-eqn}}
So: 
:$\map {f_a} x = \exp a$
for all $a, x \in \R$. 
That is: 
:$\map \exp {a - x} \map \exp x = \exp a$
for all $a, x \in \R$. 
Hence the result.
{{qed}}
Theorem: Exponential of Sum/Real Numbers

Let $x, y \in \R$ be real numbers.
Let $\exp x$ be the exponential of $x$.
Then:
:$\map \exp {x + y} = \paren {\exp x} \paren {\exp y}$

Proof:
Let $\exp$ be defined as the limit of a sequence:
:$\ds \map \exp x = \lim_{n \mathop \to \infty} \paren {1 + \frac x n}^n$
Then:
{{begin-eqn}}
{{eqn | l = \paren {\exp x} \paren {\exp y}
      | r = \paren {\lim_{n \mathop \to \infty} \paren {1 + \frac x n}^n} \paren {\lim_{n \mathop \to \infty} \paren {1 + \frac y n}^n}
      | c = {{Defof|Real Exponential Function}}
}}
{{eqn | r = \lim_{n \mathop \to \infty} \paren {1 + \frac x n}^n \paren {1 + \frac y n}^n
      | c = Product Rule for Real Sequences
}}
{{eqn | r = \lim_{n \mathop \to \infty} \paren {1 + \frac {x + y} n + \frac {xy} {n^2} }^n
}}
{{end-eqn}}
Now, let:
:$\nu_n = n$
:$\xi_n = \dfrac {x + y} n + \dfrac {xy} {n^2}$
for all $n \in \N$
Since:
{{begin-eqn}}
{{eqn | l = \lim_{n \mathop \to \infty} \nu_n \xi_n
      | r = \lim_{n \mathop \to \infty} x + y + \dfrac {xy} n
}}
{{eqn | r = x + y
}}
{{end-eqn}}
it follows from Generalized Exponential Limit that:
:$\ds\lim_{n \mathop \to \infty} \paren {1 + \frac {x + y} n + \frac {xy} {n^2} }^n = \map \exp {x + y}$
with $\exp$ defined as a power series.
Hence, by Equivalence of Definitions of Real Exponential Function:
:$\paren {\exp x} \paren {\exp y} = \map \exp {x + y}$
{{qed}}
Theorem: Exponential of Product

Let $x, y \in \R$ be real numbers.
Let $\exp x$ be the exponential of $x$.
Then:
:$\map \exp {x y} = \paren {\exp y}^x$

Proof:
Let $Y = \exp y$.
From Exponential of Natural Logarithm:
:$\map \ln {\exp y} = y$
From Logarithms of Powers, we have:
:$\ln Y^x = x \ln Y = x \, \map \ln {\exp y} = x y$
Thus:
:$\map \exp {x y} = \map \exp {\ln Y^x} = Y^x = \paren {\exp y}^x$
{{qed}}
Theorem: Exponential of Product

Let $x, y \in \R$ be real numbers.
Let $\exp x$ be the exponential of $x$.
Then:
:$\map \exp {x y} = \paren {\exp y}^x$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {\exp y}^x
      | r = \map \exp {x \map \ln {\exp y} }
      | c = {{Defof|Power to Real Number}}
}}
{{eqn | r = \map \exp {x y}
      | c = Exponential of Natural Logarithm
}}
{{end-eqn}}
{{qed}}
Theorem: Exponential of Product

Let $x, y \in \R$ be real numbers.
Let $\exp x$ be the exponential of $x$.
Then:
:$\map \exp {x y} = \paren {\exp y}^x$

Proof:
For $n \in \Z_{\ge 0}$:
{{begin-eqn}}
{{eqn | l = \map \exp {n y}
      | r = \map \exp {\sum_{k \mathop = 1}^n y}
}}
{{eqn | r = \prod_{k \mathop = 1}^n \exp y
      | c = Exponential of Sum of Real Numbers
}}
{{eqn | n = 1
      | r = \paren {\exp y}^n
}}
{{end-eqn}}
That is:
:$\forall n \in \Z_{\ge 0}: \map \exp {n y} = \paren {\exp y}^n$
Now let $n \in \Z_{<0}$.
It follows that $-n \in \Z_{>0}$, so:
{{begin-eqn}}
{{eqn | l = \exp n
      | r = \map \exp {-\paren {-n y} }
}}
{{eqn | r = \frac 1 {\map \exp {-n y} }
      | c = Reciprocal of Real Exponential
}}
{{eqn | r = \frac 1 {\paren {\exp y}^{-n} }
      | c = from $(1)$
}}
{{eqn | r = \paren {\exp y}^n
      | c = Real Number to Negative Power: Positive Integer
}}
{{end-eqn}}
Thus:
:$(2): \quad \forall m \in \Z: \map \exp {m y} = \paren {\exp y}^m$
Next, for $n \in \Z_{>0}$:
{{begin-eqn}}
{{eqn | l = \exp y
      | r = \map \exp {n \frac y n}
}}
{{eqn | r = \paren {\map \exp {\frac y n} }^n
      | c = from $(1)$
}}
{{eqn | n = 3
      | ll= \leadsto
      | l = \sqrt [n] {\exp y}
      | r = \map \exp {\frac y n}
}}
{{end-eqn}}
So fix $r \in \Q$.
Let $r = \dfrac m n$, where $m \in \Z$ is an integer and $n \in \Z_{>0}$ is a strictly positive integer.
From the above:
{{begin-eqn}}
{{eqn | l = \map \exp {r y}
      | r = \map \exp {\frac m n y}
}}
{{eqn | r = \sqrt [n] {\map \exp {m y} }
      | c = from $(3$
}}
{{eqn | r = \sqrt [n] {\paren {\exp y}^m}
      | c = from $(2)$
}}
{{eqn | r = \paren {\exp y}^r
}}
{{end-eqn}}
Thus, from the definition of $\paren {\exp y}^x$ as the unique continuous extension of $r \mapsto \paren {\exp y}^r$ from $\Q$ to $\R$:
:$\map \exp {x y} = \paren {\exp y}^x$
{{qed}}
Theorem: Exponent Combination Laws

Let $a, b \in \R_{>0}$ be strictly positive real numbers.
Let $x, y \in \R$ be real numbers.
Let $a^x$ be defined as $a$ to the power of $x$.
Then:
=== Product of Powers ===
{{:Exponent Combination Laws/Product of Powers}}
=== Power of Product ===
{{:Exponent Combination Laws/Power of Product}}
=== Negative Power ===
{{:Exponent Combination Laws/Negative Power}}
=== Power of Power ===
{{:Exponent Combination Laws/Power of Power}}
=== Quotient of Powers ===
{{:Exponent Combination Laws/Quotient of Powers}}
=== Power of Quotient ===
{{:Exponent Combination Laws/Power of Quotient}}
=== Negative Power of Quotient ===
{{:Exponent Combination Laws/Negative Power of Quotient}}

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

Let $a, b \in \R_{>0}$ be strictly positive real numbers.
Let $x, y \in \R$ be real numbers.
Let $a^x$ be defined as $a$ to the power of $x$.
Then:
=== Product of Powers ===
{{:Exponent Combination Laws/Product of Powers}}
=== Power of Product ===
{{:Exponent Combination Laws/Power of Product}}
=== Negative Power ===
{{:Exponent Combination Laws/Negative Power}}
=== Power of Power ===
{{:Exponent Combination Laws/Power of Power}}
=== Quotient of Powers ===
{{:Exponent Combination Laws/Quotient of Powers}}
=== Power of Quotient ===
{{:Exponent Combination Laws/Power of Quotient}}
=== Negative Power of Quotient ===
{{:Exponent Combination Laws/Negative Power of Quotient}}

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

Let $a, b \in \R_{>0}$ be strictly positive real numbers.
Let $x, y \in \R$ be real numbers.
Let $a^x$ be defined as $a$ to the power of $x$.
Then:
=== Product of Powers ===
{{:Exponent Combination Laws/Product of Powers}}
=== Power of Product ===
{{:Exponent Combination Laws/Power of Product}}
=== Negative Power ===
{{:Exponent Combination Laws/Negative Power}}
=== Power of Power ===
{{:Exponent Combination Laws/Power of Power}}
=== Quotient of Powers ===
{{:Exponent Combination Laws/Quotient of Powers}}
=== Power of Quotient ===
{{:Exponent Combination Laws/Power of Quotient}}
=== Negative Power of Quotient ===
{{:Exponent Combination Laws/Negative Power of Quotient}}

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}}