Fermat congruence criteria for twin and Sophie Germain primes

TheoremFermat-type characterizations of twin primes#●ready to prove

Let \(n \ge 3\) be odd, and suppose neither \(n\) nor \(n + 2\) is a Carmichael number. Then \(n\) and \(n + 2\) are both prime if and only if \(2a^{n+1} \equiv (n + 2)\,a^2 - n \pmod{n(n + 2)}\) for every integer \(a\) coprime to \(n(n + 2)\); and \(n\) and \(n + 2\) are both prime if and only if \(n\,a^{n+1} \equiv (n + 2)\,a^{n-1} - 2 \pmod{n(n + 2)}\) for every integer \(a\) coprime to \(n(n + 2)\).

public theorem_wanted twinPrime_iff_forall_fermat_congruence {n : ℕ} (hodd : Odd n)
    (hn : 3 ≤ n) (hnc : ¬Nat.IsCarmichaelNumber n) (hn2c : ¬Nat.IsCarmichaelNumber (n + 2)) :
    ((n.Prime ∧ (n + 2).Prime) ↔ ∀ a : ℤ, IsCoprime a ((n : ℤ) * (n + 2)) →
        2 * a ^ (n + 1) ≡ (n + 2) * a ^ 2 - n [ZMOD (n : ℤ) * (n + 2)]) ∧
      ((n.Prime ∧ (n + 2).Prime) ↔ ∀ a : ℤ, IsCoprime a ((n : ℤ) * (n + 2)) →
        n * a ^ (n + 1) ≡ (n + 2) * a ^ (n - 1) - 2 [ZMOD (n : ℤ) * (n + 2)])
Sources
  • Takashi Agoh, A Note on Fermat's Congruence, INTEGERS 25 (2025), Article A31, Theorem 3.1, Congruences (3.2).
Uses 1
Statement usesCarmichael numbers

TheoremAlahmadi–Luca theorem on Carmichael numbers#●ready to prove

For every natural number \(n\) and every odd prime \(p\), the number \(2^n p + 1\) is not a Carmichael number.

public theorem_wanted not_isCarmichaelNumber_two_pow_mul_prime_add_one (n : ℕ) {p : ℕ}
    (hp : p.Prime) (hodd : Odd p) : ¬Nat.IsCarmichaelNumber (2 ^ n * p + 1)
Sources
  • Takashi Agoh, A Note on Fermat's Congruence, INTEGERS 25 (2025), Article A31, Theorem 3.2, quoting A. Alahmadi and F. Luca, C. R. Math. Acad. Sci. Paris 360 (2022).
Uses 1
Statement usesCarmichael numbers

TheoremFermat-type characterizations of Sophie Germain primes#●ready to prove

Let \(p\) be a prime. Then \(p\) is a Sophie Germain prime if and only if \(a^{2p} \equiv (2p + 1)\,a^{p+1} - 2p \pmod{p(2p + 1)}\) for every integer \(a\) coprime to \(p(2p + 1)\); and \(p\) is a Sophie Germain prime if and only if \((2p + 1)\,a^{p-1} \equiv p\,a^{2p} + p + 1 \pmod{p(2p + 1)}\) for every integer \(a\) coprime to \(p(2p + 1)\).

public theorem_wanted isSophieGermainPrime_iff_forall_fermat_congruence {p : ℕ}
    (hp : p.Prime) :
    (Nat.IsSophieGermainPrime p ↔ ∀ a : ℤ, IsCoprime a ((p : ℤ) * (2 * p + 1)) →
        a ^ (2 * p) ≡ (2 * p + 1) * a ^ (p + 1) - 2 * p [ZMOD (p : ℤ) * (2 * p + 1)]) ∧
      (Nat.IsSophieGermainPrime p ↔ ∀ a : ℤ, IsCoprime a ((p : ℤ) * (2 * p + 1)) →
        (2 * p + 1) * a ^ (p - 1) ≡ p * a ^ (2 * p) + p + 1 [ZMOD (p : ℤ) * (2 * p + 1)])
Sources
  • Takashi Agoh, A Note on Fermat's Congruence, INTEGERS 25 (2025), Article A31, Theorem 3.3, Congruences (3.5).
Uses 1
Statement usesSophie Germain primes

TheoremFermat-type congruences along a Sophie Germain prime chain#●ready to prove

Let \(p\) and \(j\) be natural numbers and put \(q_{i+1} = 2^i (p + 1) - 1\) for \(i \ge 0\), so that \(q_1 = p\) and \(q_{i+2} = 2q_{i+1} + 1\). Suppose \(q_1, \dots, q_{j+2}\) are all prime, and write \(q = q_{j+1}\) and \(q' = q_{j+2} = 2q + 1\). Then for every integer \(a\) coprime to \(qq'\), \(a^{q'-1} \equiv q'\,a^{q+1} - 2q \pmod{qq'}\) and \(q'\,a^{q-1} \equiv q\,a^{q'-1} + q + 1 \pmod{qq'}\).

public theorem_wanted sophieGermainChain_fermat_congruence {p j : ℕ}
    (hchain : ∀ i ≤ j + 1, (2 ^ i * (p + 1) - 1).Prime) (a : ℤ) :
    let q : ℕ := 2 ^ j * (p + 1) - 1
    let q' : ℕ := 2 ^ (j + 1) * (p + 1) - 1
    IsCoprime a ((q : ℤ) * q') →
      a ^ (q' - 1) ≡ q' * a ^ (q + 1) - 2 * q [ZMOD (q : ℤ) * q'] ∧
        q' * a ^ (q - 1) ≡ q * a ^ (q' - 1) + q + 1 [ZMOD (q : ℤ) * q']
Sources
  • Takashi Agoh, A Note on Fermat's Congruence, INTEGERS 25 (2025), Article A31, Corollary 3.4, Congruences (3.8).

TheoremLength of a Sophie Germain prime chain#●ready to prove

Let \(p\) be an odd prime and let \(\mathrm{ord}_p(2)\) be the multiplicative order of \(2\) modulo \(p\). Then there is some \(j \le \mathrm{ord}_p(2)\) such that \(2^j (p + 1) - 1\) is not prime. Thus the Sophie Germain prime chain \(q_1 = p\), \(q_{i+1} = 2q_i + 1 = 2^i (p + 1) - 1\) begins with at most \(\mathrm{ord}_p(2)\) consecutive primes.

public theorem_wanted sophieGermainChain_length_le_orderOf_two {p : ℕ} (hp : p.Prime)
    (hp2 : p ≠ 2) :
    ∃ j ≤ orderOf (2 : ZMod p), ¬(2 ^ j * (p + 1) - 1).Prime
Sources
  • Takashi Agoh, A Note on Fermat's Congruence, INTEGERS 25 (2025), Article A31, Theorem 3.5, quoting T. Agoh, Tatra Mt. Math. Publ. 20 (2000), Proposition 3.1.

TheoremFermat's congruence for a product of coprime moduli#●ready to prove

Let \(n\) and \(m\) be coprime natural numbers with \(0 < n < m\). Since \(\gcd(m - n, nm) = 1\), the residue of \(m - n\) is invertible in \(\mathbb{Z}/nm\mathbb{Z}\); write \(u\) for its inverse. Then the equalities \(a^{m-1} = (a^{m-n} - 1)\,u\,n + a^{m-n}\) and \((a^{m-n} - 1)\,u\,n + a^{m-n} = (a^{m-n} - 1)\,u\,m + 1\) in \(\mathbb{Z}/nm\mathbb{Z}\) hold for every integer \(a\) coprime to \(nm\) if and only if both \(n\) and \(m\) have the Fermat property: for \(k = n\) and for \(k = m\), \(a^{k-1} \equiv 1 \pmod{k}\) for every integer \(a\) coprime to \(k\).

This is the source's congruence \(a^{m-1} \equiv \frac{a^{m-n} - 1}{m - n}\,n + a^{m-n} \equiv \frac{a^{m-n} - 1}{m - n}\,m + 1 \pmod{nm}\), with the division by \(m - n\) read as multiplication by \(u\).

public theorem_wanted forall_fermat_congruence_iff_of_coprime {n m : ℕ} (hn : 0 < n)
    (hnm : n < m) (hcop : Nat.Coprime n m) :
    (∀ a : ℤ, IsCoprime a ((n : ℤ) * m) →
        ((a : ZMod (n * m)) ^ (m - 1) =
            ((a : ZMod (n * m)) ^ (m - n) - 1) * ((m - n : ℕ) : ZMod (n * m))⁻¹ * n +
              (a : ZMod (n * m)) ^ (m - n) ∧
          ((a : ZMod (n * m)) ^ (m - n) - 1) * ((m - n : ℕ) : ZMod (n * m))⁻¹ * n +
              (a : ZMod (n * m)) ^ (m - n) =
            ((a : ZMod (n * m)) ^ (m - n) - 1) * ((m - n : ℕ) : ZMod (n * m))⁻¹ * m + 1)) ↔
      (∀ a : ℤ, IsCoprime a (n : ℤ) → a ^ (n - 1) ≡ 1 [ZMOD n]) ∧
        (∀ a : ℤ, IsCoprime a (m : ℤ) → a ^ (m - 1) ≡ 1 [ZMOD m])
Sources
  • Takashi Agoh, A Note on Fermat's Congruence, INTEGERS 25 (2025), Article A31, Theorem 1.1 (a).
6 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.