avewright/proofwiki-math huggingface dataset:
Theorem: Union of Unordered Tuples

Let $x_1, \dots, x_n, x_{n+1}, \dots, x_m$ be arbitrary.
Then
:$\set {x_1, \dots, x_n} \cup \set {x_{n + 1}, \dots, x_m} = \set {x_1, \dots, x_n, x_{n + 1}, \dots, x_m}$

Proof:
Let $a$ be arbitrary.
:$a \in \set {x_1, \dots, x_n} \cup \set {x_{n + 1}, \dots, x_m}$
{{iff}}
:$a \in \set {x_1, \dots, x_n}$ or $a \in \set {x_{n + 1}, \dots, x_m}$ by definition of union
{{iff}}
:$a = x_1 \lor \dots \lor a = x_n$ or $a = x_{n + 1} \lor \dots \lor a = x_m$ by definition of unordered tuple
{{iff}}
:$a = x_1 \lor \dots \lor a = x_n \lor a = x_{n + 1} \lor \dots \lor a = x_m$
{{iff}}
:$a \in \set {x_1, \dots, x_n, x_{n + 1}, \dots, x_m}$ by definition of unordered tuple
Thus result follows by definition of set equality.
{{qed}}
Category:Set Theory
e5gxlqozltwspxusogyf4rkscz2r779
Theorem: Gauss-Lucas Theorem

Let $P$ be a non-constant polynomial in $\C$.
Then all zeroes of its derivative $P'$ belong to the convex hull of the set of zeroes of $P$.

Proof:
Over the complex numbers, $P$ is a product of prime factors:
:$\ds \map P z = \alpha \prod_{i \mathop = 1}^n \paren{ z - a_i }$
where:
:$a_1, a_2, \ldots, a_n \in \C$ are the (not necessary distinct) zeroes of $P$
:$\alpha \in \C$ is the leading coefficient of $P$
:$n$ is the degree of $P$.
Let $z$ be any complex number for which $\map P z \ne 0$.
Then we have for the logarithmic derivative:
:$\ds \frac {\map {P'} z} {\map P z} = \sum_{i \mathop = 1}^n \frac 1 {z - a_i}$
In particular, if $z$ is a zero of $P'$ and $\map P z \ne 0$, then:
:$\ds \sum_{i \mathop = 1}^n \frac 1 {z - a_i} = 0$
or:
:$\ds \sum_{i \mathop = 1}^n \frac {\overline z - \overline {a_i} } {\size {z - a_i}^2} = 0$
This may also be written as:
:$\ds \paren {\sum_{i \mathop = 1}^n \frac 1 {\size {z - a_i}^2} } \overline z = \paren {\sum_{i \mathop = 1}^n \frac 1 {\size {z - a_i}^2} \overline {a_i} }$
Taking their conjugates, we see that $z$ is a weighted sum with positive coefficients that sum to one, or the barycenter on affine coordinates, of the complex numbers $a_i$ (with different mass assigned on each root whose weights collectively sum to $1$).
On the other hand, if $\map P z = \map {P'} z = 0$, then:
:$z = 1 \cdot z + 0 \cdot a_i$
and is still a convex combination of the zeroes of $P$.
{{qed}}
{{Namedfor|Carl Friedrich Gauss|name2 = François Édouard Anatole Lucas|cat = Gauss|cat2 = Lucas}}
Category:Complex Analysis
asmmso73ybdf03yf23mjce6a8fb9now
Theorem: Way Below implies Preceding

Let $\left({S, \preceq}\right)$ be an ordered set.
Let $x, y \in S$ such that
:$x \ll y$
where $\ll$ denotes element is way below second element.
Then
:$x \preceq y$

Proof:
By Singleton is Directed and Filtered Subset:
:$\left\{ {y}\right\}$ is directed.
By Supremum of Singleton:
:$\left\{ {y}\right\}$ admits a supremum and $\sup \left\{ {y}\right\} = y$
By definition of reflexivity:
:$y \preceq \sup \left\{ {y}\right\}$
By definition of way below:
:$\exists d \in \left\{ {y}\right\}: x \preceq d$
Thus by definition of singleton:
:$x \preceq y$
{{qed}}
Theorem: Preceding and Way Below implies Way Below

Let $\struct {S, \preceq}$ be an ordered set.
Let $u, x, y, z \in S$ such that
:$u \preceq x \ll y \preceq z$
where $\ll$ denotes the way below relation.
Then
:$u \ll z$

Proof:
Let $D$ be a directed subset of $S$ such that
:$D$ admits a supremum
and
:$z \preceq \sup D$
By definition of transitivity:
:$y \preceq \sup D$
By definition of way below relation:
:$\exists d \in D: x \preceq d$
Thus by definition of transitivity:
:$\exists d \in D: u \preceq d$
Thus by definition of way below relation:
:$u \ll z$
{{qed}}
Theorem: Join is Way Below if Operands are Way Below

Let $\struct {S, \vee, \preceq}$ be a join semilattice.
Let $x, y, z \in S$ such that
:$x \ll z$ and $y \ll z$
where $\ll$ denotes the way below relation.
Then
:$x \vee y \ll z$

Proof:
Let $D$ be a directed subset of $S$ such that
:$D$ admits a supremum
and
:$z \preceq \sup D$
By definition of way below relation:
:$\exists d_1 \in D: x \preceq d_1$
and
:$\exists d_2 \in D: y \preceq d_2$
By definition of directed subset:
:$\exists d \in D: d_1 \preceq d$ and $d_2 \preceq d$
By definition of transitivity:
:$x \preceq d$ and $y \preceq d$
Thus by definition of supremum:
:$x \vee y \preceq d$
Thus by definition way below relation:
:$x \vee y \ll z$
{{qed}}
Theorem: Way Below Relation is Transitive

Let $\left({S, \preceq}\right)$ be an ordered set.
Let $x, y, z \in S$ such that
:$x \ll y \ll z$
Then
:$x \ll z$

Proof:
By Way Below implies Preceding:
:$x \preceq y$
By definition of reflexivity:
:$z \preceq z$
Thus by Preceding and Way Below implies Way Below:
:$x \ll z$
{{qed}}
Theorem: Way Below Relation is Antisymmetric

Let $\struct {S, \preceq}$ be an ordered set.
Let $x, y \in S$ such that
:$x \ll y$ and $y \ll x$
Then
:$x = y$

Proof:
By Way Below implies Preceding:
:$x \preceq y$ and $y \preceq x$
Thus by definition of antisymmetry:
:$x = y$
{{qed}}
Theorem: Continued Fraction Expansion of Golden Mean

The golden mean has the simplest possible continued fraction expansion, namely $\sqbrk {1, 1, 1, 1, \ldots}$:
:$\phi = 1 + \cfrac 1 {1 + \cfrac 1 {1 + \cfrac 1 {\ddots} } }$

Proof:
Let:
:$x = 1 + \cfrac 1 {1 + \cfrac 1 {1 + \cfrac 1 {\ddots} } }$
Then:
{{begin-eqn}}
{{eqn | l = x
      | r = 1 + \frac 1 x
      | c = substituting for $x$
}}
{{eqn | ll= \leadsto
      | l = x^2
      | r = x + 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x^2 - x - 1
      | r = 0
      | c = 
}}
{{end-eqn}}
The result follows from Golden Mean as Root of Quadratic.
{{qed}}
Theorem: Fibonacci Number less than Golden Section to Power less One

For all $n \in \N_{> 0}$:
:$F_n \le \phi^{n - 1}$
where:
:$F_n$ is the $n$th Fibonacci number
:$\phi$ is the golden section: $\phi = \dfrac {1 + \sqrt 5} 2$

Proof:
The proof proceeds by induction.
For all $n \in \N_{> 0}$, let $\map P n$ be the proposition:
:$F_n \le \phi^{n - 1}$
Theorem: Square of Golden Mean equals One plus Golden Mean

:$\phi^2 = \phi + 1$
where $\phi$ denotes the golden mean.

Proof:
{{begin-eqn}}
{{eqn | l = \phi
      | r = \frac 1 {\phi - 1}
      | c = {{Defof|Golden Mean|index = 3}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \phi \paren {\phi - 1}
      | r = 1
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \phi^2
      | r = \phi + 1
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Fibonacci Number greater than Golden Section to Power less Two

For all $n \in \N_{\ge 2}$:
:$F_n \ge \phi^{n - 2}$
where:
:$F_n$ is the $n$th Fibonacci number
:$\phi$ is the golden section: $\phi = \dfrac {1 + \sqrt 5} 2$

Proof:
The proof proceeds by induction.
For all $n \in \N_{\ge 2}$, let $\map P n$ be the proposition:
:$F_n \ge \phi^{n - 2}$
Theorem: Triangular Number as Alternating Sum and Difference of Squares

{{begin-eqn}}
{{eqn | q = \forall n \in \N
      | l = \frac {n \paren {n + 1} } 2
      | r = \sum_{j \mathop = 0}^{n - 1} \paren {-1}^j \paren {n - j}^2
      | c = 
}}
{{eqn | r = n^2 - \paren {n - 1}^2 + \paren {n - 2}^2 - \cdots + \paren {-1}^{n - 1} 
      | c = 
}}
{{end-eqn}}
Thus the $n$th triangular number can be expressed as the alternating sum and difference of squares:
So:
{{begin-eqn}}
{{eqn | l = 1
      | r = 1^2
      | c = 
}}
{{eqn | l = 3
      | r = 2^2 - 1^2
      | c = 
}}
{{eqn | l = 6
      | r = 3^2 - 2^2 + 1^2
      | c = 
}}
{{eqn | l = 10
      | r = 4^2 - 3^2 + 2^2 - 1^2
      | c = 
}}
{{end-eqn}}
and so on.

Proof:
The proof proceeds by induction.
For all $n \in \N_{> 0}$, let $\map P n$ be the proposition:
:$\ds \frac {n \paren {n + 1} } 2 = \sum_{j \mathop = 0}^{n - 1} \paren {-1}^j \paren {n - j}^2$
Theorem: Bernoulli's Inequality/Corollary

Let $x \in \R$ be a real number such that $0 < x < 1$.
Let $n \in \Z_{\ge 0}$ be a positive integer.
Then:
:$\paren {1 - x}^n \ge 1 - n x$

Proof:
Let $0 < x < 1$.
Let $y = -x$.
Then $y > -1$ and by Bernoulli's Inequality:
:$\paren {1 + y}^n \ge 1 + n y$
Thus:
:$\paren {1 + \paren {-x} }^n \ge 1 + n \paren {-x}$
Hence the result.
{{qed}}
Theorem: Bernoulli's Inequality/Corollary

Let $x \in \R$ be a real number such that $0 < x < 1$.
Let $n \in \Z_{\ge 0}$ be a positive integer.
Then:
:$\paren {1 - x}^n \ge 1 - n x$

Proof:
Proof by induction:
Let $0 < x < 1$.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\paren {1 - x}^n \ge 1 - n x$
=== Basis for the Induction ===
$\map P 0$ is the case:
:$\paren {1 - x}^0  = 1 \ge 1 - 0 x = 1$
so $\map P 0$ holds.
This is our basis for the induction.
=== Induction Hypothesis ===
Now we need to show that, if $\map P k$ is true, where $k \ge 0$, then it logically follows that $\map P {k + 1}$ is true.
So this is our induction hypothesis:
:$\paren {1 - x}^k \ge 1 - k x$
We need to show that:
:$\paren {1 - x}^{k + 1} \ge 1 - \paren {k + 1} x$
=== Induction Step ===
This is our induction step:
{{begin-eqn}}
{{eqn | l = \paren {1 - x}^{k + 1}
      | r = \paren {1 - x}^k \paren {1 - x}
}}
{{eqn | o = \ge
      | r = \paren {1 - k x} \paren {1 - x}
      | c = Induction Hypothesis
}}
{{eqn | r = 1 - \paren {k + 1} x + k x^2
}}
{{eqn | o = \ge
      | r = 1 - \paren {k + 1} x
}}
{{end-eqn}}
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
{{qed}}
Theorem: 2 to the n is Greater than n Cubed when n is 10 and above

:$\forall n \in \Z, n \ge 10: 2^n > n^3$

Proof:
Proof by induction:
For all $n \in \Z$ such that $n \ge 10$, let $\map P n$ be the proposition:
:$2^n > n^3$
We note that:
:$2^9 = 512 < 729 = 9^3$
so when $n < 10$ the proposition does not hold.
Theorem: Set of Integers is not Well-Ordered by Usual Ordering

The set of integers $\Z$ is not well-ordered under the usual ordering $\le$.

Proof:
{{AimForCont}} $\Z$ is a well-ordered set.
Then by definition, all subsets of $\Z$ has a smallest element.
But take $\Z$ itself.
Suppose $x \in \Z$ is a smallest element.
Then $x - 1 \in \Z$.
But $x - 1 < x$, which contradicts the supposition that $x \in \Z$ is a smallest element.
Hence there can be no such smallest element.
So by Proof by Contradiction, $\Z$ is not well-ordered by $\le$.
{{qed}}
Theorem: Set of Integers can be Well-Ordered

The set of integers $\Z$ can be well-ordered with an appropriately chosen ordering.

Proof:
Consider the ordering $\preccurlyeq \subseteq \Z \times \Z$ defined as:
:$x \preccurlyeq y \iff \left({\left\vert{x}\right\vert < \left\vert{y}\right\vert}\right) \lor \left({\left\vert{x}\right\vert = \left\vert{y}\right\vert \land x \le y}\right)$
{{finish|It remains to be shown that $\preccurlyeq$ is an ordering, and also that it is a well-ordering.}}
Theorem: Set of Non-Negative Real Numbers is not Well-Ordered by Usual Ordering

The set of non-negative real numbers $\R_{\ge 0}$ is not well-ordered under the usual ordering $\le$.

Proof:
{{AimForCont}} $\R_{\ge 0}$ is a well-ordered set.
Then by definition, all subsets of $\R_{\ge 0}$ has a smallest element.
Take the subset $\R_{> 0}$:
:$\R_{> 0} = \left\{ {x \in \R_{\ge 0}: x > 0}\right\} = \R_{\ge 0} \setminus \left\{ {0}\right\}$
Suppose $x \in \R_{> 0}$ is a smallest element.
Then $\dfrac x 2 \in \R_{> 0}$.
But $\dfrac x 2 < x$, which contradicts the supposition that $x \in \R_{> 0}$ is a smallest element.
Hence there can be no such smallest element.
So by Proof by Contradiction, $\R_{\ge 0}$ is not well-ordered by $\le$.
{{qed}}
Theorem: Existence of Digital Root

Let $n \in \N$ be a natural number.
Let $b \in \N$ such that $b \ge 2$ also be a natural number.
Let $n$ be expressed in base $b$.
Then the digital root base $b$ exists for $n$.

Proof:
By definition, the digital root base $b$ for $n$ is the single digit resulting from:
:adding up the digits in $n$, and expressing the result in base $b$
:adding up the digits in that result, and again expressing the result in base $b$
:repeating until down to one digit.
Let $n = d_1 + b d_2 + \dotsb + b^{m - 1} d_m$ where, for all $i$, $0 \le d_i < b$.
Let $\map S n$ be the digit sum of $n$.
Then:
:$\map S n = d_1 + d_2 + \dotsb + d_m$
Thus:
:$\map S n < n$
unless $d_2, d_3, \dotsb, d_m = 0$
in which case $n$ is a one digit number.
Similarly: 
:$\map S {\map S n} < \map S n$
Every time the digit sum is taken, the result is at least one less than the previous digit sum.
As $n$ is finite, it will take a finite number of steps to reduce the result to a one digit number.
Hence the result.
{{qed}}
Category:Number Bases
Category:Digital Roots
mpaudks30690sblwqpoq04gaklxdkhf
Theorem: Golden Mean is Irrational

The golden mean $\phi$ is irrational.

Proof:
By definition of golden mean:
:$\phi = \dfrac {1 + \sqrt 5} 2$
By Square Root of Prime is Irrational:
:$\sqrt 5$ is irrational.
By Rational Number plus Irrational Number is Irrational:
:$1 + \sqrt 5$ is irrational.
By Irrational Number divided by Rational Number is Irrational:
:$\dfrac {1 + \sqrt 5} 2$ is irrational.
{{qed}}
Theorem: Way Below iff Preceding Finite Supremum

Let $\struct {S, \vee, \wedge, \preceq}$ be a complete lattice.
Let $x, y \in S$.
Then $x \ll y$ {{iff}}
:$\forall X \subseteq S: y \preceq \sup X \implies \exists A \in \map {\it Fin} X: x \preceq \sup A$
where
:$\ll$ denotes the way below relation,
:$\map {\it Fin} X$ denotes the set of all finite subsets of $X$.

Proof:
=== Sufficient Condition ===
Let $x \ll y$
Let $X \subseteq S$ such that:
:$y \preceq \sup X$
Define:
:$F := \set {\sup A: A \in \map {\it Fin} X}$
By definition of union:
:$X = \bigcup \map {\it Fin} X$
By Supremum of Suprema:
:$\sup X = \sup F$
We will prove that:
:$F$ is directed
Let $a, b \in F$.
By definition of $F$:
:$\exists A \in \map {\it Fin} X: a = \sup A$
and
:$\exists B \in \map {\it Fin} X: b = \sup B$
By Union of Subsets is Subset:
:$A \cup B \subseteq X$
By Finite Union of Finite Sets is Finite:
:$A \cup B$ is finite
By definition of ${\it Fin}$:
:$A \cup B \in \map {\it Fin} X$
By definition of $F$:
:$\map \sup {A \cup B} \in F$
By Set is Subset of Union:
:$A \subseteq A \cup B$ and $B \subseteq A \cup B$
By Supremum of Subset:
:$a \preceq \map \sup {A \cup B}$ and $b \preceq \map \sup {A \cup B}$
Thus by definition:
:$F$ is directed
By definition of way below relation:
:$\exists d \in F: x \preceq d$
Thus by definition of $F$:
:$\exists A \in \map {\it Fin} X: x \preceq \sup A$
{{qed|lemma}}
Theorem: Exponent Combination Laws/Product of Powers/Proof 2

Let $a \in \R_{> 0}$ be a positive real number.
Let $x, y \in \R$ be real numbers.
Let $a^x$ be defined as $a$ to the power of $x$.
Then:
:$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}}
Theorem: Exponent Combination Laws/Power of Power/Proof 1

Let $a \in \R_{>0}$ be a (strictly) positive real number.
{{:Power of Power}}

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: Rational Sequence Increasing to Real Number

Let $x \in \R$ be a real number.
Then there exists some increasing rational sequence that converges to $x$.

Proof:
Let $\sequence {x_n}$ denote the sequence defined as:
:$\forall n \in \N: x_n = \dfrac {\floor {n x} } n$
where $\floor {n x}$ denotes the floor of $n x$.
From Floor Function is Integer, $\floor {n x}$ is an integer.
Hence by definition of rational number, $\sequence {x_n}$ is a rational sequence.
From Real Number is between Floor Functions:
:$n x - 1 < \floor {n x} \le n x$
Thus:
:$\dfrac {n x - 1} n < \dfrac {\floor {n x} } n \le x$
Further:
{{begin-eqn}}
{{eqn | l = \lim_{n \mathop \to \infty} \frac {n x - 1} n
      | r = \lim_{n \mathop \to \infty} \paren {x - \frac 1 n}
}}
{{eqn | r = \lim_{n \mathop \to \infty} x - \lim_{n \mathop \to \infty} \frac 1 n
      | c = Combined Sum Rule for Real Sequences
}}
{{eqn | r = x - 0
      | c = Quotient Rule for Limits of Real Functions
}}
{{eqn | r = x
}}
{{end-eqn}}
From the Squeeze Theorem for Real Sequences:
:$\ds \lim_{n \mathop \to \infty} \frac {\floor {n x} } n = x$
From Peak Point Lemma, there is a monotone subsequence $\sequence {x_{n_k} }$ of $\sequence {x_n}$.
We have that $\sequence {x_n}$ is bounded above by $x$.
Hence $\sequence {x_{n_k} }$ is increasing.
From Limit of Subsequence equals Limit of Real Sequence, $\sequence {x_{n_k} }$ converges to $x$.
Hence the result.
{{qed}}
Category:Limits of Sequences
Category:Rational Sequences
shnjiaoct65iab77ukfvkrehzpw8tbd
Theorem: Rational Sequence Decreasing to Real Number

Let $x \in \R$ be a real number.
Then there exists some decreasing rational sequence that converges to $x$.

Proof:
Let $\sequence {x_n}$ denote the sequence defined as:
:$\forall n \in \N : x_n = \dfrac {\ceiling {n x} } n$
where $\ceiling {n x}$ denotes the ceiling of $n x$.
From Ceiling Function is Integer, $\ceiling {n x}$ is an integer.
Hence by definition of rational number, $\sequence {x_n}$ is a rational sequence.
From Real Number is between Ceiling Functions:
:$n x < \ceiling {n x} \le n x + 1$
Thus:
:$x < \dfrac {\ceiling {n x} } n \le \dfrac {n x + 1} n$
Further:
{{begin-eqn}}
{{eqn | l = \lim_{n \mathop \to \infty} \frac {nx + 1} n
      | r = \lim_{n \mathop \to \infty} \paren {x + \frac 1 n}
}}
{{eqn | r = \lim_{n \mathop \to \infty} x + \lim_{n \mathop \to \infty} \frac 1 n
      | c = Combined Sum Rule for Real Sequences
}}
{{eqn | r = x + 0
      | c = Quotient Rule for Limits of Real Functions
}}
{{eqn | r = x
}}
{{end-eqn}}
Thus, from the Squeeze Theorem for Real Sequences:
:$\ds \lim_{n \mathop \to \infty} \frac {\ceiling {n x} } n = x$
From Peak Point Lemma, there is a monotone subsequence $\sequence {x_{n_k} }$ of $\sequence {x_n}$.
We have that $\sequence {x_n}$ is bounded below by $x$.
Hence $\sequence {x_{n_k} }$ is decreasing.
From Limit of Subsequence equals Limit of Real Sequence, $\sequence {x_{n_k} }$ converges to $x$.
Hence the result.
{{qed}}
Category:Limits of Sequences
Category:Rational Sequences
tovzg6izmzp3qs087nsllee1xz44jot
Theorem: Power Function on Base Greater than One is Strictly Increasing/Real Number

Let $a \in \R$ be a real number such that $a > 1$.
Let $f: \R \to \R$ be the real function defined as:
:$\map f x = a^x$
where $a^x$ denotes $a$ to the power of $x$.
Then $f$ is strictly increasing.

Proof:
Let $x, y \in \R$ be such that $x < y$.
Let $\delta = \dfrac {y - x} 2$.
From Rational Sequence Decreasing to Real Number, there is some rational sequence $\sequence {x_n}$ that decreases to $x$.
From Rational Sequence Increasing to Real Number, there is some rational sequence $\sequence {y_n}$ that increases to $y$.
From Convergent Real Sequence is Bounded:
:$\exists N_1 \in \N: n \ge N_1 \implies x - \delta < x_n < x + \delta$
Since $\sequence {x_n}$ is decreasing:
:$n \ge N_1 \implies x \le x_n < x + \delta$
From Convergent Real Sequence is Bounded:
:$\exists N_2 \in \N : n \ge N_2 \implies y - \delta < y_n < y + \delta$
Since $\sequence {y_n}$ is increasing:
:$n \ge N_2 \implies y - \delta < y_n \le y$
Let $N = \max \set {N_1, N_2}$.
Then, for $n \ge N$:
{{begin-eqn}}
{{eqn | l = x
      | o = \le
      | r = x_n
}}
{{eqn | o = <
      | r = x + \delta
}}
{{eqn | r = y - \delta
}}
{{eqn | o = <
      | r = y_n
}}
{{eqn | o = \le
      | r = y
}}
{{end-eqn}}      
From Power Function on Strictly Positive Base is Continuous and Sequential Continuity is Equivalent to Continuity in the Reals:
:$x_n \to x \implies a^{x_n} \to a^x$
:$y_n \to y \implies a^{y_n} \to a^y$
Also, from Power Function on Base Greater than One is Strictly Increasing: Rational Number:
:$\sequence {a^{x_n} }$ decreases to $a^x$
and:
:$\sequence {a^{y_n} }$ increases to $a^y$.
So, for $n \ge N$:
{{begin-eqn}}
{{eqn | l = a^x
      | o = \le
      | r = a^{x_n}
      | c = as $\sequence {a^{x_n} }$ decreases to $a^x$
}}
{{eqn | o = <
      | r = a^{y_n}
      | c = Power Function on Base Greater than One is Strictly Increasing: Rational Number
}}
{{eqn | o = \le
      | r = a^y
      | c = as $\sequence {a^{y_n} }$ increases to $a^y$
}}
{{end-eqn}}
Hence the result.
{{qed}}
Category:Power Function on Base Greater than One is Strictly Increasing
Category:Real Analysis
h6viuyi4p04ksskr37pmf1oug9im86j
Theorem: Power Function on Strictly Positive Base is Continuous/Real Power

Let $f : \R \to \R$ be the real function defined as:
:$\map f x = a^x$
where $a^x$ denotes $a$ to the power of $x$.
Then $f$ is continuous.

Proof:
By definition, $a^x$ is the unique continuous extension of $a^r$, for rational $r$.
By definition, continuous extensions are continuous.
Hence the result.
{{qed}}
Theorem: Power Function on Strictly Positive Base is Continuous/Rational Power

Let $f: \Q \to \R$ be the real-valued function defined as:
:$\map f x = a^x$
where $a^x$ denotes $a$ to the power of $x$.
Then $f$ is continuous.

Proof:
{{proof wanted|first part of proof of Power Function to Rational Power permits Unique Continuous Extension}}
Category:Powers
9cv5bkcj132536wk0xqjpjveimowda4
Theorem: Defining Sequence of Natural Logarithm is Convergent

Let $x \in \R$ be a real number such that $x > 0$.
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}$
Then $\sequence {f_n}$ is pointwise convergent.

Proof:
Fix $x \in \R_{>0}$.
From Defining Sequence of Natural Logarithm is Strictly Decreasing, $\sequence {\map {f_n} x}$ is strictly decreasing.
From Lower Bound of Natural Logarithm, $\sequence {\map {f_n} x}$ is bounded below.
From Monotone Convergence Theorem, $\sequence {\map {f_n} x}$ is convergent.
Hence the result, by definition of pointwise convergence.
{{qed}}
Category:Natural Logarithms
a23v088dwlxvpu32akfqk6vm7hy8nxf
Theorem: Sum of Indices of Real Number/Rational Numbers

Let $x, y \in \Q$ be rational numbers.
Let $r^x$ be defined as $r$ to the power of $n$.
Then:
: $r^{x + y} = r^x \times r^y$

Proof:
Let $x = \dfrac p q, y = \dfrac u v$.
Then:
{{begin-eqn}}
{{eqn | l = r^\paren {x + y}
      | r = r^\paren {\paren {p / q} + \paren {u / v} }
      | c = 
}}
{{eqn | r = r^\paren {\paren {p v + u q} / q v}
      | c = 
}}
{{eqn | r = \paren {r^\paren {1 / q v} }^\paren {p v + u q}
      | c = {{Defof|Rational Power}}
}}
{{eqn | r = \paren {r^\paren {1 / q v} }^\paren {p v} \times \paren {r^\paren {1 / q v} }^\paren {u q}
      | c = Sum of Indices of Real Number: Integers
}}
{{eqn | r = r^\paren {p v / q v} \times r^\paren {u q / q v}
      | c = {{Defof|Rational Power}}
}}
{{eqn | r = r^\paren {p / q} \times r^\paren {u / v}
      | c = 
}}
{{eqn | r = r^x \times r^y
      | c = 
}}
{{end-eqn}}
{{qed}}