Primes just above factorials and primorials

TheoremPrime gaps near \(n!\), general form#✓fully proved

Let \(n\), \(p\) and \(r\) be natural numbers such that every prime \(q > n\) satisfies \(q \ge r\). If \(p\) is a prime with \(n! + 1 < p < n! + r^2\), then \(p - n!\) is prime.

theorem prime_gap_factorial_general
    (n p r : ℕ) (hrmin : ∀ q : ℕ, q.Prime → n < q → r ≤ q)
    (hp : p.Prime) (hlo : Nat.factorial n + 1 < p)
    (hhi : p < Nat.factorial n + r ^ 2) :
    (p - Nat.factorial n).Prime

Used by 1

Used byPrime gaps near \(n!\)

TheoremPrime gaps near \(n!\)#✓fully proved

Let \(n\) be a natural number and let \(r\) be the smallest prime greater than \(n\). If \(p\) is a prime with \(n! + 1 < p < n! + r^2\), then \(p - n!\) is prime.

The source's proof: if \(p - n!\) were composite, its least prime factor \(m\) would satisfy \(m^2 \le p - n! < r^2\), so \(m < r\) and hence \(m \le n\). Then \(m\) divides \(n!\) and therefore \(p\), contradicting \(p > n! + 1\).

theorem prime_gap_factorial
    (n p r : ℕ)
    (hr : r.Prime) (hrn : n < r) (hrmin : ∀ q : ℕ, q.Prime → n < q → r ≤ q)
    (hp : p.Prime) (hlo : Nat.factorial n + 1 < p)
    (hhi : p < Nat.factorial n + r ^ 2) :
    (p - Nat.factorial n).Prime

Sources

• Antonín Čejchan, Michal Křížek, and Lawrence Somer, "On Remarkable Properties of Primes Near Factorials and Primorials," Journal of Integer Sequences 25 (2022), Article 22.1.4, Theorem, lines 153–159, https://cs.uwaterloo.ca/journals/JIS/VOL25/Krizek/krizek3.tex

Uses 1

Proof usesPrime gaps near \(n!\), general form

TheoremPrimes just above a primorial, general form#✓fully proved

Let \(q\) and \(r\) be natural numbers such that no prime \(s\) satisfies \(q < s < r\), and let \(q\#\) be the primorial of \(q\), the product of all primes at most \(q\). If \(p\) is a prime with \(q\# + 1 < p < q\# + r^2\), then \(p - q\#\) is prime.

Neither \(q\) nor \(r\) needs to be prime, and \(q < r\) is not assumed.

theorem prime_sub_primorial_prime_of_between_consecutive_primes_general
    {q r p : ℕ}
    (hconsecutive : ∀ s : ℕ, q < s → s < r → ¬ Nat.Prime s)
    (hp : Nat.Prime p)
    (hlower : primorial q + 1 < p)
    (hupper : p < primorial q + r ^ 2) :
    Nat.Prime (p - primorial q)

Used by 2

Used byPrimes just above a primorial, for a consecutive-prime pair · Primes just above a primorial (Čejchan–Křížek–Somer)

TheoremPrimes just above a primorial (Čejchan–Křížek–Somer)#✓fully proved

Let \(q < r\) be consecutive primes, so that no prime lies strictly between them, and let \(q\#\) be the primorial of \(q\), the product of all primes at most \(q\). If \(p\) is a prime with \(q\# + 1 < p < q\# + r^2\), then \(p - q\#\) is prime.

theorem prime_sub_primorial_prime_of_between_consecutive_primes
    {q r p : ℕ}
    (hq : Nat.Prime q)
    (hr : Nat.Prime r)
    (hqr : q < r)
    (hconsecutive : ∀ s : ℕ, q < s → s < r → ¬ Nat.Prime s)
    (hp : Nat.Prime p)
    (hlower : primorial q + 1 < p)
    (hupper : p < primorial q + r ^ 2) :
    Nat.Prime (p - primorial q)

Sources

• Antonín Čejchan, Michal Křížek, and Lawrence Somer, "On Remarkable Properties of Primes Near Factorials and Primorials," Journal of Integer Sequences 25 (2022), Article 22.1.4, Theorem, lines 471–477, https://cs.uwaterloo.ca/journals/JIS/VOL25/Krizek/krizek3.tex It follows from prime_sub_primorial_prime_of_between_consecutive_primes_general; the hypotheses hq, hr and hqr are unused and keep the source's shape.

Uses 1

Proof usesPrimes just above a primorial, general form

TheoremPrimes just above a primorial, for a consecutive-prime pair#✓fully proved

Let \(q < r\) be consecutive primes and let \(q\#\) be the primorial of \(q\), the product of all primes at most \(q\). If \(p\) is a prime with \(q\# + 1 < p < q\# + r^2\), then \(p - q\#\) is prime.

theorem AreConsecutivePrimes.prime_sub_primorial_prime {q r p : ℕ}
    (hqr : AreConsecutivePrimes q r) (hp : Nat.Prime p)
    (hlower : primorial q + 1 < p) (hupper : p < primorial q + r ^ 2) :
    Nat.Prime (p - primorial q)

Uses 2

Statement usesConsecutive primes

Proof usesPrimes just above a primorial, general form

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.