avewright/proofwiki-math huggingface dataset:
Theorem: Parameterization of Unit Circle is Simple Loop

Let $\mathbb S^1$ denote the unit circle whose center is at the origin of the Euclidean space $\R^2$.
Let $p: \closedint 0 1 \to \R^2$ be defined by:
:$\forall t \in \closedint 0 1 : \map p t = \tuple {\map \cos {2 \pi t}, \map \sin {2 \pi t} }$
Then $p$ is a simple loop with image equal to $\mathbb S^1$.

Proof:
Parametric Equation of Circle shows that for all $r \in \R$, the point $\tuple {\map \cos r, \map \sin r}$ lies on the unit circle $\mathbb S^1$.
Parametric Equation of Circle also shows that for all points $\tuple {x, y}$ on the unit circle $\mathbb S^1$, the point can be expressed as $\tuple {x, y} = \tuple {\map \cos r, \map \sin r}$ for some $r \in \R$.
Sine and Cosine are Periodic on Reals shows that sine and cosine functions are periodic functions with period equal to $2 \pi$.
It follows that the image of $p$ is equal to $\mathbb S^1$.
Let $t_1, t_2 \in \closedint 0 1$ such that $\tuple {\map \cos {2 \pi t_1}, \map \sin {2 \pi t_1} } = \tuple {\map \cos {2 \pi t_2}, \map \sin {2 \pi t_2} }$ with $t_1 \ne t_2$.
Shape of Cosine Function shows that the cosine function is strictly decreasing on the interval $\closedint 0 \pi$, and strictly increasing on the interval $\closedint \pi {2 \pi}$.
Strictly Monotone Real Function is Bijective shows that with $t_1 \ne t_2$, we cannot have:
:both $t_1, t_2 \in \closedint 0 {\dfrac 1 2}$, as this would imply $\map \cos {2 \pi t_1} \ne \map \cos {2 \pi t_2}$
:or both $t_1, t_2 \in \closedint {\dfrac 1 2} 1$, as this would imply $\map \cos {2 \pi t_1} \ne \map \cos {2 \pi t_2}$
{{WLOG}}, we have $t_1 \in \closedint 0 {\dfrac 1 2}$, and $t_2 \in \closedint {\dfrac 1 2} 1$.
Sine and Cosine are Periodic on Reals/Corollary shows that the sine function is strictly positive on the interval $\openint 0 \pi$, and strictly negative on the interval $\openint \pi {2 \pi}$.
It follows that we have $\map \sin {2 \pi t_1} \ne \map \sin {2 \pi t_2}$, unless we have $t_1 = 0, t_2 = 1$, in which case:
:$\tuple {\map \cos 0, \map \sin 0} = \tuple {\map \cos {2 \pi}, \map \sin {2 \pi} } = \tuple {1, 0}$
by Cosine of Zero is One and Sine of Zero is Zero.
We have that Real Sine Function is Continuous and Cosine Function is Continuous.
Multiple Rule for Continuous Real Functions and Composite of Continuous Mappings between Metric Spaces is Continuous shows that the two coordinate projections:
:$\map \cos {2 \pi t}, \map \sin {2 \pi t}$
are continuous.
Hence from Continuity of Composite with Inclusion: Inclusion on Mapping and Continuous Mapping to Product Space, it follows that $p$ is continuous.
By definition of simple loop, it follows that $p$ is a simple loop.
{{qed}}
Category:Circles
Category:Loops (Topology)
6m10avntdxobjt0nbvb2t99ydwo9yzu
Theorem: Countably Additive Function Dichotomy by Empty Set

Let $\AA$ be a $\sigma$-algebra.
Let $\overline \R$ denote the extended set of real numbers.
Let $f: \AA \to \overline \R$ be a function be a countably additive function.
Then the exactly one of the following is true:
:$\paren 1$: $\map f \O = 0$
:$\paren 2$: $\map f \O = + \infty$. Moreover, $\map f A = + \infty$ for all $A \in \AA$.
:$\paren 3$: $\map f \O = - \infty$. Moreover, $\map f A = - \infty$ for all $A \in \AA$.

Proof:
Suppose $\map f \O \ne 0$.
Then:
{{begin-eqn}}
{{eqn | l = \map f \O
      | r = \map f {\bigcup_{n \mathop \in \N} \O}
}}
{{eqn | r = \sum_{n \mathop \in \N} \map f \O
      | c = {{Defof|Countably Additive Function}}
}}
{{eqn | o = \in
      | r = \set {+\infty, -\infty}
}}
{{end-eqn}}
{{qed|lemma}}
Furthermore, for each $A \in \AA$ we have:
{{begin-eqn}}
{{eqn | l = \map f A
      | r = \map f {A \cup \bigcup_{\N_{>0} }\O}
}}
{{eqn | r = \map f A + \sum_{n \mathop \in \N_{>0} } \map f \O
      | c = {{Defof|Countably Additive Function}}
}}
{{eqn | r = \begin {cases}
+\infty & : \map f \O = +\infty \\
-\infty & : \map f \O = -\infty \end {cases}
}}
{{end-eqn}}
{{qed}}
Category:Countably Additive Functions
Category:Empty Set
9m62e0nt0bsb6t8xs6m4s0sqw94qgg2
Theorem: Simple Loop Image Equals Set Homeomorphic to Circle

Let $\struct { X, \tau_X }$ be a Hausdorff space.
Let $C \subseteq X$ be a subset of $X$.
Let $\tau_C$ be the subspace topology on $C$ induced by $\tau_X$.
Let $\mathbb S^1$ denote the unit circle whose center is at the origin of the Euclidean space $\R^2$.
Let $\tau_{\mathbb S^1}$ be the subspace topology on $\mathbb S^1$ induced by the Euclidean topology on $\R^2$.
Then $\struct{ C, \tau_C }$ is homeomorphic to $\struct { \mathbb S^1 , \tau_{\mathbb S^1} }$, {{iff}} there exists a simple loop $\gamma : \closedint 0 1 \to X$ with image equal to $C$.

Proof:
=== Sufficient condition ===
Let $\sim$ be the equivalence relation on the closed real interval $\closedint 0 1$ defined by:
{{begin-eqn}}
{{eqn | q = \forall t_1 \in \openint 0 1, t_2 \in \closedint 0 1
      | l = t_1 \sim t_2
      | o = \iff
      | r = t_2 = t_1
}}
{{eqn | q = \forall t_1 \in \set {0, 1}, t_2 \in \closedint 0 1
      | l = t_1 \sim t_2
      | o = \iff
      | r = t_2 \in \set {0, 1}
}}
{{end-eqn}}
Let $q : \closedint 0 1 \to \closedint 0 1 / \sim$ be the canonical surjection induced by $\sim$.
Let $\tau_q$ be the quotient topology on the quotient space $\closedint 0 1 / \sim$ induced by $q$.
By definition of quotient topology, $\tau_q$ is the identification topology on $\closedint 0 1 / \sim$ by the identification mapping $q$.
Identification Mapping is Continuous shows that $q$ is continuous.
Parameterization of Unit Circle is Simple Loop shows that there exists a simple loop in $\R^2$ with image equal to $\mathbb S^1$.
Euclidean Space is Complete Metric Space and Metric Space is Hausdorff shows that $\R^2$ is a Hausdorff space.
Simple Loop in Hausdorff Space is Homeomorphic to Quotient Space of Interval shows that there exists a homeomorphism $f: \closedint 0 1 / \sim \to \mathbb S^1$.
By assumption, there exists a homeomorphism $h: \mathbb S^1 \to C$.
Composite of Continuous Mappings is Continuous shows that the mapping:
:$h \circ f \circ q : \closedint 0 1 \to C$
is continuous.
By definition of homeomorphism, $h$ and $f$ are bijections.
Quotient Mapping is Surjection shows that $q$ is a surjective mapping.
Composite of Surjections is Surjection shows that $h \circ f \circ q$ is a surjective mapping, so $\Img {h \circ f \circ q} = C$.
By definition of $\sim$, we see that:
:$\map q {t_1} \ne \map q {t_2}$ for all $t_1 ,t_2 \in \hointr 0 1$ with $t_1 \ne t_2$
:$\map q 0 = \map q 1$
It follows that $h \circ f \circ q$ is a simple loop, as:
:$\map {h \circ f \circ q }{t_1} \ne \map {h \circ f \circ q}{t_2}$ for all $t_1 ,t_2 \in \hointr 0 1$ with $t_1 \ne t_2$
:$\map {h \circ f \circ q} 0 = \map {h \circ f \circ q} 1$
Define $\gamma : \closedint 0 1 \to X$ by $\map \gamma t = \map {h \circ f \circ q} t$.
Continuity of Composite with Inclusion/Inclusion on Mapping shows that $\gamma$ is continuous.
It follows that $\gamma$ is a simple loop.
{{qed|lemma}}
Theorem: GCD of Sum and Difference of Coprime Integers

Let $a, b \in \Z$ be coprime integers.
Then:
:$\gcd \set {a + b, a - b} = 1 \text { or } 2$
where:
:$\gcd$ denotes greatest common divisor.

Proof:
Let:
:$d = \gcd \set {a + b, a - b}$
We have:
{{begin-eqn}}
{{eqn | l = \gcd \set {a + b, a - b}
      | r = \gcd \set {a + b, a + b - 2 b}
      | c = 
}}
{{eqn | o = \divides
      | r = 2 b
      | c = GCD of Integer with Integer + n
}}
{{eqn | l = \gcd \set {a + b, a - b}
      | r = \gcd \set {-\paren {a + b}, a - b}
      | c = GCD for Negative Integers
}}
{{eqn | r = \gcd \set {-a - b, a - b}
      | c = 
}}
{{eqn | r = \gcd \set {-a - b, a - b - 2 a}
      | c = 
}}
{{eqn | o = \divides
      | r = 2 a
      | c = GCD of Integer with Integer + n
}}
{{eqn | ll= \leadsto
      | l = d
      | r = \gcd \set {2 a, 2 b}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = d
      | o = \le
      | r = \gcd \set {2 a, 2 b}
      | c = 
}}
{{eqn | r = 2 \gcd \set {a, b}
      | c = GCD of Integers with Common Divisor
}}
{{end-eqn}}
Hence:
:$1 \le d \le 2$
and the result follows.
{{qed}}
Theorem: Jordan Curve Image Equals Set Homeomorphic to Circle

Let $C \subseteq \R^2$ be a subset of the Euclidean space $\R^2$.
Let $\mathbb S^1$ denote the unit circle whose center is at the origin of the Euclidean space $\R^2$.
Let $\tau_C$ and $\tau_{\mathbb S^1}$ be the subspace topologies on $C$ respectively $\mathbb S^1$ induced by the Euclidean topology on $\R^2$.
Then $\struct{ C, \tau_C }$ is homeomorphic to $\struct { \mathbb S^1 , \tau_{\mathbb S^1} }$, {{iff}} there exists a Jordan curve $\gamma : \closedint 0 1 \to \R^2$ with image equal to $C$.

Proof:
By definition of simple loop, a Jordan curve is a simple loop in $\R^2$.
Euclidean Space is Complete Metric Space and Metric Space is Hausdorff shows that $\R^2$ is a Hausdorff space.
The result now follows from Simple Loop Image Equals Set Homeomorphic to Circle.
{{qed}}
Category:Circles
Category:Examples of Homeomorphisms
Category:Jordan Curves
g83gude9z5ct4xhm1zv6fayohlcj56w
Theorem: Canonical P-adic Expansion of Rational is Eventually Periodic/Lemma 11

:$\forall n \in \N : \dfrac {a - \paren {p^{n + 1} - 1} b } {p^{n + 1} } \le r_n \le \dfrac a {p^{n + 1} }$

Proof:
We have:
{{begin-eqn}}
{{eqn | l = 0
      | o = \le
      | m = \dfrac a b - \paren{p^{n + 1} \dfrac {r_n} b}
      | mo= \le
      | r = p^{n + 1} - 1
}}
{{eqn | ll= \leadsto
      | l = -\paren {p^{n + 1} - 1}
      | o = \le
      | m = \paren{p^{n + 1} \dfrac {r_n} b} - \dfrac a b
      | mo= \le
      | r = 0
}}
{{eqn | ll= \leadsto
      | l = -\paren {p^{n + 1} - 1} b
      | o = \le
      | m = p^{n + 1} r_n - a
      | mo= \le
      | r = 0
}}
{{eqn | ll= \leadsto
      | l = a - \paren {p^{n + 1} - 1} b
      | o = \le
      | m = p^{n + 1} r_n
      | mo= \le
      | r = a
}}
{{eqn | ll= \leadsto
      | l = \dfrac {a - \paren {p^{n + 1} - 1} b} {p^{n + 1} }
      | o = \le
      | m = r_n
      | mo= \le
      | r = \dfrac a {p^{n + 1} }
}}
{{end-eqn}}
The result follows.
{{qed}}
Category:Canonical P-adic Expansion of Rational is Eventually Periodic
9lx3dpb5j3nr6xynpfq93pr0jamlrv7
Theorem: Jordan-Schönflies Theorem

Let $\gamma : \closedint 0 1 \to \R^2$ be a Jordan curve.
Let $\Img \gamma$ denote the image of $\gamma$, $\Int \gamma$ denote the interior of $\gamma$, and $\Ext \gamma$ denote the exterior of $\gamma$.
Let $\mathbb S^1$ denote the unit circle whose center is at the origin $\mathbf 0$ of the Euclidean space $\R^2$..
Let $\map {B_1} { \mathbf 0 }$ denote the open ball in $\R^2$ with radius $1$ and center $\mathbf 0$, and let $\map {B_1^-} { \mathbf 0 }$ denote the closed ball in $\R^2$ with radius $1$ and center $\mathbf 0$.
Then there exists a homeomorphism $\phi : \R^2 \to \R^2$ such that:
:The restriction of $\phi$ to $\Img \gamma \times \mathbb S^1$ is a homeomorphism between $\Img \gamma$ and $\mathbb S^1$.
:The restriction of $\phi$ to $\Int \gamma \times \map {B_1} { \mathbf 0 }$ is a homeomorphism between $\Int \gamma$ and $\map {B_1} { \mathbf 0 }$.
:The restriction of $\phi$ to $\Ext \gamma \times \R^2 \setminus \map {B_1^-} { \mathbf 0 }$ is a homeomorphism between $\Ext \gamma$ and $\R^2 \setminus \map {B_1^-} { \mathbf 0 }$.

Proof:
{{proof wanted}}
{{Namedfor|Marie Ennemond Camille Jordan|name2 = Arthur Moritz Schönflies|cat = Jordan, C|cat2 = Schönflies}}
Theorem: Zeroes of Sine and Cosine/Cosine

:$\cos x = 0$ {{iff}} $x = \paren {n + \dfrac 1 2} \pi$ for some $n \in \Z$.

Proof:
From Sine and Cosine are Periodic on Reals: Corollary:
$\cos x$ is:
:strictly positive on the interval $\openint {-\dfrac \pi 2} {\dfrac \pi 2}$
and:
:strictly negative on the interval $\openint {\dfrac \pi 2} {\dfrac {3 \pi} 2}$
The result follows directly from Sine and Cosine are Periodic on Reals.
{{qed}}
Category:Zeroes of Sine and Cosine
68xzyvu7ad2q7hw9dze3k4kpg6v9m24
Theorem: Zeroes of Sine and Cosine/Sine

:$\sin x = 0$, {{iff}} $x = n \pi$ for some $n \in \Z$.

Proof:
From Sine and Cosine are Periodic on Reals: Corollary:
$\sin x$ is:
:strictly positive on the interval $\openint 0 \pi$
and:
:strictly negative on the interval $\openint \pi {2 \pi}$
The result follows directly from Sine and Cosine are Periodic on Reals.
{{qed}}
Category:Zeroes of Sine and Cosine
1zgall37peqab11t4tjgjdejbh7ajh0
Theorem: Sine and Cosine are Periodic on Reals/Pi

The real number $\pi$ (called '''pi''', pronounced '''pie''') is uniquely defined as:
:$\pi := \dfrac p 2$
where $p \in \R$ is the period of $\sin$ and $\cos$.

Proof:
From the Real Cosine Function is Periodic and Real Sine Function is Periodic, we have that $\cos x$ and $\sin x$ are periodic on $\R$ with the same period.
If we denote the period of $\cos x$ and $\sin x$ as $p$, it follows that $\pi = \dfrac p 2$ is uniquely defined.
{{qed}}
Theorem: Sine and Cosine are Periodic on Reals/Pi

The real number $\pi$ (called '''pi''', pronounced '''pie''') is uniquely defined as:
:$\pi := \dfrac p 2$
where $p \in \R$ is the period of $\sin$ and $\cos$.

Proof:
By Cosine of Zero is One:
:$\cos 0 = 1$
By Cosine of 2 is Strictly Negative:
:$\cos 2 < 0$
Thus by {{Corollary|Intermediate Value Theorem}} there exists an $h \in \openint 0 2$ such that:
:$\cos h = 0$
By Sine of Sum for all $x \in \R$:
{{begin-eqn}}
{{eqn | l = \sin x
      | r = \map \sin {x - h} \cos h + \map \cos {x -h} \sin h
}}
{{eqn | n = 1
      | r = \map \cos {x -h} \sin h
}}
{{end-eqn}}
By Cosine of Sum for all $x \in \R$:
{{begin-eqn}}
{{eqn | l = \cos x
      | r = \map \cos {x - h} \cos h - \map \sin {x -h} \sin h
}}
{{eqn | n = 2
      | r = -\map \sin {x - h} \sin h
}}
{{end-eqn}}
By Sum of Squares of Sine and Cosine:
{{begin-eqn}}
{{eqn | l = \sin^2 h
      | r = \cos^2 h + \sin^2 h
}}
{{eqn | n = 3
      | r = 1
}}
{{end-eqn}}
Thus for all $x \in \R$:
{{begin-eqn}}
{{eqn | l = \map \cos {x + 4 h}
      | r = - \map \sin {x + 3 h} \sin h
      | c = by $(2)$
}}
{{eqn | r = - \map \cos {x + 2 h} \sin^2 h
      | c = by $(1)$
}}
{{eqn | r = \map \cos {x + h} \sin^3 h
      | c = by $(2)$
}}
{{eqn | r = \cos x \sin^4 h
      | c = by $(1)$
}}
{{eqn | r = \cos x
      | c = by $(3)$
}}
{{end-eqn}}
In particular, $\cos$ is periodic.
By Nonconstant Periodic Function with no Period is Discontinuous Everywhere, $\cos$ has a period $p \in \R_{>0}$.
In view of $(1)$ and $\sin h \ne 0$, the periodic elements of $\sin$ are exactly those of $\cos$.
Thus $p$ is also the period of $\sin$.
{{qed}}
Theorem: Sine and Cosine are Periodic on Reals/Sine

The real sine function is periodic
with the same period as the real cosine function.

Proof:
Since Real Cosine Function is Periodic, let $K$ be its period.
Then:
:$\cos K = \map \cos {0 + K} = \cos 0$
Because Cosine of Zero is One:
:$\cos K = 1$
Furthermore:
{{begin-eqn}}
{{eqn | l = \cos^2 K + \sin^2 K
      | r = 1
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | l = \sin^2 K
      | r = 0
      | c = $\cos K = 1$
}}
{{eqn | l = \sin K
      | r = 0
}}
{{end-eqn}}
Then, the following holds:
{{begin-eqn}}
{{eqn | l = \map \sin {x + K}
      | r = \sin x \cos K + \cos x \sin K
      | c = Sine of Sum
}}
{{eqn | r = \sin x \cdot 1 + \cos x \cdot 0
      | c = $\cos K = 1$; $\sin K = 0$
}}
{{eqn | r = \sin x}}
{{end-eqn}}
Thus $\sin$ is periodic with some period $L \leq K$.
{{qed|lemma}}
The following also hold:
{{begin-eqn}}
{{eqn | l = \sin L
      | r = \map \sin {0 + L}
}}
{{eqn | r = \sin 0
      | c = Period of Periodic Real Function
}}
{{eqn | r = 0
      | c = Sine of Zero is Zero
}}
{{eqn | l = \cos L
      | r = \bigvalueat { \dfrac{\d \sin x} {\d x} } {x \mathop = L}
      | c = Derivative of Sine Function
}}
{{eqn | r = \lim_{h \mathop \to 0} \dfrac{\map \sin {L + h} - \map \sin L}{h}
      | c = Derivative of Real Function at Point
}}
{{eqn | r = \lim_{h \mathop \to 0} \dfrac{\map \sin {0 + h} - \map \sin 0}{h}
      | c = Period of Periodic Real Function
}}
{{eqn | r = \bigvalueat { \dfrac{\d \sin x} {\d x} } {x \mathop = 0}
      | c = Derivative of Real Function at Point
}}
{{eqn | r = \cos 0
      | c = Derivative of Sine Function
}}
{{eqn | r = 1
      | c = Cosine of Zero is One
}}
{{end-eqn}}
So we may conclude:
{{begin-eqn}}
{{eqn | l = \map \cos {x + L}
      | r = \cos x \cos L - \sin x \sin L
      | c = Cosine of Sum
}}
{{eqn | r = \cos x \cdot 1 - \sin x \cdot 0
      | c = $\cos L = 1$ and $\sin L = 0$
}}
{{eqn | r = \cos x}}
{{end-eqn}}
Therefore the period of cosine is at most that of sine:
:$K \leq L$
But if $K \leq L \leq K$ then:
:$K = L$
{{qed}}
Theorem: Sine and Cosine are Periodic on Reals/Sine

The real sine function is periodic
with the same period as the real cosine function.

Proof:
Since Real Cosine Function is Periodic, let $L$ be its period.
From Primitive of Cosine Function:
{{:Primitive of Cosine Function}}
for any constant $C$.
Therefore $\sin x$ is a Primitive of $\cos x$, for the special case of $C = 0$.
From Primitive of Periodic Real Function, it follows that $\sin x$ is periodic with period $L$.
{{qed}}
Theorem: Sine and Cosine are Periodic on Reals/Cosine

:$\exists L \in \R_{\neq 0}: \forall x \in \R: \cos x = \map \cos {x + L}$

Proof:
From Real Cosine Function has Zeroes, the cosine function has at least one positive zero.
Therefore there exists a Greatest Lower Bound $\eta \in \R_{>0}$ to the set of positive zeroes.
Since Cosine Function is Continuous, $\eta$ is a zero.
Because Cosine Function is Even:
:$\cos \eta = \map \cos {-\eta} = 0$
By definition of greatest lower bound:
:$\cos x \neq 0$ for $-\eta < x < \eta$
Because Cosine of Zero is One, it follows from the Intermediate Value Theorem that:
:$\cos x > 0$ for $-\eta < x < \eta$
From Sum of Squares of Sine and Cosine:
:$\cos^2 x + \sin^2 x = 1$
Hence as $\cos \eta = 0$ it follows that:
:$\sin^2 \eta = 1$
So either $\sin \eta = 1$ or $\sin \eta = -1$.
But from Derivative of Sine Function:
:$\map {\dfrac \d {\d x} } {\sin x} = \cos x$
On the interval $\openint {-\eta} \eta$, it has been shown that $\cos x > 0$.
Thus by Derivative of Monotone Function, $\sin x$ is increasing on $\closedint {-\eta} \eta$.
Since Sine of Zero is Zero it follows that:
:$\sin \eta > 0$
So it must be the case that:
:$\sin \eta = 1$
Now we apply Sine of Sum and Cosine of Sum:
{{begin-eqn}}
{{eqn | l = \map \sin {x + \eta}
      | r = \sin x \cos \eta + \cos x \sin \eta
      | c = Sine of Sum
}}
{{eqn | r = \cos x
      | c = 
}}
{{eqn | l = \map \cos {x + \eta}
      | r = \cos x \cos \eta - \sin x \sin \eta
      | c = 
}}
{{eqn | r = -\sin x
      | c = Cosine of Sum
}}
{{end-eqn}}
Hence it follows that:
{{begin-eqn}}
{{eqn | l = \map \cos {x + 4 \eta}
      | r = -\map \sin {x + 3 \eta}
      | c = 
}}
{{eqn | r = -\map \cos {x + 2 \eta}
      | c = 
}}
{{eqn | r = \map \sin {x + \eta}
      | c = 
}}
{{eqn | r = \cos x
      | c = 
}}
{{end-eqn}}
Thus $\cos$ is periodic on $\R$ with a period $L \leq 4 \eta$.
{{qed}}
Theorem: P-Sequence Space admits Schauder Basis

Let $1 \le p < \infty$.
Let $\ell^p$ be the $p$-sequence space.
Let $\sequence {\mathbf e_n}_{n \mathop \in \N } \in \ell^p$ be a sequence such that:
:$\mathbf e_n = \tuple {\underbrace{0, \ldots, 0}_n, 1, 0, \ldots}$
Then $\set {\mathbf e_n : n \in \N}$ is a Schauder basis for $\ell^p$.

Proof:
Let $\mathbf x = \sequence {x_n}_{n \mathop \in \N} = \tuple {x_1, x_2, x_3, \ldots} \in \ell^p$.
Theorem: Vector Addition on Normed Vector Space is Continuous

Let $\struct {X, \norm {\, \cdot \,}_X }$ be a normed vector space.
Let $\struct {X \times X, \norm {\, \cdot \,}_P }$ be the direct product of $X$ and $X$ with the direct product norm $\norm {\, \cdot \,}_P$. 
Let $+_{\scriptscriptstyle X} : X \times X \to X$ be the vector addition defined on $X$.
Then $+_{\scriptscriptstyle X} : X \times X \to X$ is a continuous mapping.

Proof:
Let $x_0, y_0 \in X$.
Let $\epsilon \in \R_{>0}$.
For $a, b \in X$, let $a-_{\scriptscriptstyle X} b$ denote the sum $a +_{\scriptscriptstyle X} \paren { -b }$, where $-b$ is the inverse vector of $b$ in $X$.
To show that $+_{\scriptscriptstyle X}$ is continuous, let $x, y \in X$ such that $\norm { x_0 -_{\scriptscriptstyle X} x}_X < \dfrac \epsilon 2$, and $\norm {y_0 -_{\scriptscriptstyle X} y }_X < \dfrac \epsilon 2$.
By definition of direct product norm, it follows that:
:$\norm { \tuple {x_0,y_0} -_{\scriptscriptstyle {X \times X} } \tuple {x,y} }_P = \map \max {\norm {x_0 -_{\scriptscriptstyle X} x}_X, \norm {y_0 -_{\scriptscriptstyle X} y}_X } < \dfrac \epsilon 2$
To show that $+_{\scriptscriptstyle X}$ is continuous at $\tuple {x_0, y_0}$, we calculate:
{{begin-eqn}}
{{eqn | l = \norm {\paren {x_0 +_{\scriptscriptstyle X} y_0} -_{\scriptscriptstyle X} \paren { x +_{\scriptscriptstyle X} y} }_X
      | r = \norm {\paren {x_0 +_{\scriptscriptstyle X} y_0} -_{\scriptscriptstyle X} x -_{\scriptscriptstyle X} y}_X
      | c = 
}}
{{eqn | r = \norm {x_0 -_{\scriptscriptstyle X} x +_{\scriptscriptstyle X} y_0 -_{\scriptscriptstyle X} y}_X
      | c = {{Abelian-group-axiom|C||underlying}} and {{Abelian-group-axiom|1||underlying}}
}}
{{eqn | o = \le
      | r = \norm {x_0 -_{\scriptscriptstyle X} x}_X + \norm {y_0 -_{\scriptscriptstyle X} y}_X
      | c = {{NormAxiomVector|3}}
}}
{{eqn | o = <
      | r = \dfrac \epsilon 2 + \dfrac \epsilon 2
      | c = {{hypothesis}}
}}
{{eqn | r = \epsilon
}}
{{end-eqn}}
It follows that $+_{\scriptscriptstyle X}$ is continuous from $X \times X$ to $X$.
{{qed}}
Theorem: Abel's Summation Formula

Let $\sequence {a_n}_{n \in \N_{>0} }$ be a sequence in $\R$.
Let $f : \R_{\ge 1} \to \R$ be a continuously differentiable function.
Let $A : \R_{\ge 1} \to \R$ be defined as:
:$\ds \map A x := \sum_{1 \mathop \le n \mathop \le x} a_n$
Then for all $x \in \R_{\ge 1}$:
:$\ds \sum_{1 \mathop \le n \mathop \le x} a_n \map f n = \map A x \map f x - \int _1 ^x \map A u \map {f'} u \rd u$

Proof:
{{ProofWanted}}
{{Namedfor|Niels Henrik Abel|cat = Abel}}
Category:Integral Calculus
Category:Analytic Number Theory
s5ovd2lpotvbn0usbfr1opzq5rli6m8
Theorem: Babbage's Congruence

Let $p$ be a prime number.
Let $a, b \in \Z$ be integers.
Then:
:$\dbinom {a p} {b p} \equiv \dbinom a b \pmod {p^2}$
where $\dbinom a b$ denotes a binomial coefficient.

Proof:
By Lucas' Theorem, for $a, b \in \mathbb Z_{\ge 0}$:
:$\dbinom {a p} {b p} \equiv \dbinom {\floor {a p / p}} {\floor {b p / p}} \dbinom {a \mod p} {b \mod p} \pmod p$
Proof by Mathematical Induction on $a$:
For all $a \in \Z$, let $\map P a$ be the proposition:
:$\forall b \in \Z: \dbinom {a p} {b p} \equiv \dbinom a b \pmod {p^2}$
Theorem: Divisibility of Numerator of Sum of Sequence of Reciprocals

Let $p$ be a prime number such that $p > 3$.
Consider the sum of the finite sequence of reciprocals as follows:
:$S = 1 + \dfrac 1 2 + \dfrac 1 3 + \cdots + \dfrac 1 {p - 1}$
Let $S$ be expressed as a fraction in canonical form, that is:
:$S = \dfrac a b$
where $a$ and $b$ are coprime.
Then:
:$p^2 \divides a$
where $\divides$ denotes divisibility.

Proof:
=== Lemma ===
{{:Divisibility of Numerator of Sum of Sequence of Reciprocals/Lemma}}
{{ProofWanted}}
Theorem: Integral Expression of Harmonic Number

Let $\sequence {H_n}_{n \mathop \in \N}$ be the harmonic numbers.
Then:
:$\ds H_n = 1 + \int_1 ^n \dfrac {\floor u} {u^2} \rd u$
where $\floor u$ denotes the floor of $u$.

Proof:
Observe that:
:$\ds \forall x \in \R_{\ge 1} : \floor x = \sum_{1 \mathop \le k \mathop \le x} 1$
Let $f: \R_{\ge 1} \to \R$ be defined as:
:$\ds \map f x := \dfrac 1 x$
Then:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 1}^n \frac 1 k
      | r = \sum_{k \mathop = 1}^n 1 \cdot \map f k
}}
{{eqn | r = \floor n \map f n - \int_1^n \floor u \map {f'} u \rd u
      | c = Abel's Summation Formula
}}
{{eqn | r = 1 + \int_1 ^n \dfrac {\floor u} {u^2} \rd u
      | c = Derivative of Reciprocal
}}
{{end-eqn}}
{{qed}}
Category:Harmonic Numbers
Category:Analytic Number Theory
2rsaz6m46stbnb3c8u4wgjscqm3bl39