avewright/proofwiki-math huggingface dataset:
Theorem: Cycle of Subsets implies Set Equality

Let $A_1, A_2, \dotsc, A_n$ be sets.
Let:
:$\forall k \in \set {2, 3, \dotsc, n}: A_{k - 1} \subseteq A_k$
and:
:$A_n \subseteq A_1$
Then:
:$\forall j, k \in \set {1, 2, \dotsc, n}: A_j = A_k$

Proof:
Consider the set of sets $\mathbb A = \set {A_1, A_2, \dotsc, A_n}$
Consider the relational structure $S = \struct {\mathbb A, \subseteq}$.
We have from Subset Relation is Ordering that $S$ is an ordered structure.
The result follows from Ordering Cycle implies Equality.
{{qed}}
Theorem: Integral Representation of Dirichlet Beta Function in terms of Gamma Function

:$\ds \map \beta s = \frac 1 {\map \Gamma s} \int_0^\infty \frac {x^{s - 1} e^{-x} } {1 + e^{-2 x} } \rd x$

Proof:
We have, by Laplace Transform of Power: 
:$\ds \frac {\paren {-1}^n \map \Gamma s} {\paren {2 n + 1}^s} = \paren {-1}^n \int_0^\infty x^{s - 1} e^{-\paren {2 n + 1} x} \rd x$
for $\map \Re s > 0$.
Summing, we have:  
{{begin-eqn}}
{{eqn	| l = \map \Gamma s \sum_{n \mathop = 0}^N \frac {\paren {-1}^n} {\paren {2 n + 1}^s}
	| r = \sum_{n \mathop = 0}^N \paren {-1}^n \int_0^\infty x^{s - 1} e^{-\paren {2 n + 1} x} \rd x
}}
{{eqn	| r = \int_0^\infty x^{s - 1} \sum_{n \mathop = 0}^N \paren {-1}^n e^{-\paren {2 n + 1} x} \rd x
	| c = Linear Combination of Definite Integrals
}}
{{eqn	| r = \int_0^\infty x^{s - 1} e^{-x} \paren {\sum_{n \mathop = 0}^N \paren {-e^{-2 x} }^n} \rd x
}}
{{end-eqn}}
We have: 
{{begin-eqn}}
{{eqn	| l = \lim_{N \mathop \to \infty} \paren {\map \Gamma s \sum_{n \mathop = 0}^N \frac {\paren {-1}^n} {\paren {2 n + 1}^s} }
	| r = \map \Gamma s \lim_{N \mathop \to \infty} \paren {\sum_{n \mathop = 0}^N \frac {\paren {-1}^n} {\paren {2 n + 1}^s} }
	| c = Multiple Rule for Limits of Complex Functions
}}
{{eqn	| r = \map \Gamma s \map \beta s
	| c = {{Defof|Dirichlet Beta Function}}
}}
{{end-eqn}}
Therefore: 
{{begin-eqn}}
{{eqn	| l = \map \Gamma s \map \beta s
	| r = \lim_{N \mathop \to \infty} \paren {\int_0^\infty x^{s - 1} e^{-x} \paren {\sum_{n \mathop = 0}^N \paren {-e^{-2 x} }^n} \rd x}
}}
{{eqn	| r = \int_0^\infty x^{s - 1} e^{-x} \paren {\lim_{N \mathop \to \infty} \sum_{n \mathop = 0}^N \paren {-e^{-2 x} }^n} \rd x
	| c = Lebesgue's Dominated Convergence Theorem
}}
{{eqn	| r = \int_0^\infty x^{s - 1} e^{-x} \paren {\sum_{n \mathop = 0}^\infty \paren {-e^{-2 x} }^n} \rd x
}}
{{eqn	| r = \int_0^\infty \frac {x^{s - 1} e^{-x} } {1 - \paren {-e^{- 2x} } } \rd x
	| c = Sum of Infinite Geometric Sequence
}}
{{eqn	| r = \int_0^\infty \frac {x^{s - 1} e^{-x} } {1 + e^{-2 x} } \rd x
}}
{{end-eqn}}
giving: 
:$\ds \map \beta s = \frac 1 {\map \Gamma s} \int_0^\infty \frac {x^{s - 1} e^{-x} } {1 + e^{-2 x} } \rd x$
{{qed}}
Category:Dirichlet Beta Function
Category:Gamma Function
an75w008p0871z6wpjqzrbqqkoxyd4t
Theorem: Dirichlet Beta Function at Odd Positive Integers

{{begin-eqn}}
{{eqn | l = \map \beta {2 n + 1}
      | r = \sum_{k \mathop = 0}^\infty \frac {\paren {-1}^k} {\paren {2 k + 1}^{2 n + 1} }
      | c = 
}}
{{eqn | r = \frac 1 {1^{2 n + 1} } - \frac 1 {3^{2 n + 1} } + \frac 1 {5^{2 n + 1} } - \frac 1 {7^{2 n + 1} } + \cdots
      | c =
}}
{{eqn | r = \paren {-1}^n \dfrac {E_{2 n} \pi^{2 n + 1} } {4^{n + 1} \paren {2 n}!}
      | c =
}}
{{end-eqn}}
where:
:$\beta$ denotes the Dirichlet beta function
:$E_n$ denotes the $n$th Euler number
:$n$ is a non-negative integer.

Proof:
{{begin-eqn}}
{{eqn | l = \map \beta {2 n + 1}
      | r = \dfrac 1 {4^{2 n + 1} } \paren {\map \zeta {2 n + 1, \frac 1 4} - \map \zeta {2 n + 1, \frac 3 4} }
      | c = Dirichlet Beta Function in terms of Hurwitz Zeta Function
}}
{{eqn | r = \dfrac 1 {4^{2 n + 1} } \paren { \dfrac {\map {\psi_{2 n} } {\dfrac 1 4} - \map {\psi_{2 n} } {\dfrac 3 4} } {\paren {-1}^{2 n + 1} \map \Gamma {2 n + 1} } }
      | c = Polygamma Function in terms of Hurwitz Zeta Function
}}
{{eqn | r = -\dfrac 1 {4^{2 n + 1} \paren {2 n}!} \paren {\map {\psi_{2 n} } {\dfrac 1 4} - \map {\psi_{2 n} } {\dfrac 3 4} }
      | c =
}}
{{eqn | r = - \dfrac 1 {4^{2 n + 1} \paren {2 n}!} \paren {-\pi \valueat {\frac {\d^{2 n} } {\d z^{2 n} } \cot \pi z} {z \mathop = \frac 1 4} }
      | c = Polygamma Reflection Formula for $z = \dfrac 1 4$
}}
{{eqn | r = \dfrac \pi {4^{2 n + 1} \paren {2 n}!} \valueat {\dfrac {\d^{2 n} } {\d z^{2 n} } \cot \pi z} {z \mathop = \frac 1 4}
      | c = 
}}
{{eqn | r = \dfrac \pi {4^{2 n + 1} \paren {2 n}!} \paren {-1}^n \paren {2 \pi}^{2 n} E_{2 n}
      | c = Even Derivatives of Cotangent of Pi Z at One Fourth
}}
{{eqn | r = \paren {-1}^n \dfrac { E_{2 n} \pi^{2 n + 1} } {4^{n + 1} \paren {2 n}!}
      | c =
}}
{{end-eqn}}
{{qed}}
Theorem: Correspondence between Set and Ordinate of Cartesian Product is Mapping

Let $S$ and $T$ be sets such that $T \ne \O$.
Let $S \times T$ denote their cartesian product.
Let $t \in T$ be given.
Let $j_t \subseteq S \times \paren {S \times T}$ be the relation on $S \times {S \times T}$ defined as:
:$\forall s \in S: \map {j_t} s = \tuple {s, t}$
Then $j_t$ is a mapping.

Proof:
First it is to be shown that $j_t$ is left-total.
This follows from the fact that $j_t$ is defined for all $s$:
:$\map {j_t} s = \tuple {s, t}$
{{qed|lemma}}
Next it is to be shown that $j_t$ is many-to-one, that is:
:$\forall s_1, s_2 \in S: \map {j_t} {s_1} \ne \map {j_t} {s_2} \implies s_1 \ne s_2$
We have that:
{{begin-eqn}}
{{eqn | l = \map {j_t} {s_1}
      | o = \ne
      | r = \map {j_t} {s_2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \tuple {s_1, t}
      | o = \ne
      | r = \tuple {s_2, t}
      | c = Definition of $j_t$
}}
{{eqn | ll= \leadsto
      | l = s_1
      | o = \ne
      | r = s_2
      | c = {{Defof|Ordered Pair}}
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Mapping from Set to Ordinate of Cartesian Product is Injection

Let $S$ and $T$ be sets such that $T \ne \O$.
Let $S \times T$ denote their cartesian product.
Let $t \in T$ be given.
Let $j_t: S \to S \times T$ be the mapping from $S$ to $S \times T$ defined as:
:$\forall s \in S: \map {j_t} s = \tuple {s, t}$
Then $j_t$ is an injection.

Proof:
It has been shown in Correspondence between Set and Ordinate of Cartesian Product is Mapping that $j_t$ is a mapping.
Now it is to be shown that $j_t$ is injective, that is:
:$\forall s_1, s_2 \in S: \map {j_t} {s_1} = \map {j_t} {s_2} \implies s_1 = s_2$
We have that:
{{begin-eqn}}
{{eqn | l = \map {j_t} {s_1}
      | r = \map {j_t} {s_2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \tuple {s_1, t}
      | r = \tuple {s_2, t}
      | c = Definition of $j_t$
}}
{{eqn | ll= \leadsto
      | l = s_1
      | r = s_2
      | c = {{Defof|Ordered Pair}}
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Primitive of Sine Integral Function

:$\ds \int \map \Si x \rd x = x \map \Si x + \cos x + C$

Proof:
By Derivative of Sine Integral Function, we  have: 
:$\map {\dfrac \d {\d x} } {\map \Si x} = \dfrac {\sin x} x$
So:
{{begin-eqn}}
{{eqn	| l = \int \map \Si x \rd x
	| r = \int 1 \times \map \Si x \rd x
}}
{{eqn	| r = x \map \Si x - \int x \frac {\sin x} x \rd x
	| c = Integration by Parts
}}
{{eqn	| r = x \map \Si x - \int \sin x \rd x
}}
{{eqn	| r = x \map \Si x + \cos x + C
	| c = Primitive of Sine Function
}}
{{end-eqn}}
{{qed}}
Category:Primitives
Category:Sine Integral Function
jtcttpqr0vgbxe6mbo7ua49tmu4kfso
Theorem: Preimage of Subset of Cartesian Product under Injection from Factor

Let $S$ and $T$ be sets such that $T \ne \O$.
Let $S \times T$ denote their cartesian product.
Let $t \in T$ be given.
Let $j_t: S \to S \times T$ be the injection from $S$ to $S \times T$ defined as:
:$\forall s \in S: \map {j_t} s = \tuple {s, t}$
Let $W \subseteq S \times T$.
Let $V = {j_t}^{-1} \sqbrk W$ denote the preimage of $W$ under $j_t$.
Then:
:$V = \set {s \in S : \tuple {s, t} \in W}$

Proof:
That $j_t$ is actually an injection is demonstrated in Mapping from Set to Ordinate of Cartesian Product is Injection.
Then:
{{begin-eqn}}
{{eqn | l = V
      | r = {j_t}^{-1} \sqbrk W
      | c = 
}}
{{eqn | r = \set {s \in S : \map {j_t} s \in W}
      | c = 
}}
{{eqn | r = \set {s \in S : \tuple {s, t} \in W}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Gauss Error Function

:$\ds \int \map \erf x \rd x = x \map \erf x + \frac 1 {\sqrt \pi} e^{-x^2} + C$

Proof:
By Derivative of Gauss Error Function, we have:
:$\dfrac \d {\d x} \paren {\map \erf x} = \dfrac 2 {\sqrt \pi} e^{-x^2}$
So:
{{begin-eqn}}
{{eqn | l = \int \map \erf x \rd x
      | r = \int 1 \times \map \erf x \rd x
}}
{{eqn | r = x \map \erf x - \frac 2 {\sqrt \pi} \int x e^{-x^2} \rd x
      | c = Integration by Parts
}}
{{eqn | r = x \map \erf x + \frac 1 {\sqrt \pi} \int \paren {-2 x e^{-x^2} } \rd x
}}
{{eqn | r = x \map \erf x + \frac 1 {\sqrt \pi} \int e^u \rd u
      | c = substituting $u = -x^2$
}}
{{eqn | r = x \map \erf x + \frac 1 {\sqrt \pi} e^u + C
      | c = Primitive of Exponential Function
}}
{{eqn | r = x \map \erf x + \frac 1 {\sqrt \pi} e^{-x^2} + C
      | c = substituting back for $u$
}}
{{end-eqn}}
{{qed}}
Category:Gauss Error Function
Category:Primitives
2h8fiqistp4lrn1uy1rvo5jc0mvcp57
Theorem: Derivative of Gauss Error Function

:$\map {\dfrac \d {\d x} } {\map \erf x} = \dfrac 2 {\sqrt \pi} e^{-x^2}$

Proof:
We have, by the definition of the Gauss error function:
:$\ds \map \erf x = \frac 2 {\sqrt \pi} \int_0^x e^{-t^2} \rd t$
By Fundamental Theorem of Calculus (First Part): Corollary, we therefore have:
:$\map {\dfrac \d {\d x} } {\map \erf x} = \dfrac 2 {\sqrt \pi} e^{-x^2}$
{{qed}}
Category:Gauss Error Function
Category:Derivatives
sn5ecot7scj22szqk9okxbv4vx3aes7
Theorem: Limit to Infinity of Gauss Error Function

:$\ds \lim_{x \mathop \to \infty} \map \erf x = 1$

Proof:
{{begin-eqn}}
{{eqn | l = \lim_{x \mathop \to \infty} \map \erf x
      | r = \lim_{x \mathop \to \infty} \paren {\frac 2 {\sqrt \pi} \int_0^x e^{-t^2} \rd t}
      | c = {{Defof|Gauss Error Function}}
}}
{{eqn | r = \frac 2 {\sqrt \pi} \int_0^\infty e^{-t^2} \rd t
      | c = Multiple Rule for Limits of Real Functions
}}
{{eqn | r = \frac 2 {\sqrt \pi} \times \frac {\sqrt \pi} 2
      | c = Integral to Infinity of Exponential of -t^2
}}
{{eqn | r = 1
}}
{{end-eqn}}
{{qed}}
Theorem: Dirichlet Beta Function in terms of Hurwitz Zeta Function

:$\map \beta s = \dfrac 1 {4^s} \paren {\map \zeta {s, \dfrac 1 4} - \map \zeta {s, \dfrac 3 4} }$

Proof:
{{begin-eqn}}
{{eqn | l = \map \beta s
      | r = \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^n} {\paren {2 n + 1}^s}
      | c = {{Defof|Dirichlet Beta Function}}
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \frac 1 {\paren {4 n + 1}^s} - \sum_{n \mathop = 0}^\infty \frac 1 {\paren {4 n + 3}^s}
      | c = splitting summation into positive and negative parts
}}
{{eqn | r = \frac 1 {4^s} \paren {\sum_{n \mathop = 0}^\infty \frac 1 {\paren {n + \frac 1 4 }^s} - \sum_{n \mathop = 0}^\infty \frac 1 {\paren {n + \frac 3 4}^s} }
      | c = factoring out $\dfrac 1 {4^s}$
}}
{{eqn | l = 
      | r = \frac 1 {4^s} \paren {\map \zeta {s, \frac 1 4} - \map \zeta {s, \frac 3 4} }
      | c = {{Defof|Hurwitz Zeta Function}}
}}
{{end-eqn}}
Our reliance upon the Hurwitz zeta function requires that $s \in \C$ and $\map \Re s > 1$.
{{qed}}
Category:Dirichlet Beta Function
Category:Hurwitz Zeta Function
1yjctm7qfzyxicwgxizzgwltjdevnjf
Theorem: Inverse of Right-Total Relation is Left-Total

:$\RR$ is right-total {{iff}} $\RR^{-1}$ is left-total.

Proof:
=== Sufficient Condition ===
Let $\RR$ be right-total.
Then by definition:
:$\forall t \in T: \exists s \in S: \tuple {s, t} \in \RR$
By definition of the inverse of $\RR$, it follows that:
:$\forall t \in T: \exists s \in S: \tuple {t, s} \in \RR^{-1}$
So by definition $\RR^{-1}$ is left-total.
{{qed|lemma}}
Theorem: Inverse of Left-Total Relation is Right-Total

:$\RR$ is left-total {{iff}} $\RR^{-1}$ is right-total.

Proof:
From Inverse of Inverse Relation, the inverse of $\RR^{-1}$ is $\RR$.
From Inverse of Right-Total Relation is Left-Total:
:$\RR^{-1}$ is right-total {{iff}} $\RR$ is left-total.
Hence the result.
{{qed}}
Category:Inverse Relations
Category:Left-Total Relations
Category:Right-Total Relations
p7et19gof1t0i11wuqbu8ugwwstxry0
Theorem: Inverse of Mapping is Right-Total Relation

Let $f$ be a mapping.
Then its inverse $f^{-1}$ is a right-total relation.

Proof:
We have that $f$ is a mapping.
Hence $f$ is {{afortiori}} a left-total relation.
Then from Inverse of Left-Total Relation is Right-Total, $f^{-1}$ is right-total.
{{Qed}}
Category:Inverse Relations
Category:Inverse Mappings
Category:Right-Total Relations
rbbo0ijqmjzkhouyjoifa8s3qq0i868
Theorem: Inverse of One-to-One Relation is One-to-One

The inverse of a one-to-one relation is a one-to-one relation.

Proof:
Let $\RR$ be a one-to-one relation.
Let $\RR^{-1}$ denote its inverse
By definition, $\RR$ is a relation which is both many-to-one and one-to-many.
From Inverse of Many-to-One Relation is One-to-Many:
:$\RR^{-1}$ is both one-to-many and many-to-one.
Hence the result by definition of one-to-one relation.
{{qed}}
Category:Inverse Relations
38i2x22s1p8077snqedjfr59djnaphc
Theorem: Inverse of Injection is One-to-One Relation

Let $f$ be an injective mapping.
Then its inverse $f^{-1}$ is a one-to-one relation.

Proof:
We are given that $f$ is an injective mapping.
Hence by definition $f$ is a one-to-one relation.
The result follows from from Inverse of One-to-One Relation is One-to-One.
{{Qed}}
Theorem: Inverse of Surjection is Relation both Left-Total and Right-Total

Let $f$ be an surjective mapping.
Then its inverse $f^{-1}$ is a relation which is both left-total and right-total.

Proof:
We are given that $f$ is a surjective mapping.
By Inverse of Mapping is Right-Total Relation, $f^{-1}$ is a right-total relation.
By definition of surjection, $f$ is itself a right-total relation.
From Inverse of Right-Total Relation is Left-Total, $f^{-1}$ is a left-total relation.
Hence the result.
{{Qed}}
Category:Inverse Relations
Category:Surjections
Category:Inverse Mappings
Category:Right-Total Relations
Category:Left-Total Relations
kr0qzdqt5tquxsasgzr8xbxqd6icwt4
Theorem: Inverse is Mapping implies Mapping is Injection

Let $S$ and $T$ be sets.
Let $f: S \to T$ be a mapping.
Let the inverse $f^{-1} \subseteq T \times S$ itself be a mapping.
Then $f$ is an injection.

Proof:
Let $f^{-1}: T \to S$ be a mapping.
Let $\map f {x_a} = y$ and $\map f {x_b} = y$.
Then:
{{begin-eqn}}
{{eqn | l = \tuple {x_a, y}
      | o = \in
      | r = f
      | c = {{Defof|Mapping}}
}}
{{eqn | lo= \land
      | l = \tuple {x_b, y}
      | o = \in
      | r = f
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \tuple {y, x_a}
      | o = \in
      | r = f^{-1}
      | c = {{Defof|Inverse of Mapping}}
}}
{{eqn | lo= \land
      | l = \tuple {y, x_b}
      | o = \in
      | r = f^{-1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x_a
      | r = x_b
      | c = {{Defof|Mapping|index = 4}}: $f^{-1}$ is many-to-one
}}
{{end-eqn}}
Thus, by definition, $f$ is an injection.
{{qed}}
Theorem: Inverse is Mapping implies Mapping is Injection

Let $S$ and $T$ be sets.
Let $f: S \to T$ be a mapping.
Let the inverse $f^{-1} \subseteq T \times S$ itself be a mapping.
Then $f$ is an injection.

Proof:
Let $f^{-1}: T \to S$ be a mapping.
{{begin-eqn}}
{{eqn | l = \map f x
      | r = \map f y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {f^{-1} } {\map f x}
      | r = \map {f^{-1} } {\map f y}
      | c = as $f^{-1}$ is a mapping
}}
{{eqn | ll= \leadsto
      | l = x
      | r = y
      | c = {{Defof|Inverse Mapping|index = 1}}: as $\map {f^{-1} } {\map f x}$ and so on
}}
{{end-eqn}}
Thus $f$ is by definition an injection.
{{qed}}
Theorem: Inverse is Mapping implies Mapping is Surjection

Let $S$ and $T$ be sets.
Let $f: S \to T$ be a mapping.
Let the inverse $f^{-1} \subseteq T \times S$ itself be a mapping.
Then $f$ is a surjection.

Proof:
Let $f^{-1}: T \to S$ be a mapping.
We have:
{{begin-eqn}}
{{eqn | l = t
      | o = \in
      | r = T
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {f^{-1} } t
      | o = \in
      | r = S
      | c = as $f^{-1}$ is a mapping
}}
{{eqn | ll= \leadsto
      | l = \map f {\map {f^{-1} } t}
      | r = t
      | c = {{Defof|Inverse Mapping|index = 1}}
}}
{{eqn | ll= \leadsto
      | q = \exists s \in S
      | l = \map f s
      | r = t
      | c = setting $s = \map {f^{-1} } t$
}}
{{end-eqn}}
Thus $f$ is by definition a surjection.
{{qed}}
Theorem: Derivative Function is not Invertible

Let $\Bbb I = \closedint a b$ be a closed interval on the set of real numbers $\R$ such that $a < b$.
Let $A$ denote the set of all continuous real functions $f: \Bbb I \to \R$.
Let $B \subseteq A$ denote the set of all functions differentiable on $\Bbb I$ whose derivative is continuous on $\Bbb I$.
Let $d: B \to A$ denote the mapping defined as:
:$\forall \map f x \in B: \map d f = \map {D_x} f$
where $D_x$ denotes the derivative of $f$ {{WRT|Differentiation}} $x$.
Then $d$ is not an invertible mapping.

Proof:
By definition, $d$ is invertible {{iff}} $d$ is a bijection.
It is sufficient to demonstrate that $d$ is not an injection.
Hence a fortiori $d$ is shown to not be a bijection.
Consider a differentiable function $f \in B$.
Then consider the function $g \in B$ defined as:
:$\forall x \in \Bbb I: \map g x = \map f x + C$
where $C \in \R$ is a constant.
Then we have that:
{{begin-eqn}}
{{eqn | l = \map {D_x} g
      | r = \map {D_x} f
      | c = Derivative of Function plus Constant
}}
{{eqn | ll= \leadsto
      | l = \map d f
      | r = \map d g
      | c = Definition of $d$
}}
{{end-eqn}}
demonstrating that $d$ is not an injection.
The result follows.
{{qed}}
Theorem: Equivalence of Definitions of Convergent Sequence in Metric Space

Let $M = \struct {A, d}$ be a metric space or a pseudometric space.
Let $\sequence {x_k}$ be a sequence in $A$.
{{TFAE|def = Convergent Sequence|context = Metric Space|contextview = Metric Spaces}}

Proof:
=== Definition 1 iff Definition 2 ===
{{:Equivalence of Definitions of Convergent Sequence in Metric Space/Definition 1 iff Definition 2}}{{qed|lemma}}
Theorem: Equivalence of Definitions of Convergent Sequence in Metric Space/Definition 2 implies Definition 4

Let $\sequence {x_k}$ satisfy:
:$\forall \epsilon > 0: \exists N \in \R_{>0}: \forall n \in \N: n > N \implies x_n \in \map {B_\epsilon} l$
where $\map {B_\epsilon} l$ is the open $\epsilon$-ball of $l$.

Proof:
Let a fixed $\epsilon \in \R{>0}$ be selected.
Then:
:$\exists N \in \R_{>0}: \forall n \in \N: n > N \implies x_n \in \map {B_\epsilon} l$
Hence the only $x_k$ that cannot be in the open $\epsilon$-ball $\map {B_\epsilon} l$ of $l$ are those for which $n \le N$.
There are finitely many of these.
Theorem: Equivalence of Definitions of Convergent Sequence in Metric Space/Definition 4 implies Definition 2

Let $\sequence {x_k}$ satisfy:
:for every $\epsilon \in \R{>0}$, the open $\epsilon$-ball about $l$ contains all but finitely many of the $p_n$.

Proof:
Let $\map {B_\epsilon} l$ be any open $\epsilon$-ball of $l$.
Let $A = \set {n: x_n \notin \map {B_\epsilon} l}$.
By assumption $A$ is finite.
From Finite Non-Empty Subset of Totally Ordered Set has Smallest and Greatest Elements, any finite subset of $\N$ has a maximum.
Let $N$ be the maximum of $A$.
Then for every $n > N$, $x_n$ must be in the open $\epsilon$-ball $\map {B_\epsilon} l$.
Theorem: Definite Integral from 0 to 2 Pi of Reciprocal of a plus b Cosine x

:$\ds \int_0^{2 \pi} \frac {\d x} {a + b \cos x} = \frac {2 \pi} {\sqrt {a^2 - b^2} }$

Proof:
{{begin-eqn}}
{{eqn	| l = \int_0^{2 \pi} \frac {\d x} {a + b \cos x}
	| r = \int_0^\pi \frac {\d x} {a + b \cos x} + \int_\pi^{2 \pi} \frac {\d x} {a + b \cos x}
	| c = Sum of Integrals on Adjacent Intervals for Integrable Functions
}}
{{eqn	| r = \intlimits {\frac 2 {\sqrt {a^2 - b^2} } \map \arctan {\sqrt {\frac {a - b} {a + b} } \tan \frac x 2} } 0 \pi + \intlimits {\frac 2 {\sqrt {a^2 - b^2} } \map \arctan {\sqrt {\frac {a - b} {a + b} } \tan \frac x 2} } \pi {2 \pi}
	| c = Primitive of $\dfrac 1 {p + q \cos a x}$
}}
{{eqn	| r = \frac 2 {\sqrt {a^2 - b^2} } \paren {\lim_{x \mathop \to \pi^+} \map \arctan {\sqrt {\frac {a - b} {a + b} } \tan \frac x 2} - \map \arctan {\sqrt {\frac {a - b} {a + b} } \tan 0} }
}}
{{eqn	| o = 
	| ro= +
	| r = \frac 2 {\sqrt {a^2 - b^2} } \paren {\map \arctan {\sqrt {\frac {a - b} {a + b} } \tan \pi} - \lim_{x \mathop \to \pi^-} \map \arctan {\sqrt {\frac {a - b} {a + b} } \tan \frac x 2} }
}}
{{eqn	| r = \frac 2 {\sqrt {a^2 - b^2} } \paren {\lim_{x \mathop \to \pi^+} \map \arctan {\sqrt {\frac {a - b} {a + b} } \tan \frac x 2} - \map \arctan {\sqrt {\frac {a - b} {a + b} } \tan 0} }
	| c = Tangent Function is Periodic on Reals
}}
{{eqn	| o = 
	| ro= +
	| r = \frac 2 {\sqrt {a^2 - b^2} } \paren { \map \arctan {\sqrt {\frac {a - b} {a + b} } \tan 0} - \lim_{x \mathop \to \pi^-} \map \arctan {\sqrt {\frac {a - b} {a + b} } \tan \frac x 2} }
	| c = 
}}
{{eqn	| r = \frac 2 {\sqrt {a^2 - b^2} } \paren {\lim_{x \mathop \to \pi^+} \map \arctan {\sqrt {\frac {a - b} {a + b} } \tan \frac x 2} - \lim_{x \mathop \to \pi^-} \map \arctan {\sqrt {\frac {a - b} {a + b} } \tan \frac x 2} }
	| c = simplfying
}}
{{eqn	| r = \frac 2 {\sqrt {a^2 - b^2} } \paren {\lim_{u \mathop \to \infty} \map \arctan {\sqrt {\frac {a - b} {a + b} } u} - \lim_{u \mathop \to -\infty} \map \arctan {\sqrt {\frac {a - b} {a + b} } u} }
	| c = letting $u = \tan \dfrac x 2$: Tangent Function $\to \pm \infty$
}}
{{eqn	| r = \frac 2 {\sqrt {a^2 - b^2} } \paren {\frac \pi 2 - \paren {-\frac \pi 2} }
	| c = Limit to Positive and Negative Infinity of Arctangent Function
}}
{{eqn	| r = \frac {2 \pi} {\sqrt {a^2 - b^2} } 
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral from 0 to 2 Pi of Reciprocal of Square of a plus b Cosine x

:$\ds \int_0^{2 \pi} \frac {\d x} {\paren {a + b \cos x}^2} = \frac {2 \pi a} {\paren {a^2 - b^2}^{3/2} }$

Proof:
From Definite Integral from $0$ to $2 \pi$ of $\dfrac 1 {a + b \cos x}$, we have: 
:$\ds \int_0^{2 \pi} \frac {\d x} {a + b \cos x} = \frac {2 \pi} {\sqrt {a^2 - b^2} }$
We have: 
{{begin-eqn}}
{{eqn	| l = \frac \partial {\partial a} \int_0^{2 \pi} \frac {\d x} {a + b \cos x}
	| r = \int_0^{2 \pi} \frac \partial {\partial a} \paren {\frac 1 {a + b \cos x} } \rd x
	| c = Definite Integral of Partial Derivative 
}}
{{eqn	| r = -\int_0^{2 \pi} \frac {\d x} {\paren {a + b \cos x}^2}
	| c = Quotient Rule for Derivatives
}}
{{end-eqn}}
and: 
{{begin-eqn}}
{{eqn	| l = \frac \partial {\partial a} \paren {\frac {2 \pi} {\sqrt {a^2 - b^2} } }
	| r = 2 \pi \paren {\frac {-2 a} {2 \sqrt {a^2 - b^2} } } \paren {\frac 1 {a^2 - b^2} }
	| c = Quotient Rule for Derivatives
}}
{{eqn	| r = -\frac {2 \pi a} {\paren {a^2 - b^2}^{3/2} } 
}}
{{end-eqn}}
giving:
:$\ds \int_0^{2 \pi} \frac {\d x} {\paren {a + b \cos x}^2} = \frac {2 \pi a} {\paren {a^2 - b^2}^{3/2} }$
{{qed}}
Theorem: Derivative of Function plus Constant

Let $f$ be a real function which is differentiable on $\R$.
Let $c \in \R$ be a constant.
Then:
:$\map {\dfrac \d {\d x} } {\map f x + c} = \map {\dfrac \d {\d x} } {\map f x}$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\dfrac \d {\d x} } {\map f x + c}
      | r = \map {\dfrac \d {\d x} } {\map f x} + \map f x \, c
      | c = Sum Rule for Derivatives
}}
{{eqn | r = \map {\dfrac \d {\d x} } {\map f x} + 0
      | c = Derivative of Constant
}}
{{eqn | r = \map {\dfrac \d {\d x} } {\map f x}
      | c =
}}
{{end-eqn}}
{{qed}}
Category:Differential Calculus
grdogyhb7dxb44j669k1k2awche17bo