avewright/proofwiki-math huggingface dataset:
Theorem: Decomposition into Product of Power of 2 and Odd Integer is Unique

Let $n \in \Z$ be an integer.
Then $n$ can be decomposed into the product of a power of $2$ and an odd integer.

Proof:
{{AimForCont}} there exists $n \in \Z$ which can be decomposed into a power of $2$ and an odd integer in more than one way.
That is:
:$n = 2^a r$
and:
:$n = 2^b s$
where:
:$a, b \in \Z_{\ge 0}$
:$r$ and $s$ are odd integers.
:either $a \ne b$ or $r \ne s$.
Suppose $r = s$.
Then:
:$\dfrac n r = \dfrac n s = 2^a = 2^b$
which leads to:
:$a = b$
which contradicts our supposition that either $r \ne s$ or $a \ne b$.
Similarly, suppose $a = b$.
Then:
:$\dfrac n {2^a} = \dfrac n {2^b} = r = s$
which also contradicts our supposition that either $r \ne s$ or $a \ne b$.
Thus both $r \ne s$ and $a \ne b$.
{{WLOG}}, let $a > b$.
Then $2^{a - b} = 2^c$ where $c \ge 1$.
Thus:
:$\dfrac n {2^b} = 2^c r = s$
which means $s = 2 u$ for some $u \in \Z$.
Thus $s$ is an even integer.
This contradicts our supposition that $r$ and $s$ are both odd.
All possibilities have been investigated:
:$a = b, r \ne s$
:$a \ne b, r = s$
:$a \ne b, r \ne s$
All have been shown to lead to a contradiction.
Thus by Proof by Contradiction it can be seen that an decomposition of $n$ into the product of a power of $2$ and an odd integer is unique.
Hence the result.
{{qed}}
Theorem: Prime Decomposition of Integer is Unique

Let $n$ be an integer such that $n > 1$.
Then the prime decomposition of $n$ is unique.

Proof:
From Integer is Expressible as Product of Primes, $n$ can be expressed as the product of one or more primes.
Let $n = q_1 q_2 \dotsm q_s$ where $q_1, q_2, \ldots, q_s$ are all primes such that:
:$(1): \quad n = q_1 \le q_2 \le \dotsb \le q_s$
From Expression for Integer as Product of Primes is Unique, the expression for $(1)$ is unique.
By the Fundamental Theorem of Equivalence Relations, we can partition $\set {q_1, q_2, \dotsc, q_s}$ in $(1)$ according to equality.
Thus the equivalence classes $\eqclass {q_j} =$ contain all repetitions of $q_j$.
Hence the contribution of $q_j$ to $n$ is:
:${q_j}^{k_j}$
where $k_j = \card {\eqclass {q_j} =}$, the cardinality of $\eqclass {q_j} =$.
Renaming the representative elements of the various $\eqclass {q_r} =$ as $p_1, p_2, \ldots, p_r$, where $r$ is the number of equivalence classes.
Hence:
:$n = {p_1}^{k_1} {p_2}^{k_2} \dotsm {p_r}^{k_r}$
As $n = q_1 \le q_2 \le \dotsb \le q_s$ is a unique representation, so is $n = {p_1}^{k_1} {p_2}^{k_2} \dotsm {p_r}^{k_r}$.
{{qed}}
Theorem: Expression for Integers as Powers of Same Primes

Let $a, b \in \Z$ be integers.
Let their prime decompositions be given by:
{{begin-eqn}}
{{eqn | l = a
      | r = {q_1}^{e_1} {q_2}^{e_2} \cdots {q_r}^{e_r}
}}
{{eqn | r = \prod_{\substack {q_i \mathop \divides a \\ \text {$q_i$ is prime} } } {q_i}^{e_i}
}}
{{eqn | l = b
      | r = {s_1}^{f_1} {s_2}^{f_2} \cdots {s_u}^{f_u}
}}
{{eqn | r = \prod_{\substack {s_i \mathop \divides b \\ \text {$s_i$ is prime} } } {s_i}^{f_i}
}}
{{end-eqn}}
Then there exist prime numbers:
:$t_1 < t_2 < \dotsb < t_v$
such that:
{{begin-eqn}}
{{eqn | n = 1
      | l = a
      | r = {t_1}^{g_1} {t_2}^{g_2} \cdots {t_v}^{g_v}
}}
{{eqn | n = 2
      | l = b
      | r = {t_1}^{h_1} {t_2}^{h_2} \cdots {t_v}^{h_v}
}}
{{end-eqn}}

Proof:
In the prime decompositions $(1)$ and $(2)$, we have that:
:$q_1 < q_2 < \dotsb < q_r$
and:
:$s_1 < s_2 < \dotsb < s_u$
Hence we can define:
{{begin-eqn}}
{{eqn | l = E
      | r = \set {q_1, q_2, \ldots, q_r}
}}
{{eqn | l = F
      | r = \set {s_1, s_2, \ldots, s_u}
}}
{{end-eqn}}
as all the $q_1, q_2, \dotsc, q_r$ are distinct, and all the $s_1, s_2, \dotsc, s_u$ are distinct.
Then let:
:$T = E \cup F$
and let the elements of $T$ be renamed as:
:$T = \set {t_1, t_2, \ldots, t_v}$
where all the $t_1, t_2, \dotsc, t_v$ are distinct, and:
:$t_1 < t_2 < \dotsb < t_v$
Let $\iota: E \to T$ be the inclusion mapping:
:$\forall q_i \in E: \map \iota {q_i} = q_i$
Let $\iota: F \to T$ be the inclusion mapping:
:$\forall s_i \in F: \map \iota {s_i} = s_i$
Then we have that:
{{begin-eqn}}
{{eqn | l = a
      | r = \prod_{i \mathop = 1}^r {q_i}^{e_i}
      | c = 
}}
{{eqn | r = \prod_{q_i \mathop \in E} {q_i}^{e_i} \times \prod_{t_i \mathop \in T \mathop \setminus E} {t_i}^0
      | c = 
}}
{{eqn | r = \prod_{t_j \mathop \in T} {t_j}^{g_j}
      | c = where $g_j = \begin {cases} e_i & : t_j = q_i \\ 0 & : t_j \notin E \end{cases}$
}}
{{eqn | r = {t_1}^{g_1} {t_2}^{g_2} \dotsm {t_v}^{g_v} 
      | c = for some $g_1, g_2, \dotsc, g_v \in \Z_{\ge 0}$
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = b
      | r = \prod_{i \mathop = 1}^r {s_i}^{f_i}
      | c = 
}}
{{eqn | r = \prod_{s_i \mathop \in F} {s_i}^{f_i} \times \prod_{t_i \mathop \in T \mathop \setminus F} {t_i}^0
      | c = 
}}
{{eqn | r = \prod_{t_j \mathop \in T} {t_j}^{h_j}
      | c = where $h_j = \begin {cases} f_i & : t_j = s_i \\ 0 & : t_j \notin F \end{cases}$
}}
{{eqn | r = {t_1}^{h_1} {t_2}^{h_2} \dotsm {t_v}^{h_v} 
      | c = for some $h_1, h_2, \dotsc, h_v \in \Z_{\ge 0}$
}}
{{end-eqn}}
Thus $a$ and $b$ can be expressed as the product of powers of the same primes, on the understanding that one or more of the powers in either product may be zero.
{{qed}}
Theorem: Expression for Integers as Powers of Same Primes/General Result

Let $a_1, a_2, \dotsc, a_n \in \Z$ be integers.
Let their prime decompositions be given by:
:$\ds a_i = \prod_{\substack {p_{i j} \mathop \divides a_i \\ \text {$p_{i j}$ is prime} } } {p_{i j} }^{e_{i j} }$
Then there exists a set $T$ of prime numbers:
:$T = \set {t_1, t_2, \dotsc, t_v}$
such that:
:$t_1 < t_2 < \dotsb < t_v$
:$\ds a_i = \prod_{j \mathop = 1}^v {t_j}^{g_{i j} }$

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 2}$, let $\map P n$ be the proposition:
:for all $a_i \in \set {a_1, a_2, \ldots, a_n}$: there exists a set $T = \set {t_1, t_2, \dotsc, t_v}$ of prime numbers such that $t_1 < t_2 < \dotsb < t_v$ such that:
::$\ds a_i = \prod_{j \mathop = 1}^v {t_j}^{g_{i j} }$
Theorem: GCD from Prime Decomposition/General Result

Let $n \in \N$ be a natural number such that $n \ge 2$.
Let $\N_n$ be defined as:
:$\N_n := \set {1, 2, \dotsc, n}$
Let $A_n = \set {a_1, a_2, \dotsc, a_n} \subseteq \Z$ be a set of $n$ integers.
From Expression for Integers as Powers of Same Primes, let:
:$\ds \forall i \in \N_n: a_i = \prod_{p_j \mathop \in T} {p_j}^{e_{i j} }$
where:
:$T = \set {p_j: j \in \N_r}$
such that:
:$\forall j \in \N_{r - 1}: p_j < p_{j - 1}$
:$\forall j \in \N_r: \exists i \in \N_n: p_j \divides a_i$
where $\divides$ denotes divisibility.
Then:
:$\ds \map \gcd {A_n} = \prod_{j \mathop \in \N_r} {p_j}^{\min \set {e_{i j}: \, i \in \N_n} }$
where $\map \gcd {A_n}$ denotes the greatest common divisor of $A_n$.

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\ds \map \gcd {A_n} = \prod_{j \mathop \in \N_r} {p_j}^{\min \set {e_{i j}: \, i \in \N_n} }$
=== Basis for the Induction ===
$\map P 2$ is the case:
:$\ds \gcd \set {a_1, a_2} = \prod_{j \mathop \in \N_r} {p_j}^{\min \set {e_{1 j}, e_{2 j} } }$
This is GCD from Prime Decomposition.
Thus $\map P 2$ is seen to hold.
This is the basis for the induction.
=== Induction Hypothesis ===
Now it needs to be shown that, if $\map P k$ is true, where $k \ge 1$, then it logically follows that $\map P {k + 1}$ is true.
So this is the induction hypothesis:
:$\ds \map \gcd {A_k} = \prod_{j \mathop \in \N_r} {p_j}^{\min \set {e_{i j}: \, i \in \N_k} }$
from which it is to be shown that:
:$\ds \map \gcd {A_{k + 1} } = \prod_{j \mathop \in \N_r} {p_j}^{\min \set {e_{i j}: \, i \in \N_{k + 1} } }$
=== Induction Step ===
This is the induction step:
{{begin-eqn}}
{{eqn | l = \map \gcd {A_{k + 1} }
      | r = \map \gcd {A_k \cup a_{k + 1} }
      | c = 
}}
{{eqn | r = 
      | c = 
}}
{{end-eqn}}
{{finish|I think we need to prove $\gcd \set {a, b, c} {{=}} \gcd \set {\gcd \set {a, b}, c}$ }}
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\forall n \in \Z_{\ge 2}: \ds \map \gcd {A_n} = \prod_{j \mathop \in \N_r} {p_j}^{\min \set {e_{i j}: i \in \N_n} }$
Theorem: LCM from Prime Decomposition/General Result

Let $n \in \N$ be a natural number such that $n \ge 2$.
Let $\N_n$ be defined as:
:$\N_n := \set {1, 2, \dotsc, n}$
Let $A_n = \set {a_1, a_2, \dotsc, a_n} \subseteq \Z$ be a set of $n$ integers.
From Expression for Integers as Powers of Same Primes, let:
:$\ds \forall i \in \N_n: a_i = \prod_{p_j \mathop \in T} {p_j}^{e_{i j} }$
where:
:$T = \set {p_j: j \in \N_r}$
such that:
:$\forall j \in \N_{r - 1}: p_j < p_{j - 1}$
:$\forall j \in \N_r: \exists i \in \N_n: p_j \divides a_i$
where $\divides$ denotes divisibility.
Then:
:$\ds \map \lcm {A_n} = \prod_{j \mathop \in \N_r} {p_j}^{\max \set {e_{i j}: \, i \in \N_n} }$
where $\map \lcm {A_n}$ denotes the greatest common divisor of $a_1, a_2, \dotsc, a_n$.

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\ds \map \lcm {A_n} = \prod_{j \mathop \in \N_r} {p_j}^{\max \set {e_{i j}: \, i \in \N_n} }$
Theorem: LCM of 3 Integers in terms of GCDs of Pairs of those Integers

Let $a, b, c \in \Z_{>0}$ be strictly positive integers.
Then:
:$\lcm \set {a, b, c} = \dfrac {a b c \gcd \set {a, b, c} } {d_1 d_2 d_3}$
where:
:$\gcd$ denotes greatest common divisor
:$\lcm$ denotes lowest common multiple
:$d_1 = \gcd \set {a, b}$
:$d_2 = \gcd \set {b, c}$
:$d_3 = \gcd \set {a, c}$

Proof:
{{begin-eqn}}
{{eqn | l = \lcm \set {a, b, c}
      | r = \lcm \set {a, \lcm \set {b, c} }
}}
{{eqn | r = \frac {a \lcm \set {b, c} } {\gcd \set {a, \lcm \set {b, c} } }
      | c = Product of GCD and LCM
}}
{{eqn | r = \frac {a b c} {\gcd \set {b, c} } \paren {\frac 1 {\gcd \set {a, \lcm \set {b, c} } } }
      | c = Product of GCD and LCM
}}
{{eqn | r = \frac {a b c} {\gcd \set {b, c} } \paren {\frac 1 {\lcm \set {\gcd \set {a, b}, \gcd \set {a, c} } } }
      | c = GCD and LCM Distribute Over Each Other
}}
{{eqn | r = \frac {a b c} {\gcd \set {b, c} } \paren {\frac {\gcd \set {\gcd \set {a, b}, \gcd \set {a, c} } } {\gcd \set {a, b} \gcd \set {a, c} } }
      | c = Product of GCD and LCM
}}
{{eqn | r = \frac {a b c \gcd \set {a, b, c} } {d_1 d_2 d_3}
      | c = by Lemma
}}
{{end-eqn}}
{{qed}}
Theorem: Alternating Summation of Binomial Coefficient of Summation of Binomial Coefficient of Sequence

Let $\sequence a, \sequence b$ be real sequences which satisfy the condition:
:$a_n = \ds \sum_{r \mathop = 0}^n \binom n r b_r$
Then:
:$\ds \paren {-1}^n b_n = \sum_{s \mathop = 0}^n \binom n s \paren {-1}^s a_s$

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{s \mathop = 0}^n \binom n s \paren {-1}^s a_s
      | r = \sum_{s \mathop = 0}^n \binom n s \paren {-1}^s \paren {\sum_{r \mathop = 0}^s \binom s r b_r}
      | c = 
}}
{{eqn | r = \sum_{s \mathop = 0}^n \sum_{\substack {r \mathop \le 0 \mathop \le n \\ s \mathop \ge r} } \binom n s \binom s r \paren {-1}^s b_r
      | c = 
}}
{{eqn | r = \sum_{r \mathop = 0}^n b_r \sum_{s \mathop = r}^n \dfrac {n!} {s! \, \paren{n - s}!} \dfrac {s!} {r! \, \paren{s - r}!} \paren {-1}^s
      | c = 
}}
{{eqn | r = \sum_{r \mathop = 0}^n \dfrac {n!} {r! \, \paren{n - r}!} b_r \sum_{s \mathop = r}^n \dfrac {\paren{n - r}! \paren {-1}^s} {\paren{n - s}! \paren{s - r}!}
      | c = 
}}
{{eqn | r = \sum_{r \mathop = 0}^n \binom n r b_r \sum_{s \mathop = r}^n \binom {n - r} {s - r} \paren {-1}^s
      | c = 
}}
{{eqn | n = 1
      | r = \sum_{r \mathop = 0}^n \binom n r b_r \sum_{s \mathop = 0}^{n - r} \binom {n - r} s \paren {-1}^{s + r}
      | c = 
}}
{{end-eqn}}
For $n - r > 1$ we can use Binomial Theorem for Integral Index with $x = 1$ and $y = -1$:
:$0 = \paren {1 - 1}^{n - r} = \ds \sum_{s \mathop = 0}^{n \mathop - r} \binom {n - r} s \paren {-1}^s$
Hence all terms of $(1)$ vanish except for where $n - r$.
That term is:
:$\paren {-1}^n b_n$
{{qed}}
Theorem: Sum of Sequence of Product of Fibonacci Number with Binomial Coefficient

Let $F_n$ denote the $n$th Fibonacci number.
Then:
{{begin-eqn}}
{{eqn | q = \forall n \in \Z_{>0}
      | l = F_{2 n}
      | r = \sum_{k \mathop = 1}^n \dbinom n k F_k
      | c = 
}}
{{eqn | r = \dbinom n 1 F_1 + \dbinom n 2 F_2 + \dbinom n 3 F_3 + \dotsb + \dbinom n {n - 1} F_{n - 1} + \dbinom n n F_n
      | c = 
}}
{{end-eqn}}
where $\dbinom n k$ denotes a binomial coefficient.

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$F_{2 n} = \ds \sum_{k \mathop = 1}^n \dbinom n k F_k$
$\map P 0$ is the case:
{{begin-eqn}}
{{eqn | l = F_0
      | r = 0
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 1}^0 \dbinom 0 k F_k
      | c = vacuously
}}
{{end-eqn}}
Thus $\map P 0$ is seen to hold.
=== Basis for the Induction ===
$\map P 1$ is the case:
{{begin-eqn}}
{{eqn | l = F_2
      | r = 1
      | c = 
}}
{{eqn | r = \dbinom 1 1 F_1
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 1}^1 \dbinom 1 k F_k
      | c = 
}}
{{end-eqn}}
Thus $\map P 1$ is seen to hold.
This is the basis for the induction.
=== Induction Hypothesis ===
Now it needs to be shown that, if $\map P m$ is true, where $m \ge 1$, then it logically follows that $\map P {m + 1}$ is true.
So this is the induction hypothesis:
:$F_{2 m} = \ds \sum_{k \mathop = 1}^m \dbinom m k F_k$
from which it is to be shown that:
:$F_{2 \paren {m + 1} } = \ds \sum_{k \mathop = 1}^{m + 1} \dbinom {m + 1} k F_k$
=== Induction Step ===
This is the induction step:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 1}^{m + 1} \dbinom {m + 1} k F_k
      | r = \sum_{k \mathop = 1}^m \dbinom {m + 1} k F_k + \dbinom {m + 1} {m + 1} F_{m + 1}
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 1}^m \paren {\dbinom m {k - 1} + \dbinom m k} F_k + F_{m + 1}
      | c = Pascal's Rule
}}
{{eqn | r = \sum_{k \mathop = 1}^m \dbinom m {k - 1} F_k  + F_{2 m} + F_{m + 1}
      | c = Induction Hypothesis
}}
{{eqn | r = \sum_{k \mathop = 1}^m \dbinom m {k - 1} \paren {F_{k - 1} + F_{k - 2} } + F_{2 m} + F_{m + 1}
      | c = {{Defof|Fibonacci Numbers}}
}}
{{end-eqn}}
{{finish|Can't see where this is going -- anyone care to have a go at this?}}
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\forall n \in \Z_{\ge 0}: F_{2 n} = \ds \sum_{k \mathop = 1}^n \dbinom n k F_k$
Theorem: Sum of Sequence of Product of Fibonacci Number with Binomial Coefficient

Let $F_n$ denote the $n$th Fibonacci number.
Then:
{{begin-eqn}}
{{eqn | q = \forall n \in \Z_{>0}
      | l = F_{2 n}
      | r = \sum_{k \mathop = 1}^n \dbinom n k F_k
      | c = 
}}
{{eqn | r = \dbinom n 1 F_1 + \dbinom n 2 F_2 + \dbinom n 3 F_3 + \dotsb + \dbinom n {n - 1} F_{n - 1} + \dbinom n n F_n
      | c = 
}}
{{end-eqn}}
where $\dbinom n k$ denotes a binomial coefficient.

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 1}^n \dbinom n k F_k
      | r = \sum_{k \mathop = 1}^n \dbinom n k \paren {\frac {\phi^k - \hat \phi^k} {\sqrt 5} }
      | c = Euler-Binet Formula
}}
{{eqn | r = \frac 1 {\sqrt 5} \paren {\sum_{k \mathop = 1}^n \dbinom n k \phi^k - \sum_{k \mathop = 1}^n \dbinom n k \hat \phi^k}
      | c = Summation is Linear
}}
{{eqn | r = \frac 1 {\sqrt 5} \paren {\sum_{k \mathop = 0}^n \dbinom n k \phi^k 1^{n - k} - \sum_{k \mathop = 0}^n \dbinom n k \hat \phi^k 1^{n - k} }
      | c = Binomial Coefficient with Zero
}}
{{eqn | r = \frac 1 {\sqrt 5} \paren {\paren {1 + \phi}^n - \paren {1 + \hat \phi}^n}
      | c = Binomial Theorem
}}
{{eqn | r = \frac 1 {\sqrt 5} \paren {\paren {\phi^2}^n - \paren {\hat \phi^2}^n}
      | c = Golden Mean as Root of Quadratic $x^2 = x + 1$
}}
{{eqn | r = F_{2 n}
      | c = Euler-Binet Formula
}}
{{end-eqn}}
{{qed}}
Theorem: Integer and Fifth Power have same Last Digit

Let $n \in \Z$ be an integer.
Then $n^5$ has the same last digit as $n$ when both are expressed in conventional decimal notation.

Proof:
It suffices to check $10$ digit cases:
{{explain|what does the above line mean?}}
{{begin-eqn}}
{{eqn | l = 0^5 = 0 \times 0 \times 0 \times 0 \times 0
      | r = 0
      | rr= \equiv 0 \pmod {10}
      | c = 
}}
{{eqn | l = 1^5 = 1 \times 1 \times 1 \times 1 \times 1
      | r = 1
      | rr= \equiv 1 \pmod {10}
      | c = 
}}
{{eqn | l = 2^5 = 2 \times 2 \times 2 \times 2 \times 2
      | r = 32
      | rr= \equiv 2 \pmod {10}
      | c = 
}}
{{eqn | l = 3^5 = 3 \times 3 \times 3 \times 3 \times 3
      | r = 243
      | rr= \equiv 3 \pmod {10}
      | c = 
}}
{{eqn | l = 4^5 = 4 \times 4 \times 4 \times 4 \times 4
      | r = 1024
      | rr= \equiv 4 \pmod {10}
      | c = 
}}
{{eqn | l = 5^5 = 5 \times 5 \times 5 \times 5 \times 5
      | r = 3125
      | rr= \equiv 5 \pmod {10}
      | c = 
}}
{{eqn | l = 6^5 = 6 \times 6 \times 6 \times 6 \times 6
      | r = 7776
      | rr= \equiv 6 \pmod {10}
      | c = 
}}
{{eqn | l = 7^5 = 7 \times 7 \times 7 \times 7 \times 7
      | r = 16 \, 807
      | rr= \equiv 7 \pmod {10}
      | c = 
}}
{{eqn | l = 8^5 = 8 \times 8 \times 8 \times 8 \times 8
      | r = 32 \, 768
      | rr= \equiv 8 \pmod {10}
      | c = 
}}
{{eqn | l = 9^5 = 9 \times 9 \times 9 \times 9 \times 9
      | r = 59 \, 049
      | rr= \equiv 9 \pmod {10}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Sufficient Condition for 5 to divide n^2+1

Let:
{{begin-eqn}}
{{eqn | l = 5
      | o = \nmid
      | r = n - 1
}}
{{eqn | l = 5
      | o = \nmid
      | r = n
}}
{{eqn | l = 5
      | o = \nmid
      | r = n + 1
}}
{{end-eqn}}
where $\nmid$ denotes non-divisibility.
Then:
:$5 \divides n^2 + 1$
where $\divides$ denotes divisibility.

Proof:
We have that:
{{begin-eqn}}
{{eqn | l = 5
      | o = \nmid
      | r = n - 1
}}
{{eqn | ll= \leadsto
      | l = n - 1
      | o = \not \equiv
      | r = 0
      | rr= \pmod 5
}}
{{eqn | ll= \leadsto
      | l = n
      | o = \not \equiv
      | r = 1
      | rr= \pmod 5
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = 5
      | o = \nmid
      | r = n
}}
{{eqn | ll= \leadsto
      | l = n
      | o = \not \equiv
      | r = 0
      | rr= \pmod 5
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = 5
      | o = \nmid
      | r = n + 1
}}
{{eqn | ll= \leadsto
      | l = n + 1
      | o = \not \equiv
      | r = 0
      | rr= \pmod 5
}}
{{eqn | ll= \leadsto
      | l = n
      | o = \not \equiv
      | r = 4
      | rr= \pmod 5
}}
{{end-eqn}}
So either:
:$n \equiv 2 \pmod 5$
or:
:$n \equiv 3 \pmod 5$
and so:
{{begin-eqn}}
{{eqn | l = n
      | o = \equiv
      | r = 2
      | rr= \pmod 5
}}
{{eqn | ll= \leadsto
      | l = n^2
      | o = \equiv
      | r = 4
      | rr= \pmod 5
}}
{{eqn | ll= \leadsto
      | l = n^2 + 1
      | o = \equiv
      | r = 0
      | rr= \pmod 5
}}
{{eqn | ll= \leadsto
      | l = 5
      | o = \divides
      | r = n^2 + 1
}}
{{end-eqn}}
or:
{{begin-eqn}}
{{eqn | l = n
      | o = \equiv
      | r = 3
      | rr= \pmod 5
}}
{{eqn | ll= \leadsto
      | l = n^2
      | o = \equiv
      | r = 3^2
      | rr= \pmod 5
}}
{{eqn | o = \equiv
      | r = 4
      | rr= \pmod 5
}}
{{eqn | ll= \leadsto
      | l = n^2 + 1
      | o = \equiv
      | r = 0
      | rr= \pmod 5
}}
{{eqn | ll= \leadsto
      | l = 5
      | o = \divides
      | r = n^2 + 1
}}
{{end-eqn}}
{{qed}}
Theorem: Wilson's Theorem/Necessary Condition

Let $p$ be a prime number.
Then:
:$\paren {p - 1}! \equiv -1 \pmod p$

Proof:
If $p = 2$ the result is obvious.
Therefore we assume that $p$ is an odd prime.
Let $p$ be prime.
Consider $n \in \Z, 1 \le n < p$.
As $p$ is prime, $n \perp p$.
From Law of Inverses (Modulo Arithmetic), we have:
:$\exists n' \in \Z, 1 \le n' < p: n n' \equiv 1 \pmod p$
By Solution of Linear Congruence, for each $n$ there is '''exactly one''' such $n'$, and $\paren {n'}' = n$.
So, provided $n \ne n'$, we can pair any given $n$ from $1$ to $p$ with another $n'$ from $1$ to $p$.
We are then left with the numbers such that $n = n'$.
Then we have $n^2 \equiv 1 \pmod p$.
Consider $n^2 - 1 = \paren {n + 1} \paren {n - 1}$ from Difference of Two Squares.
So either $n + 1 \divides p$ or $n - 1 \divides p$.
Observe that these cases do not occur simultaneously, as their difference is $2$, and $p$ is an odd prime.
From Negative Number is Congruent to Modulus minus Number:
:$p - 1 \equiv -1 \pmod p$
Hence $n = 1$ or $n = p - 1$.
So, we have that $\paren {p - 1}!$ consists of numbers multiplied together as follows:
:in pairs whose product is congruent to $1 \pmod p$
:the numbers $1$ and $p - 1$.
The product of all these numbers is therefore congruent to $1 \times 1 \times \cdots \times 1 \times p - 1 \pmod p$ by modulo multiplication.
From Negative Number is Congruent to Modulus minus Number:
:$\paren {p - 1}! \equiv -1 \pmod p$
{{qed}}
Theorem: Wilson's Theorem/Necessary Condition

Let $p$ be a prime number.
Then:
:$\paren {p - 1}! \equiv -1 \pmod p$

Proof:
If $p = 2$ the result is obvious.
Therefore we assume that $p$ is an odd prime.
Consider $p$ points on the circumference of a circle $C$ dividing it into $p$ equal arcs.
By joining these points in a cycle, we can create polygons, some of them stellated.
From Number of Different n-gons that can be Inscribed in Circle, the number of different such polygons is $\dfrac {\paren {p - 1}!} 2$.
When you rotate these polygons through an angle of $\dfrac {2 \pi} p$, exactly $\dfrac {p - 1} 2$ are unaltered.
These are the regular $p$-gons and regular stellated $p$-gons.
That there are $\dfrac {p - 1} 2$ of them follows from Number of Regular Stellated Odd n-gons.
The remaining $\dfrac {\paren {p - 1}!} 2 - \dfrac {p - 1} 2$ polygons can be partitioned into sets of $p$ elements: those which can be obtained from each other by rotation through multiples of $\dfrac {2 \pi} p$.
{{Explain|Why are there always $p$ of them? See Fermat's Little Theorem/Corollary 1.}}
The total number of such sets is then:
:$\dfrac {\paren {p - 1}! - \paren {p - 1} } {2 p}$
Thus we have that:
:$2 p \divides \paren {\paren {p - 1}! - \paren {p - 1} }$
That is:
:$p \divides \paren {\paren {p - 1}! + 1}$
{{qed}}
Theorem: Wilson's Theorem/Necessary Condition

Let $p$ be a prime number.
Then:
:$\paren {p - 1}! \equiv -1 \pmod p$

Proof:
Let $p$ be prime.
Consider $\struct {\Z_p, +, \times}$, the ring of integers modulo $m$.
From Ring of Integers Modulo Prime is Field, $\struct {\Z_p, +, \times}$ is a field.
Hence, apart from $\eqclass 0 p$, all elements of $\struct {\Z_p, +, \times}$ are units
As $\struct {\Z_p, +, \times}$ is a field, it is also by definition an integral domain, we can apply:
From Product of Units of Integral Domain with Finite Number of Units, the product of all elements of $\struct {\Z_p, +, \times}$ is $-1$.
But the product of all elements of $\struct {\Z_p, +, \times}$ is $\paren {p - 1}!$
The result follows.
{{qed}}
Theorem: Wilson's Theorem/Sufficient Condition

Let $p$ be a (strictly) positive integer such that:
:$\paren {p - 1}! \equiv -1 \pmod p$
Then $p$ is a prime number.

Proof:
Assume $p$ is composite, and $q$ is a prime such that $q \divides p$.
Then both $p$ and $\paren {p - 1}!$ are divisible by $q$.
{{AimForCont}} the congruence $\paren {p - 1}! \equiv -1 \pmod p$ were satisfied.
From Congruence by Divisor of Modulus:
:$\paren {p - 1}! \equiv -1 \pmod q$
However, this amounts to:
:$0 \equiv -1 \pmod q$
which is a contradiction.
Hence for $p$ composite, the congruence $\paren {p - 1}! \equiv -1 \pmod p$ cannot hold.
{{qed}}