euclid-primes

For all natural numbers $n$ and $k$: if $0 < k$ and $k \le n$, then $k$ divides $n!$.

Divisibility here is the problem's own definition Opn.Divides: $k$ divides $m$ when $m = k \cdot c$ for some natural number $c$.

The theorem infinitude_of_primes__h2 asserts the following. For every natural number $n$, suppose every natural number $k$ with $0 < k$ and $k \le n$ divides $n!$, where "divides" is Opn.Divides. Under that hypothesis, for every natural number $m$ with $2 \le m$ there exists some $p$ such that $p$ is prime and $p$ divides $m$. Here "prime" is Opn.IsPrime and "divides" is again Opn.Divides.

The hypothesis about $n$ does not mention $m$ or $p$, so the conclusion does not depend on $n$. The file does not write the type of $p$; it is whatever argument type Opn.IsPrime and Opn.Divides take. No gloss of either definition from Defs.IsPrime was provided, so their meanings are taken from their names only. The proof in the file is sorry.

$\displaystyle \forall n\in\mathbb{N}:\ \bigl(\forall k,\ 0<k\le n\Rightarrow k\mid n!\bigr)\Rightarrow\bigl(\forall m\ge 2,\ \exists p,\ p\ \text{prime}\wedge p\mid m\bigr)\Rightarrow\ \forall d,m\in\mathbb{N},\ d\mid m\ \wedge\ d\mid m+1\ \Rightarrow\ d=1$

For every natural number $n$, under the two inherited hypotheses (every $k$ with $0<k\le n$ divides $n!$, and every $m\ge 2$ has a prime divisor; the earlier holes' claims, which the conclusion does not use), any natural number $d$ dividing both $m$ and $m+1$ equals $1$. Divisibility is the problem's own Opn.Divides ($a\mid b$ when $b=a\cdot c$ for some natural $c$), prime is Opn.IsPrime, and $n!$ is Nat.factorial.

$\displaystyle \forall n\in\mathbb{N}:\ \bigl(\forall k,\ 0<k\le n\Rightarrow k\mid n!\bigr)\Rightarrow\bigl(\forall m\ge 2,\ \exists p,\ p\ \text{prime}\wedge p\mid m\bigr)\Rightarrow\bigl(\forall d,m,\ d\mid m\wedge d\mid m+1\Rightarrow d=1\bigr)\Rightarrow\ \forall k\in\mathbb{N},\ 0<k!$

For every natural number $n$, under the three inherited hypotheses (every $k$ with $0<k\le n$ divides $n!$; every $m\ge 2$ has a prime divisor; a common divisor of $m$ and $m+1$ is $1$; the earlier holes' claims, which the conclusion does not use), every factorial $k!$ is positive. Divisibility is the problem's own Opn.Divides, prime is Opn.IsPrime, and the factorial is Mathlib's Nat.factorial.

$\displaystyle \forall\, l\in\operatorname{List}(\mathbb{N})\ \ \exists p\in\mathbb{N}:\quad p\ \text{prime}\ \wedge\ p\notin l$

For every list of natural numbers there is a prime that is not a member of it (Euclid, Elements IX.20). Prime is the problem's own Opn.IsPrime: $2\le p$ and every $d$ with $p=d\cdot c$ for some natural $c$ is $1$ or $p$.

$\displaystyle \forall\, l\in\operatorname{List}(\mathbb{N}),\ \forall x\in l:\quad x\le \sum l$

Every element of a list of natural numbers is at most the sum of the list (List.sum, the empty list summing to $0$). There are no other hypotheses.

$\displaystyle \forall\, l\in\operatorname{List}(\mathbb{N}):\quad \bigl(\forall x\in l,\ x\le \textstyle\sum l\bigr)\ \Rightarrow\ \exists p\in\mathbb{N},\ \textstyle\sum l<p\ \wedge\ p\ \text{prime}$

For every list of natural numbers, under the inherited hypothesis that each of its entries is at most its sum (the earlier hole's claim), there is a prime strictly greater than the sum of the list (List.sum). Prime is the problem's own Opn.IsPrime: $2\le p$ and every $d$ with $p=d\cdot c$ for some natural $c$ is $1$ or $p$.

$\displaystyle \forall n\in\mathbb{N}\ \ \exists p\in\mathbb{N}:\quad n<p\ \wedge\ p\le n!+1\ \wedge\ p\ \text{prime}$

For every natural number $n$ there is a prime $p$ with $n<p\le n!+1$, where $n!$ is Mathlib's Nat.factorial. Prime is the problem's own Opn.IsPrime: $2\le p$ and every $d$ with $p=d\cdot c$ for some natural $c$ is $1$ or $p$.

$\displaystyle \forall n\in\mathbb{N}\ \ \exists p\in\mathbb{N}:\quad n<p\ \wedge\ \bigl(\exists k\in\mathbb{N},\ p=100+k\bigr)\ \wedge\ p\ \text{prime}$

For every natural number $n$ there is a prime $p>n$ that is at least $100$, the bound being written as "$p=100+k$ for some natural number $k$" rather than as $100\le p$. Prime is the problem's own Opn.IsPrime: $2\le p$ and every $d$ with $p=d\cdot c$ for some natural $c$ is $1$ or $p$.

$\displaystyle \forall n\in\mathbb{N}\ \ \exists p\in\mathbb{N}:\quad n<p\ \wedge\ 100\le p\ \wedge\ p\ \text{prime}$

For every natural number $n$ there is a prime $p$ with $p>n$ and $p\ge 100$. Prime is the problem's own Opn.IsPrime: $2\le p$ and every $d$ with $p=d\cdot c$ for some natural $c$ is $1$ or $p$.

$\displaystyle \forall n\in\mathbb{N}\ \ \exists p\in\mathbb{N}:\quad n<p\ \wedge\ p\ \text{prime}\ \wedge\ p \bmod 4 = 3$

For every natural number $n$ there is a prime $p>n$ whose remainder on division by $4$ is $3$ (Lean's p % 4 = 3). Prime is the problem's own Opn.IsPrime: $2\le p$ and every $d$ with $p=d\cdot c$ for some natural $c$ is $1$ or $p$.

$\displaystyle \{\,p\in\mathbb{N}\ :\ p\ \text{prime}\,\}\ \text{is infinite}$

The set of natural numbers that are prime is infinite, in Mathlib's sense Set.Infinite (not a finite set). Prime is the problem's own Opn.IsPrime: $2\le p$ and every $d$ with $p=d\cdot c$ for some natural $c$ is $1$ or $p$.