Primes of the form 6k − 1

TheoremBreusch's theorem for primes of the form \(6k - 1\)#●ready to prove

For every natural number \(x \ge 7\) there is a prime \(p\) with \(x < p < 2x\) and \(p \equiv 5 \pmod 6\), that is, a prime of the form \(6k - 1\) strictly between \(x\) and \(2x\).

theorem_wanted exists_prime_modEq_five_between (x : ℕ)
    (hx : 7 ≤ x) :
    ∃ p : ℕ, p.Prime ∧ x < p ∧ p < 2 * x ∧ p % 6 = 5

Sources

• Elchin Hasanalizade, "Sums of Distinct Eisenstein Primes", Lemma 2 (citing Breusch).

TheoremMakowski's theorem on sums of distinct primes of the form \(6k - 1\)#●ready to prove

Every natural number \(n > 161\) is the sum of the elements of some finite set of primes \(p\) with \(p \equiv 5 \pmod 6\); that is, \(n\) is a sum of distinct primes of the form \(6k - 1\).

theorem_wanted eq_sum_distinct_primes_modEq_five (n : ℕ)
    (hn : 161 < n) :
    ∃ S : Finset ℕ, (∀ p ∈ S, p.Prime ∧ p % 6 = 5) ∧
      (∑ p ∈ S, p) = n

Sources

• Elchin Hasanalizade, "Sums of Distinct Eisenstein Primes", Lemma 3 (citing Makowski).

2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.