9.4. Escaping every finite set🔗

Theorem9.4.1

Statement uses 2

Statement dependency previews

Preview

Theorem 9.2.1

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

used by 1✓L∃∀N

Finite-set escape. For every finite set S\subset\mathbb{N}, there is a prime p\notin S such that p is not regular.

Theorem 9.3.2 Theorem 9.2.1

Lean code for Theorem9.4.1●1 theorem

theoremdefined in BernoulliRegular/IrregularPrimes/Infinitude.lean

complete

theorem BernoulliRegular.exists_not_isRegularPrime_not_mem_carlitz
  (S : Finset ℕ) : ∃ p, ∃ (_ : Nat.Prime p), ¬IsRegularPrime p ∧ p ∉ S

theorem BernoulliRegular.exists_not_isRegularPrime_not_mem_carlitz
  (S : Finset ℕ) :
  ∃ p,
    ∃ (_ : Nat.Prime p),
      ¬IsRegularPrime p ∧ p ∉ S

Carlitz finite-set contradiction.

Proof for Theorem 9.4.1

uses 0

Apply Theorem 9.3.2 to S, obtaining a prime p\notin S and a positive even M with p\mid\operatorname{num}\left(\frac{B_M}{M}\right). The same theorem gives p\ne 2. Therefore the Carlitz divisor criterion Theorem 9.2.1 applies and proves that p is not regular.