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:
We will show that:
:$\forall \epsilon \in \R_{>0}: \size {a^{x y} - \paren {a^x}^y} < \epsilon$
{{WLOG}}, suppose that $x < y$.
Consider $I := \closedint x y$.
Let $I_\Q = I \cap \Q$.
Let $M = \max \set {\size x, \size y}$
Fix $\epsilon \in \R_{>0}$.
From Real Polynomial Function is Continuous:
:$\exists \delta' \in \R_{>0}: \size {a^x - a^{x'} } < \delta' \leadsto \size {\paren {a^x}^{y'} - \paren {a^{x'} }^{y'} } < \dfrac \epsilon 4$
From Power Function on Strictly Positive Base is Continuous:
{{begin-eqn}}
{{eqn | q =\exists \delta_1 \in \R_{>0}
      | l = \size {x x' - y y'}
      | o = <
      | r = \delta_1
}}
{{eqn | ll= \leadsto
      | l = \size {a^{x x'} - a^{x y'} }
      | o = <
      | r = \dfrac \epsilon 4
}}
{{eqn | q =\exists \delta_2 \in \R_{>0}
      | l = \size {x y' - x' y'}
      | o = <
      | r = \delta_2
}}
{{eqn | ll= \leadsto
      | l = \size {a^{x y'} - a^{x' y'} }
      | o = <
      | r = \dfrac \epsilon 4
}}
{{eqn | q = \exists \delta_3 \in \R_{>0}
      | l = \size {x' - x}
      | o = <
      | r = \delta_3
}}
{{eqn | ll= \leadsto
      | l = \size {a^{x'} - a^x}
      | o = <
      | r = \delta'
}}
{{eqn | ll= \leadsto
      | l = \size {\paren {a^x}^{y'} - \paren {a^{x'} }^{y'} }
      | o = <
      | r = \dfrac \epsilon 4
}}
{{eqn | q = \exists \delta_4 \in \R_{>0}
      | l = \size {y' - y}
      | o = <
      | r = \delta_4
}}
{{eqn | ll= \leadsto
      | l = \size {\paren {a^x}^{y'} - \paren {a^x}^{y} }
      | o = <
      | r = \dfrac \epsilon 4
}}
{{end-eqn}}
Further:
{{begin-eqn}}
{{eqn | l = \size {y - y'}
      | o = <
      | r = \frac {\delta_1} {\size x}
}}
{{eqn | ll= \leadsto
      | l = \size {x y - x y'}
      | r = \size x \size {y - y'}
      | c = Absolute Value Function is Completely Multiplicative
}}
{{eqn | o = <
      | r = \size x \frac {\delta_1} {\size x}
      | c = multiplying both sides by $\size x \ge 0$
}}
{{eqn | r = \delta_1
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \size {x - x'}
      | o = <
      | r = \frac {\delta_2} M
}}
{{eqn | ll= \leadsto
      | l = \size {x y' - x'y'}
      | r = \size {y'} \size {x - x'}
      | c = Absolute Value Function is Completely Multiplicative
}}
{{eqn | o = \le
      | r = M \size {x - x'}
      | c = Real Number Ordering is Compatible with Multiplication
}}
{{eqn | o = <
      | r = M \frac {\delta_1} M
      | c = multiplying both sides by $M \ge 0$
}}
{{eqn | r = \delta_2
}}
{{end-eqn}}
Let $\delta = \max \set {\dfrac {\delta_1} {\size x}, \dfrac {\delta_2} M, \delta_3, \delta_4}$.
From Closure of Rational Interval is Closed Real Interval:
:$\exists r, s \in I_\Q: \size {x - r} < \delta \land \size {y - s} < \delta$
Thus:
{{begin-eqn}}
{{eqn | l = \size {a^{x y} - \paren {a^x}^y}
      | o = \le
      | r = \size {a^{x y} - a^{x s} } + \size {a^{x s} - a^{r s} } + \size {a^{r s} - \paren {a^r}^s} + \size {\paren {a^r}^s - \paren {a^x}^s} + \size {\paren {a^x}^s - \paren {a^x}^y}
      | c = Triangle Inequality for Real Numbers
}}
{{eqn | r = \size {a^{x y} - a^{x s} } + \size {a^{x s} - a^{r s} } + \size {\paren {a^r}^s - \paren {a^x}^s} + \size {\paren {a^x}^s - \paren {a^x}^y}
      | c = Product of Indices of Real Number: Rational Numbers
}}
{{eqn | o = < 
      | r = \frac \epsilon 4 + \frac \epsilon 4 + \frac \epsilon 4 + \frac \epsilon 4
      | c = Definition of $r$ and $s$
}}
{{eqn | r = \epsilon
}}
{{end-eqn}}
Hence the result, by Real Plus Epsilon.
{{qed}}