avewright/proofwiki-math huggingface dataset:
Theorem: Product 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 $x$.
Then:
:$\paren {r^x}^y = r^{x y}$

Proof:
Let $x = \dfrac p q, y = \dfrac u v$.
Consider $\paren {\paren {r^x}^y}^{q v}$.
Then:
{{begin-eqn}}
{{eqn | l = \paren {\paren {r^x}^y}^{q v}
      | r = \paren {\paren {r^\paren {p / q} }^\paren {u / v} }^{q v}
      | c = 
}}
{{eqn | r = \paren {\paren {\paren {r^\paren {p / q} }^\paren {u / v} }^v}^q
      | c = Product of Indices of Real Number: Integers
}}
{{eqn | r = \paren {\paren {r^\paren {p / q} }^u}^q
      | c = {{Defof|Rational Power}}
}}
{{eqn | r = \paren {r^\paren {p / q} }^{q u}
      | c = Product of Indices of Real Number: Integers
}}
{{eqn | r = \paren {\paren {r^\paren {p / q} }^q}^u
      | c = Product of Indices of Real Number: Integers
}}
{{eqn | r = \paren {r^p}^u
      | c = {{Defof|Rational Power}}
}}
{{eqn | r = r^{p u}
      | c = Product of Indices of Real Number: Integers
}}
{{eqn | ll= \leadsto
      | l = \paren {\paren {r^\paren {p / q} }^\paren {u / v} }
      | r = r^{\paren {p u} / \paren {q v} }
      | c = taking $q v$th root of both sides
}}
{{eqn | ll= \leadsto
      | l = \paren {r^x}^y
      | r = r^{x y}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Indices of Real Number/Integers

Let $n, m \in \Z$ be integers.
Let $r^n$ be defined as $r$ to the power of $n$.
Then:
:$r^{n + m} = r^n \times r^m$

Proof:
From Sum of Indices of Real Number: Positive Integers, we have that:
:$m \in \Z_{\ge 0}: \forall n \in \Z: r^{n + m} = r^n \times r^m$
It remains to be shown that:
:$\forall m \in \Z_{<0}: \forall n \in \Z: r^{n + m} = r^n \times r^m$
The proof will proceed by induction on $m$.
As $m < 0$ we have that $m = -p$ for some $p \in \Z_{> 0}$.
For all $p \in \Z_{>0}$, let $\map P p$ be the proposition:
:$\forall n \in \Z: r^{n + \paren {-p} } = r^n \times r^{-p}$
that is:
:$\forall n \in \Z: r^{n - p} = r^n \times r^{-p}$
Theorem: Product of Indices of Real Number/Integers

Let $n, m \in \Z$ be positive integers.
Let $r^n$ be defined as $r$ to the power of $n$.
Then:
:$\paren {r^n}^m = r^{n m}$

Proof:
From Product of Indices of Real Number: Positive Integers, we have that:
:$m \in \Z_{\ge 0}: \forall n \in \Z: \paren {r^n}^m = r^{n m}$
It remains to be shown that:
:$\forall m \in \Z_{<0}: \forall n \in \Z: \paren {r^n}^m = r^{n m}$
As $m < 0$ we have that $m = -p$ for some $p \in \Z_{> 0}$.
Thus:
{{begin-eqn}}
{{eqn | l = \paren {r^n}^{- p}
      | r = \dfrac 1 {\paren {r^n}^p}
      | c = Real Number to Negative Power: Integer
}}
{{eqn | r = \dfrac 1 {r^{n p} }
      | c = from $(1)$
}}
{{eqn | r = r^{-n p}
      | c = Real Number to Negative Power: Integer
}}
{{end-eqn}}
Hence the result, by replacing $-p$ with $m$.
{{qed}}
Theorem: Uniformly Convergent iff Difference Under Supremum Metric Vanishes

Let $X$ be a set.
Let $\struct {Y, d}$ be a metric space.
Let $S$ be the set of all bounded mappings from $X$ to $Y$.
Let $\sequence {f_n}_{n \mathop \in \N}$ be a sequence in $S$.
Let $f \in S$.
Let $d_S: S \times S \to Y$ denote the supremum metric on $S$.
Then:
:$\sequence {f_n}$ converges uniformly to $f$ on $S$
{{iff}}:
:$\map {d_S} {f_n, f} \to 0$ as $n \to \infty$.

Proof:
{{begin-eqn}}
{{eqn | q = \forall \epsilon \in \R_{>0}: \exists N \in \R_{>0}: \forall n \in \N_{>N}: \forall x \in X
      | l = \map d {\map {f_n} x, \map f x}
      | o = <
      | r = \epsilon
      | c = {{Defof|Uniform Convergence}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall \epsilon \in \R_{>0}: \exists N \in \R_{>0}: \forall n \in \N_{>N}
      | l = \sup_{x \mathop \in X} \map d {\map {f_n} x, \map f x}
      | o = \le
      | r = \epsilon
      | c = {{Defof|Supremum of Set}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall \epsilon \in \R_{>0}: \exists N \in \R_{>0}: \forall n \in \N_{>N}
      | l = \map {d_S} {f_n, f}
      | o = \le
      | r = \epsilon
      | c = {{Defof|Supremum Metric}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \map {d_S} {f_n, f}
      | o = \to
      | r = 0
      | rr= \text{as } n \to \infty
      | c = {{Defof|Limit of Sequence in Metric Space}}
}}
{{end-eqn}}
{{qed}}
Category:Metric Spaces
Category:Uniform Convergence
euflg5p8gcy5qr1npvlm911ty7amykl
Theorem: Uniform Convergence is Hereditary

Let $M = \struct {A, d}$ be a metric space.
Let $\sequence {f_n}$ be a sequence of mappings defined on $A$.
Let $\sequence {f_n}$ be uniformly convergent on $S \subseteq A$.
Then $\sequence {f_n}$ is uniformly convergent on every metric subspace of $S$.
That is, uniform convergence is a hereditary property of a metric space.

Proof:
{{ProofWanted}}
Category:Metric Spaces
3bkrpgwg5yp9kn5et5d2op3zfqsnlf6
Theorem: Real Number to Negative Power/Integer

Let $n \in \Z$ be an integer.
Let $r^n$ be defined as $r$ to the power of $n$.
Then:
:$r^{-n} = \dfrac 1 {r^n}$

Proof:
Let $n \in \Z_{\ge 0}$.
Then from Real Number to Negative Power: Positive Integer:
:$r^{-n} = \dfrac 1 {r^n}$
It remains to show that this holds when $n < 0$.
Let $n \in \Z_{<0}$.
Then $n = - m$ for some $m \in \Z_{> 0}$.
Thus:
{{begin-eqn}}
{{eqn | l = r^{-m}
      | r = \dfrac 1 {r^m}
      | c = Real Number to Negative Power: Positive Integer
}}
{{eqn | ll= \leadsto
      | l = \dfrac 1 {r^{-m} }
      | r = \dfrac 1 {1 / r^m}
      | c = taking reciprocal of both sides
}}
{{eqn | r = r^m
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac 1 {r^n}
      | r = r^{-n}
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Real Number to Negative Power
4zc1zz4qxk30z8m08dkjq464sgh5wcd
Theorem: Real Number to Negative Power/Positive Integer

Let $n \in \Z_{\ge 0}$ be a positive integer.
Let $r^n$ be defined as $r$ to the power of $n$.
Then:
:$r^{-n} = \dfrac 1 {r^n}$

Proof:
Proof by induction on $m$:
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$r^{-n} = \dfrac 1 {r^n}$
$\map P 0$ is the case:
{{begin-eqn}}
{{eqn | l = r^{-0}
      | r = r^0
      | c = 
}}
{{eqn | r = 1
      | c = {{Defof|Integer Power}}
}}
{{eqn | r = \dfrac 1 1
      | c = 
}}
{{eqn | r = \dfrac 1 {r^0}
      | c = {{Defof|Integer Power}}
}}
{{end-eqn}}
Theorem: Way Below iff Second Operand Preceding Supremum of Ideal implies First Operand is Element of Ideal

Let $\mathscr S = \struct {S, \preceq}$ be an up-complete ordered set.
Let $x, y \in S$.
Then $x \ll y$ {{iff}}
:$\forall I \in \map {\operatorname {Ids} } {\mathscr S}: y \preceq \sup I \implies x \in I$
where
:$\ll$ denotes the way below relation,
:$\map {\operatorname {Ids} } {\mathscr S}$ denotes the set of all ideals in $\mathscr S$.

Proof:
=== Sufficient Condition ===
Let $x \ll y$
Let $I \in \map {\operatorname {Ids} } {\mathscr S}$ such that
:$y \preceq \sup I$
By definition of ideal:
:$I$ is directed and lower.
By definition of up-complete:
:$I$ admits a supremum.
By definition of way below relation:
:$\exists i \in I: x \preceq i$
Thus by definition of lower section:
:$x \in I$
{{qed|lemma}}
Theorem: Lower Closure of Directed Subset is Ideal

Let $\mathscr S = \struct {S, \preceq}$ be an ordered set.
Let $D$ be a directed subset of $S$.
Then
:$D^\preceq$ is an ideal in $\mathscr S$
where $D^\preceq$ denotes the lower closure of $D$.

Proof:
By Directed iff Lower Closure Directed:
:$D^\preceq$ is directed.
By Lower Closure is Lower Section:
:$D^\preceq$ is a lower section.
Thus by definition
:$D^\preceq$ is an ideal in $\mathscr S$
{{qed}}
Theorem: Sum from 0 to n-1 of r x^r

:$\ds \sum_{r \mathop = 0}^{n - 1} r x^r = \frac {\paren {n - 1} x^{n + 1} - n x^n + x} {\paren {x - 1}^2}$

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{r \mathop = 0}^{n - 1} r x^{r - 1}
      | r = \sum_{r \mathop = 0}^{n - 1} D_x x^r
      | c = Power Rule for Derivatives
}}
{{eqn | r = D_x \sum_{j \mathop = 0}^{n - 1} x^r
      | c = Sum Rule for Derivatives
}}
{{eqn | r = D_x \frac {x^n - 1} {x - 1}
      | c = Sum of Geometric Sequence
}}
{{eqn | r = \frac {\paren {n x^{n - 1} } \paren {x - 1} - \paren 1 \paren {x^n - 1} } {\paren {x - 1}^2}
      | c = Quotient Rule for Derivatives
}}
{{eqn | r = \frac {\paren {n - 1} x^n - n x^{n - 1} + 1} {\paren {x - 1}^2}
}}
{{eqn | ll= \leadsto
      | l = \sum_{r \mathop = 0}^{n - 1} r x^r
      | r = x \sum_{r \mathop = 0}^{n - 1} r x^{r - 1}
      | c = Distributive Property
}}
{{eqn | r = x \frac {\paren {n - 1} x^n - n x^{n - 1} + 1} {\paren {x - 1}^2}
      | c = by the above result
}}    
{{eqn | r = \frac {\paren {n - 1} x^{n + 1} - n x^n + x} {\paren {x - 1}^2}
}}
{{end-eqn}}
{{qed}}
Category:Examples of Power Series
Category:Sum of Geometric Sequence
e0acch2vbh3wukh6v6zz8era6lztulz
Theorem: Defining Sequence of Natural Logarithm is Strictly Decreasing

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 $\forall x \in \R_{>0}: \sequence {\map {f_n} x}$ is strictly decreasing.

Proof:
Fix $t \in \R_{>0}$.
Then:
{{begin-eqn}}
{{eqn | l = n \paren {t^{n + 1} - 1} - \paren {n + 1} \paren {t^n - 1}
      | r = \paren {t - 1}^2 \paren {1 + 2 t + 3 t^2 + \ldots + n t^{n - 1} }
      | c = Sum from $0$ to $n - 1$ of $r x^r$
}}
{{eqn | o = >
      | r = 0
      | c = Product of Real Numbers is Positive iff Numbers have Same Sign
}}
{{end-eqn}}
Thus:
:$n \paren {t^{n + 1} - 1} > \paren {n + 1} \paren {t^n - 1}$
Fix $x \in \R_{>0}$.
From Power of Positive Real Number is Positive: Rational Number:
:$\forall n \in \N : x^{1 / \paren {n \paren {n + 1} } } \in \R_{>0}$
Thus:
{{begin-eqn}}
{{eqn | q = \forall t \in \R_{>0}
      | l = n \paren {t^{n + 1} - 1}
      | o = >
      | r = \paren {n + 1} \paren {t^n - 1}
      | c = by the result obtained above
}}
{{eqn | ll= \leadsto
      | l = n \paren {\paren {x^{1 / \paren {n \paren {n + 1} } } }^{n + 1} - 1}
      | o = > 
      | r = \paren {n + 1} \paren {\paren {x^{1 / \paren {n \paren {n + 1} } } }^n - 1 }
      | c = as $x^{1 / \paren {n \paren {n + 1} } } \in \R_{>0}$
}}
{{eqn | ll= \leadsto
      | l = n \paren {x^{1 / n} - 1}
      | o = >
      | r = \paren {n + 1} \paren {x^{1 / \paren {n + 1} } - 1}
      | c = Product of Indices of Real Number: Rational Numbers
}}
{{eqn | ll= \leadsto
      | l = n \paren {\sqrt [n] x - 1}
      | o = >
      | r = \paren {n + 1} \paren {\map {f_n} x - 1 }
      | c = {{Defof|Root of Number}}
}}
{{end-eqn}}
Hence the result, by definition of strictly decreasing sequence.
{{qed}}
Category:Natural Logarithms
lnxz35wrk2rz6gwvbgezsgfps42wrhj
Theorem: Logarithm Base 10 of 2 is Irrational

The common logarithm of $2$:
:$\log_{10} 2 \approx 0.30102 \, 99956 \, 63981 \, 19521 \, 37389 \ldots$
is irrational.

Proof:
{{AimForCont}} $\log_{10} 2$ is rational.
Then:
{{begin-eqn}}
{{eqn | l = \log_{10} 2
      | r = \frac p q
      | c = for some $p, q \in \Z_{\ne 0}$
}}
{{eqn | ll= \leadsto
      | l = 2
      | r = 10^{p / q}
      | c = {{Defof|General Logarithm}}
}}
{{eqn | ll= \leadsto
      | l = 2^q
      | r = 10^p
      | c = raising both sides to the power of $q$
}}
{{end-eqn}}
Both $10^p$ and $2^q$ are integers, by construction.
But $10^p$ is divisible by $5$, while $2^p$, which has only $2$ as a prime factor, is not.
So $10^p \ne 2^q$.
So, by Proof by Contradiction, it follows that $\log_{10} 2$ is irrational.
{{qed}}
Theorem: Logarithm Base 10 of 2 is Irrational

The common logarithm of $2$:
:$\log_{10} 2 \approx 0.30102 \, 99956 \, 63981 \, 19521 \, 37389 \ldots$
is irrational.

Proof:
Because $5$ is a divisor of $10$ but not $2$, it cannot be the case that $2^a = 10^b$ for $a, b \in \Z_{>0}$.
Hence this is a special case of Irrationality of Logarithm.
{{qed}}
Theorem: Nth Root of 1 plus x not greater than 1 plus x over n

Let $x \in \R_{>0}$ be a (strictly) positive real number.
Let $n \in \Z_{>0}$ be a (strictly) positive integer.
Then:
:$\sqrt [n] {1 + x} \le 1 + \dfrac x n$

Proof:
From Bernoulli's Inequality:
:$\paren {1 + y}^n \ge 1 + n y$
which holds for:
:$y \in \R$ where $y > -1$
:$n \in \Z_{\ge 0}$
Thus it holds for $y \in \R_{> 0}$ and  $n \in \Z_{> 0}$.
So:
{{begin-eqn}}
{{eqn | l = 1 + n y
      | o = \le
      | r = \paren {1 + y}^n
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 1 + n \frac x n
      | o = \le
      | r = \paren {1 + \frac x n}^n
      | c = substituting $y = \dfrac x n$
}}
{{eqn | ll= \leadsto
      | l = 1 + x
      | o = \le
      | r = \paren {1 + \frac x n}^n
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sqrt [n] {1 + x}
      | o = \le
      | r = 1 + \dfrac x n
      | c = Root is Strictly Increasing
}}
{{end-eqn}}
{{qed}}
Theorem: Reciprocal of Logarithm

Let $x, y \in \R_{> 0}$ be (strictly) positive real numbers.
Then:
:$\dfrac 1 {\log_x y} = \log_y x$

Proof:
From Primitive of $\dfrac {x^m} {\ln x}$:
:$\ds \int \frac {x^m \rd x} {\ln x} = \map \ln {\ln x} + \paren {m + 1} \ln x + \sum_{k \mathop \ge 2}^n \frac {\paren {m + 1}^k \paren {\ln x}^k} {k \times k!} + C$
The result follows by setting $m = 0$.
{{qed}}
Theorem: Reciprocal of Logarithm

Let $x, y \in \R_{> 0}$ be (strictly) positive real numbers.
Then:
:$\dfrac 1 {\log_x y} = \log_y x$

Proof:
{{begin-eqn}}
{{eqn | l = \log_x y \log_y x
      | r = \log_y y
      | c = Change of Base of Logarithm
}}
{{eqn | r = 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \log_y x
      | r = \dfrac 1 {\log_x y}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Discontinuity of Monotonic Function is Jump Discontinuity

Let $X$ be an open set of $\R$.
Let $f: X \to Y$ be a monotone real function.
Then $f$ is discontinuous at a point $c \in X$ {{iff}} $c$ is a jump discontinuity of $f$.

Proof:
The backwards implication follows directly from definition of a jump discontinuity.
{{qed|lemma}}
For the forwards implication, we prove the contrapositive.
{{WLOG}} suppose $f$ is increasing.
If $f$ is decreasing, note that $-f$ is increasing and we can simply replace $f$ by $-f$ in the following analysis.
Suppose that $c \in X$ is not a jump discontinuity of $f$.
By definition of jump discontinuity, it is not the case that:
:$\ds \map f {c^-} = \lim_{x \mathop \to c^-} \map f x$ and $\ds \map f {c^+} = \lim_{x \mathop \to c^+} \map f x$ exist and are not equal.
By definition of an open set:
:there exists $\epsilon \in \R_{>0}$ such that $\openint {c - \epsilon} {c + \epsilon} \subseteq X$.
By Limit of Monotone Real Function/Increasing/Corollary, since $c \in \openint {c - \epsilon} {c + \epsilon}$:
:$\map f {c^-}$ and $\map f {c^+}$ both exist;
:$\map f {c^-} \le \map f c \le \map f {c^+}$
Hence by Modus Ponendo Tollens:
:$\map f {c^-} = \map f {c^+}$
Therefore we have:
:$\map f {c^-} = \map f c = \map f {c^+}$
By Limit iff Limits from Left and Right:
:$\map f x \to \map f c$ as $x \to c$
Hence $f$ is continuous at $c$ by definition.
Thus we have shown the contrapositive of the forwards implication.
{{qed}}
Category:Monotone Real Functions
Category:Real Analysis
Category:Proofs by Contraposition
4atz2rfij7vo24q6znq9q8arjybji9x
Theorem: Surjective Monotone Function is Continuous

Let $X$ be an open set of $\R$.
Let $Y$ be a real interval.
Let $f: X \to Y$ be a surjective monotone real function.
Then $f$ is continuous on $X$.

Proof:
{{Tidy}}
{{MissingLinks}}
{{WLOG}}, let $f$ be increasing.
Let $c \in X$.
From Limit of Monotone Real Function: Corollary, the one sided limits of monotone functions exist:
{{begin-eqn}}
{{eqn | l = L^-_c
      | m = \lim_{x \mathop \to c^-} \map f x
      | mo= =
      | r = \sup_{x \mathop < c} \map f x
}}
{{eqn | l = L^+_c
      | m = \lim_{x \mathop \to c^+} \map f x
      | mo= =
      | r = \inf_{x \mathop > c} \map f x
}}
{{end-eqn}}
and satisfy:
:$L^-_c, L^+_c \in Y$
:$L^-_c \le \map f c \le L^+_c$
Suppose that $\ds L = \lim_{x \mathop \to c} \map f x$ exists.
From Limit iff Limits from Left and Right:
:$L = L^-_c$
This leads to:
:$L \le \map f c$
Similarly:
:$L = L^+_c$
which leads to:
:$L \ge \map f c$
Hence:
:$\ds \lim_{x \mathop \to c} \map f x = \map f c$
proving continuity at $c$.
By assumption, $f$ is increasing.
Suppose $\ds \lim_{x \mathop \to c} \map f x$ does not exist.
Then from Discontinuity of Monotonic Function is Jump Discontinuity, there is a jump discontinuity at $c$.
{{AimForCont}} $f$ has a jump discontinuity at $c$.
From Real Numbers are Densely Ordered:
:$L^-_c < y < L^+_c$
for some $y \in Y$.
By surjectivity, $y = \map f a$ for some $a \in X$.
Hence:
:$L^-_c < \map f a < L^+_c$
If $a < c$ then $\map f a \le L^-_c$.
This contradicts the previous inequality.
There is a similar contradiction if $a \ge c$.
{{finish}}
Category:Monotone Real Functions
Category:Real Analysis
Category:Continuity
o9b9az0kz3zpbakexpdv9nf8g59uy7y
Theorem: Upper Bound of Natural Logarithm/Corollary

:$\forall s \in \R_{>0}: \ln x \le \dfrac {x^s} s$

Proof:
{{begin-eqn}}
{{eqn | l = s \ln x
      | r = \ln {x^s}
      | c = Logarithm of Power
}}
{{eqn | o = \le
      | r = x^s - 1
      | c = Upper Bound of Natural Logarithm
}}
{{eqn | o = \le
      | r = x^s
      | c =
}}
{{end-eqn}}
The result follows by dividing both sides by $s$.
{{qed}}
Theorem: Powers Drown Logarithms/Corollary

:$\ds \lim_{y \mathop \to 0_+} y^r \ln y = 0$

Proof:
Put $y = \dfrac 1 x$ in the Powers Drown Logarithms.
{{qed}}
Theorem: Logarithm of Logarithm in terms of Natural Logarithms

Let $b, x \in \R_{>0}$ be (strictly) positive real numbers.
Then:
:$\map {\log_b} {\log_b x} = \dfrac {\map \ln {\ln x} - \map \ln {\ln b} } {\ln b}$
where $\ln x$ denotes the natural logarithm of $x$.

Proof:
{{begin-eqn}}
{{eqn | l = \map {\log_b} {\log_b x}
      | r = \map {\log_b} {\frac {\ln x} {\ln b} }
      | c = Change of Base of Logarithm
}}
{{eqn | r = \map {\log_b} {\ln x} - \map {\log_b} {\ln b}
      | c = Difference of Logarithms
}}
{{eqn | r = \frac {\map \ln {\ln x} } {\ln b} - \frac {\map \ln {\ln b} } {\ln b}
      | c = Change of Base of Logarithm
}}
{{eqn | r = \frac {\map \ln {\ln x} - \map \ln {\ln b} } {\ln b}
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Limit of Bounded Convergent Sequence is Bounded

Let $\sequence {x_n}$, $\sequence {a_n}$, and $\sequence {b_n}$ be convergent sequences in $\R$.
Let $\sequence {x_n}$, $\sequence {a_n}$, and $\sequence {b_n}$ converge to $x, a, b \in \R$, respectively.
Suppose that:
:$\exists N \in \N: n \ge N \implies a_n \le x_n \le b_n$
Then:
:$a \le x \le b$

Proof:
{{AimForCont}} that $x < a$.
Let $\epsilon = \dfrac {a - x} 2 > 0$
From the convergence of $\sequence {x_n}$:
:$\exists M_1 \in \N : n \ge M \implies x - \epsilon < x_n < x + \epsilon$
Or, equivalently:
:$\exists M_1 \in \N : n \ge M \implies \dfrac {3 x - a} 2 < x_n < \dfrac {x + a} 2$
From the convergence of $\sequence {a_n}$:
:$\exists M_2 \in \N : n \ge M \implies a - \epsilon < a_n < a + \epsilon$
Or, equivalently:
:$\exists M_2 \in \N : n \ge M \implies \dfrac {x + a} 2 < a_n < \dfrac {3 a - x} 2$
Let $M = \max \set {N, M_1, M_2}$
Then, for any $n \ge M$:
{{begin-eqn}}
{{eqn | l = x_n
      | o = <
      | r = \dfrac {x + a} 2
}}
{{eqn | o = <
      | r = a_n
}}
{{end-eqn}}
This contradicts the hypothesis that:
:$\forall n \ge N : a_n \le x_n$
The same argument, mutatis mutandis, brings us to a contradiction if we suppose $x > b$.
Hence the result, by Proof by Contradiction.
{{qed}}
Category:Limits of Sequences
Category:Real Analysis
dcq9lxk7nb6ry21yy1rijkvehze75a9
Theorem: Logarithm of Power/Natural Logarithm/Natural Power

Let $x \in \R$ be a strictly positive real number.
Let $n \in \Z_{\ge 0}$ be any natural number.
Let $\ln x$ be the natural logarithm of $x$.
Then:
:$\map \ln {x^n} = n \ln x$

Proof:
Proof by Mathematical Induction:
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\forall x \in \R_{>0}: \map \ln {x^n} = n \ln x$
Theorem: Logarithm of Power/Natural Logarithm/Integer Power

Let $x \in \R$ be a strictly positive real number.
Let $n \in \R$ be any integer.
Let $\ln x$ be the natural logarithm of $x$.
Then:
:$\map \ln {x^n} = n \ln x$

Proof:
From Logarithm of Power/Natural Logarithm/Natural Power, the theorem is already proven for positive integers.
Let $j \in \Z_{<0}$.
Let $-j = k \in Z_{>0}$.
Then:
{{begin-eqn}}
{{eqn | l = 0
      | r = \ln 1
      | c = Logarithm of 1 is 0
}}
{{eqn | r = \map \ln {x^k x^{-k} }
}}
{{eqn | r = \map \ln {x^k} + \map \ln {x^{-k} }
}}
{{eqn | r = k \ln x + \map \ln {x^{-k} }
      | c = Logarithm of Power/Natural Logarithm/Natural Power
}}
{{eqn | ll= \leadsto
      | l = \map \ln {x^{-k} }
      | r = -k \ln x
}}
{{eqn | ll= \leadsto
      | l = \map \ln {x^j}
      | r = j \ln x
}}
{{end-eqn}}
{{qed}}
Category:Logarithm of Power
4mwud0k8rwsm3ckeg5j0busz5uvra2m
Theorem: Logarithm of Power/Natural Logarithm/Rational Power

Let $x \in \R$ be a strictly positive real number.
Let $r \in \R$ be any rational number.
Let $\ln x$ be the natural logarithm of $x$.
Then:
:$\map \ln {x^r} = r \ln x$

Proof:
Let $r = \dfrac s t$, where $s \in \Z$ and $t \in \Z_{>0}$.
First:
{{begin-eqn}}
{{eqn | l = \map \ln x
      | r = \map \ln {x^{t / t} }
}}
{{eqn | r = \map \ln {\paren {x^{1 / t} }^t}
      | c = Product of Indices of Real Number/Rational Numbers
}}
{{eqn | r = t \map \ln {x^{1 / t} }
      | c = Logarithm of Power/Natural Logarithm/Integer Power
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = \map \ln {x^{1 / t} }
      | r = \frac 1 t \map \ln x
      | c = dividing both sides by $t$
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \map \ln {x^{s / t} }
      | r = \map \ln {\paren {x^{1 / t} }^s}
      | c = Product of Indices of Real Number/Rational Numbers
}}
{{eqn | r = s \map \ln {x^{1 / t} }
      | c = Logarithm of Power/Natural Logarithm/Integer Power
}}
{{eqn | r = \frac s t \map \ln x
      | c = from $(1)$
}}
{{eqn | r = r \map \ln x
      | c = Definition of $s$ and $t$
}}
{{end-eqn}}
{{qed}}
Category:Logarithm of Power
pvsbxnmlvieknx088wn8p6wdffzkxs8
Theorem: Dini's Theorem

Let $K \subseteq \R$ be compact.
Let $\sequence {f_n}$ be a sequence of continuous real functions defined on $K$.
Let $\sequence {f_n}$ converge pointwise to a continuous function $f$.
Suppose that:
:$\forall x \in K : \sequence {\map {f_n} x}$ is monotone.
Then the convergence of $\sequence {f_n}$ to $f$ is uniform.

Proof:
For each $n$, define $d_n : K \to \R$ by:
:$d_n := \size {f_n - f}$
We have:
:$(1): \quad \sequence {d_n}$ converge pointwise to $0$
since $\sequence {f_n}$ converges pointwise to $f$.
We also have:
:$(2): \quad \forall x \in K : \sequence {\map {d_n} x}$ is monotonically decreasing
since $\sequence {\map {f_n} x}$ is monotone.
Let $\epsilon > 0$.
Consider $\sequence {A_n}$ defined by:
:$A_n := \set {x \in K : \map {d_n} x < \epsilon}$
As $d_n$ are continuous, $A_n$ are open sets.
In view of $(1)$, we have:
:$K = \bigcup A_n$
Since $K$ is compact, there exists a finite subcover:
:$K = A_{n_1} \cup \cdots \cup A_{n_m}$
for some $m \in \N_{>0}$.
Let $N := \max \set {n_1, \ldots, n_m}$ be the maximum element among $n_1, \ldots, n_m$.
Then, since $\sequence {A_n}$ is increasing in view of $(2)$, we have:
:$\forall n \ge N : K = A_n$
That is:
:$\forall n \ge N : \forall x \in K :\quad \map {d_n} x = \size{\map {f_n} x - \map f x} < \epsilon$
{{qed}}
{{Namedfor|Ulisse Dini|cat = Dini}}
Category:Real Analysis
mx2zg5y03qqga4xzeahp6w7g84x5v06
Theorem: Way Below in Meet-Continuous Lattice

Let $\mathscr S = \struct {S, \vee, \wedge, \preceq}$ be a meet-continuous bounded below lattice.
Let $x, y \in S$.
Then $x \ll y$ {{iff}}
:$\forall I \in \map {\operatorname {Ids} } {\mathscr S}: y = \sup I \implies x \in I$
where
:$\ll$ denotes the way below relation,
:$\map {\operatorname {Ids} } {\mathscr S}$ denotes the set of all ideals in $\mathscr S$.

Proof:
=== Sufficient Condition ===
Let $x \ll y$
Let $I \in \map {\operatorname {Ids} } {\mathscr S}$ such that
:$y = \sup I$
By definition of reflexivity:
:$y \preceq \sup I$
By definition of meet-continuous:
:$\mathscr S$ is up-complete.
Thus by Way Below iff Second Operand Preceding Supremum of Ideal implies First Operand is Element of Ideal:
:$x \in I$
{{qed|lemma}}