Formal target: Corpus.Mathoverflow17560.mathoverflow_17560

If $2^x$ and $3^x$ are integers, then $x$ must be an integer.

Exact formal statement

∀ {x : Real},
  (Exists.{1} fun m => Eq.{1} (HPow.hPow.{0, 0, 0} 2 x) (Nat.cast.{0} m)) →
    (Exists.{1} fun m => Eq.{1} (HPow.hPow.{0, 0, 0} 3 x) (Nat.cast.{0} m)) →
      Exists.{1} fun m => Eq.{1} x (Nat.cast.{0} m)

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record