[GOAL]
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
[PROOFSTEP]
rw [← Int.natAbs_mul]
[GOAL]
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)
[PROOFSTEP]
apply Int.coe_nat_dvd.1 <| Int.dvd_natAbs.2 hpmn
[GOAL]
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
[PROOFSTEP]
apply Int.dvd_natAbs.1
[GOAL]
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)
[PROOFSTEP]
apply Int.coe_nat_dvd.2 hsd1
[GOAL]
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
[PROOFSTEP]
apply Int.dvd_natAbs.1
[GOAL]
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)
[PROOFSTEP]
apply Int.coe_nat_dvd.2 hsd2
[GOAL]
p : ℕ
hp : Nat.Prime p
k : ℤ
h : ↑p ∣ k ^ 2
⊢ p ∣ natAbs k
[PROOFSTEP]
apply @Nat.Prime.dvd_of_dvd_pow _ _ 2 hp
[GOAL]
p : ℕ
hp : Nat.Prime p
k : ℤ
h : ↑p ∣ k ^ 2
⊢ p ∣ natAbs k ^ 2
[PROOFSTEP]
rwa [sq, ← natAbs_mul, ← coe_nat_dvd_left, ← sq]
