succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul

English

Русский

Пусть p — простое, p^k делит m, p^l делит n, и p^(k+l+1) делит mn. Тогда либо p^(k+1) делит m, либо p^(l+1) делит n.

LaTeX

$$$$ \forall p,m,n,k,l \in \mathbb{N},\text{Prime}(p) \rightarrow (p^k \mid m) \rightarrow (p^l \mid n) \rightarrow (p^{k+l+1} \mid m n) \rightarrow (p^{k+1} \mid m \lor p^{l+1} \mid n). $$$$

Lean4

theorem succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul {p : ℕ} (p_prime : Prime p) {m n k l : ℕ} (hpm : p ^ k ∣ m)
    (hpn : p ^ l ∣ n) (hpmn : p ^ (k + l + 1) ∣ m * n) : p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n :=
  by
  have hpd : p ^ (k + l) * p ∣ m * n :=
    by
    let hpmn' : p ^ (succ (k + l)) ∣ m * n := hpmn
    rwa [pow_succ'] at hpmn'
  have hpd2 : p ∣ m * n / p ^ (k + l) := dvd_div_of_mul_dvd hpd
  have hpd3 : p ∣ m * n / (p ^ k * p ^ l) := by simpa [pow_add] using hpd2
  have hpd4 : p ∣ m / p ^ k * (n / p ^ l) := by simpa [Nat.div_mul_div_comm hpm hpn] using hpd3
  have hpd5 : p ∣ m / p ^ k ∨ p ∣ n / p ^ l := (Prime.dvd_mul p_prime).1 hpd4
  suffices p ^ k * p ∣ m ∨ p ^ l * p ∣ n by rwa [_root_.pow_succ, _root_.pow_succ]
  exact
    hpd5.elim (fun h : p ∣ m / p ^ k => Or.inl <| mul_dvd_of_dvd_div hpm h) fun h : p ∣ n / p ^ l =>
      Or.inr <| mul_dvd_of_dvd_div hpn h

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