avewright/proofwiki-math huggingface dataset:
Theorem: Definite Integral over Reals of Exponential of -(a x^2 plus b x plus c)

:$\ds \int_{-\infty}^\infty \map \exp {-\paren {a x^2 + b x + c} } \rd x = \sqrt {\frac \pi a} \map \exp {\frac {b^2 - 4 a c} {4 a} }$

Proof:
{{begin-eqn}}
{{eqn	| l = \int_{-\infty}^\infty \map \exp {-\paren {a x^2 + b x + c} } \rd x
	| r = \int_{-\infty}^\infty \map \exp {-a \paren {x + \frac b {2 a} }^2 + \frac {b^2} {4 a} - c} \rd x
	| c = Completing the Square
}}
{{eqn	| r = \map \exp {\frac {b^2 - 4 a c} {4 a} } \int_{-\infty}^\infty \map \exp {-a \paren {x + \frac b {2 a} }^2} \rd x
	| c = Exponential of Sum
}}
{{eqn	| r = \map \exp {\frac {b^2 - 4 a c} {4 a} } \int_{-\infty}^\infty \map \exp {-\paren {\sqrt a x + \frac b {2 \sqrt a} }^2} \rd x
}}
{{eqn	| r = \frac 1 {\sqrt a} \map \exp {\frac {b^2 - 4 a c} {4 a} } \int_{-\infty}^\infty \map \exp {-u^2} \rd u
	| c = substituting $u = \sqrt a + \dfrac b {2 \sqrt a}$
}}
{{eqn	| r = \sqrt {\frac \pi a} \map \exp {\frac {b^2 - 4 a c} {4 a} }
	| c = Gaussian Integral
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral to Infinity of Power of x by Exponential of -a x^2

:$\ds \int_0^\infty x^m e^{-a x^2} \rd x = \frac {\map \Gamma {\paren {m + 1}/2} } {2 a^{\paren {m + 1}/2} }$

Proof:
{{begin-eqn}}
{{eqn | l = \int_0^\infty x^m e^{-a x^2} \rd x
      | r = \int_0^\infty \frac 1 {2 \sqrt t} \paren {\sqrt t}^m e^{-a t} \rd t
      | c = substituting $t = x^2$
}}
{{eqn | r = \frac 1 2 \int_0^\infty t^{\paren {\paren {m + 1}/2} - 1} e^{-a t} \rd t
}}
{{eqn | r = \frac {\map \Gamma {\paren {m + 1}/2} } {2 a^{\paren {m + 1}/2} }
      | c = Laplace Transform of Real Power
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral to Infinity of Exponential of -(a x^2 plus b over x^2)

:$\ds \int_0^\infty \map \exp {-\paren {a x^2 + \frac b {x^2} } } \rd x = \frac 1 2 \sqrt {\frac \pi a} \map \exp {-2 \sqrt {a b} }$

Proof:
{{begin-eqn}}
{{eqn	| l = \int_0^\infty \map \exp {-\paren {a x^2 + \frac b {x^2} } } \rd x
	| r = \int_0^\infty \map \exp {-a \paren {x^2 + \frac b {a x^2} } } \rd x
}}
{{eqn	| r = \int_0^\infty \map \exp {-a \paren {\paren {x - \frac 1 x \sqrt {\frac b a} }^2 + 2 \sqrt {\frac b a} } } \rd x
	| c = Completing the Square
}}
{{eqn	| r = \map \exp {-2 \sqrt {a b} } \int_0^\infty \map \exp {-a \paren {x - \frac 1 x \sqrt {\frac b a} }^2} \rd x
	| c = Exponential of Sum
}}
{{eqn	| r = \frac 1 2 \map \exp {-2 \sqrt {a b} } \int_{-\infty}^\infty \map \exp {-a \paren {x - \frac 1 x \sqrt {\frac b a} }^2} \rd x
	| c = Definite Integral of Even Function
}}
{{eqn	| r = \frac 1 2 \map \exp {-2 \sqrt {a b} } \int_{-\infty}^\infty \map \exp {-a u^2} \rd u
	| c = Glasser's Master Theorem
}}
{{eqn	| r = \map \exp {-2 \sqrt {a b} } \int_0^\infty \map \exp {-a u^2} \rd u
	| c = Definite Integral of Even Function
}}
{{eqn	| r = \frac 1 2 \sqrt {\frac \pi a} \map \exp {-2 \sqrt {a b} } 
	| c = Definite Integral to Infinity of $\map \exp {-a x^2}$
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral to Infinity of x over Exponential of x minus One

:$\ds \int_0^\infty \frac x {e^x - 1} \rd x = \frac {\pi^2} 6$

Proof:
{{begin-eqn}}
{{eqn	| l = \int_0^\infty \frac x {e^x - 1} \rd x
	| r = \int_0^\infty \frac {x^{2 - 1} } {e^x - 1} \rd x
}}
{{eqn	| r = \map \zeta 2 \map \Gamma 2
	| c = Integral Representation of Riemann Zeta Function in terms of Gamma Function
}}
{{eqn	| r = \frac {\pi^2} 6 \times 1!
	| c = Basel Problem, Gamma Function Extends Factorial
}}
{{eqn	| r = \frac {\pi^2} 6
}}
{{end-eqn}}
{{qed}}
Theorem: Integral Representation of Dirichlet Eta Function in terms of Gamma Function

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

Proof:
{{begin-eqn}}
{{eqn	| l = \int_0^\infty \frac {x^{s - 1} } {e^x + 1} \rd x
	| r = \int_0^\infty \frac {x^{s - 1} e^{-x} } {1 - \paren {-e^{-x} } } \rd x
}}
{{eqn	| r = \int_0^\infty x^{s - 1} e^{-x} \paren {\sum_{n \mathop = 0}^\infty \paren {-e^{-x} }^n} \rd x
	| c = Sum of Infinite Geometric Sequence
}}
{{eqn	| r = \sum_{n \mathop = 0}^\infty \paren {\paren {-1}^n \int_0^\infty x^{s - 1} e^{-\paren {n + 1} x} \rd x}
	| c = Fubini's Theorem
}}
{{eqn	| r = \map \Gamma s \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^n} {\paren {n + 1}^s}
	| c = Laplace Transform of Complex Power
}}
{{eqn	| r = \map \Gamma s \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n - 1} } {n^s}
	| c = shifting the index
}}
{{eqn	| r = \map \Gamma s \map \eta s
	| c = {{Defof|Dirichlet Eta Function}}
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral to Infinity of x over Exponential of x plus One

:$\ds \int_0^\infty \frac x {e^x + 1} \rd x = \frac {\pi^2} {12}$

Proof:
{{begin-eqn}}
{{eqn	| l = \int_0^\infty \frac x {e^x + 1} \rd x
	| r = \int_0^\infty \frac {x^{2 - 1} } {e^x + 1} \rd x
}}
{{eqn	| r = \map \eta 2 \map \Gamma 2
	| c = Integral Representation of Dirichlet Eta Function in terms of Gamma Function
}}
{{eqn	| r = \paren {\sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n - 1} } {n^2} } 1!
	| c = {{Defof|Dirichlet Eta Function}}, Gamma Function Extends Factorial
}}
{{eqn	| r = \frac {\pi^2} {12}
	| c = Sum of Reciprocals of Squares Alternating in Sign
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral from 0 to 1 of Logarithm of x by Logarithm of One minus x

:$\ds \int_0^1 \ln x \map \ln {1 - x} \rd x = 2 - \frac {\pi^2} 6$

Proof:
{{begin-eqn}}
{{eqn | l = \int_0^1 \ln x \map \ln {1 - x} \rd x
      | r = -\int_0^1 \ln x \paren {\sum_{n \mathop = 1}^\infty \frac {x^n} n} \rd x
      | c = Power Series Expansion for $\map \ln {1 - x}$
}}
{{eqn | r = -\sum_{n \mathop = 1}^\infty \frac 1 n \paren {\int_0^1 x^n \ln x \rd x}
      | c = Fubini's Theorem
}}
{{eqn | r = \paren {-1}^2 \sum_{n \mathop = 1}^\infty \frac 1 n \paren {\frac {\map \Gamma 2} {\paren {n + 1}^2} }
      | c = Definite Integral from $0$ to $1$ of $x^m \paren {\ln x}^n$
}}
{{eqn | r = 1! \sum_{n \mathop = 1}^\infty \frac 1 {n \paren {n + 1}^2}
      | c = Gamma Function Extends Factorial
}}
{{eqn | r = \sum_{n \mathop = 1}^\infty \paren {\frac 1 n - \frac 1 {n + 1} } - \sum_{n \mathop = 1}^\infty \paren {\frac 1 {\paren {n + 1}^2} }
      | c = partial fraction expansion
}}
{{eqn | r = 1 - \paren {\sum_{n \mathop = 1}^\infty \frac 1 {n^2} - 1}
      | c = Telescoping Series: Example 1
}}
{{eqn | r = 2 - \frac {\pi^2} 6
      | c = Basel Problem
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral from 0 to 1 of Logarithm of x by Logarithm of One minus x

:$\ds \int_0^1 \ln x \map \ln {1 - x} \rd x = 2 - \frac {\pi^2} 6$

Proof:
{{begin-eqn}}
{{eqn	| l = \int_0^1 \dfrac {\ln x \map \ln {1 - x} } {\paren {1 - x} } \rd x
	    | r = \int_1^0 \dfrac {\map \ln {1 - u} \ln u } u \paren {-\rd u}
	    | c = $x \to \paren {1 - u}$ and $\rd x \to -\rd u$
}}
{{eqn	| r = \int_0^1 \dfrac {\map \ln {1 - u} \ln u } u \rd u
	    | c = reversing limits of integration
}}
{{eqn	| r = -\int_0^1 \frac {\ln u} u \paren {\sum_{n \mathop = 1}^\infty \frac {u^n} n}
	    | c = Power Series Expansion for $\map \ln {1 - x}$
}}
{{eqn	| r = -\int_0^1 \ln u \paren {\sum_{n \mathop = 1}^\infty \frac {u^{n - 1} } n}
	    | c = 
}}
{{eqn	| r = -\sum_{n \mathop = 1}^\infty \frac 1 n \paren {\int_0^1 u^{n - 1} \ln u \rd u}
	    | c = Fubini's Theorem
}}
{{eqn	| r = \paren {-1}^2 \sum_{n \mathop = 1}^\infty \frac 1 n \paren {\frac {\map \Gamma 2} {\paren {\paren {n - 1} + 1}^2} }
	    | c = Definite Integral from $0$ to $1$ of $x^m \paren {\ln x}^n$
}}
{{eqn	| r = 1! \sum_{n \mathop = 1}^\infty \frac 1 {n^3}
	    | c = Gamma Function Extends Factorial
}}
{{eqn	| r = \map \zeta {3}
	    | c = {{Defof|Apéry's Constant}}
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral from 0 to 1 of Logarithm of x by Logarithm of One minus x

:$\ds \int_0^1 \ln x \map \ln {1 - x} \rd x = 2 - \frac {\pi^2} 6$

Proof:
With a view to expressing the primitive in the form:
{{begin-eqn}}
{{eqn | l = \int u \frac {\d v} {\d x} \rd x
      | r = u v - \int v \frac {\d u} {\d x} \rd x
      | c = Integration by Parts
}}
{{end-eqn}}
let:
{{begin-eqn}}
{{eqn | l = u
      | r = \ln x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = \frac 1 x
      | c = Derivative of $\ln x$
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = \frac {\map \ln {1 - x} } {\paren {1 - x} }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = - \frac 1 2 \paren {\map \ln {1 - x} }^2
      | c = Primitive of Power
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int_0^1 \frac {\map \ln {1 - x} \ln x } {\paren {1 - x} } \rd x 
      | r = \intlimits {\ln x \paren {-\frac 1 2 \paren {\map \ln {1 - x} }^2} } 0 1 + \frac 1 2 \int_0^1 \frac {\paren {\map \ln {1 - x} }^2} x \rd x 
      | c = Integration by Parts
}}
{{eqn | r = 0 + \frac 1 2 \int_0^1 \frac {\paren {\map \ln {1 - x} }^2} x \rd x 
      | c = 
}}
{{eqn | r = \frac 1 2 \int_1^0 \frac {\paren {\map \ln u}^2} {1 - u} \paren {-\d u} 
      | c = $x \to \paren {1 - u}$ and $\rd x \to -\rd u$
}}
{{eqn | r = \frac 1 2 \int_0^1 \frac {\paren {-\map \ln u} \paren {-\map \ln u} } {1 - u} \rd u  
      | c = reversing limits of integration
}}
{{eqn | r = \frac 1 2 \int_0^1 \frac {\paren {\map \ln {\dfrac 1 u} }^{3 - 1} } {1 - u} \rd u 
      | c = Logarithm of Reciprocal
}}
{{eqn | r = \frac {\map \zeta 3 \map \Gamma 3} 2 
      | c = Integral Representation of Riemann Zeta Function in terms of Gamma Function: $\ds \map \zeta s \map \Gamma s = \int_0^1 \frac {\paren {\map \ln {\frac 1 u} }^{s - 1} } {1 - u} \rd u$
}}
{{eqn | r = \map \zeta 3 
      | c = Gamma Function of 3
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral from 0 to 1 of Logarithm of x by Logarithm of One plus x

:$\ds \int_0^1 \ln x \map \ln {1 + x} \rd x = 2 - 2 \ln 2 - \frac {\pi^2} {12}$

Proof:
{{begin-eqn}}
{{eqn	| l = \int_0^1 \ln x \map \ln {1 + x} \rd x
	| r = \int_0^1 \ln x \paren {\sum_{n \mathop = 1}^\infty \paren {-1}^{n - 1} \frac {x^n} n} \rd x
	| c = Power Series Expansion for $\map \ln {1 + x}$
}}
{{eqn	| r = \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n - 1} } n \paren {\int_0^1 x^n \ln x \rd x}
	| c = Fubini's Theorem
}}
{{eqn	| r = \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^n} n \paren {\frac {\map \Gamma 2} {\paren {n + 1}^2} }
	| c = Definite Integral from $0$ to $1$ of $x^m \paren {\ln x}^n$
}}
{{eqn	| r = 1! \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^n} {n \paren {n + 1}^2}
	| c = Gamma Function Extends Factorial
}}
{{eqn	| r = \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^n} n - \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^n} {n + 1} - \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^n} {\paren {n + 1}^2}
	| c = partial fraction expansion
}}
{{eqn	| r = -\sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n - 1} } n - \sum_{n \mathop = 2}^\infty \frac {\paren {-1}^{n - 1} } n - \sum_{n \mathop = 2}^\infty \frac {\paren {-1}^{n - 1} } {n^2}
	| c = shifting indexes
}}
{{eqn	| r = -\sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n - 1} } n - \paren {\sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n - 1} } n - 1} - \paren {\sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n - 1} } {n^2} - 1}
}}
{{eqn	| r = 2 - 2 \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n - 1} } n - \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n - 1} } {n^2}
}}
{{eqn	| r = 2 - 2 \ln 2 - \frac {\pi^2} {12}
	| c = Newton-Mercator Series for $\ln 2$, Sum of Reciprocals of Squares Alternating in Sign
}}
{{end-eqn}}
{{qed}}
Theorem: Set is Subset of Intersection of Supersets/Set of Sets

Let $T$ be a set.
Let $\mathbb S$ be a set of sets.
Suppose that for each $S \in \mathbb S$, $T \subseteq S$.
Then:
:$T \subseteq \ds \bigcap \mathbb S$

Proof:
Let $x \in T$.
We are given that:
:$\forall S \in \mathbb S: T \subseteq S$ 
Thus by definition of subset:
:$\forall S \in \mathbb S: x \in S$
Hence by definition of intersection:
:$x \in \ds \bigcap \mathbb S$
Thus by definition of subset:
:$T \subseteq \ds \bigcap \mathbb S$
{{qed}}
Category:Set is Subset of Intersection of Supersets
ivrgq2c1apz7g05yjov2jo20sjle7y2
Theorem: Power Series Expansion for Gauss Error Function

{{begin-eqn}}
{{eqn | l = \map \erf x
      | r = \frac 2 {\sqrt \pi} \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{2 n + 1} } {n! \paren {2 n + 1} }
      | c = 
}}
{{eqn | r = \frac 2 {\sqrt \pi} \paren {x - \frac {x^3} {3 \times 1!} + \frac {x^5} {5 \times 2!} - \frac {x^7} {7 \times 3!} + \frac {x^9} {9 \times 4!} - \cdots}
      | c = 
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = \map \erf x
      | r = \frac 2 {\sqrt \pi} \int_0^x e^{-u^2} \rd u
      | c = {{Defof|Gauss Error Function}}
}}
{{eqn | r = \frac 2 {\sqrt \pi} \int_0^x \paren {\sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {u^{2 n} } {n!} } \rd u
      | c = {{Defof|Real Exponential Function}}
}}
{{eqn | r = \frac 2 {\sqrt \pi} \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^n} {n!} \paren {\int_0^x u^{2 n} \rd u}
      | c = Power Series is Termwise Integrable within Radius of Convergence
}}
{{eqn | r = \frac 2 {\sqrt \pi} \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{2 n + 1} } {n! \paren {2 n + 1} }
      | c = Primitive of Power
}}
{{end-eqn}}
{{qed}}
Theorem: Set is Subset of Intersection of Supersets/General Result

Let $\family {S_i}_{i \mathop \in I}$ be a family of sets indexed by $I$.
Let $X$ be a set such that:
:$\forall i \in I: X \subseteq S_i$
Then:
:$\ds X \subseteq \bigcap_{i \mathop \in I} S_i$
where $\ds \bigcap_{i \mathop \in I} S_i$ is the intersection of $\family {S_i}$.

Proof:
Let $X \subseteq S_i$ for all $i \in I$.
Then:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = X
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \forall i \in I
      | l = x
      | o = \in
      | r = S_i
      | c = {{Defof|Subset}}
}}
{{eqn | ll= \leadsto
      | q = \forall i \in I
      | l = x
      | o = \in
      | r = \bigcap_{i \mathop \in I} S_i
      | c = {{Defof|Intersection of Family}}
}}
{{eqn | ll= \leadsto
      | l = X
      | o = \subseteq
      | r = \bigcap_{i \mathop \in I} S_i
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
{{qed}}
Theorem: Gauss Error Function is Odd

:$\map \erf {-x} = -\map \erf x$

Proof:
{{begin-eqn}}
{{eqn | l = \map \erf {-x}
      | r = \frac 2 {\sqrt \pi} \int_0^{-x} e^{-u^2} \rd u
      | c = {{Defof|Gauss Error Function}}
}}
{{eqn | r = -\frac 2 {\sqrt \pi} \int_0^{-\paren {-x} } e^{-\paren {-u}^2} \rd u
      | c = substituting $u \mapsto -u$
}}
{{eqn | r = -\frac 2 {\sqrt \pi} \int_0^x e^{-u^2} \rd u
}}
{{eqn | r = -\map \erf x
      | c = {{Defof|Gauss Error Function}}
}}
{{end-eqn}}
{{qed}}
Theorem: Gauss Error Function of Zero

:$\map \erf 0 = 0$

Proof:
By Gauss Error Function is Odd, $\erf$ is a odd function. 
Therefore, by Odd Function of Zero is Zero:
:$\map \erf 0 = 0$
{{qed}}
Theorem: Power Series Expansion for Complementary Error Function

{{begin-eqn}}
{{eqn | l = \map \erfc x
      | r = 1 - \frac 2 {\sqrt \pi} \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{2 n + 1} } {n! \paren {2 n + 1} }
      | c = 
}}
{{eqn | r = 1 - \frac 2 {\sqrt \pi} \paren {x - \frac {x^3} {3 \times 1!} + \frac {x^5} {5 \times 2!} - \frac {x^7} {7 \times 3!} + \frac {x^9} {9 \times 4!} - \cdots}
      | c = 
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = \map \erfc x
      | r = 1 - \map \erf x
      | c = {{Defof|Complementary Error Function}}
}}
{{eqn | r = 1 - \frac 2 {\sqrt \pi} \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{2 n + 1} } {n! \paren {2 n + 1} }
      | c = Power Series Expansion for Gauss Error Function
}}
{{end-eqn}}
{{qed}}
Theorem: P-adic Expansion is a Cauchy Sequence in P-adic Norm

Let $p$ be a prime number.
Let $\norm {\,\cdot\,}_p$ be the $p$-adic norm on the rationals numbers $\Q$.
Let $\ds \sum_{n \mathop = m}^\infty d_n p^n$ be a $p$-adic expansion.
Then the sequence of partial sums of the series:
:$\ds \sum_{n \mathop = m}^\infty d_n p^n$
is a Cauchy sequence in the valued field  $\struct{\Q, \norm{\,\cdot\,}_p}$.
=== Corollary 1 ===
{{:P-adic Expansion is a Cauchy Sequence in P-adic Norm/Represents a P-adic Number}}
=== Corollary 2 ===
{{:P-adic Expansion is a Cauchy Sequence in P-adic Norm/Converges to P-adic Number}}

Proof:
Let $\sequence {s_N}$ be the sequence of partial sums defined by:
:$\forall N \in \Z_{\ge m}: s_N = \ds \sum_{n \mathop = m}^N d_n p^n$
From Sequence of Consecutive Integers Modulo Power of p is Cauchy in P-adic Norm:
:the sequence $\sequence {s_N}$ is a Cauchy sequence if:
::$\forall N \in \Z_{\ge m}: s_{N + 1} \equiv s_N \pmod {p^n}$
Now for all $N \in \Z_{\ge m}$:
{{begin-eqn}}
{{eqn | l = s_{N + 1} - s_N
      | r = \sum_{n \mathop = m}^{N + 1} d_n p^ n - \sum_{n \mathop = m}^{N} d_n p^n
      | c = {{Defof|Sequence of Partial Sums|Partial Sum}}
}}
{{eqn | r = d_{N + 1} p^{N + 1}
}}
{{eqn | ll= \leadsto
      | l = s_{N + 1}
      | o = \equiv
      | r = s_N \pmod {p^N}
      | c = {{Defof|Congruence (Number Theory)|subdef = Integer Multiple|Congruence modulo $p^N$}}
}}
{{end-eqn}}
The result follows.
{{qed}}
Theorem: P-adic Expansion is a Cauchy Sequence in P-adic Norm/Converges to P-adic Number

Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.

Proof:
From P-adic Expansion is a Cauchy Sequence in P-adic Norm, the sequence of partial sums of the series:
:$\ds \sum_{n \mathop = m}^\infty d_n p^n$
is a Cauchy sequence in the rationals $\Q$ with the $p$-adic norm.
From Sequence is Cauchy in P-adic Norm iff Cauchy in P-adic Numbers, the sequence of partial sums of the series:
:$\ds \sum_{n \mathop = m}^\infty d_n p^n$
is a Cauchy sequence in the $p$-adic numbers $\Q_p$ with the $p$-adic norm.
From P-adic Numbers form Completion of Rational Numbers with P-adic Norm:
:the $p$-adic numbers $\Q_p$ form a complete normed division ring.
By definition of a complete normed division ring, every Cauchy sequence is convergent in $\struct{\Q_p, \norm{\,\cdot\,}_p}$.
{{qed}}
Theorem: Characterization of 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:
:$\ds \map \Ei x = -\gamma - \ln x + \int_0^x \frac {1 - e^{-u} } u \rd u$

Proof:
We have, by Derivative of $e^{a x}$: 
:$\map {\dfrac \d {\d u} } {1 - e^{-u} } = e^{-u}$
By Primitive of Reciprocal:
:$\ds \int \frac {\d u} u = \ln u + C$
So: 
{{begin-eqn}}
{{eqn | l = \int_0^x \frac {1 - e^{-u} } u \rd u
      | r = \bigintlimits {\paren {1 - e^{-u} } \ln u} 0 x - \int_0^x e^{-u} \ln u \rd u
      | c = Integration by Parts
}}
{{eqn | r = \paren {1 - e^{-x} } \ln x - \lim_{x \mathop \to 0^+} \paren {1 - e^{-x} } \ln x - \paren {\int_0^\infty e^{-u} \ln u \rd u - \int_x^\infty e^{-u} \ln u \rd u}
      | c = Sum of Integrals on Adjacent Intervals for Integrable Functions
}}
{{end-eqn}}
We have: 
{{begin-eqn}}
{{eqn | l = \lim_{x \mathop \to 0^+} \paren {1 - e^{-x} } \ln x
      | r = \paren {\lim_{x \mathop \to 0^+} \frac {1 - e^{-x} - \paren {1 - e^0} } x} \paren {\lim_{x \mathop \to 0^+} x \ln x}
      | c = Product Rule for Limits of Real Functions
}}
{{eqn | r = \valueat {\map {\frac \d {\d x} } {1 - e^{-x} } } {x \mathop = 0} \paren {\lim_{x \mathop \to 0^+} x \ln x}
      | c = {{Defof|Derivative}}
}}
{{eqn | r = e^0 \times 0
      | c = Derivative of $e^{a x}$, Limit of $x^m \paren {\ln x}^n$
}}
{{eqn | r = 0
}}
{{end-eqn}}
Also applying Definite Integral to Infinity of $e^{-x} \ln x$ gives:
:$\ds \int_0^x \frac {1 - e^{-u} } u \rd u = \paren {1 - e^{-x} } \ln x + \gamma + \int_x^\infty e^{-u} \ln u \rd u$ 
We have, by Primitive of $e^{a x}$:
:$\ds \int e^{-u} \rd u = -e^{-u} + C$
We have by Derivative of Logarithm Function:
:$\dfrac \d {\d u} \paren {\ln u} = \dfrac 1 u$
We therefore have: 
{{begin-eqn}}
{{eqn | l = \paren {1 - e^{-x} } \ln x + \gamma + \int_x^\infty e^{-u} \ln u \rd u
      | r = \paren {1 - e^{-x} } \ln x + \gamma + \paren {\bigintlimits {-e^{-u} \ln u} x \infty + \int_x^\infty \frac {e^{-u} } u \rd u}
      | c = Integration by Parts
}}
{{eqn | r = \paren {1 - e^{-x} } \ln x + \gamma - \lim_{u \mathop \to \infty} \paren {e^{-u} \ln u} + e^{-x} \ln x + \map \Ei x
      | c = {{Defof|Exponential Integral Function/Formulation 1|Exponential Integral Function}}
}}
{{eqn | r = \ln x + \gamma + \map \Ei x - \lim_{u \mathop \to \infty} \paren {e^{-u} \ln u}
}}
{{end-eqn}}
It remains to evaluate the limit on the {{RHS}}. 
We have, for $u > 1$:
:$e^{-u} \ln u > 0$
and by Bounds of Natural Logarithm: 
:$e^{-u} \ln u < u e^{-u} - e^{-u}$
We have, from Limit to Infinity of $x^n e^{-a x}$: 
:$\ds \lim_{u \mathop \to \infty} \paren {u e^{-u} - e^{-u} } = 0$
So, by the Squeeze Theorem: 
:$\ds \lim_{u \mathop \to \infty} \paren {e^{-u} \ln u} = 0$
So: 
:$\ds \int_0^x \frac {1 - e^{-u} } u \rd u = \ln x + \gamma + \map \Ei x$
Rearranging gives: 
:$\ds \map \Ei x = -\gamma - \ln x + \int_0^x \frac {1 - e^{-u} } u \rd u$
{{qed}}
Theorem: Complementary Error Function of Zero

:$\map \erfc 0 = 1$

Proof:
{{begin-eqn}}
{{eqn | l = \map \erfc 0 
      | r = 1 - \map \erf 0
      | c = {{Defof|Complementary Error Function}}
}}
{{eqn | r = 1
      | c = Gauss Error Function of Zero
}}
{{end-eqn}}
{{qed}}
Theorem: Limit to Infinity of Complementary Error Function

:$\ds \lim_{x \mathop \to \infty} \map \erfc x = 0$

Proof:
{{begin-eqn}}
{{eqn | l = \lim_{x \mathop \to \infty} \map \erfc x
      | r = \lim_{x \mathop \to \infty} \paren {1 - \map \erf x}
      | c = {{Defof|Complementary Error Function}}
}}
{{eqn | r = 1 - \lim_{x \mathop \to \infty} \map \erf x
      | c = Sum Rule for Limits of Real Functions
}}
{{eqn | r = 1 - 1
      | c = Limit to Infinity of Gauss Error Function
}}
{{eqn | r = 0
}}
{{end-eqn}}
{{qed}}
Theorem: Membership Relation is Not Reflexive

Let $\Bbb S$ be a set of sets in the context of pure set theory
Let $\RR$ denote the membership relation on $\Bbb S$:
:$\forall \tuple {a, b} \in \Bbb S \times \Bbb S: \tuple {a, b} \in \RR \iff a \in b$
$\RR$ is not in general a reflexive relation.

Proof:
In the extreme pathological edge case:
:$S = \set S$
it is seen that:
:$S \in S$
and so:
:$\forall x \in S: x \in x$
demonstrating that $\RR$ is reflexive in this specific case.
However, in this case $\set S$ is a set on which the Axiom of Foundation does not apply.
This is seen in Set is Not Element of Itself.
Hence this set is not supported by Zermelo-Fraenkel set theory.
Consider the set:
:$T = \set {\O, \set \O}$
Then we immediately see that:
:$\O \notin \O$
and so $\RR$ is seen to be not reflexive.
{{qed}}
Theorem: Membership Relation is Not Symmetric

Let $\Bbb S$ be a set of sets in the context of pure set theory
Let $\RR$ denote the membership relation on $\Bbb S$:
:$\forall \tuple {a, b} \in \Bbb S \times \Bbb S: \tuple {a, b} \in \RR \iff a \in b$
$\RR$ is not in general a symmetric relation.

Proof:
In the extreme pathological edge case:
:$S = \set S$
it is seen that:
:$S \in S$
and so:
:$\forall x \in S: \tuple {a, b} \in \RR \implies \tuple {b, a} \in \RR$
demonstrating that $\RR$ is symmetric in this specific case.
However, in this case $\set S$ is a set on which the Axiom of Foundation does not apply.
This is seen in Set is Not Element of Itself.
Hence this set is not supported by Zermelo-Fraenkel set theory.
Consider the set:
:$T = \set {\O, \set \O}$
Then we immediately see that while:
:$\O \in \set \O$
we have that:
:$\set \O \notin \O$
and so $\RR$ is seen to be not symmetric.
{{qed}}
Theorem: Membership Relation is Antisymmetric

Let $\Bbb S$ be a set of sets in the context of pure set theory
Let $\RR$ denote the membership relation on $\Bbb S$:
:$\forall \tuple {a, b} \in \Bbb S \times \Bbb S: \tuple {a, b} \in \RR \iff a \in b$
$\RR$ is an antisymmetric relation.

Proof:
{{ProofWanted|Applies in the case where the Axiom of Foundation applies, but I'm not so sure about non-standard sets.}}