avewright/proofwiki-math huggingface dataset:
Theorem: Power Function to Rational Power permits Unique Continuous Extension

Let $a \in \R_{> 0}$.
Let $f: \Q \to \R$ be the real-valued function defined as:
:$\map f q = a^q$
where $a^q$ denotes $a$ to the power of $q$.
Then there exists a unique continuous extension of $f$ to $\R$.

Proof:
Consider $I_k := \openint {-k} k$ for arbitrary $k \in \N$.
Let $I_k' = I_k \cap \Q$.
Note that, for all $x, y \in I_k'$:
{{begin-eqn}}
{{eqn | l = \size {a^x - a^y}
      | r = \size {a^{x - y + y} - a^y}
}}
{{eqn | r = \size {a^{x - y} a^y - a^y}
      | c = Powers of Group Elements
}}
{{eqn | r = \size {a^y} \size {a^{x - y} - 1}
      | c = Absolute Value Function is Completely Multiplicative
}}
{{eqn | r = a^y \size {a^{x - y} - 1}
      | c = Power of Positive Real Number is Positive over Rationals
}}
{{eqn | o = \le
      | r = M \size {a^{x - y} - 1}
      | c = Power Function is Monotone over Rationals
}}
{{end-eqn}}
where $M = \map \max {a^{-k}, a^k}$.
Fix $\epsilon \in \R_{> 0}$.
From Power Function tends to One as Power tends to Zero: Rational Number:
{{begin-eqn}}
{{eqn | q = \exists \delta \in \R_{>0}
      | l = 0
      | o = <
      | m = \size {x - y}
      | mo= <
      | r = \delta
}}
{{eqn | ll= \leadsto
      | o = 
      | m = \size {a^{x - y} - a^0}
      | mo= <
      | r = \dfrac \epsilon M
}}
{{eqn | ll= \leadsto
      | o = 
      | m = \size {a^{x - y} - 1}
      | mo= <
      | r = \dfrac \epsilon M
      | c = {{Defof|Integer Power|Power of Zero}}
}}
{{end-eqn}}
where $M$ is defined as above.
Therefore, $\exists \delta \in \R_{> 0}$ such that:
{{begin-eqn}}
{{eqn | l = \size {x - y}
      | o = <
      | r = \delta
}}
{{eqn | ll= \leadsto
      | l = \size {a^x - a^y}
      | o = \le
      | r = M \size {a^{x - y} - 1}
}}
{{eqn | o = <
      | r = M \dfrac \epsilon M
}}
{{eqn | r = \epsilon
}}
{{end-eqn}}
That is, $f$ is uniformly continuous on $I_k'$.
From Rationals are Everywhere Dense in Topological Space of Reals, $I_k'$ is everywhere dense in $I_k$.
From Continuous Extension from Dense Subset, there exists a unique continuous extension of $f$ to $I_k$.
Call this function $f_k$.
Define:
:$\ds F = \bigcup \set {f_k : k \in \N}$
Note that $\sequence {I_k}$ is an exhausting sequence of sets in $\R$.
By the Union of Functions Theorem, $F$ defines a function $\R \to \R$
From the Pasting Lemma, $F$ is continuous on $\R$.
Hence the result.
{{qed}}
Category:Powers
k9es9t7n8jqiucub1u3641kum1j23u8
Theorem: Meet-Continuous iff Meet of Suprema equals Supremum of Meet of Directed Subsets

Let $\mathscr S = \struct {S, \vee, \wedge, \preceq}$ be an up-complete lattice.
Then:
:$\mathscr S$ is meet-continuous
{{iff}}:
:for every directed subsets $D_1, D_2$ of $S$: $\paren {\sup D_1} \wedge \paren {\sup D_2} = \sup \set {d_1 \wedge d_2: d_1 \in D_1, d_2 \in D_2}$

Proof:
=== Sufficient Condition ===
Let $\mathscr S$ be meet-continuous.
By Meet-Continuous iff Meet of Suprema equals Supremum of Meet of Ideals:
:for every ideals $I, J$ in $\mathscr S$: $\paren {\sup I} \wedge \paren {\sup J} = \sup \set {i \wedge j: i \in I, j \in J}$
Let $D_1, D_2$ directed subsets of $S$.
By definition of up-complete:
:$D_1$ and $D_2$ admit suprema
By Supremum of Lower Closure of Set:
:$D_1^\preceq$ and $D_2^\preceq$ admit suprema
where
:$D_1^\preceq$ denotes the lower closure of $D_1$.
Thus
{{begin-eqn}}
{{eqn | l = \paren {\sup D_1} \wedge \paren {\sup D_2}
      | r = \paren {\sup D_1^\preceq} \wedge \paren {\sup D_2^\preceq}
      | c = Supremum of Lower Closure of Set
}}
{{eqn | r = \sup \set {i_1 \wedge i_2: i_1 \in D_1^\preceq, i_2 \in D_2^\preceq}
      | c = $D_1^\preceq$ is ideal in $\mathscr S$
}}
{{eqn | r = \sup \set {i_1 \wedge i_2: i_1 \in D_1^\preceq, i_2 \in D_2^\preceq}^\preceq
      | c = Supremum of Lower Closure of Set
}}
{{eqn | r = \sup \set {i_1 \wedge i_2: i_1 \in D_1, i_2 \in D_2}^\preceq
      | c = Lower Closure of Meet of Lower Closures
}}
{{eqn | r = \sup \set {i_1 \wedge i_2: i_1 \in D_1, i_2 \in D_2}
      | c = Supremum of Lower Closure of Set
}}
{{end-eqn}}
{{qed|lemma}}
Theorem: Brouwerian Lattice iff Meet-Continuous and Distributive

Let $\mathscr S = \left({S, \vee, \wedge, \preceq}\right)$ be a complete lattice.
Then
:$\mathscr S$ is a Brouwerian lattice
{{iff}}
:$\mathscr S$ is meet-continuous and distributive.

Proof:
=== Sufficient Condition ===
Let $\mathscr S$ be a Brouwerian lattice.
By Relative Pseudocomplement and Shift Mapping form Galois Connection in Brouwerian Lattice:
:for every $x \in S$, a mapping $f: S \to S$ if $\forall y \in S: f\left({y}\right) = x \wedge y$, then $f$ is lower adjoint of Galois connection
By Shift Mapping is Lower Adjoint iff Meet is Distributive with Supremum:
:$\forall x \in S, X \subseteq S: x \wedge \sup X = \sup \left\{ {x \wedge y: y \in X}\right\}$
Thus by definition of complete lattice:
:$\mathscr S$ is up-complete.
Thus
:for every an element $x \in S$ and a directed subset $D$ of $S$: $x \wedge \sup D = \sup \left\{ {x \wedge d: d \in D}\right\}$
Thus by definition
:$\mathscr S$ is meet-continuous.
Thus by Brouwerian Lattice is Distributive:
:$\mathscr S$ is distributive.
{{qed|lemma}}
Theorem: Power is Well-Defined/Integer

Let $x$ be a non-zero real number.
Let $k$ be an integer.
Then $x^k$ is well-defined.

Proof:
Fix $x \in \R \setminus \set 0$.
Theorem: Power is Well-Defined/Rational

Let $x \in \R_{> 0}$ be a (strictly) positive real number.
Let $q$ be a rational number.
Then $x^q$ is  well-defined.

Proof:
Let $x \in \R_{>0}$ be fixed.
Let $q \in \Q \setminus \set 0$.
Let $\dfrac r s$ and $\dfrac t u$ be two representations of $q$.
That is, $r, s, t, u$ are non-zero integers.
We now show that:
: $\dfrac r s = \dfrac t u \implies x^{r / s} = x^{t / u}$
So:
{{begin-eqn}}
{{eqn | l = \dfrac r s
      | r = \dfrac t u
}}
{{eqn | ll= \leadsto
      | l = r u
      | r = t s
}}
{{eqn | ll= \leadsto
      | l = x^{r u}
      | r = x^{s t}
      | c = Power is Well-Defined: Integer
}}
{{eqn | ll= \leadsto
      | l = \paren {x^r}^u
      | r = \paren {x^t}^s
      | c = Product of Indices of Real Number: Integers
}}
{{eqn | ll= \leadsto
      | l = \sqrt [u] {\paren {x^r}^u}
      | r = \sqrt [u] {\paren {x^t}^s}
      | c = Existence and Uniqueness of Positive Root of Positive Real Number
}}
{{eqn | ll= \leadsto
      | l = x^r
      | r = \sqrt [u] {\paren {x^t}^s}
      | c = {{Defof|Root of Number}}
}}
{{eqn | ll= \leadsto
      | l = \sqrt [s] {\paren {x^r} }
      | r = \sqrt [s] {\sqrt [u] {\paren {x^t}^s} }
      | c = Existence and Uniqueness of Positive Root of Positive Real Number
}}
{{eqn | ll= \leadsto
      | l = \sqrt [s] {\paren {x^r} }
      | r = \sqrt [u] {\sqrt [s] {\paren {x^t}^s} }
      | c = Root is Commutative
}}
{{eqn | ll= \leadsto
      | l = \sqrt [s] {\paren {x^r} }
      | r = \sqrt [u] {\paren {x^t} }
      | c = {{Defof|Root of Number}}
}}
{{eqn | ll= \leadsto
      | l = x^{r / s}
      | r = x^{t / u}
      | c = {{Defof|Rational Power}}
}}
{{end-eqn}}
Hence the result.
{{qed}}
Category:Powers
5o7t8gu54q0ow3pu3gufpgl34fkczsf
Theorem: Real Number between Zero and One is Greater than Power/Natural Number

Let $x \in \R$.
Let $0 < x < 1$.
Let $n$ be a natural number.
Then:
: $0 < x^n \le x$

Proof:
For all $n \in \N$, let $\map P n$ be the proposition:
:$0 < x < 1 \implies 0 < x^n \le x$
=== Basis for the Induction ===
$\map P 1$ is true, since $0 < x < 1 \implies 0 < x^1 \le x$ by definition of exponent of $1$.
This is our basis for the induction.
=== Induction Hypothesis ===
Now we need to show that, if $\map P k$ is true, where $k \ge 1$, then it logically follows that $\map P {k + 1}$ is true.
So this is our induction hypothesis:
:$0 < x < 1 \implies 0 < x^k \le x$
Then we need to show:
:$0 < x < 1 \implies 0 < x^{k + 1} \le x$
=== Induction Step ===
This is our induction step:
{{begin-eqn}}
{{eqn | l = 0 < x < 1
      | o = \leadsto
      | r = 0 < x^k \le x
      | c = Induction Hypothesis
}}
{{eqn | o = \leadsto
      | r = 0 < x^{k + 1} \le x \cdot x
      | c = Real Number Ordering is Compatible with Multiplication
}}
{{eqn | o = \leadsto
      | r = 0 < x^{k + 1} \le x
      | c = Multiple of Positive Real Number with Number Less Than One is Less Than Real Number
}}
{{end-eqn}}
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\forall n \in \N: 0 < x < 1 \implies 0 < x^n \le x$
Hence the result.
{{qed}}
Theorem: Power Function is Strictly Increasing over Positive Reals/Natural Exponent

Let $n \in \Z_{>0}$ be a strictly positive integer.
Let $f: \R_{>0} \to \R$ be the real function defined as:
:$\map f x = x^n$
where $x^n$ denotes $x$ to the power of $n$.
Then $f$ is strictly increasing.

Proof:
Proof by induction on $n$:
Let $x, y \in \R_{>0}$ be strictly positive real numbers.
For all $n \in \Z_{>0}$, let $P \left({n}\right)$ be the proposition:
:$x < y \implies x^n < y^n$
Theorem: Root is Strictly Increasing

Let $x \in \R_{> 0}$.
Let $n \in \N$.
Let $f: \R_{> 0} \to \R$ be the real function defined as:
:$\map f x = \sqrt [n] x$
where $\sqrt [n] x$ denotes the $n$th root of $x$.
Then $f$ is strictly increasing.

Proof:
Let $x, y \in \R$ such that $0 < x < y$.
{{AimForCont}} that:
:$\sqrt [n] x \ge \sqrt [n] y$
We have:
{{begin-eqn}}
{{eqn | l = \sqrt [n] x
      | o = \ge
      | r = \sqrt [n] y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {\sqrt [n] x}^n
      | o = \ge
      | r = \paren {\sqrt [n] y}^n
      | c = Power Function is Strictly Increasing over Positive Reals: Natural Exponent
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \ge
      | r = y
      | c = {{Defof|Root of Number}}
}}
{{end-eqn}}
This contradicts the hypothesis that $x < y$.
Therefore, by Proof by Contradiction:
:$0 < x < y \implies \sqrt [n] x \le \sqrt [n] y$
Hence the result by definition of strictly increasing real function.
{{qed}}
Category:Examples of Strictly Increasing Real Functions
Category:Roots of Numbers
iz5vjrbqqzsntn2vnzehsa540znx0tp
Theorem: Shift Mapping is Lower Adjoint iff Meet is Distributive with Supremum

Let $\struct {S, \preceq}$ be a complete lattice.
Then:
:$\forall x \in S, f: S \to S: \paren {\forall y \in S: \map f y = x \wedge y} \implies f$ is lower adjoint of a Galois connection
{{iff}}:
:$\forall x \in S, X \subseteq S: x \wedge \sup X = \sup \set {x \wedge y: y \in X}$

Proof:
=== Sufficient Condition ===
Assume that
:$\forall x \in S, f: S \to S: \paren {\forall y \in S: \map f y = x \wedge y} \implies f$ is lower adjoint of a Galois connection
Let $x \in S, X \subseteq S$.
Define a mapping $f: S \to S$:
:$\forall y \in S: \map f y := x \wedge y$
By assumption:
:$f$ is lower adjoint of a Galois connection.
By Lower Adjoint Preserves All Suprema:
:$f$ preserves all suprema.
By definition of mapping preserves all suprema
:$f$ preserves the supremum of $X$.
By definition of complete lattice:
:$X$ admits a supremum.
Thus
{{begin-eqn}}
{{eqn | l = x \wedge \sup X
      | r = \map f {\sup X}
      | c = Definition of $f$
}}
{{eqn | r = \map \sup {\map {f^\to} X}
      | c = {{Defof|Mapping Preserves Supremum|subdef = Subset}}
}}
{{eqn | r = \sup \set {\map f y: y \in X}
      | c = {{Defof|Image of Subset under Mapping}}
}}
{{eqn | r = \sup \set {x \wedge y: y \in X}
      | c = Definition of $f$
}}
{{end-eqn}}
{{qed|lemma}}
Theorem: Greatest Common Divisor is Associative

Let $a, b, c \in \Z$.
Then:
:$\gcd \set {a, \gcd \set {b, c} } = \gcd \set {\gcd \set {a, b}, c}$
where $\gcd$ denotes the greatest common divisor.

Proof:
Follows directly from GCD from Prime Decomposition and Min Operation is Associative.
Theorem: Lowest Common Multiple is Associative

Let $a, b, c \in \Z$.
Then:
:$\lcm \set {a, \lcm \set {b, c} } = \lcm \set {\lcm \set {a, b}, c}$
where $\lcm$ denotes the lowest common multiple.

Proof:
Follows directly from LCM from Prime Decomposition and Max Operation is Associative.
Theorem: LCM equals Product iff Coprime

Let $a, b \in \Z_{>0}$ be strictly positive integers.
Then:
:$\lcm \set {a, b} = a b$
{{iff}}:
:$a$ and $b$ are coprime
where $\lcm$ denotes the lowest common multiple.

Proof:
=== Necessary Condition ===
Let $a$ and $b$ be coprime.
Then:
{{begin-eqn}}
{{eqn | l = \lcm \set {a, b}
      | r = \frac {a b} {\gcd \set {a, b} }
      | c = Product of GCD and LCM
}}
{{eqn | r = \frac {a b} 1
      | c = {{Defof|Coprime Integers}}
}}
{{eqn | r = a b
}}
{{end-eqn}}
{{qed|lemma}}
Theorem: GCD with One Fixed Argument is Multiplicative Function

Let:
:$a, b, c \in \Z: b \perp c$
where $b \perp c$ denotes that $b$ is coprime to $c$.
Then:
:$\gcd \set {a, b} \gcd \set {a, c} = \gcd \set {a, b c}$
That is, GCD is multiplicative.

Proof:
{{begin-eqn}}
{{eqn | l = \gcd \set {a, b c}
      | r = \gcd \set {a, \lcm \set {b, c} }
      | c = LCM equals Product iff Coprime
}}
{{eqn | r = \lcm \set {\gcd \set {a, b}, \gcd \set {a, c} }
      | c = GCD and LCM Distribute Over Each Other
}}
{{eqn | r = \frac {\gcd \set {a, b} \gcd \set {a, c} } {\gcd \set {\gcd \set {a, b}, \gcd \set {a, c} } }
      | c = Product of GCD and LCM
}}
{{eqn | r = \frac {\gcd \set {a, b} \gcd \set {a, c} } {\gcd \set {a, \gcd \set {b, \gcd \set {a, c} } } }
      | c = Greatest Common Divisor is Associative
}}
{{eqn | r = \frac {\gcd \set {a, b} \gcd \set {a, c} } {\gcd \set {a, \gcd \set {\gcd \set {b, c}, a} } }
      | c = Greatest Common Divisor is Associative
}}
{{eqn | r = \frac {\gcd \set {a, b} \gcd \set {a, c} } {\gcd \set {a, \gcd \set {1, a} } }
      | c = {{Defof|Coprime Integers}}
}}
{{eqn | r = \frac {\gcd \set {a, b} \gcd \set {a, c} } {\gcd \set {a, 1} }
}}
{{eqn | r = \frac {\gcd \set {a, b} \gcd \set {a, c} } 1
}}
{{eqn | r = \gcd \set {a, b} \gcd \set {a, c}
}}
{{end-eqn}}
{{qed}}
Category:Greatest Common Divisor
Category:Examples of Multiplicative Functions
rz23hulypq9m7rq0no6dbrj6m19wbxg
Theorem: Power Function on Base between Zero and One is Strictly Decreasing/Positive Integer

Let $a \in \R$ be a real number such that $0 < a < 1$.
Let $f: \Z_{\ge 0} \to \R$ be the real-valued function defined as:
:$\map f n = a^n$
where $a^n$ denotes $a$ to the power of $n$.
Then $f$ is strictly decreasing.

Proof:
Proof by induction on $n$:
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$a^{n + 1} < a^n$
$\map P 0$ is the case:
{{begin-eqn}}
{{eqn | l = a^1
      | r = a
      | c = {{Defof|Integer Power}}
}}
{{eqn | o = <
      | r = 1 
      | c = 
}}
{{eqn | r = a^0
      | c = {{Defof|Integer Power}}
}}
{{end-eqn}}
Theorem: Power Function on Base between Zero and One is Strictly Decreasing/Rational Number

Let $a \in \R$ be a real number such that $0 < a < 1$.
Let $f: \Q \to \R$ be the real-valued function defined as:
:$\map f q = a^q$
where $a^q$ denotes $a$ to the power of $q$.
Then $f$ is strictly decreasing.

Proof:
Let $\dfrac r s, \dfrac t u \in \Q$, where $r, t \in \Z, s, u \in \Z_{>0}$.
Let $\dfrac r s < \dfrac t u$.
Then:
{{begin-eqn}}
{{eqn | l = r u
      | o = <
      | r = t s
      | c = Real Number Ordering is Compatible with Multiplication
}}
{{eqn | ll= \leadsto
      | l = a^{r u}
      | o = >
      | r = a^{t s}
      | c = Power Function on Base between Zero and One is Strictly Decreasing: Integer
}}
{{eqn | ll= \leadsto
      | l = \paren {a^r}^u 
      | o = > 
      | r = \paren {a^t}^s
      | c = Product of Indices of Real Number: Integers
}}
{{eqn | ll= \leadsto
      | l = \sqrt [u] {\paren {a^r}^u} 
      | o = >
      | r = \sqrt [u] {\paren {a^t}^s}
      | c = Root is Strictly Increasing
}}
{{eqn | ll= \leadsto
      | l = a^r 
      | o = > 
      | r = \sqrt [u] {\paren {a^t}^s}
      | c = {{Defof|Root of Number|$u$th Root}}
}}
{{eqn | ll= \leadsto
      | l = \sqrt [s] {\paren {a^r} } 
      | o = > 
      | r = \sqrt [s] {\sqrt [u] {\paren {a^t}^s} }
      | c = Root is Strictly Increasing
}}
{{eqn | ll= \leadsto
      | l = \sqrt [s] {\paren {a^r} } 
      | o = > 
      | r = \sqrt [u] {\sqrt [s] {\paren {a^t}^s} }
      | c = Root is Commutative
}}
{{eqn | ll= \leadsto
      | l = \sqrt [s] {\paren {a^r} } 
      | o = > 
      | r = \sqrt [u] {\paren {a^t} }
      | c = {{Defof|Root of Number|$s$th Root}}
}}
{{eqn | ll= \leadsto
      | l = a^{r / s}
      | o = > 
      | r = a^{t / u}
      | c = {{Defof|Rational Power}}
}}
{{end-eqn}}
{{qed}}
Category:Power Function on Base between Zero and One is Strictly Decreasing
a4j6hhdbjrjgo3ott0hql6a1lqby82b
Theorem: Power Function on Base Greater than One is Strictly Increasing/Positive Integer

Let $a \in \R$ be a real number such that $a > 1$.
Let $f: \Z_{\ge 0} \to \R$ be the real-valued function defined as:
:$\map f n = a^n$
where $a^n$ denotes $a$ to the power of $n$.
Then $f$ is strictly increasing.

Proof:
Fix $n \in \Z_{\ge 0}$.
From Ordering of Reciprocals:
:$0 < \dfrac 1 a < 1$
From Power Function on Base between Zero and One is Strictly Decreasing: Positive Integer:
:$\paren {\dfrac 1 a}^{n + 1} < \paren {\dfrac 1 a}^n$
From Real Number to Negative Power: Positive Integer:
:$\dfrac 1 {a^{n + 1} } < \dfrac 1 {a^n}$
From Ordering of Reciprocals:
:$a^n < a^{n + 1}$
Hence the result.
{{qed}}
Category:Power Function on Base Greater than One is Strictly Increasing
9ty6jg9ov8atkj9p3yw8oxqprdu02lk
Theorem: Root of Reciprocal is Reciprocal of Root

Let $x \in \R_{\ge 0}$.
Let $n \in \N$.
Let $\sqrt [n] x$ denote the $n$th root of $x$.
Then:
:$\sqrt [n] {\dfrac 1 x} = \dfrac 1 {\sqrt [n] x}$

Proof:
Let $y = \sqrt [n] {\dfrac 1 x}$.
Then:
{{begin-eqn}}
{{eqn | l = \sqrt [n] {\dfrac 1 x}
      | r = y
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \dfrac 1 x
      | r = y^n
      | c = {{Defof|Root of Number|$n$th root}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | r = \dfrac 1 {y^n}
      | c = Reciprocal of Real Number is Unique
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | r = \paren {\dfrac 1 y}^n
      | c = Powers of Group Elements/Negative Index
}}
{{eqn | ll= \leadstoandfrom
      | l = \sqrt [n] x
      | r = \dfrac 1 y
      | c = {{Defof|Root of Number|$n$th root}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \dfrac 1 {\sqrt [n] x}
      | r = y
      | c = Reciprocal of Real Number is Unique
}}
{{eqn | ll= \leadstoandfrom
      | l = \dfrac 1 {\sqrt [n] x}
      | r = \sqrt [n] {\dfrac 1 x}
      | c = Definition of $y$
}}
{{end-eqn}}
Hence the result.
{{qed}}
Category:Roots of Numbers
954vh8t02n45kn56701jfr626g6gdcv
Theorem: Power Function on Base Greater than One is Strictly Increasing/Rational Number

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

Proof:
Let $\dfrac r s, \dfrac t u \in \Q$, where $r, t \in \Z$ are integers and $s, u \in \Z_{>0}$ are strictly positive integers.
Let $\dfrac r s < \dfrac t u$.
From Ordering of Reciprocals:
:$0 < \dfrac 1 a < 1$
So:
{{begin-eqn}}
{{eqn | l = \paren {\frac 1 a}^{t / u} 
      | o = < 
      | r = \paren {\frac 1 a}^{r / s}
      | c = Power Function on Base between Zero and One is Strictly Decreasing: Rational Number
}}
{{eqn | ll= \leadsto
      | l = \sqrt [u] {\paren {\frac 1 a}^t}
      | o = < 
      | r = \sqrt [s] {\paren {\frac 1 a}^r}
      | c =  {{Defof|Rational Power}}
}}
{{eqn | ll= \leadsto
      | l = \sqrt [u] {\paren {\frac 1 {a^t} } } 
      | o = < 
      | r = \sqrt [s] {\paren {\frac 1 {a^r} } }
      | c = Real Number to Negative Power: Integer
}}
{{eqn | ll= \leadsto
      | l = \frac 1 {\sqrt [u] {a^t} }
      | o = <
      | r = \frac 1 {\sqrt [s] {a^r} }
      | c = Root of Reciprocal is Reciprocal of Root
}}
{{eqn | ll= \leadsto
      | l = \frac 1 {a^{t / u} }
      | o = <
      | r = \frac 1 {a^{r / s} }
      | c = {{Defof|Rational Power}}
}}
{{eqn | ll= \leadsto
      | l = a^{r / s}
      | o = <
      | r = a^{t / u}
      | c = Ordering of Reciprocals
}}
{{end-eqn}}
Hence the result.
{{qed}}
Category:Power Function on Base Greater than One is Strictly Increasing
lm6ydcb44fyxnfu932l30zdwqxas4s4
Theorem: Existence of Square Roots of Positive Real Number

Let $r \in \R_{\ge 0}$ be a positive real number.
Then:
:$\exists y_1 \in \R_{\ge 0}: {y_1}^2 = r$
:$\exists y_2 \in \R_{\le 0}: {y_2}^2 = r$

Proof:
Let $S = \set {x \in \R: x^2 < r}$.
As $0 \in S$, it follows that $S$ is non-empty.
To show that $S$ is bounded above, we note that $r + 1$ is an upper bound:
:$y > r + 1 \implies y^2 > r^2 + 2 r + 1 > r$
and so $y \notin S$.
Thus $x \in S \implies x < r + 1$.
By the Completeness Axiom, $S$ has a supremum, say:
:$u = \sup S$
We already have that $u \ge 0$, as $0 \in S$ as seen.
It remains to demonstrate that $u^2 = r$.
{{AimForCont}} $u^2 \ne r$.
Then either $u^2 > r$ or $u^2 < r$.
Suppose that $u^2 > r$.
Then:
:$\dfrac {u^2 - r} {2 u} > 0$
So there exists $n \in \N$ such that:
:$0 < \dfrac 1 n < \dfrac {u^2 - r} {2 u}$
We note that:
{{begin-eqn}}
{{eqn | l = u - \dfrac {u^2 - 2 r} {2 u}
      | r = \dfrac {u^2 + 2 r} {2 u}
      | c = algebraic manipulation
}}
{{eqn | o = >
      | r = 0
      | c = as $u > 0$ and $r > 0$
}}
{{eqn | ll= \leadsto
      | l = \dfrac 1 n
      | o = <
      | r = u
      | c = 
}}
{{eqn | ll= \leadsto
      | l = u - \dfrac 1 n
      | o = >
      | r = 0
      | c = 
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \paren {u - \dfrac 1 n}^2
      | r = u^2 - \dfrac {2 u} n + \dfrac 1 {n^2}
      | c = 
}}
{{eqn | o = >
      | r = u^2 - \dfrac {2 u} n
      | c = 
}}
{{eqn | o = >
      | r = u^2 - \paren {u^2 - r}
      | c = as $\dfrac 1 n < \dfrac {u^2 - r} {2 u}$
}}
{{eqn | r = r
      | c = 
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = S
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x^2
      | o = <
      | r = r
      | c = 
}}
{{eqn | o = <
      | r = \paren {u - \dfrac 1 n}^2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = <
      | r = u - \dfrac 1 n
      | c = 
}}
{{end-eqn}}
which contradicts the leastness of $u$.
Suppose instead that $u^2 < r$.
Then $\exists n \in \N$ such that:
:$0 < \dfrac 1 n \le \dfrac {r - u^2} {4 u}$
and:
:$\dfrac 1 n < 2 u$
Then:
{{begin-eqn}}
{{eqn | l = \paren {u + \dfrac 1 n}^2
      | r = u^2 + \dfrac {2 u} n + \dfrac 1 {n^2}
      | c = 
}}
{{eqn | o = <
      | r = u^2 + \dfrac {2 u} n + \dfrac {2 u} n
      | c = as $\dfrac 1 n < 2 u$
}}
{{eqn | o = \le
      | r = u^2 + r - u^2
      | c = as $r - u^2 \ge \dfrac {4 u} n$
}}
{{eqn | r = r
      | c = 
}}
{{end-eqn}}
Hence:
:$u + \dfrac 1 n \in S$
which contradicts the fact that $u$ is an upper bound of $S$.
Hence by Proof by Contradiction it follows that $u^2 = r$.
Hence let:
:$y_1=u$
and:
:$y_2=-u$
{{qed}}
Theorem: Inequality iff Difference is Positive

Let $x, y \in \R$.
{{TFAE}}
{{begin-itemize}}
{{item|(1):|$x < y$}}
{{item|(2):|$y - x > 0$}}
{{end-itemize}}

Proof:
{{begin-eqn}}
{{eqn | l = x < y
      | o = \leadstoandfrom
      | r = y > x
      | c = {{Defof|Dual Ordering}}
}}
{{eqn | o = \leadstoandfrom
      | r = y + \paren {-x} > x + \paren {-x}
      | c = Real Number Ordering is Compatible with Addition
}}
{{eqn | o = \leadstoandfrom
      | r = y + \paren {-x} > 0
      | c = {{Real-number-axiom|A4}}
}}
{{eqn | o = \leadstoandfrom
      | r = y - x > 0
      | c = {{Defof|Field Subtraction}}
}}
{{end-eqn}}
Hence the result.
{{qed}}