English
For natural numbers n and d, d | n if and only if for all primes p and k, p^k | d implies p^k | n.
Русский
Для натуральных n и d: d | n тогда и только тогда, когда для всех простых p и целых k выполняется p^k | d ⇒ p^k | n.
LaTeX
$$$$ d \mid n \iff \forall p,k \in \mathbb{N},\ p \text{ prime} \land p^{k} \mid d \Rightarrow p^{k} \mid n. $$$$
Lean4
theorem dvd_iff_prime_pow_dvd_dvd (n d : ℕ) : d ∣ n ↔ ∀ p k : ℕ, Prime p → p ^ k ∣ d → p ^ k ∣ n :=
by
rcases eq_or_ne n 0 with (rfl | hn)
· simp
rcases eq_or_ne d 0 with (rfl | hd)
· simp only [zero_dvd_iff, hn, false_iff, not_forall]
exact ⟨2, n, prime_two, dvd_zero _, mt (le_of_dvd hn.bot_lt) (n.lt_two_pow_self).not_ge⟩
refine ⟨fun h p k _ hpkd => dvd_trans hpkd h, ?_⟩
rw [← factorization_prime_le_iff_dvd hd hn]
intro h p pp
simp_rw [← pp.pow_dvd_iff_le_factorization hn]
exact h p _ pp (ordProj_dvd _ _)
