Formal target: Corpus.OEIS211417.supercongruence

Supercongruence: "a(p^k) == a(p^(k-1)) ( mod p^(3*k) ) for any prime p >= 5 and any positive integer k." - _Peter Bala_, Jan 24 2020 More generally, "the congruences a(n*p^k) == a(n*p^(k-1)) ( mod p^(3*k) ) may hold for any prime p >= 5 and any positive integers n and k."

Exact formal statement

∀ (p k : Nat),
  Nat.Prime p →
    LE.le.{0} 5 p →
      LT.lt.{0} 0 k →
        Dvd.dvd.{0} (HPow.hPow.{0, 0, 0} (Nat.cast.{0} p) (HMul.hMul.{0, 0, 0} 3 k))
          (HSub.hSub.{0, 0, 0} (Nat.cast.{0} (Corpus.OEIS211417.a (HPow.hPow.{0, 0, 0} p k)))
            (Nat.cast.{0} (Corpus.OEIS211417.a (HPow.hPow.{0, 0, 0} p (HSub.hSub.{0, 0, 0} k 1)))))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record