avewright/proofwiki-math huggingface dataset:
Theorem: Divisibility by Power of 10

Let $r \in \Z_{\ge 1}$ be a strictly positive integer.
An integer $N$ expressed in decimal notation is divisible by $10^r$ {{iff}} the last $r$ digits of $N$ are all $0$.
That is:
:$N = \sqbrk {a_n \ldots a_2 a_1 a_0}_{10} = a_0 + a_1 10 + a_2 10^2 + \cdots + a_n 10^n$ is divisible by $10^r$ 
{{iff}}:
:$a_0 + a_1 10 + a_2 10^2 + \cdots + a_r 10^r = 0$

Proof:
Let $N$ be divisible by $10^r$.
Then:
{{begin-eqn}}
{{eqn | l = N
      | o = \equiv
      | r = 0 \pmod {10^r}
}}
{{eqn | ll= \leadstoandfrom
      | l = \sum_{k \mathop = 0}^n a_k 10^k
      | o = \equiv
      | r = 0 \pmod {10^r}
}}
{{eqn | ll= \leadstoandfrom
      | l = \sum_{k \mathop = 0}^r a_k 10^r + \sum_{k \mathop = r + 1}^n a_k 10^k
      | o = \equiv
      | r = 0 \pmod {10^r}
}}
{{eqn | ll= \leadstoandfrom
      | l = \sum_{k \mathop = 0}^r a_k 10^r + 10^r \sum_{k \mathop = r + 1}^n a_k 10^{k - r}
      | o = \equiv
      | r = 0 \pmod {10^r}
}}
{{eqn | ll= \leadstoandfrom
      | l = \sum_{k \mathop = 0}^r a_k 10^r
      | o = \equiv
      | r = 0 \pmod {10^r}
      | c = as $10^r \equiv 0 \pmod {10^r}$
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Difference of Two Squares cannot equal 2 modulo 4

Let $n \in \Z_{>0}$ be of the form $4 k + 2$ for some $k \in \Z$.
Then $n$ cannot be expressed in the form:
:$n = a^2 - b^2$
for $a, b \in \Z$.

Proof:
Let $n = a^2 - b^2$ for some $a, b \in \Z$.
By Square Modulo 4, both $a$ and $b$ are of the form $4 k$ or $4 k + 1$ for some integer $k$.
There are $4$ cases:
;$a \equiv b \equiv 0 \pmod 4$:
Then:
:$a^2 - b^2 \equiv 0 \pmod 4$
and so $n$ is in the form $4 k$.
;$a \equiv 0 \pmod 4$, $b \equiv 1 \pmod 4$:
Then:
:$a^2 - b^2 \equiv -1 \pmod 4 \equiv 3 \pmod 4$
and so $n$ is in the form $4 k + 3$.
;$a \equiv 1 \pmod 4$, $b \equiv 0 \pmod 4$:
Then:
:$a^2 - b^2 \equiv 1 \pmod 4$
and so $n$ is in the form $4 k + 1$.
;$a \equiv b \equiv 1 \pmod 4$:
Then:
:$a^2 - b^2 \equiv 0 \pmod 4$
and so $n$ is in the form $4 k$.
Thus it is never the case that $a^2 - b^2 = 4 k + 2$.
{{qed}}
Theorem: Difference of Two Squares cannot equal 2 modulo 4

Let $n \in \Z_{>0}$ be of the form $4 k + 2$ for some $k \in \Z$.
Then $n$ cannot be expressed in the form:
:$n = a^2 - b^2$
for $a, b \in \Z$.

Proof:
Let $n_0 = c^2 - d^2$ for some $c, d \in \Z$.
Then:
:$n_0 = \paren {c + d} \paren {c - d}$
and so:
:$\paren {c + d} - \paren {c - d} = 2 d$
Therefore $n$ must be expressible as a product of two integers whose difference is even.
Now consider the integer $n \in \Z$ that satisfies $n \equiv 2 \pmod 4$.
$n$ is an even number that is not divisible by 4.
This implies that any even number that divides $n$ will produce an odd number.
Consider the ordered pairs of integers $\tuple {a, b}, a < b$ such that $ab = n$.
If  $a$ is odd, then $b = \dfrac n a$ must in turn be even.
Hence the difference will not be even.
If $a$ is even, $b$ must be odd by the implication mentioned earlier.
Hence the difference will once again not be even.
Hence, $n$ cannot be expressed as a product of two integers whose difference is even.
In turn it cannot be expressed as a Difference of Two Squares.
{{qed}}
Theorem: Compact Closure is Set of Finite Subsets in Lattice of Power Set

Let $X$ be a set.
Let $L = \struct {\powerset X, \cup, \cap, \preceq}$ be the lattice of power set of $X$ where $\mathord\preceq = \mathord\subseteq \cap \powerset X \times \powerset X$
Let $x \in \powerset X$.
Then $x^{\mathrm{compact} } = \map {\operatorname{Fin} } x$
where $\map {\operatorname{Fin} } x$ denotes the set of all finite subsets of $x$.

Proof:
=== $\subseteq$ ===
Let $y \in x^{\mathrm{compact} }$.
By definition of compact closure:
:$y \preceq x$ and $y$ is compact.
By definition of $\preceq$:
:$y \subseteq x$
By Element is Finite iff Element is Compact in Lattice of Power Set:
"$y$ is a finite set.
Thus by definition of $\operatorname{Fin}$:
:$y \in \map {\operatorname{Fin} } x$
{{qed|lemma}}
Theorem: 10 is Only Triangular Number that is Sum of Consecutive Odd Squares

$10$ is the only triangular number which is the sum of two consecutive odd squares:
:$10 = 1^2 + 3^2$

Proof:
{{:Closed Form for Triangular Numbers}}
for $n \in \Z_{\ge 0}$.
The expression for the $n$th odd square number is:
:$4 n^2 + 4 n + 1$
again, for $n \in \Z_{\ge 0}$.
Therefore the closed-form expression for the $n$th sum of two consecutive odd squares is:
:$4 n^2 + 4 n + 1 + 4 \paren {n + 1}^2 + 4 \paren {n + 1} + 1$
This simplifies to:
:$8 n^2 + 16 n + 10$
Equate the two with a variable replacing $n$:
:$8 x^2 + 16 x + 10 = \dfrac {y \paren {y + 1} } 2$
This simplifies to:
:$16 x^2 + 32 x + 20 = y^2 + y$
We then apply Solutions to Diophantine Equation $16 x^2 + 32 x + 20 = y^2 + y$:
{{:Solutions to Diophantine Equation 16x^2+32x+20 = y^2+y}}
Due to the restrictions on the variables, solutions with negative inputs are invalid.
This leaves one solution:
:$\tuple {0, 4}$
as follows:
{{begin-eqn}}
{{eqn | l = 8 \paren 0^2 + 16 \paren 0 + 10
      | r = \frac {\paren 4 \paren {\paren 4 + 1} } 2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 1^2 + 3^2
      | r = 10
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: 10 Consecutive Integers contain Coprime Integer

Let $n \in \Z$ be an integer.
Let $S := \set {n, n + 1, n + 2, \ldots, n + 9}$ be the set of $10$ consecutive integers starting from $n$.
Then at least one element of $S$ is coprime to every other element of $S$.

Proof:
Consider $2$ elements $a, b$ of $S$ which share a common divisor $d$.
Then $d \divides \size {a - b}$ and so $d < 10$.
Now from the Fundamental Theorem of Arithmetic, $d$ must have a prime factor which is strictly less than $10$.
So for $a$ and $b$ to have a common divisor, at least one such common divisor is in $\set {2, 3, 5, 7}$.
There are exactly $5$ elements of $S$ which have a common divisor of $2$.
There are either $3$ or $4$ elements of $S$ common divisor of $3$.
The case where there are $4$ happens when $n = 3 k$ and $n + 9 = 3 \paren {k + 3}$.
Of these $3$ or $4$, no more than $2$ are odd and so have not been accounted for.
There are exactly $2$ elements of $S$ which have $5$ as a common divisor.
One of those is even and so has been counted already.
There are at most $2$ elements of $S$ which have $7$ as a common divisor.
One of those is even and so has been counted already.
Thus we have a count of how many elements of $S$ which can possibly share a common divisor with another element of $S$:
:$5$ are divisible by $2$
:$2$ or fewer are divisible by $3$ and not $2$
:$1$ at the most is divisible by $5$ and not by $2$ or $3$
:$1$ at the most is divisible by $7$ and not by $2$, $3$ or $5$.
That makes a total of $9$ elements of $S$ which are divisible by $2$, $3$, $5$ or $7$.
Thus there exists (at least) $1$ element of $S$ which is not divisible by $2$, $3$, $5$ or $7$ and so cannot share a common divisor with another element of $S$.
Hence the result.
{{qed}}
Theorem: Two Fifths as Pandigital Fraction

There are $3$ ways $\dfrac 2 5$ can be expressed as a pandigital fraction:
:$\dfrac 2 5 = \dfrac {6894} {17235}$
:$\dfrac 2 5 = \dfrac {8694} {21735}$
:$\dfrac 2 5 = \dfrac {9486} {23715}$

Proof:
Can be verified by brute force.
Category:Pandigital Fractions
055zswhtnrwnvqeqdxkph8z2yd2qqse
Theorem: Two Sevenths as Pandigital Fraction

There are $6$ ways $\dfrac 2 7$ can be expressed as a pandigital fraction:
:$\dfrac 2 7 = \dfrac {3654} {12789}$
:$\dfrac 2 7 = \dfrac {3674} {12859}$
:$\dfrac 2 7 = \dfrac {5342} {18697}$
:$\dfrac 2 7 = \dfrac {7418} {25963}$
:$\dfrac 2 7 = \dfrac {9786} {34251}$
:$\dfrac 2 7 = \dfrac {9862} {34517}$

Proof:
Can be verified by brute force.
Category:Pandigital Fractions
3vg8lm7xffdosxq7mvyuxv48daojqy2
Theorem: Two Ninths as Pandigital Fraction

There are $2$ ways $\dfrac 2 9$ can be expressed as a pandigital fraction:
{{begin-eqn}}
{{eqn | l = \dfrac 2 9
      | r = \dfrac {3924} {17658}
}}
{{eqn | l = \dfrac 2 9
      | r = \dfrac {7596} {34182}
}}
{{end-eqn}}

Proof:
Can be verified by brute force.
Category:Pandigital Fractions
aw7pqsuqjxc9s094hdo4vcrm83po897
Theorem: Closed Form for Tetrahedral Numbers

The closed-form expression for the $n$th tetrahedral number is:
:$H_n = \dfrac {n \paren {n + 1} \paren {n + 2} } 6$

Proof:
{{begin-eqn}}
{{eqn | l = H_n
      | r = \sum_{r \mathop = 1}^n T_r
      | c = {{Defof|Tetrahedral Number}}
}}
{{eqn | r = \sum_{r \mathop = 1}^n \frac {r \paren {r + 1} } 2
      | c = Closed Form for Triangular Numbers
}}
{{eqn | r = \sum_{r \mathop = 1}^n \paren {\frac 1 2 r^2 + \frac 1 2 r}
      | c = 
}}
{{eqn | r = \frac 1 2 \sum_{r \mathop = 1}^n r^2 + \frac 1 2 \sum_{r \mathop = 1}^n r
      | c = Summation is Linear
}}
{{eqn | r = \frac 1 2 \sum_{r \mathop = 1}^n r^2 + \frac 1 2 T_n
      | c = {{Defof|Triangular Number|index = 2}}
}}
{{eqn | r = \frac 1 2 \frac {n \paren {n + 1} \paren {2 n + 1} } 6 + \frac 1 2 \frac {n \paren {n + 1} } 2
      | c = Sum of Sequence of Squares, Closed Form for Triangular Numbers
}}
{{eqn | r = \frac {n \paren {n + 1} } {12} \paren {\paren {2 n + 1} + 3}
      | c = 
}}
{{eqn | r = \frac {n \paren {n + 1} \paren {n + 2} } 6
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Factorial as Product of Two Factorials

Apart from the general pattern, following directly from the definition of the factorial:
:$\paren {n!}! = n! \paren {n! - 1}!$
the only known factorial which is the product of two factorials is:
:$10! = 6! \, 7!$

Proof:
{{begin-eqn}}
{{eqn | l = 10!
      | r = 7! \times 8 \times 9 \times 10
      | c = {{Defof|Factorial}}
}}
{{eqn | r = 7! \times \paren {2 \times 4} \times \paren {3 \times 3} \times \paren {2 \times 5}
}}
{{eqn | r = 7! \times 2 \times 4 \times 3 \times \paren {3 \times 2} \times 5
}}
{{eqn | r = 7! \times 2 \times 3 \times 4 \times 5 \times 6
}}
{{eqn | r = 6! \, 7!
      | c = {{Defof|Factorial}}
}}
{{end-eqn}}
{{qed}}
Theorem: Factorial as Product of Three Factorials

This general pattern can be used to find a factorial which is the product of three factorials:
:$\paren {\paren {n!}!}! = n! \paren {n! - 1}! \paren {\paren {n!}! - 1}!$
while there are instances of factorials which do not fit that pattern.

Proof:
{{begin-eqn}}
{{eqn | l = \paren {\paren {n!}!}!
      | r = \paren {n!}! \times \paren {\paren {n!}! - 1}!
      | c = Factorial as Product of Two Factorials
}}
{{eqn | r = n! \times \paren {n! - 1}! \times \paren {\paren {n!}! - 1}!
      | c = Factorial as Product of Two Factorials
}}
{{end-eqn}}
{{qed}}
Theorem: Two Thirds as Pandigital Fraction

$\dfrac 2 3$ cannot be expressed as a pandigital fraction.

Proof:
Can be verified by brute force.
Category:Pandigital Fractions
5itdiplla5qizaah8gv9ev3z2sozpk9
Theorem: Three Quarters as Pandigital Fraction

$\dfrac 3 4$ cannot be expressed as a pandigital fraction.

Proof:
Can be verified by brute force.
Category:Pandigital Fractions
s57iaxw90tqkcob960zu0fhvdy8ue5s
Theorem: Three Fifths as Pandigital Fraction

$\dfrac 3 5$ cannot be expressed as a pandigital fraction.

Proof:
Can be verified by brute force.
Category:Pandigital Fractions
t2wttw0dnqbst5g9t3c17e2qgc53t5p
Theorem: Three Sevenths as Pandigital Fraction

$\dfrac 3 7$ cannot be expressed as a pandigital fraction.

Proof:
Can be verified by brute force.
Category:Pandigital Fractions
9as5b4nk5h9f4g64bx10vunxe6pm2sl
Theorem: Three Eighths as Pandigital Fraction

$\dfrac 3 8$ cannot be expressed as a pandigital fraction.

Proof:
Can be verified by brute force.
Category:Pandigital Fractions
i2ruxvt2pmp3tnlu4isqnkejpfbe1ry
Theorem: Four Sevenths as Pandigital Fraction

$\dfrac 4 7$ cannot be expressed as a pandigital fraction.

Proof:
Can be verified by brute force.
Category:Pandigital Fractions
ekzrdi64qubrwjuffq00ynvvqr31xzy
Theorem: Five Sevenths as Pandigital Fraction

$\dfrac 5 7$ cannot be expressed as a pandigital fraction.

Proof:
Can be verified by brute force.
Category:Pandigital Fractions
kmgdxe5yibpy0lk6s7whooizqedd8tk
Theorem: Six Sevenths as Pandigital Fraction

$\dfrac 6 7$ cannot be expressed as a pandigital fraction.

Proof:
Can be verified by brute force.
Category:Pandigital Fractions
7j9wpx06dq7cikndvmfc4ckkfnyj1km
Theorem: Five Sixths as Pandigital Fraction

$\dfrac 5 6$ cannot be expressed as a pandigital fraction.

Proof:
Can be verified by brute force.
Category:Pandigital Fractions
8wmrbiarp95of35q9y7yfswbm6lup6m
Theorem: Five Eighths as Pandigital Fraction

$\dfrac 5 8$ cannot be expressed as a pandigital fraction.

Proof:
Can be verified by brute force.
Category:Pandigital Fractions
msdo74yu6ouq74zjz79o04aqzfa96k8
Theorem: Seven Eighths as Pandigital Fraction

$\dfrac 7 8$ cannot be expressed as a pandigital fraction.

Proof:
Can be verified by brute force.
Category:Pandigital Fractions
75q6t9qdl4n76fgzmne9at71y5yhwc7
Theorem: Four Ninths as Pandigital Fraction

$\dfrac 4 9$ cannot be expressed as a pandigital fraction.

Proof:
Can be verified by brute force.
Category:Pandigital Fractions
rb2cdg84i5nvjusdmsp187c9sqxjlma
Theorem: Five Ninths as Pandigital Fraction

$\dfrac 5 9$ cannot be expressed as a pandigital fraction.

Proof:
Can be verified by brute force.
Category:Pandigital Fractions
2wf5bsw1mdpjj1o554kpuzfui1u2u4y
Theorem: Seven Ninths as Pandigital Fraction

$\dfrac 7 9$ cannot be expressed as a pandigital fraction.

Proof:
Can be verified by brute force.
Category:Pandigital Fractions
r6s00mwho0u132y6az41r1wjeere5d3
Theorem: Eight Ninths as Pandigital Fraction

$\dfrac 8 9$ cannot be expressed as a pandigital fraction.

Proof:
Can be verified by brute force.
Category:Pandigital Fractions
01jl5wmi3om94ivfpddlhdg7pv9khuu
Theorem: Generating Function for Triangular Numbers

Let $T_n$ denote the $n$th triangular number.
Then the generating function for $\sequence {T_n}$ is given as:
:$\ds \map G z = \frac z {\paren {1 - z}^3}$

Proof:
{{begin-eqn}}
{{eqn | l = \frac z {\paren {1 - z}^3}
      | r = z \paren {1 - z}^{-3}
      | c = Exponent Combination Laws for Negative Power
}}
{{eqn | r = z \sum_{n \mathop = 0}^\infty \dbinom {-3} n \paren {-z}^n
      | c = General Binomial Theorem
}}
{{eqn | r = z \sum_{n \mathop = 0}^\infty \paren {-1}^n \dbinom {n + 2} n \paren {-z}^n
      | c = Negated Upper Index of Binomial Coefficient
}}
{{eqn | r = z \sum_{n \mathop = 0}^\infty \dbinom {n + 2} n z^n
      | c = 
}}
{{eqn | r = z \sum_{n \mathop = 0}^\infty \dbinom {n + 2} 2 z^n
      | c = Symmetry Rule for Binomial Coefficients
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \dbinom {n + 2} 2 z^{n + 1}
      | c = 
}}
{{eqn | r = \sum_{n \mathop = 1}^\infty \dbinom {n + 1} 2 z^n
      | c = 
}}
{{eqn | r = \sum_{n \mathop = 1}^\infty T_n z^n
      | c = {{Corollary|Binomial Coefficient with Two}}
}}
{{eqn | r = 0 z^0 + \sum_{n \mathop = 1}^\infty T_n z^n
      | c = 
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty T_n z^n
      | c = $T_0 = 0$ by {{Defof|Triangular Number|index = 1}}
}}
{{eqn | r = \map G z
      | c = {{Defof|Generating Function}}
}}
{{end-eqn}}
{{qed}}
Category:Triangular Numbers
Category:Examples of Generating Functions
bq2fu8qstqwed0yfcmk606u2uay8x9v
Theorem: Lattice of Power Set is Algebraic

Let $X$ be a set.
Let $L = \struct {\powerset X, \cup, \cap, \preceq}$ be the lattice of power set of $X$
where $\mathord \preceq = \mathord \subseteq \cap \paren {\powerset X \times \powerset X}$
Then $L$ is algebraic.

Proof:
We will prove that
:$\forall x \in \powerset X: x^{\mathrm{compact} }$ is directed.
Let $x \in \powerset X$.
By Empty Set is Bottom of Lattice of Power Set:
:$\O = \bot$
where $\bot$ denotes the bottom of $L$.
By Bottom is Way Below Any Element:
:$\bot \ll \bot$
where $\ll$ is the way below relation.
By definition:
:$\bot$ is compact.
By definition of the smallest element:
:$\bot \preceq x$
By definition of compact closure:
:$\bot \in x^{\mathrm{compact} }$
By definition:
:$x^{\mathrm{compact} }$ is non-empty.
Thus by Non-Empty Compact Closure is Directed:
:$x^{\mathrm{compact} }$ is directed.
{{qed|lemma}}
By Power Set is Complete Lattice:
:$L$ is complete lattice.
Thus by definition of complete lattice:
:$L$ is up-complete.
It remains to prove that:
:$L$ satisfies the axiom of $K$-approximation.
Let $x \in \powerset X$.
We will prove that:
:$\forall a \in \powerset X: a$ is upper bound for $x^{\mathrm{compact} } \implies x \preceq a$
Let $a \in \powerset X$ such that:
:$a$ is upper bound for $x^{\mathrm{compact} }$
We will prove that:
:$x \subseteq a$
Let $t \in x$.
By definition of power set:
:$x \subseteq X$
By definitions of subset and singleton:
:$\set t \subseteq X$ and $\set t \subseteq x$
By definition of power set:
:$\set t \in \powerset X$
By Singleton is Finite:
:$\set t$ is finite.
By definition of $\operatorname {Fin}$:
:$\set t \in \map {\operatorname {Fin} } x$
where $\map {\operatorname {Fin} } x$ denotes the set of all finite subset of $x$.
By Compact Closure is Set of Finite Subsets in Lattice of Power Set:
:$\set t \in x^{\mathrm{compact} }$
By definition of upper bound:
:$\set t \preceq a$
By definition of $\preceq$:
:$\set t \subseteq a$
Thus by definitions of subset and singleton:
:$t \in a$
{{qed|lemma}}
Thus by definition of $\preceq$:
:$x \preceq a$
{{qed|lemma}}
By definition of compact closure:
:$\forall y \in x^{\mathrm{compact} }: y \preceq x$
By definition of upper bound:
:$x$ is upper bound for $x^{\mathrm{compact} }$
Thus by definition of supremum:
:$x = \map \sup {x^{\mathrm{compact} } }$
{{qed}}
Theorem: Difference of Squares of Sum and Difference

:$\forall a, b \in \R: \paren {a + b}^2 - \paren {a - b}^2 = 4 a b$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = \left({a + b}\right)^2 - \left({a - b}\right)^2
      | c = 
}}
{{eqn | r = \left({a^2 + 2 a b + b^2}\right) - \left({a^2 - 2 a b + b^2}\right)
      | c = Square of Sum and Square of Difference
}}
{{eqn | r = a^2 + 2 a b + b^2 - a^2 + 2 a b - b^2
      | c = 
}}
{{eqn | r = 2 a b + 2 a b
}}
{{eqn | r = 4 a b
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Non-Empty Compact Closure is Directed

Let $L = \left({S, \vee, \preceq}\right)$ be a join semilattice.
Let $x \in S$ such that
:$x^{\mathrm{compact} }$ is a non-empty set,
where $x^{\mathrm{compact} }$ denotes the compact closure of $x$.
Then :$x^{\mathrm{compact} }$ is directed.

Proof:
Thus by assumption:
:$x^{\mathrm{compact} }$ is a non-empty set.
Let $y, z \in x^{\mathrm{compact} }$.
By definition of compact closure:
:$y \preceq x$, $z \preceq x$, and $y$ and $z$ are compact.
By definition of compact element:
:$y \ll y$ and $z \ll z$
where $\ll$ denotes the way below relation.
By Way Below is Congruent for Join:
:$y \vee z \ll y \vee z$
By definition:
:$y \vee z$ is a compact element
By definition of supremum:
:$y \vee z \preceq x$
Thus by definition of compact closure:
:$y \vee z \in x^{\mathrm{compact} }$
Thus by Join Succeeds Operands:
:$y \preceq y \vee z$ and $z \preceq y \vee z$
{{qed}}
Theorem: Set of Cardinality not Greater than Cardinality of Finite Set is Finite

Let $X, Y$ be sets such that
:$\card X \le \card Y$
and
:$Y$ is finite,
where $\card X$ denotes the cardinality of $X$.
Then $X$ is finite.

Proof:
By Finite iff Cardinality Less than Aleph Zero:
:$\card Y < \aleph_0$
Then
:$\card X < \aleph_0$
Thus by Finite iff Cardinality Less than Aleph Zero:
:$X$ is a finite set.
{{qed}}
Theorem: Finite iff Cardinality Less than Aleph Zero

Let $X$ be a set.
Then $X$ is finite {{iff}} $\card X < \aleph_0$
where:
:$\card X$ denotes the cardinality of $X$
:$\aleph_0 = \card \N$ by Aleph Zero equals Cardinality of Naturals.

Proof:
=== Sufficient Condition ===
Let $X$ be finite.
By definition of finite set:
:$\exists n \in \N: X \sim \N_n$
where:
:$\sim$ denotes the set equivalence
:$\N_n$ denotes the initial segment of natural numbers less than $n$.
By the von Neumann construction of natural numbers:
:$\N_n = n$
By definition of cardinality:
:$\card X = n$
By the von Neumann construction of natural numbers:
:$\forall i \in \N: i \subseteq \N$
Then:
:$n + 1 \subseteq \N$
By Subset implies Cardinal Inequality:
:$n + 1 = \card {n + 1} \le \card \N = \aleph_0$
Also:
:$n < n + 1$
Thus:
:$\card X < \aleph_0$
{{qed|lemma}}
Theorem: P-adic Valuation of Difference of Powers with Coprime Exponent

Let $x, y \in \Z$ be distinct integers.
Let $n \ge 1$ be a natural number.
Let $p$ be a prime number.
Let:
:$p \divides x - y$
and:
:$p \nmid x y n$.
Then 
:$\map {\nu_p} {x^n - y^n} = \map {\nu_p} {x - y}$

Proof:
From Difference of Two Powers:
:$x^n - y^n = \paren {x - y} \paren {x^{n - 1} + \cdots + y^{n - 1} }$
We have to show that:
:$p \nmid x^{n - 1} + \cdots + y^{n - 1}$
Because $x \equiv y \pmod p$:
:$x^{n - 1} + \cdots + y^{n - 1} \equiv x^{n - 1} + x^{n - 1} + \cdots + x^{n - 1} = n x^{n - 1} \pmod p$
Because $p \nmid x$ and $p \nmid n$:
:$p \nmid n x^{n - 1}$
{{qed}}
Theorem: P-adic Valuation of Difference of Powers with Coprime Exponent

Let $x, y \in \Z$ be distinct integers.
Let $n \ge 1$ be a natural number.
Let $p$ be a prime number.
Let:
:$p \divides x - y$
and:
:$p \nmid x y n$.
Then 
:$\map {\nu_p} {x^n - y^n} = \map {\nu_p} {x - y}$

Proof:
From Difference of Two Powers:
:$x^n - y^n = \paren {x - y} \paren {x^{n - 1} + \cdots + y^{n - 1} }$
We have to prove that:
:$p \nmid x^{n - 1} + \cdots + y^{n - 1}$
Let $\map P u = u^n - y^n$.
If $p \divides x^{n - 1} + \cdots + y^{n - 1}$, then $x$ would be a double root of $P$ modulo $p$.
By Double Root of Polynomial is Root of Derivative (or a version of this in modular arithmetic):
:$p \divides \map {P'} x = n x^{n - 1}$
which is impossible.
Therefore:
:$p \nmid x^{n - 1} + \cdots + y^{n - 1}$
{{finish}}
Theorem: Fundamental Theorem of Line Integrals

Let $\CC$ be a smooth curve given by the vector function $\map {\mathbf r} t$ for $a \le t \le b$.
Let $f$ be a differentiable function of two or three variables whose gradient vector $\nabla f$ is continuous on $\CC$.
Then:
:$\ds \int_\CC \nabla f \cdot d \mathbf r = \map f {\map {\mathbf r} b} - \map f {\map {\mathbf r} a}$

Proof:
{{begin-eqn}}
{{eqn | l = \int_\CC \nabla f \cdot \rd \mathbf r
      | r = \int_a^b \nabla f \cdot \map {\mathbf r'} t \rd t
}}
{{eqn | r = \int_a^b \frac {\partial f} {\partial x} \frac {\rd x} {\rd t} + \frac {\partial f} {\partial y} \frac {\rd y} {\rd t} + \frac {\partial f} {\partial z} \frac {\rd z} {\rd t} \rd t}}
{{eqn | r = \int_a^b \frac \rd {\rd t} \map f {\map {\mathbf r} t} \rd t
      | c = Chain Rule for Real-Valued Functions
}}
{{eqn | r = \map f {\map {\mathbf r} b} - \map f {\map {\mathbf r} a}
      | c = Fundamental Theorem of Calculus
}}
{{end-eqn}}
{{qed}}
Category:Vector Calculus
Category:Fundamental Theorems
r2s8xlo76c5d212l8o5od215ua0ttxl
Theorem: 11 is Only Palindromic Prime with Even Number of Digits

$11$ is the only palindromic prime with an even number of digits when expressed in decimal notation.

Proof:
Let $P$ be a palindromic number with $2 n$ digits:
:$P = \sqbrk {a_{2 n - 1} a_{2 n - 2} \ldots a_2 a_1 a_0}_{10}$
Thus:
:$P = \ds \sum_{j \mathop = 0}^{n - 1} a_j + 10^{2 n - 1 - j}$
Consider the summation:
:$S = \ds \sum_{k \mathop = 0}^{2 n - 1} \paren {-1}^k a_k$
As $a_k = a_{2 n - 1 - k}$ we have:
{{begin-eqn}}
{{eqn | l = S
      | r = \sum_{k \mathop = 0}^{n - 1} \paren {-1}^k a_k + \paren {-1}^{2 n - 1 - k} a_k
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 0}^{n - 1} a_k \paren {\paren {-1}^k + \paren {-1}^{2 n - 1 - k} }
      | c = 
}}
{{end-eqn}}
As $2 n - 1$ is odd, it follows that $k$ and $2 n - 1 - k$ are of opposite parity.
Thus:
:$\paren {-1}^k = -\paren {-1}^{2 n - 1 - k}$
and it follows that:
:$S = 0$
It follows by Divisibility by 11 that $P$ is divisible by $11$.
Thus, except for $11$ itself, a palindromic number with an even number of digits cannot be prime.
The result follows.
{{qed}}
Theorem: Ratio of Consecutive Lucas Numbers

For $n \in \N$, let $L_n$ be the $n$th Lucas number.
Then:
:$\ds \lim_{n \mathop \to \infty} \frac {L_{n + 1} } {L_n} = \phi$
where $\phi = \dfrac {1 + \sqrt 5} 2$ is the golden mean.

Proof:
{{begin-eqn}}
{{eqn | l = \lim_{n \mathop \to \infty} \frac {L_{n + 1} } {L_n}
      | r = \lim_{n \mathop \to \infty} \frac {\phi^{n + 1} + \paren {-\phi^{-1} }^{n + 1} } {\phi^n + \paren {-\phi^{-1} }^n}
      | c = Closed Form for Lucas Numbers
}}
{{eqn | r = \lim_{n \mathop \to \infty} \frac {\phi - \phi^{-1} \paren {-\phi^{-2} }^n } {1 + \paren {-\phi^{-2} }^n}
      | c = dividing both numerator and denominator by $\phi^n$
}}
{{eqn | r = \frac \phi 1
      | c = Quotient Rule for Limits of Real Functions
}}
{{eqn | r = \phi
}}
{{end-eqn}}
{{qed}}