avewright/proofwiki-math huggingface dataset:
Theorem: Number of Digits in Number

Let $n \in \Z_{>0}$ be a strictly positive integer.
Let $b \in \Z_{>1}$ be an integer greater than $1$.
Let $n$ be expressed in base $b$.
Then the number of digits $d$ in this expression for $n$ is:
:$d = 1 + \floor {\log_b n}$
where:
:$\floor {\, \cdot \,}$ denotes the floor function
:$\log_b$ denotes the logarithm to base $b$.

Proof:
Let $n$ have $d$ digits when expressed in base $b$.
Then $n$ is expressed as:
:$n = \sqbrk {n_{d - 1} n_{d - 2} \dotsm d_1 d_0}$
where:
:$n = \ds \sum_{k \mathop = 0}^{d - 1} n_k b^k$
Thus:
:$b^{d - 1} \le n < b^d$
Thus we have:
{{begin-eqn}}
{{eqn | l = b^{d - 1}
      | o = \le
      | m = n
      | mo= <
      | r = b^d
      | c = 
}}
{{eqn | ll= \leadsto
      | l = d - 1
      | o = \le
      | m = \log_b n
      | mo= <
      | r = d
      | c = 
}}
{{end-eqn}}
By Integer equals Floor iff Number between Integer and One More:
:$d - 1 \le \log_b n < d \iff \floor {\log_b n} = d - 1$
and the result follows.
{{Qed}}
Category:Number Theory
2cw5g7zr10qou94oj9cjrllfnar534l
Theorem: Power of 2^10 Minus Power of 10^3 is Divisible by 24

Let $n \in \Z_{\ge 0}$ be a non-negative integer.
Then $2^{10 n} - 10^{3 n}$ is divisible by $24$.
That is:
:$2^{10 n} - 10^{3 n} \equiv 0 \pmod {24}$

Proof:
{{begin-eqn}}
{{eqn | l = 2^{10 n}
      | r = \paren {2^{10} }^n
      | c = Power of Power
}}
{{eqn | r = 1024^n
      | c = as $2^{10} = 1024$
}}
{{eqn | r = \paren {1000 + 24}^n
      | c = rewriting $1024$ as the sum of a power of $10$ and some integer
}}
{{eqn | r = \sum_{k \mathop = 0}^n 1000^{n - k} \, 24^k
      | c = Binomial Theorem
}}
{{eqn | n = 1
      | r = 1000^n + \sum_{k \mathop = 1}^n 1000^{n - k} \, 24^k
      | c = extracting first term from summation
}}
{{eqn | r = 1000^n + 24 \paren {\sum_{k \mathop = 1}^n 1000^{n - k} \, 24^{k - 1} }
      | c = extracting $24$ as a divisor
}}
{{eqn | ll= \leadsto
      | l = 2^{10 n} - 1000^x
      | r = 24 i
      | c = setting $i = \ds \sum_{k \mathop = 1}^n 1000^{n - k} \, 24^{k - 1}$
}}
{{eqn | ll= \leadsto
      | l = 2^{10 n} - 10^{3 n}
      | r = 24 i
      | c = rewriting $1000^n$ as a power of $10$
}}
{{eqn | ll= \leadsto
      | l = 2^{10 n} - 10^{3 n}
      | o = \equiv
      | r = 0 \pmod {24}
      | c = {{Defof|Congruence Modulo Integer}}
}}
{{end-eqn}}
{{qed}}
Theorem: Power of 2^10 Minus Power of 10^3 is Divisible by 24

Let $n \in \Z_{\ge 0}$ be a non-negative integer.
Then $2^{10 n} - 10^{3 n}$ is divisible by $24$.
That is:
:$2^{10 n} - 10^{3 n} \equiv 0 \pmod {24}$

Proof:
For $n = 0$ both powers are $1$, and $1 - 1 = 0$ is divisible by $24$.
For $n > 1$:
{{begin-eqn}}
{{eqn | l = 2^{10 n} - 10^{3 n}
      | r = 2^{3 n} \paren {2^{7 n} - 5^{3 n} }
}}
{{eqn | o = \equiv
      | r = 0
      | rr= \pmod 8
      | c = because $2^3 \divides 2^{3 n}$
}}
{{eqn | l = 2^{10 n} - 10^{3 n}
      | o = \equiv
      | r = \paren {-1}^{10 n} - 1^{3 n}
      | rr= \pmod 3
      | c = Congruence of Powers
}}
{{eqn | o = \equiv
      | r = 1 - 1
      | rr= \pmod 3
}}
{{eqn | o = \equiv
      | r = 0
      | rr= \pmod 3
}}
{{eqn | ll= \leadsto
      | l = 2^{10 n} - 10^{3 n}
      | o = \equiv
      | r = 0
      | rr= \pmod {24}
      | c = Chinese Remainder Theorem
}}
{{end-eqn}}
{{qed}}
Theorem: Power of 2^10 Minus Power of 10^3 is Divisible by 24

Let $n \in \Z_{\ge 0}$ be a non-negative integer.
Then $2^{10 n} - 10^{3 n}$ is divisible by $24$.
That is:
:$2^{10 n} - 10^{3 n} \equiv 0 \pmod {24}$

Proof:
{{begin-eqn}}
{{eqn | l = 2^{10 n} - 10^{3 n}
      | r = \paren {2^{10} }^n - \paren {10^3}^n
      | c = Power of Power
}}
{{eqn | r = \paren {2^{10} - 10^3} \sum_{j \mathop = 0}^{n - 1} \paren {2^{10} }^{n - j - 1} \paren {10^3}^j
      | c = Difference of Two Powers
}}
{{eqn | r = 24 k
      | c = where $\ds k = \sum_{j \mathop = 0}^{n - 1} {2^{10} }^{n - j - 1} \paren {10^3}^j$ is an integer
}}
{{eqn | ll= \leadsto
      | l = 2^{10 n} - 10^{3 n}
      | o = \equiv
      | r = 0 \pmod {24}
      | c = {{Defof|Congruence Modulo Integer}}
}}
{{end-eqn}}
{{qed}}
Theorem: Space of Almost-Zero Sequences is Everywhere Dense in 2-Sequence Space

Let $\struct {\ell^2, \norm {\, \cdot \,}_2}$ be the 2-sequence space equipped with Euclidean norm.
Let $c_{00}$ be the space of almost-zero sequences.
Then $c_{00}$ is everywhere dense in $\struct {\ell^2, \norm {\, \cdot \,}_2}$

Proof:
Let $\mathbf x = \sequence {x_n}_{n \mathop \in \N} \in \ell^2$.
By definition of $\ell^2$:
:$\ds \sum_{i \mathop = 0}^\infty \size {x_i}^2 < \infty$
Let $\ds s_n := \sum_{i \mathop = 0}^n \size {x_i}^2$ be a sequence of partial sums of $\ds s = \sum_{i \mathop = 0}^\infty \size {x_i}^2$.
We have that $s$ is a convergent sequence:
:$\forall \epsilon \in \R_{>0}: \exists N \in \N: \forall n \in \N: n > N \implies \size {s_n - s} < \epsilon$
Note that:
{{begin-eqn}}
{{eqn | l = \size {s_n - s}
      | r = \size {\sum_{i \mathop = 0}^n \size {x_i}^2 - \sum_{i \mathop = 0}^\infty \size {x_i}^2}
}}
{{eqn | r = \size {\sum_{i \mathop = n \mathop + 1}^\infty \size {x_i}^2}
}}
{{end-eqn}}
Let $\ds N \in \N : \sum_{n \mathop = N + 1}^\infty \size {x_n}^2 < \epsilon^2$
Let $\mathbf y := \tuple {x_1 \ldots, x_N, 0, \ldots}$.
By definition, $\mathbf y \in c_{00}$.
We have that:
{{begin-eqn}}
{{eqn | l = \norm {\mathbf x - \mathbf y}_2^2
      | r = \sum_{i \mathop = 0}^\infty \size {x_i - y_i}^2
      | c = {{Defof|Euclidean Norm}}
}}
{{eqn | r = \sum_{i \mathop = N + 1}^\infty \size {x_i}^2
}}
{{eqn | o = <
      | r = \epsilon^2
}}
{{eqn | ll= \leadsto
      | l = \norm {\mathbf x - \mathbf y}_2
      | o = <
      | r = \epsilon
}}
{{end-eqn}}
Hence by definition, $c_{00}$ is dense in $\ell^2$.
{{qed}}
Theorem: Linear Function on Stationary Stochastic Model is Stationary

Let $S$ be a strictly stationary stochastic process giving rise to a time series $T$.
Let $\sequence {s_n}$ be a sequence of $n$ successive values of $T$:
:$\sequence {s_n} = \tuple {z_1, z_2, \dotsb, z_n}$
Let $L_t$ be a linear function of $\sequence {s_n}$:
:$L_t = l_1 z_t + l_2 z_{t - 1} + \dotsb + l_n z_{t - n + 1}$
Then $L_t$ is itself stationary.

Proof:
Follows by definition of stationarity.
{{qed}}
Theorem: Ordering of Integers is Reversed by Negation

Let $x, y \in \Z$ such that $x > y$.
Then:
:$-x < -y$

Proof:
From the formal definition of integers, $\eqclass {a, b} {}$ is an equivalence class of ordered pairs of natural numbers.
Let $x = \eqclass {a, b} {}$ and $y = \eqclass {c, d} {}$ for some $x, y \in \Z$.
We have:
{{begin-eqn}}
{{eqn | l = x
      | o = >
      | r = y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \eqclass {a, b} {}
      | o = >
      | r = \eqclass {c, d} {}
      | c = {{Defof|Integer|subdef = Formal Definition}}
}}
{{eqn | ll= \leadsto
      | l = a + d
      | o = >
      | r = b + c
      | c = {{Defof|Strict Ordering on Integers}}
}}
{{eqn | ll= \leadsto
      | l = b + c
      | o = <
      | r = a + d
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \eqclass {b, a} {}
      | o = <
      | r = \eqclass {d, c} {}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = -\eqclass {a, b} {}
      | o = <
      | r = -\eqclass {c, d} {}
      | c = Negative of Integer
}}
{{eqn | ll= \leadsto
      | l = -x
      | o = <
      | r = -y
      | c = {{Defof|Integer|subdef = Formal Definition}}
}}
{{end-eqn}}
{{qed}}
Theorem: Strict Ordering on Integers is Well-Defined

Let $\eqclass {a, b} {}$ denote an integer, as defined by the formal definition of integers.
Let:
{{begin-eqn}}
{{eqn | l = \eqclass {a, b} {}
      | r = \eqclass {a', b'} {}
      | c = 
}}
{{eqn | l = \eqclass {c, d} {}
      | r = \eqclass {c', d'} {}
      | c = 
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \eqclass {a, b} {}
      | o = <
      | r = \eqclass {c, d} {}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \eqclass {a', b'} {}
      | o = <
      | r = \eqclass {c', d'} {}
      | c = 
}}
{{end-eqn}}

Proof:
This is a direct application of the Extension Theorem for Total Orderings.
{{qed}}
Theorem: Characterization of Stationary Gaussian Process

Let $S$ be a Gaussian stochastic process giving rise to a time series $T$.
Let the the mean of $S$ be fixed.
Let the autocovariance matrix of $S$ also be fixed.
Then $S$ is stationary.

Proof:
From Characterization of Multivariate Normal Distribution, the normal distribution is completely characterized by its expectation and its variance.
The result follows.
{{qed}}
Theorem: Sufficient Conditions for Weak Stationarity of Order 2

Let $S$ be a stochastic process giving rise to a time series $T$.
Let the mean of $S$ be fixed.
Let the autocovariance matrix of $S$ be of the form:
:$\boldsymbol \Gamma_n = \begin {pmatrix}
\gamma_0 & \gamma_1 & \gamma_2 & \cdots & \gamma_{n - 1} \\
\gamma_1 & \gamma_0 & \gamma_1 & \cdots & \gamma_{n - 2} \\
\gamma_2 & \gamma_1 & \gamma_0 & \cdots & \gamma_{n - 3} \\
\vdots   & \vdots   & \vdots   & \ddots & \vdots \\
\gamma_{n - 1} & \gamma_{n - 2} & \gamma_{n - 3} & \cdots & \gamma_0
\end {pmatrix} = \sigma_z^2 \mathbf P_n = \begin {pmatrix}
1 & \rho_1 & \rho_2 & \cdots & \rho_{n - 1} \\
\rho_1 & 1 & \rho_1 & \cdots & \rho_{n - 2} \\
\rho_2 & \rho_1 & 1 & \cdots & \rho_{n - 3} \\
\vdots   & \vdots   & \vdots   & \ddots & \vdots \\
\rho_{n - 1} & \rho_{n - 2} & \rho_{n - 3} & \cdots & 1
\end {pmatrix}$
Then $S$ is weakly stationary of order $2$.

Proof:
Follows from the definition of weak stationarity.
Theorem: Second Order Weakly Stationary Gaussian Stochastic Process is Strictly Stationary

Let $S$ be a Gaussian stochastic process giving rise to a time series $T$.
Let $S$ be weakly stationary of order $2$.
Then $S$ is strictly stationary.

Proof:
By definition of a Gaussian process, the probability distribution of $T$ be a multivariate normal distribution.
By definition, a normal distribution is characterized completely by its expectation and its variance.
That is, its $1$st and $2$nd moments.
The result follows.
{{qed}}
Theorem: Ordering on Integers is Transitive

Let $\eqclass {a, b} {}$ denote an integer, as defined by the formal definition of integers.
Then:
{{begin-eqn}}
{{eqn | l = \eqclass {a, b} {}
      | o = \le
      | r = \eqclass {c, d} {}
      | c = 
}}
{{eqn | lo= \land
      | l = \eqclass {c, d} {}
      | o = \le
      | r = \eqclass {e, f} {}
      | c = 
}}
{{eqn | ll= \implies
      | l = \eqclass {a, b} {}
      | o = \le
      | r = \eqclass {e, f} {}
      | c = 
}}
{{end-eqn}}
That is, ordering on the integers is transitive.

Proof:
By the formal definition of integers, we have that $a, b, c, d, e, f$ are all natural numbers.
To eliminate confusion between integer ordering and the ordering on the natural numbers, let $a \preccurlyeq b$ denote that the natural number $a$ is less than or equal to the natural number $b$.
We have:
{{begin-eqn}}
{{eqn | l = \eqclass {a, b} {}
      | o = \le
      | r = \eqclass {c, d} {}
      | c = 
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = a + d
      | o = \preccurlyeq
      | r = b + c
      | c = {{Defof|Ordering on Integers}}
}}
{{eqn | l = \eqclass {c, d} {}
      | o = <
      | r = \eqclass {e, f} {}
      | c = 
}}
{{eqn | n = 2
      | ll= \leadsto
      | l = c + f
      | o = \preccurlyeq
      | r = d + e
      | c = {{Defof|Ordering on Integers}}
}}
{{eqn | ll= \leadsto
      | l = a + d + f
      | o = \preccurlyeq
      | r = b + c + f
      | c = adding $f$ to both sides of $(1)$
}}
{{eqn | ll= \leadsto
      | l = a + d + f
      | o = \preccurlyeq
      | r = b + d + e
      | c = from $(2)$: $b + \paren {c + f} \preccurlyeq b + \paren {d + e}$
}}
{{eqn | ll= \leadsto
      | l = a + f
      | o = \preccurlyeq
      | r = b + e
      | c = subtracting $d$ from both sides
}}
{{eqn | ll= \leadsto
      | l = \eqclass {a, b} {}
      | o = \le
      | r = \eqclass {e, f} {}
      | c = {{Defof|Ordering on Integers}}
}}
{{end-eqn}}
{{qed}}
Category:Orderings on Integers
6ks88hv97gg4h02vn1o4gocu699l1ci
Theorem: Strict Ordering on Integers is Asymmetric

Let $\eqclass {a, b} {}$ denote an integer, as defined by the formal definition of integers.
Then:
{{begin-eqn}}
{{eqn | l = \eqclass {a, b} {}
      | o = <
      | r = \eqclass {c, d} {}
      | c = 
}}
{{eqn | lo= \implies
      | l = \eqclass {c, d} {}
      | o = \nless
      | r = \eqclass {a, b} {}
      | c = 
}}
{{end-eqn}}
That is, strict ordering on the integers is asymmetric.

Proof:
By the formal definition of integers, we have that $a, b, c, d, e, f$ are all natural numbers.
To eliminate confusion between integer ordering and the ordering on the natural numbers, let $a \prec b$ denote that the natural number $a$ is less than the natural number $b$.
We have:
{{begin-eqn}}
{{eqn | l = \eqclass {a, b} {}
      | o = <
      | r = \eqclass {c, d} {}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a + d
      | o = \prec
      | r = b + c
      | c = {{Defof|Strict Ordering on Integers}}
}}
{{eqn | ll= \leadsto
      | l = b + c
      | o = \nprec
      | r = a + d
      | c = {{Defof|Ordering on Natural Numbers}}
}}
{{eqn | ll= \leadsto
      | l = \eqclass {c, d} {}
      | o = \nless
      | r = \eqclass {a, b} {}
      | c = {{Defof|Strict Ordering on Integers}}
}}
{{end-eqn}}
{{qed}}
Theorem: Strict Ordering on Integers is Transitive

Let $\eqclass {a, b} {}$ denote an integer, as defined by the formal definition of integers.
Then:
{{begin-eqn}}
{{eqn | l = \eqclass {a, b} {}
      | o = <
      | r = \eqclass {c, d} {}
      | c = 
}}
{{eqn | lo= \land
      | l = \eqclass {c, d} {}
      | o = <
      | r = \eqclass {e, f} {}
      | c = 
}}
{{eqn | ll= \implies
      | l = \eqclass {a, b} {}
      | o = <
      | r = \eqclass {e, f} {}
      | c = 
}}
{{end-eqn}}
That is, strict ordering on the integers is transitive.

Proof:
By the formal definition of integers, we have that $a, b, c, d, e, f$ are all natural numbers.
To eliminate confusion between integer ordering and the ordering on the natural numbers, let $a \prec b$ denote that the natural number $a$ is less than the natural number $b$.
We have:
{{begin-eqn}}
{{eqn | l = \eqclass {a, b} {}
      | o = <
      | r = \eqclass {c, d} {}
      | c = 
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = a + d
      | o = \prec
      | r = b + c
      | c = {{Defof|Strict Ordering on Integers}}
}}
{{eqn | l = \eqclass {c, d} {}
      | o = <
      | r = \eqclass {e, f} {}
      | c = 
}}
{{eqn | n = 2
      | ll= \leadsto
      | l = c + f
      | o = \prec
      | r = d + e
      | c = {{Defof|Strict Ordering on Integers}}
}}
{{eqn | ll= \leadsto
      | l = a + d + f
      | o = \prec
      | r = b + c + f
      | c = adding $f$ to both sides of $(1)$
}}
{{eqn | ll= \leadsto
      | l = a + d + f
      | o = \prec
      | r = b + d + e
      | c = from $(2)$: $b + \paren {c + f} \prec b + \paren {d + e}$
}}
{{eqn | ll= \leadsto
      | l = a + f
      | o = \prec
      | r = b + e
      | c = subtracting $d$ from both sides
}}
{{eqn | ll= \leadsto
      | l = \eqclass {a, b} {}
      | o = <
      | r = \eqclass {e, f} {}
      | c = {{Defof|Strict Ordering on Integers}}
}}
{{end-eqn}}
{{qed}}
Theorem: Negative of Integer

Let $x \in \Z$ be an integer.
Let $x = \eqclass {a, b} {}$ be defined from the formal definition of integers, where $\eqclass {a, b} {}$ is an equivalence class of ordered pairs of natural numbers.
Then:
:$-x = \eqclass {b, a} {}$

Proof:
Follows from Inverse for Integer Addition.
{{finish|The whole area of construction of integers from the inverse completion needs to be reviewed}}
Category:Integers
Category:Examples of Inverse Elements
9uetksvhenii1xxcqn40gg4t1y8huzv
Theorem: Euler's Integral Theorem

:$H_n = \ln n + \gamma + \map \OO {\dfrac 1 n}$
where:
:$H_n$ denotes the $n$th harmonic number
:$\gamma$ denotes the Euler-Mascheroni constant
:$\map \OO {\dfrac 1 n}$ denotes big-$\OO$ of $\dfrac 1 n$.

Proof:
Recall the definition of the floor function:
{{Definition:Floor Function/Definition 3}}
For all $n \in \N_{>0}$:
{{begin-eqn}}
{{eqn | l = H_n - \ln n
      | r = 1 + \int_1 ^n \dfrac {\floor u} {u^2} \rd u - \ln n
      | c = Integral Expression of Harmonic Number
}}
{{eqn | r = 1 + \int_1 ^n \dfrac {\floor u} {u^2} \rd u - \int_1 ^n \dfrac 1 u \rd u
      | c = {{Defof|Real Natural Logarithm}}
}}
{{eqn | r = 1 - \int_1 ^n \dfrac {u - \floor u} {u^2} \rd u
      | c = Integral Operator is Linear
}}
{{end-eqn}}
Let $N \ge n \ge 1$.
By Sum of Integrals on Adjacent Intervals for Integrable Functions:
:$\ds (1): \quad \paren {H_n - \ln n} - \paren {H_N - \ln N} = \int_n^N \dfrac {u - \floor u} {u^2} \rd u$
On the other hand, from {{Defof|Floor Function}} follows:
:$\forall u \in \R_{\ge 1} : 0 \le \dfrac {u - \floor u} {u^2} \le \dfrac 1 {u^2}$
In view of Integral Operator is Positive, integrating the above inequality on $\closedint n N$:
{{begin-eqn}}
{{eqn | l = 0
      | o = \le
      | r = \int_n^N \dfrac {u - \floor u} {u^2} \rd u
      | n = 2
}}
{{eqn | o = \le
      | r = \int_n^N \dfrac 1 {u^2} \rd u
}}
{{eqn | r = \dfrac 1 n - \dfrac 1 N
}}
{{eqn | o = \le
      | r = \dfrac 1 n
}}
{{end-eqn}}
From $(1)$ and $(2)$, it follows:
:$(3): \quad 0 \le \paren {H_n - \ln n} - \paren {H_N - \ln N} \le \dfrac 1 n$
In particular, $\sequence {H_n - \ln n}$ is a Cauchy sequence.
Thus the limit $\gamma$, the Euler-Mascheroni constant, exists by Cauchy's Convergence Criterion.
In $(3)$, for each $n \in \N$, let $N \to \infty$.
Then:
:$\forall n \in \N : 0 \le H_n - \ln n - \gamma \le \dfrac 1 n$
{{qed}}
Theorem: Euler's Integral Theorem

:$H_n = \ln n + \gamma + \map \OO {\dfrac 1 n}$
where:
:$H_n$ denotes the $n$th harmonic number
:$\gamma$ denotes the Euler-Mascheroni constant
:$\map \OO {\dfrac 1 n}$ denotes big-$\OO$ of $\dfrac 1 n$.

Proof:
Recall the definition of the floor function:
{{Definition:Floor Function/Definition 3}}
Hence:
:$0 \le x - \floor x < 1$
For all $n \in \N_{>0}$:
{{begin-eqn}}
{{eqn | l = H_n - \ln n - \gamma
      | r = H_n - \ln n - \lim_{k \mathop \to +\infty} \paren {H_k - \ln k}
      | c = {{Defof|Euler-Mascheroni Constant}} and Existence of Euler-Mascheroni Constant
}}
{{eqn | r = 1 + \int_1^n \dfrac {\floor u} {u^2} \rd u - \ln n - \lim_{k \mathop \to +\infty} \paren {1 + \int_1^k \dfrac {\floor u} {u^2} \rd u - \ln k}
      | c = Integral Expression of Harmonic Number
}}
{{eqn | r = \int_1^n \dfrac {\floor u} {u^2} \rd u - \int_1^n \dfrac 1 u \rd u - \lim_{k \mathop \to +\infty} \paren {\int_1 ^k \dfrac {\floor u} {u^2} \rd u - \int_1^k \dfrac 1 u \rd u }
      | c = {{Defof|Real Natural Logarithm}}
}}
{{eqn | r = \lim_{k \mathop \to +\infty} \paren {-\int_n^k \dfrac {\floor u} {u^2} \rd u + \int_n^k \dfrac 1 u \rd u }
      | c = Sum of Integrals on Adjacent Intervals for Continuous Functions
}}
{{eqn | r = \lim_{k \mathop \to +\infty} \paren {\int_n^k \dfrac {u - \floor u} {u^2} \rd u }
      | c = Integral Operator is Linear
}}
{{eqn | o = <
      | r = \lim_{k \mathop \to +\infty} \paren {\int_n^k \dfrac 1 {u^2} \rd u }
      | c = Since $0 \le x - \floor x < 1$
}}
{{eqn | r = \intlimits {-\dfrac 1 u} n \infty
      | c = Primitive of Power
}}
{{eqn | r = \paren {0 - \paren {-\dfrac 1 n} }
      | c = 
}}
{{eqn | r = \dfrac 1 n
      | c = 
}}
{{end-eqn}}
From Existence of Euler-Mascheroni Constant Proof 1, we have:
:$\ds \Delta_n = \sum_{k \mathop = 1}^n \dfrac 1 k - \int_1^n \dfrac 1 x \rd x$
is decreasing and bounded below by zero.
Therefore:
:$H_n - \ln n \ge 0$
Therefore:
:$\forall n \in \N_{>0} : 0 \le \size {H_n - \ln n - \gamma} < \dfrac 1 n$
{{qed}}
Theorem: Ordering on Positive Integers is Equivalent to Ordering on Natural Numbers

Let $u, v \in \Z_{>0}$ be natural numbers.
Consider the mapping $\phi: \N_{>0} \to \Z_{>0}$ defined as:
:$\forall u \in \N_{>0}: \map \phi u = u'$
where $u' \in \Z$ denotes the (strictly) positive integer $\eqclass {b + u, b} {}$.
Let $u', v' \in \Z_{>0}$ be strictly positive integers.
Then:
:$u > v \iff u' > v'$

Proof:
Let $u' = \eqclass {b + u, b} {}$.
Let $v' = \eqclass {c + v, c} {}$.
Then:
{{begin-eqn}}
{{eqn | l = u'
      | o = >
      | r = v'
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \eqclass {b + u, b} {}
      | o = >
      | r = \eqclass {c + v, c} {}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = b + u + c
      | o = >
      | r = c + v + b
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = u
      | o = >
      | r = v
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Product of Absolute Values of Integers

Let $a, b \in \Z$ be integers.
Let $\size a$ denote the absolute value of $a$:
:$\size a = \begin {cases} a & : a \ge 0 \\ -a & : a < 0 \end {cases}$
Then:
:$\size a \times \size b = \size {a \times b}$

Proof:
From Integers form Ordered Integral Domain, $\Z$ is an ordered integral domain.
The result follows from Product of Absolute Values on Ordered Integral Domain.
{{qed}}
Theorem: Cardinality of Set of Self-Mappings on Finite Set

Let $S$ be a finite set.
Let the cardinality of $S$ be $n$.
The cardinality of the set of all mappings from $S$ to itself (that is, the total number of self-maps on $S$) is:
:$\card {S^S} = n^n$

Proof:
This is a specific example of Cardinality of Set of All Mappings where $S = T$.
{{qed}}
Theorem: Displacement of Particle under Force

Let $P$ be a particle of constant mass $m$.
Let the position of $P$ at time $t$ be specified by the position vector $\mathbf r$.
Let a force applied to $P$ be represented by the vector $\mathbf F$.
Then the motion of $P$ can be given by the differential equation:
:$\mathbf F = m \dfrac {\d^2 \mathbf r} {\d t^2}$
or using Newtonian notation:
:$\mathbf F = m \ddot {\mathbf r}$

Proof:
{{begin-eqn}}
{{eqn | l = \mathbf F
      | r = \map {\dfrac \d {\d t} } {m \mathbf v}
      | c = Newton's Second Law of Motion
}}
{{eqn | r = \map {\dfrac \d {\d t} } {m \dfrac {\d \mathbf r} {\d t} }
      | c = {{Defof|Velocity}}
}}
{{eqn | r = m \map {\dfrac \d {\d t} } {\dfrac {\d \mathbf r} {\d t} }
      | c = Derivative of Constant Multiple
}}
{{eqn | r = m \dfrac {\d^2 \mathbf r} {\d t^2}
      | c = {{Defof|Second Derivative}}
}}
{{end-eqn}}
{{qed}}
Theorem: 1-Sequence Space is Separable

$\ell^1$ space is a separable space.

Proof:
Let $D$ be the set of all finitely supported sequences with rational terms:
:$D = \set {\sequence {q_i}_{i \mathop \in \N} : n \in \N : i \le n : q_i \in \Q}$
We have that:
:Rational Numbers are Countably Infinite
:A finite set is countable
:$D$ is a union of finite sets indexed by $n$, which is countable
By Countable Union of Countable Sets is Countable, $D$ is countable.
Let $\mathbf x := \tuple {x_n}_{n \mathop \in \N} \in \ell^1$
By definition of $\ell^1$:
:$\ds \sum_{n \mathop = 1}^\infty \size {x_n} < \infty$
Let $\ds s_n := \sum_{i \mathop = 0}^n \size {x_i}$ be a sequence of partial sums of $\ds s = \sum_{i \mathop = 0}^\infty \size {x_i}$.
Then $s$ is a convergent sequence:
:$\forall \epsilon' \in \R_{>0}: \exists N \in \N: \forall n \in \N: n > N \implies \size {s_n - s} < \epsilon'$
Note that:
{{begin-eqn}}
{{eqn | l = \size {s_n - s}
      | r = \size {\sum_{i \mathop = 0}^n \size {x_i} - \sum_{i \mathop = 0}^\infty \size {x_i} }
}}
{{eqn | r = \size {\sum_{i \mathop = n \mathop + 1}^\infty \size {x_i} }
}}
{{eqn | r = \sum_{i \mathop = n \mathop + 1}^\infty \size {x_i}
      | c = {{Defof|Absolute Value}}
}}
{{end-eqn}}
Let $\epsilon' = \dfrac \epsilon 2$.
Let $\ds N \in \N : \sum_{n \mathop = N + 1}^\infty \size {x_n} < \frac \epsilon 2$.
We have that $\Q$ is dense in $\R$.
:$\forall x \in \R : \exists \epsilon' ' \in \R_{\mathop > 0} : \exists q \in \Q : \size {x - q} < \epsilon' '$
Then:
:$\ds \forall i \in \N : 1 \le i \le N : q_i \in \Q : \sum_{n \mathop = 1}^N \size {x_n - q_n} < \frac \epsilon 2$
where
:$\ds \frac \epsilon 2 = \sum_{i \mathop = 1}^N \epsilon_i' '$
Let $\mathbf x' := \tuple {q_1, \ldots, q_N, 0, \ldots} \in D$.
Then:
:$\ds \norm {\mathbf x - \mathbf x '} = \sum_{n \mathop = 1}^N \size {x_n - q_n} + \sum_{n \mathop = N + 1}^\infty \size {x_n} < \epsilon$
{{qed}}