Zsigmondy's theorem

DefinitionExceptional cases of Zsigmondy's theorem#✓fully proved

A triple \((a, b, n)\) of natural numbers is a Bang–Zsigmondy exceptional case when either \((a, b, n) = (2, 1, 6)\), or \(n = 2\) and \(a + b = 2^k\) for some natural number \(k\).

public def IsBangZsigmondyExceptional (a b n : ℕ) : Prop :=
  (a = 2 ∧ b = 1 ∧ n = 6) ∨ (n = 2 ∧ ∃ k : ℕ, a + b = 2 ^ k)

Used by 1

Used byZsigmondy's theorem

TheoremZsigmondy's theorem#✓fully proved

Let \(a\), \(b\) and \(n\) be natural numbers with \(0 < b < a\), \(a\) and \(b\) coprime, and \(n \ge 2\), and suppose that \((a, b, n)\) is not a Bang–Zsigmondy exceptional case: neither \((a, b, n) = (2, 1, 6)\), nor \(n = 2\) with \(a + b\) a power of two. Then \(a^n - b^n\) has a primitive prime divisor, that is, a prime \(p\) that divides \(a^n - b^n\) and divides no \(a^m - b^m\) with \(1 \le m < n\).

public theorem bangZsigmondy_exists_primitivePrimeDivisor {a b n : ℕ}
    (hbpos : 0 < b) (hba : b < a) (hcop : Nat.Coprime a b)
    (hn : 2 ≤ n) (hnexc : ¬ IsBangZsigmondyExceptional a b n) :
    ∃ p, IntegerSequence.IsPrimitivePrimeDivisor
      (fun m => (a : ℤ) ^ m - (b : ℤ) ^ m) n p

Sources

• Bayarmagnai lines 133–137 invoke the general theorem, with the explicit exception families per Jones Theorem Bang lines 211–215.

Uses 3

Statement usesPrimitive prime divisor of an integer sequence · Exceptional cases of Zsigmondy's theorem

Proof usesPrimitive divisor of an integer sequence

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.