p : ℕ
p_prime : Nat.Prime p
m n : ℤ
k l : ℕ
hpm : ↑(p ^ k) ∣ m
hpn : ↑(p ^ l) ∣ n
hpmn : ↑(p ^ (k + l + 1)) ∣ m * n
hpm' : p ^ k ∣ natAbs m
hpn' : p ^ l ∣ natAbs n
⊢ p ^ (k + l + 1) ∣ natAbs (m * n)
p : ℕ
p_prime : Nat.Prime p
m n : ℤ
k l : ℕ
hpm : ↑(p ^ k) ∣ m
hpn : ↑(p ^ l) ∣ n
hpmn : ↑(p ^ (k + l + 1)) ∣ m * n
hpm' : p ^ k ∣ natAbs m
hpn' : p ^ l ∣ natAbs n
⊢ p ^ (k + l + 1) ∣ natAbs m * natAbs n
rw [← Int.natAbs_mul]
no goals
p : ℕ
p_prime : Nat.Prime p
m n : ℤ
k l : ℕ
hpm : ↑(p ^ k) ∣ m
hpn : ↑(p ^ l) ∣ n
hpmn : ↑(p ^ (k + l + 1)) ∣ m * n
hpm' : p ^ k ∣ natAbs m
hpn' : p ^ l ∣ natAbs n
⊢ p ^ (k + l + 1) ∣ natAbs (m * n)
apply Int.coe_nat_dvd.1 <| Int.dvd_natAbs.2 hpmn
p : ℕ
p_prime : Nat.Prime p
m n : ℤ
k l : ℕ
hpm : ↑(p ^ k) ∣ m
hpn : ↑(p ^ l) ∣ n
hpmn : ↑(p ^ (k + l + 1)) ∣ m * n
hpm' : p ^ k ∣ natAbs m
hpn' : p ^ l ∣ natAbs n
hpmn' : p ^ (k + l + 1) ∣ natAbs m * natAbs n
hsd : p ^ (k + 1) ∣ natAbs m ∨ p ^ (l + 1) ∣ natAbs n :=
  Nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul p_prime hpm' hpn' hpmn'
hsd1 : p ^ (k + 1) ∣ natAbs m
⊢ ↑(p ^ (k + 1)) ∣ ↑(natAbs m)
p : ℕ
p_prime : Nat.Prime p
m n : ℤ
k l : ℕ
hpm : ↑(p ^ k) ∣ m
hpn : ↑(p ^ l) ∣ n
hpmn : ↑(p ^ (k + l + 1)) ∣ m * n
hpm' : p ^ k ∣ natAbs m
hpn' : p ^ l ∣ natAbs n
hpmn' : p ^ (k + l + 1) ∣ natAbs m * natAbs n
hsd : p ^ (k + 1) ∣ natAbs m ∨ p ^ (l + 1) ∣ natAbs n :=
  Nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul p_prime hpm' hpn' hpmn'
hsd1 : p ^ (k + 1) ∣ natAbs m
⊢ ↑(p ^ (k + 1)) ∣ m
apply Int.dvd_natAbs.1
no goals
p : ℕ
p_prime : Nat.Prime p
m n : ℤ
k l : ℕ
hpm : ↑(p ^ k) ∣ m
hpn : ↑(p ^ l) ∣ n
hpmn : ↑(p ^ (k + l + 1)) ∣ m * n
hpm' : p ^ k ∣ natAbs m
hpn' : p ^ l ∣ natAbs n
hpmn' : p ^ (k + l + 1) ∣ natAbs m * natAbs n
hsd : p ^ (k + 1) ∣ natAbs m ∨ p ^ (l + 1) ∣ natAbs n :=
  Nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul p_prime hpm' hpn' hpmn'
hsd1 : p ^ (k + 1) ∣ natAbs m
⊢ ↑(p ^ (k + 1)) ∣ ↑(natAbs m)
apply Int.coe_nat_dvd.2 hsd1
p : ℕ
p_prime : Nat.Prime p
m n : ℤ
k l : ℕ
hpm : ↑(p ^ k) ∣ m
hpn : ↑(p ^ l) ∣ n
hpmn : ↑(p ^ (k + l + 1)) ∣ m * n
hpm' : p ^ k ∣ natAbs m
hpn' : p ^ l ∣ natAbs n
hpmn' : p ^ (k + l + 1) ∣ natAbs m * natAbs n
hsd : p ^ (k + 1) ∣ natAbs m ∨ p ^ (l + 1) ∣ natAbs n :=
  Nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul p_prime hpm' hpn' hpmn'
hsd2 : p ^ (l + 1) ∣ natAbs n
⊢ ↑(p ^ (l + 1)) ∣ ↑(natAbs n)
p : ℕ
p_prime : Nat.Prime p
m n : ℤ
k l : ℕ
hpm : ↑(p ^ k) ∣ m
hpn : ↑(p ^ l) ∣ n
hpmn : ↑(p ^ (k + l + 1)) ∣ m * n
hpm' : p ^ k ∣ natAbs m
hpn' : p ^ l ∣ natAbs n
hpmn' : p ^ (k + l + 1) ∣ natAbs m * natAbs n
hsd : p ^ (k + 1) ∣ natAbs m ∨ p ^ (l + 1) ∣ natAbs n :=
  Nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul p_prime hpm' hpn' hpmn'
hsd2 : p ^ (l + 1) ∣ natAbs n
⊢ ↑(p ^ (l + 1)) ∣ n
apply Int.dvd_natAbs.1
no goals
p : ℕ
p_prime : Nat.Prime p
m n : ℤ
k l : ℕ
hpm : ↑(p ^ k) ∣ m
hpn : ↑(p ^ l) ∣ n
hpmn : ↑(p ^ (k + l + 1)) ∣ m * n
hpm' : p ^ k ∣ natAbs m
hpn' : p ^ l ∣ natAbs n
hpmn' : p ^ (k + l + 1) ∣ natAbs m * natAbs n
hsd : p ^ (k + 1) ∣ natAbs m ∨ p ^ (l + 1) ∣ natAbs n :=
  Nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul p_prime hpm' hpn' hpmn'
hsd2 : p ^ (l + 1) ∣ natAbs n
⊢ ↑(p ^ (l + 1)) ∣ ↑(natAbs n)
apply Int.coe_nat_dvd.2 hsd2