English
If p and q are primes and p^(m+1) = q^(n+1) for natural numbers m,n, then p = q and m = n.
Русский
Если p и q простые, и p^(m+1) = q^(n+1) для натуральных m,n, то p = q и m = n.
LaTeX
$$$p^{m+1} = q^{n+1} \Rightarrow p = q \land m = n$ (with p,q \text{ primes}).$$
Lean4
/-- Two prime powers with positive exponents are equal only when the primes and the
exponents are equal. -/
theorem pow_inj {p q m n : ℕ} (hp : p.Prime) (hq : q.Prime) (h : p ^ (m + 1) = q ^ (n + 1)) : p = q ∧ m = n :=
by
have H :=
dvd_antisymm (Prime.dvd_of_dvd_pow hp <| h ▸ dvd_pow_self p (succ_ne_zero m))
(Prime.dvd_of_dvd_pow hq <| h.symm ▸ dvd_pow_self q (succ_ne_zero n))
exact ⟨H, succ_inj.mp <| Nat.pow_right_injective hq.two_le (H ▸ h)⟩
