eq_prime_pow_of_dvd_least_prime_pow

English

Let p be prime, and if a ∤ p^k but a ∣ p^(k+1), then a = p^(k+1).

Русский

Пусть p — простое, и если a ∤ p^k, но a ∣ p^(k+1), то a = p^(k+1).

LaTeX

$$$$ \forall {a,p,k} \in \mathbb{N},\ ext{Prime}(p) \rightarrow \lnot(a \mid p^k) \rightarrow a \mid p^{k+1} \rightarrow a = p^{k+1}. $$$$

Lean4

/-- If `p` is prime,
and `a` doesn't divide `p^k`, but `a` does divide `p^(k+1)`
then `a = p^(k+1)`.
-/
theorem eq_prime_pow_of_dvd_least_prime_pow {a p k : ℕ} (pp : Prime p) (h₁ : ¬a ∣ p ^ k) (h₂ : a ∣ p ^ (k + 1)) :
    a = p ^ (k + 1) := by
  obtain ⟨l, ⟨h, rfl⟩⟩ := (dvd_prime_pow pp).1 h₂
  congr
  exact le_antisymm h (not_le.1 ((not_congr (pow_dvd_pow_iff_le_right (Prime.one_lt pp))).1 h₁))

Похожие утверждения