9.5. Infinitude🔗

Theorem9.5.1

uses 1used by 0✓L∃∀N

Infinitely many irregular primes. The set \{p:\mathbb{N} \mid p\text{ is prime and }p\text{ is not regular}\} is infinite.

Theorem 9.4.1

Lean code for Theorem9.5.1●1 theorem

theoremdefined in BernoulliRegular/IrregularPrimes/Infinitude.lean

complete

theorem BernoulliRegular.infinite_not_isRegularPrime :
  {p | ∃ (_ : Nat.Prime p), ¬IsRegularPrime p}.Infinite

theorem BernoulliRegular.infinite_not_isRegularPrime :
  {p |
      ∃ (_ : Nat.Prime p),
        ¬IsRegularPrime p}.Infinite

Infinitely many primes are not regular, by the Carlitz route.

Proof for Theorem 9.5.1

uses 0

Assume the set is finite, and let S be a finite set containing all of its elements. By Theorem 9.4.1, there is a prime p\notin S which is not regular. This contradicts the defining property of S. Hence no finite set covers all irregular primes, so the set is infinite. The finite-set-to-infinite conversion is the elementary lemma that no finite cover implies infinitude infinite_of_forall_finite_set_not_cover.

The checked proof contains no bundled Kummer provider or side-condition package. The only source bridge into irregularity is Kummer's criterion, and the unbounded congruence used by Carlitz is the public theorem Theorem 9.1.1.