Formal target: Corpus.OEIS60957.conjecture

Conjecture: let $p \le n$ be prime.

Exact formal statement

∀ (n p : Nat),
  Nat.Prime p →
    LE.le.{0} p n →
      ∀ (m a_exp : Nat),
        Membership.mem.{0, 0} (Corpus.OEIS60957.productsOfSubsets n) m →
          Membership.mem.{0, 0} (Corpus.OEIS60957.productsOfSubsets n)
              (HMul.hMul.{0, 0, 0} (HPow.hPow.{0, 0, 0} p a_exp) m) →
            ∀ (k : Nat),
              LT.lt.{0} 0 k →
                LT.lt.{0} k a_exp →
                  Membership.mem.{0, 0} (Corpus.OEIS60957.productsOfSubsets n)
                    (HMul.hMul.{0, 0, 0} (HPow.hPow.{0, 0, 0} p k) m)

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record