avewright/proofwiki-math huggingface dataset:
Theorem: Sequence is Cauchy in P-adic Norm iff Cauchy in P-adic Numbers

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $\Q$ denote the rational numbers identified as a dense subfield of $\struct {\Q_p, \norm {\,\cdot\,}_p}$.
Let $\norm {\,\cdot\,} ^\Q _p$ denote the $p$-adic norm on the rational numbers.
Let $\sequence{x_n}$ be a sequence in the rational numbers $\Q$.
Then $\sequence {x_n}$ is a Cauchy sequence in $\struct{\Q, \norm{\,\cdot\,} ^\Q _p}$ {{iff}} $\sequence {x_n}$ is a Cauchy sequence in $\struct{\Q_p, \norm{\,\cdot\,}_p}$

Proof:
From Rational Numbers are Dense Subfield of P-adic Numbers:
:the $p$-adic norm $\norm {\,\cdot\,}_p$ on the $p$-adic numbers is an extension of the $p$-adic norm $\norm {\,\cdot\,} ^\Q _p$ on the rational numbers.
That is,
:$\norm {\,\cdot\,}_p \restriction_\Q \mathop = \norm {\,\cdot\,} ^\Q _p$
The result follows from Cauchy Sequence of Subring iff Cauchy Sequence of Normed Division Ring
{{qed}}
Category:P-adic Number Theory
a0rt4rf05koods2rq3d1zek95ut5k0l
Theorem: Definite Integral to Infinity of Sine x over Root x

:$\ds \int_0^\infty \frac {\sin x} {\sqrt x} \rd x = \sqrt {\frac \pi 2}$

Proof:
{{begin-eqn}}
{{eqn	| l = \int_0^\infty \frac {\sin x} {\sqrt x} \rd x
	| r = \int_0^\infty 2 u \frac {\sin u^2} {\sqrt {u^2} } \rd u
	| c = substituting $x = u^2$
}}
{{eqn	| r = 2 \int_0^\infty \sin u^2 \rd u
}}
{{eqn	| r = \sqrt {\frac \pi 2}
	| c = Definite Integral to Infinity of $\sin a x^2$
}}
{{end-eqn}}
{{qed}}
Theorem: Digamma Function of One Half

:$\map \psi {\dfrac 1 2} = -\gamma - 2 \ln 2$

Proof:
{{begin-eqn}}
{{eqn | l = \map \psi {\frac 1 2}
      | r = -\gamma - \ln 4 - \frac \pi 2 \map \cot {\frac 1 2 \pi} + 2 \sum_{n \mathop = 1}^0 \map \cos {\frac {2 \pi n} 2} \map \ln {\map \sin {\frac {\pi n} 2} }
      | c = Gauss's Digamma Theorem
}}
{{eqn | r = -\gamma - \ln 4
      | c = Cotangent of Right Angle, noting also that the summation is an empty sum
}}
{{eqn | r = -\gamma - 2 \ln 2
      | c = Logarithm of Power
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral to Infinity of Exponential of -x^2 by Logarithm of x

:$\ds \int_0^\infty e^{-x^2} \ln x \rd x = -\frac {\sqrt \pi} 4 \paren {\gamma + 2 \ln 2}$

Proof:
Consider the integral: 
:$\ds \int_0^\infty x^t e^{-x^2} \rd x$
for positive real parameter $t$.
Using Definite Integral to Infinity of $x^m e^{-a x^2}$, we have: 
:$\ds \int_0^\infty x^t e^{-x^2} \rd x = \frac 1 2 \map \Gamma {\frac {1 + t} 2}$
Differentiating the {{LHS}} {{WRT|Differentiation}} $t$ we have: 
{{begin-eqn}}
{{eqn	| l = \frac \d {\d t} \int_0^\infty t^x e^{-x^2} \rd t
	| r = \int_0^\infty \frac \partial {\partial t} \paren {x^t e^{-x^2} } \rd x
	| c = Definite Integral of Partial Derivative
}}
{{eqn	| r = \int_0^\infty x^t e^{-x^2} \ln x \rd x
	| c = Derivative of Power of Constant
}}
{{end-eqn}}
Differentiating the {{RHS}} using the Chain Rule for Derivatives gives: 
:$\ds \int_0^\infty x^t e^{-x^2} \ln x \rd x = \frac 1 4 \map {\Gamma'} {\frac {1 + t} 2}$
We therefore have: 
{{begin-eqn}}
{{eqn	| l = \int_0^\infty e^{-x^2} \ln x \rd x
	| r = \int_0^\infty x^0 e^{-x^2} \ln x \rd x
}}
{{eqn	| r = \frac 1 4 \map {\Gamma'} {\frac 1 2}
}}
{{eqn	| r = \frac 1 4 \map \Gamma {\frac 1 2} \map \psi {\frac 1 2}
	| c = {{Defof|Digamma Function}}
}}
{{eqn	| r = -\frac {\sqrt \pi} 4 \paren {\gamma + 2 \ln 2}
	| c = Gamma Function of One Half, Digamma Function of One Half
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral to Infinity of Cosine x over Root x

:$\ds \int_0^\infty \frac {\cos x} {\sqrt x} \rd x = \sqrt {\frac \pi 2}$

Proof:
{{begin-eqn}}
{{eqn	| l = \int_0^\infty \frac {\cos x} {\sqrt x} \rd x
	| r = \int_0^\infty 2 u \frac {\cos u^2} {\sqrt {u^2} } \rd u
	| c = substituting $x = u^2$
}}
{{eqn	| r = 2 \int_0^\infty \cos u^2 \rd u
}}
{{eqn	| r = \sqrt {\frac \pi 2}
	| c = Definite Integral to Infinity of $\cos a x^2$
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral to Infinity of Cube of Sine x over x Cubed

:$\ds \int_0^\infty \frac {\sin^3 x} {x^3} \rd x = \frac {3 \pi} 8$

Proof:
Let: 
:$\ds \map I \alpha = \int_0^\infty \frac {\map {\sin^3} {\alpha x} } {x^3} \rd x$
for positive real parameter $\alpha$.
We have: 
{{begin-eqn}}
{{eqn	| l = \map I 0
	| r = \int_0^\infty \frac {\map {\sin^3} {0 x} } {x^3} \rd x
}}
{{eqn	| r = \int_0^\infty \frac 0 {x^3} \rd x
	| c = Sine of Zero is Zero
}}
{{eqn	| r = 0
}}
{{end-eqn}}
We aim to evaluate explicitly: 
:$\ds \int_0^\infty \frac {\sin^3 x} {x^3} \rd x = \map I 1$
Differentiating with respect to $\alpha$ we have: 
{{begin-eqn}}
{{eqn	| l = \map {I'} \alpha
	| r = \frac \d {\d \alpha} \int_0^\infty \frac {\map {\sin^3} {\alpha x} } {x^3} \rd x
}}
{{eqn	| r = \int_0^\infty \frac \partial {\partial \alpha} \paren {\frac {\map {\sin^3} {\alpha x} } {x^3} } \rd x
	| c = Definite Integral of Partial Derivative
}}
{{eqn	| r = \frac 1 4 \int_0^\infty \frac \partial {\partial \alpha} \paren {\frac {3 \map \sin {\alpha x} - \map \sin {3 \alpha x} } {x^3} } \rd x
	| c = Cube of Sine
}}
{{eqn	| r = \frac 3 4 \int_0^\infty \frac {\map \cos {\alpha x} - \map \cos {3 \alpha x} } {x^2} \rd x
	| c = Derivative of Cosine Function, Chain Rule for Derivatives
}}
{{eqn	| r = \frac 3 4 \times \frac \pi 2 \paren {3 \alpha - \alpha}
	| c = Definite Integral to Infinity of $\dfrac {\cos p x - \cos q x} {x^2}$
}}
{{eqn	| r = \frac {3 \alpha \pi} 4
}}
{{end-eqn}}
We therefore have: 
{{begin-eqn}}
{{eqn	| l = \int_0^1 \map {I'} \alpha \rd \alpha
	| r = \intlimits {\frac {3 \alpha^2 \pi} 8} 0 1
	| c = Primitive of Power
}}
{{eqn	| r = \frac {3 \pi} 8
}}
{{end-eqn}}
By Fundamental Theorem of Calculus: Second Part, we also have: 
:$\ds \int_0^1 \map {I'} \alpha \rd \alpha = \map I 1 - \map I 0 = \map I 1$
giving: 
:$\ds \int_0^\infty \frac {\sin^3 x} {x^3} \rd x = \frac {3 \pi} 8$ 
{{qed}}
Theorem: Equivalence of Definitions of Composition of Mappings

{{TFAE|def = Composition of Mappings}}
Let $f_1: S_1 \to S_2$ and $f_2: S_2 \to S_3$ be mappings such that the domain of $f_2$ is the same set as the codomain of $f_1$.

Proof:
Let $f_1: S_1 \to S_2$ and $f_2: S_2 \to S_3$ be mappings such that:
:$\Dom {f_2} = \Cdm {f_1}$
Theorem: Power Series Expansion for Exponential Integral Function/Formulation 1

Let $\Ei: \R_{>0} \to \R$ denote the exponential integral function:
:$\map \Ei x = \ds \int_{t \mathop = x}^{t \mathop \to +\infty} \frac {e^{-t} } t \rd t$
Then:
{{begin-eqn}}
{{eqn | l = \map \Ei x
      | r = -\gamma - \ln x + \sum_{n \mathop = 1}^\infty \paren {-1}^{n + 1} \frac {x^n} {n \times n!}
      | c = 
}}
{{eqn | r = -\gamma - \ln x + \frac x {1 \times 1!} - \frac {x^2} {2 \times 2!} + \frac {x^3} {3 \times 3!} - \cdots
      | c = 
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = \map \Ei x
      | r = -\gamma - \ln x + \int_0^x \frac {1 - e^{-u} } u \rd u
      | c = Characterization of Exponential Integral Function
}}
{{eqn | r = -\gamma - \ln x + \int_0^x \frac 1 u \paren {1 - \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {u^n} {n!} } \rd u
      | c = {{Defof|Real Exponential Function}}
}}
{{eqn | r = -\gamma - \ln x + \int_0^x \frac 1 u \paren {\sum_{n \mathop = 1}^\infty \paren {-1}^{n + 1} \frac {u^n} {n!} } \rd u
}}
{{eqn | r = -\gamma - \ln x + \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n + 1} } {n!} \paren {\int_0^x u^{n - 1} \rd u}
      | c = Power Series is Termwise Integrable within Radius of Convergence
}}
{{eqn | r = -\gamma - \ln x + \sum_{n \mathop = 1}^\infty \paren {-1}^{n + 1} \frac {x^n} {n \times n!}
      | c = Primitive of Power
}}
{{end-eqn}}
{{qed}}
Theorem: P-adic Numbers are Generated Ring Extension of P-adic Integers

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $\Z_p$ be the $p$-adic integers.
Then:
:$Q_p = \Z_p \sqbrk {1 / p}$
where $\Z_p \sqbrk {1 / p}$ denotes the ring extension generated by $1 / p$.

Proof:
Let $a \in \Q_p$.
From P-adic Number times Integer Power of p is P-adic Integer, there exists $n \in \N$ such that $p^n a \in \Z_p$.
Since $n \in \N$ and $p^n a \in \Z_p$, let $\map f X \in \Z_p \sqbrk X$ be the polynomial:
:$\paren {p^n a} X^n$
Then:
:$\map f {1 / p} = \paren {p^n a} \paren {1 / p}^n = a$.
Hence:
:$a \in \Z_p \sqbrk {1 / p}$.
Since $a \in \Q_p$ was arbitrary it follows that $\Q_p \subseteq \Z_p \sqbrk {1 / p }$.
By definition of a generated ring extension, $\Z_p \sqbrk {1 / p } \subseteq \Q_p$.
The result follows.
{{qed}}
Theorem: Asymptotic Expansion for Exponential Integral Function/Formulation 1

Let $\Ei: \R_{>0} \to \R$ denote the exponential integral function:
:$\map \Ei x = \ds \int_{t \mathop = x}^{t \mathop \to +\infty} \frac {e^{-t} } t \rd t$
Then:
{{begin-eqn}}
{{eqn | l = \map \Ei x
      | o = \sim
      | r = \frac {e^{-x} } x \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {n!} {x^n}
      | c = 
}}
{{eqn | o = \sim
      | r = \frac {e^{-x} } x \paren {1 - \dfrac {1 !} x + \dfrac {2 !} {x^2} - \dfrac {3 !} {x^3} + \cdots}
      | c = 
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = \map \Ei x
      | r = \int_x^\infty \frac {e^{-t} } t \rd t
      | c = {{Defof|Exponential Integral Function/Formulation 1|Exponential Integral Function}}
}}
{{eqn | r = \intlimits {-\frac {e^{-t} } t} {t \mathop = x} {t \mathop \to \infty} -\int_x^\infty \frac {e^{-t} } {t^2} \rd t
      | c = Integration by Parts with $\left\{ {\begin {aligned} u & = \dfrac 1 t & \d v & = e^{-t} \\ \d u & = -\dfrac 1 {t^2} \rd t & v & = -e^ {-t} \end {aligned} }\right.$
}}
{{eqn | r = \frac {e^{-x} } x - \int_x^\infty \frac {e^{-t} }{t^2} \rd t
      | c = $\ds \lim_{t\mathop \to \infty} \frac {e^{-t} } t = 0$
}}
{{eqn | r = \frac {e^{-x} } x - \intlimits {-\frac{e^{-t} } {t^2} } {t \mathop = x} {t \mathop \to \infty} + \int_x^\infty \frac {2 e^{-t} } {t^3} \rd t
      | c = Integration by Parts with $\left\{ {\begin {aligned} u & = \frac 1 {t^2} & \d v & = e^{-t} \\ \d u & = -\frac 2 {t^3} \rd t & v & = -e^{-t} \end {aligned} }\right.$
}}
{{eqn | r = \frac {e^{-x} } x - \frac {e^{-x} } {x^2} + \int_x^\infty \frac {2 e^{-t} } {t^3} \rd t
      | c = $\ds \lim_{t \mathop \to \infty} \frac {e^{-t} } {t^2} = 0$
}}
{{eqn | r = \frac {e^{-x} } x - \frac {e^{-x} } {x^2} + \intlimits {\frac {2 e^{-t} } {t^3} } {t \mathop = x} {t \mathop \to \infty} - \int_x^\infty \frac {6 e^{-t} } {t^4}
      | c = Integration by Parts with $\left\{ {\begin {aligned} u & = \frac 2 {t^3} & \d v & = e^{-t} \\ \d u & = -\frac 6 {t^4} \rd t & v & = -e^{-t} \end {aligned} }\right.$
}}
{{eqn | r = \frac {e^{-x} } x - \frac {e^{-x} } {x^2} + \frac {2 e^{-x} } {x^3} - \int_x^\infty \frac {6 e^{-t} } {t^4}
      | c = $\ds \lim_{t \mathop \to \infty} \frac {e^{-t} } {t^3} = 0$
}}
{{eqn | r = \frac {e^{-x} } x - \frac {e^{-x} } {x^2} + \frac {2 e^{-x} } {x^3} - \frac {6 e^{-x} } {x^4} + \cdots + \frac {n!e^{-x} } {x^{n + 1} } + \cdots
      | c = and so on
}}
{{eqn | r = \frac {e^{-x} } x \paren {1 - \frac 1 x + \frac 2 {x^2} - \frac 6 {x^3} + \cdots + \frac {n!} {x^n} + \cdots}
}}
{{eqn | r = \frac {e^{-x} } x \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {n!} {x^n}
}}
{{end-eqn}}
{{qed}}
Theorem: Limit to Infinity of Exponential Integral Function

Let $\Ei: \R_{>0} \to \R$ denote the exponential integral function:
:$\map \Ei x = \ds \int_{t \mathop = x}^{t \mathop \to +\infty} \frac {e^{-t} } t \rd t$
Then:
:$\ds \lim_{x \mathop \to \infty} \map \Ei x = 0$

Proof:
{{begin-eqn}}
{{eqn | l = \lim_{x \mathop \to \infty} \map \Ei x
      | r = \lim_{x \mathop \to \infty} \int_x^\infty \frac {e^{-u} } u \rd u
      | c = {{Defof|Exponential Integral Function/Formulation 1|Exponential Integral Function}}
}}
{{eqn | r = \lim_{x \mathop \to \infty} \int_1^\infty \frac {e^{-x t} } {x t} x \rd t
      | c = substituting $u = x t$
}}
{{eqn | r = \int_1^\infty \lim_{x \mathop \to \infty} \paren {\frac {e^{-x t} } t} \rd t
      | c = Lebesgue's Dominated Convergence Theorem
}}
{{eqn | r = \int_1^\infty \frac 0 t \rd t
      | c = Exponential Tends to Zero and Infinity
}}
{{eqn | r = 0
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral to Infinity of Power of x over Hyperbolic Sine of a x

:$\ds \int_0^\infty \frac {x^n} {\sinh a x} \rd x = \frac {2^{n + 1} - 1} {2^n a^{n + 1} } \map \Gamma {n + 1} \map \zeta {n + 1}$

Proof:
{{begin-eqn}}
{{eqn	| l = \int_0^\infty \frac {x^n} {\sinh a x} \rd x
	| r = \frac 1 a \int_0^\infty \frac {\paren {\frac u a}^n} {\sinh u} \rd u
	| c = substituting $u = a x$
}}
{{eqn	| r = \frac 2 {a^{n + 1} } \int_0^\infty \frac {u^n e^{-u} } {1 - e^{-2 u} } \rd u
	| c = {{Defof|Hyperbolic Sine}}
}}
{{eqn	| r = \frac 2 {a^{n + 1} } \int_0^\infty u^n e^{-u} \paren {\sum_{N \mathop = 0}^\infty \paren {e^{-2 u} }^N} \rd u
	| c = Sum of Infinite Geometric Sequence
}}
{{eqn	| r = \frac 2 {a^{n + 1} } \sum_{N \mathop = 0}^\infty \int_0^\infty u^n e^{-\paren {2 N + 1} u} \rd u
	| c = Fubini's Theorem
}}
{{eqn	| r = \frac 2 {a^{n + 1} } \map \Gamma {n + 1} \sum_{N \mathop = 0}^\infty \frac 1 {\paren {2 N + 1}^{n + 1} } 
	| c = Laplace Transform of Real Power
}}
{{end-eqn}}
We have: 
{{begin-eqn}}
{{eqn	| l = \sum_{N \mathop = 1}^\infty \frac 1 {N^{n + 1} } 
	| r = \map \zeta {n + 1}
	| c = {{Defof|Riemann Zeta Function}}
}}
{{eqn	| r = \sum_{N \mathop = 1}^\infty \frac 1 {\paren {2 N}^{n + 1} } + \sum_{N \mathop = 0}^\infty \frac 1 {\paren {2 N + 1}^{n + 1} } 
}}
{{eqn	| r = \frac 1 {2^{n + 1} } \sum_{N \mathop = 1}^\infty \frac 1 {N^{n + 1} } + \sum_{N \mathop = 0}^\infty \frac 1 {\paren {2 N + 1}^{n + 1} } 
}}
{{eqn	| r = \frac 1 {2^{n + 1} } \map \zeta {n + 1} + \sum_{N \mathop = 0}^\infty \frac 1 {\paren {2 N + 1}^{n + 1} }
	| c = {{Defof|Riemann Zeta Function}}
}}
{{end-eqn}}
So: 
{{begin-eqn}}
{{eqn	| l = \sum_{N \mathop = 0}^\infty \frac 1 {\paren {2 N + 1}^{n + 1} }
	| r = \paren {1 - \frac 1 {2^{n + 1} } } \map \zeta {n + 1}
}}
{{eqn	| r = \frac {2^{n + 1} - 1} {2^{n + 1} } \map \zeta {n + 1}
}}
{{end-eqn}}
giving: 
:$\ds \int_0^\infty \frac {x^n} {\sinh a x} \rd x = \frac {2^{n + 1} - 1} {2^n a^{n + 1} } \map \Gamma {n + 1} \map \zeta {n + 1}$
{{qed}}
Theorem: Definite Integral to Infinity of x over Hyperbolic Sine of a x

:$\ds \int_0^\infty \frac x {\sinh a x} \rd x = \frac {\pi^2} {4 a^2}$

Proof:
{{begin-eqn}}
{{eqn	| l = \int_0^\infty \frac x {\sinh a x} \rd x
	| r = \frac {2^2 - 1} {2 a^2} \map \Gamma 2 \map \zeta 2
	| c = Definite Integral to Infinity of $\dfrac {x^n} {\sinh a x}$
}}
{{eqn	| r = \frac 3 {2 a^2} \times 1! \times \frac {\pi^2} 6
	| c = Gamma Function Extends Factorial, Basel Problem
}}
{{eqn	| r = \frac \pi {4 a^2}
}}
{{end-eqn}}
{{qed}}
Theorem: Fourier Series/Identity Function over Symmetric Range

Let $\lambda \in \R_{>0}$ be a strictly positive real number.
Let $\map f x: \openint {-\lambda} \lambda \to \R$ be the identity function on the open real interval $\openint {-\lambda} \lambda$:
:$\forall x \in \openint {-\lambda} \lambda: \map f x = x$
The Fourier series of $f$ over $\openint {-\lambda} \lambda$ can be given as:
:$\map f x \sim \dfrac {2 \lambda} \pi \ds \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n + 1} } n \sin \frac {n \pi x} \lambda$

Proof:
From Identity Function is Odd Function, $\map f x$ is a odd function.
By Fourier Series for Odd Function over Symmetric Range, we have:
:$\ds \map f x \sim \sum_{n \mathop = 1}^\infty b_n \sin \frac {n \pi x} \lambda$
where:
{{begin-eqn}}
{{eqn | l = b_n
      | r = \frac 2 \lambda \int_0^\pi \map f x \sin \frac {n \pi x} \lambda \rd x
      | c = 
}}
{{eqn | r = \frac 2 \lambda \int_0^\pi x \sin \frac {n \pi x} \lambda \rd x
      | c = Definition of $\map f x$
}}
{{eqn | r = \frac {2 \lambda} {n \pi} \paren {-1}^{n + 1}
      | c = Half-Range Fourier Sine Series for Identity Function
}}
{{end-eqn}}
Substituting for $b_n$ in $(1)$: 
:$\ds x = \dfrac {2 \lambda} \pi \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n + 1} } n \sin \frac {n \pi x} \lambda$
as required. 
{{qed}}
Category:Identity Mappings
Category:Fourier Series for Identity Function
ng4c7tilyzh6bvpa6r2gyiqcxqil7vp
Theorem: Restriction of Mapping is its Intersection with Cartesian Product of Subset with Image

Let $f: S \to T$ be a mapping.
Let $X \subseteq S$.
Let $f {\restriction_X}$ be the restriction of $f$ to $X$.
Then:
:$f {\restriction_X} = f \cap \paren {X \times \Img f}$
where:
:$\Img f$ denotes the image of $f$, defined as:
::$\Img f = \set {t \in T: \exists s \in S: t = \map f s}$
:$X \times \Img f$ denotes the cartesian product of $X$ with $\Img f$.

Proof:
By Restriction of Mapping is Mapping, $f {\restriction_X}: X \to T$ is a mapping.
We have:
{{begin-eqn}}
{{eqn | l = \tuple {x, y}
      | o = \in
      | r = f {\restriction_X}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \tuple {x, y}
      | o = \in
      | r = f
      | c = {{Defof|Restriction of Mapping}}
}}
{{eqn | lo= \land
      | l = x
      | o = \in
      | r = X
      | c = Definition of $x$
}}
{{eqn | lo= \land
      | l = y
      | o = \in
      | r = \Img f
      | c = {{Defof|Mapping}}
}}
{{eqn | ll= \leadsto
      | l = \tuple {x, y}
      | o = \in
      | r = f
      | c = {{Defof|Restriction of Mapping}}
}}
{{eqn | lo= \land
      | l = \tuple {x, y}
      | o = \in
      | r = X \times \Img f
      | c = {{Defof|Cartesian Product}}
}}
{{eqn | ll= \leadsto
      | l = \tuple {x, y}
      | o = \in
      | r = f \cap \paren {X \times \Img f}
      | c = {{Defof|Set Intersection}}
}}
{{eqn | ll= \leadsto
      | l = f {\restriction_X}
      | o = \subseteq
      | r = f \cap \paren {X \times \Img f}
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
{{qed|lemma}}
Then:
{{begin-eqn}}
{{eqn | l = \tuple {x, y}
      | o = \in 
      | r = f \cap \paren {X \times \Img f}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \tuple {x, y}
      | o = \in
      | r = f
      | c = 
}}
{{eqn | lo= \land
      | l = \tuple {x, y}
      | o = \in
      | r = X \times \Img f
      | c = {{Defof|Set Intersection}}
}}
{{eqn | ll= \leadsto
      | l = \tuple {x, y}
      | o = \in
      | r = f
      | c = 
}}
{{eqn | lo= \land
      | l = x
      | o = \in
      | r = X
      | c = {{Defof|Cartesian Product}}
}}
{{eqn | lo= \land
      | l = y
      | o = \in
      | r = f \sqbrk X
      | c = {{Defof|Image of Subset under Mapping}}
}}
{{eqn | ll= \leadsto
      | l = \tuple {x, y}
      | o = \in
      | r = f
      | c = 
}}
{{eqn | lo= \land
      | l = \tuple {x, y}
      | o = \in
      | r = f {\restriction_X}
      | c = {{Defof|Restriction of Mapping}}
}}
{{eqn | ll= \leadsto
      | l = f \cap \paren {X \times \Img f}
      | o = \subseteq
      | r = f {\restriction_X}
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
{{qed|lemma}}
Thus we have:
{{begin-eqn}}
{{eqn | l = f {\restriction_X}
      | o = \subseteq
      | r = f \cap \paren {X \times \Img f}
      | c = {{Defof|Subset}}
}}
{{eqn | lo= \land
      | l = f \cap \paren {X \times \Img f}
      | o = \subseteq
      | r = f {\restriction_X}
      | c = {{Defof|Subset}}
}}
{{eqn | ll= \leadsto
      | l = f \cap \paren {X \times \Img f}
      | r = f {\restriction_X}
      | c = {{Defof|Set Equality}}
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of One plus Fourth Power of x

:$\ds \int \frac 1 {1 + x^4} \rd x = \frac 1 {2 \sqrt 2} \paren {\map \arctan {\frac 1 {\sqrt 2} \paren {x - \frac 1 x} } + \frac 1 2 \ln \size {\frac {x^2 + \sqrt 2 x + 1} {x^2 - \sqrt 2 x + 1} } } + C$

Proof:
From Primitive of $\dfrac {1 + x^2} {1 + x^4}$, we have:
:$\ds \int \frac {x^2 + 1} {x^4 + 1} \rd x = \frac 1 {\sqrt 2} \map \arctan {\frac 1 {\sqrt 2} \paren {x - \frac 1 x} } + C$
From Primitive of $\dfrac {-1 + x^2} {1 + x^4}$, we have:
:$\ds \int \frac {x^2 - 1} {x^4 + 1} \rd x = \frac 1 {2 \sqrt 2} \ln \size {\frac {x^2 - \sqrt 2 x + 1} {x^2 + \sqrt 2 x + 1} } + C$
We therefore have: 
{{begin-eqn}}
{{eqn	| l = \int \frac 1 {1 + x^4} \rd x
	| r = \frac 1 2 \int \frac {x^2 + 1 - \paren {x^2 - 1} } {1 + x^4} \rd x
}}
{{eqn	| r = \frac 1 2 \paren {\int \frac {x^2 + 1} {x^4 + 1} \rd x - \int \frac {x^2 - 1} {x^4 + 1} \rd x}
}}
{{eqn	| r = \frac 1 {2 \sqrt 2} \paren {\map \arctan {\frac 1 {\sqrt 2} \paren {x - \frac 1 x} } - \frac 1 2 \ln \size {\frac {x^2 - \sqrt 2 x + 1} {x^2 + \sqrt 2 x + 1} } } + C
}}
{{eqn	| r = \frac 1 {2 \sqrt 2} \paren {\map \arctan {\frac 1 {\sqrt 2} \paren {x - \frac 1 x} } + \frac 1 2 \ln \size {\frac {x^2 + \sqrt 2 x + 1} {x^2 - \sqrt 2 x + 1} } } + C
	| c = Logarithm of Reciprocal
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of One plus Fourth Power of x

:$\ds \int \frac 1 {1 + x^4} \rd x = \frac 1 {2 \sqrt 2} \paren {\map \arctan {\frac 1 {\sqrt 2} \paren {x - \frac 1 x} } + \frac 1 2 \ln \size {\frac {x^2 + \sqrt 2 x + 1} {x^2 - \sqrt 2 x + 1} } } + C$

Proof:
A special case of Primitive of $\dfrac 1 {x^4 + a^4}$, setting $a = 1$.
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {x^4 + a^4}
      | r = \frac 1 {4 a^3 \sqrt 2} \map \ln {\frac {x^2 + a x \sqrt 2 + a^2} {x^2 - a x \sqrt 2 + a^2} } - \frac 1 {2 a^3 \sqrt 2} \paren {\map \arctan {1 - \frac {x \sqrt 2} a} - \map \arctan {1 + \frac {x \sqrt 2} a} } + C
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \int \frac {\d x} {1 + x^4}
      | r = \frac 1 {4 \sqrt 2} \map \ln {\frac {x^2 + x \sqrt 2 + 1} {x^2 - x \sqrt 2 + 1} } - \frac 1 {2 \sqrt 2} \paren {\map \arctan {1 - x \sqrt 2} - \map \arctan {1 + x \sqrt 2} } + C
      | c = 
}}
{{eqn | r = \frac 1 {2 \sqrt 2} \paren {\dfrac 1 2 \map \ln {\frac {x^2 + x \sqrt 2 + 1} {x^2 - x \sqrt 2 + 1} } - \paren {\map \arctan {1 - x \sqrt 2} - \map \arctan {1 + x \sqrt 2} } } + C
      | c = extracting factor
}}
{{eqn | r = \frac 1 {2 \sqrt 2} \paren {\dfrac 1 2 \map \ln {\frac {x^2 + x \sqrt 2 + 1} {x^2 - x \sqrt 2 + 1} } - \map \arctan {\dfrac {\paren {1 - x \sqrt 2} - \paren {1 + x \sqrt 2} } {1 + \paren {1 - x \sqrt 2} \paren {1 + x \sqrt 2} } } } + C
      | c = Difference of Arctangents
}}
{{eqn | r = \frac 1 {2 \sqrt 2} \paren {\dfrac 1 2 \map \ln {\frac {x^2 + x \sqrt 2 + 1} {x^2 - x \sqrt 2 + 1} } - \map \arctan {\dfrac {-2 x \sqrt 2} {1 + \paren {1 - 2 x^2} } } } + C
      | c = Difference of Two Squares
}}
{{eqn | r = \frac 1 {2 \sqrt 2} \paren {\dfrac 1 2 \map \ln {\frac {x^2 + x \sqrt 2 + 1} {x^2 - x \sqrt 2 + 1} } + \map \arctan {\sqrt 2 \dfrac x {1 - x^2} } } + C
      | c = Inverse Tangent is Odd Function
}}
{{eqn | r = \frac 1 {2 \sqrt 2} \paren {\dfrac 1 2 \map \ln {\frac {x^2 + x \sqrt 2 + 1} {x^2 - x \sqrt 2 + 1} } + \paren {\frac \pi 2 - \map \arctan {\frac 1 {\sqrt 2} \paren {\frac {1 - x^2} x} } } } + C
      | c = Sum of Arctangent and Arccotangent
}}
{{eqn | r = \frac 1 {2 \sqrt 2} \paren {\frac 1 2 \ln \size {\frac {x^2 + \sqrt 2 x + 1} {x^2 - \sqrt 2 x + 1} } + \map \arctan {\frac 1 {\sqrt 2} \paren {x - \frac 1 x} } } + C'
      | c = Arctangent is Odd Function, setting $C' = \dfrac \pi 2 + C$
}}
{{end-eqn}}
{{qed}}
Theorem: Empty Set from Principle of Non-Contradiction

The empty set can be characterised as:
:$\O := \set {x: x \in E \text { and } x \notin E}$
where $E$ is an arbitrary set.

Proof:
{{AimForCont}} $x \in \O$ as defined here.
Thus we have:
:$x \in E$
and:
:$x \notin E$
This is a contradiction.
It follows by Proof by Contradiction that $x \notin \O$.
Hence, as $x$ was arbitrary, there can be no $x$ such that $x \in \O$.
Thus $\O$ is the empty set by definition.
{{qed}}
Theorem: Power Series Expansion for Sine Integral Function

{{begin-eqn}}
{{eqn | l = \map \Si x
      | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{2 n + 1} } {\paren {2 n + 1} \times \paren {2 n + 1}!}
      | c = 
}}
{{eqn | r = \dfrac x {1 \cdot 1!} - \dfrac {x^3} {3 \cdot 3!} + \dfrac {x^5} {5 \cdot 5!} - \dfrac {x^7} {7 \cdot 7!} + \cdots 
      | c = 
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = \map \Si x
      | r = \int_0^x \frac {\sin u} u \rd u
      | c = {{Defof|Sine Integral Function}}
}}
{{eqn | r = \int_0^x \frac {\paren {-1}^n} u \paren {\sum_{n \mathop = 0}^\infty \frac {u^{2 n + 1} } {\paren {2 n + 1}!} } \rd u
      | c = Power Series Expansion for Sine Function
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \paren {\int_0^x \frac {u^{2 n} } {\paren {2 n + 1}!} \rd u}
      | c = Power Series is Termwise Integrable within Radius of Convergence
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{2 n + 1} } {\paren {2 n + 1} \times \paren {2 n + 1}!}
      | c = Primitive of Power
}}
{{end-eqn}}
{{qed}}