Formal target: Corpus.WikipediaFeitThompsonPrimeConjecture.feit_thompson_primes

There are no distinct primes $p$ and $q$ such that $\frac{q^p - 1}{q - 1}$ divides $\frac{p^q - 1}{p - 1}$

Exact formal statement

∀ (p q : Nat),
  Nat.Prime p →
    Nat.Prime q →
      LT.lt.{0} p q →
        Not
          (Dvd.dvd.{0} (HDiv.hDiv.{0, 0, 0} (HSub.hSub.{0, 0, 0} (HPow.hPow.{0, 0, 0} q p) 1) (HSub.hSub.{0, 0, 0} q 1))
            (HDiv.hDiv.{0, 0, 0} (HSub.hSub.{0, 0, 0} (HPow.hPow.{0, 0, 0} p q) 1) (HSub.hSub.{0, 0, 0} p 1)))

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record