R : Type ?u.84416
inst✝ : CommMonoidWithZero R
n p : R
k a b : ℕ
hab : coprime a b
⊢ ∀ ⦃a_1 : ℕ⦄, a_1 ∣ a → a ≠ 0 → IsPrimePow a_1 → a_1 ∣ b → b ≠ 0 → ¬IsPrimePow a_1
R : Type ?u.84416
inst✝ : CommMonoidWithZero R
n p : R
k a b : ℕ
hab : coprime a b
⊢ Disjoint (Finset.filter IsPrimePow (divisors a)) (Finset.filter IsPrimePow (divisors b))
simp only [Finset.disjoint_left, Finset.mem_filter, and_imp, Nat.mem_divisors, not_and]
R : Type ?u.84416
inst✝ : CommMonoidWithZero R
n✝ p : R
k a b : ℕ
hab : coprime a b
n : ℕ
han : n ∣ a
_ha : a ≠ 0
hn : IsPrimePow n
hbn : n ∣ b
_hb : b ≠ 0
⊢ False
R : Type ?u.84416
inst✝ : CommMonoidWithZero R
n p : R
k a b : ℕ
hab : coprime a b
⊢ ∀ ⦃a_1 : ℕ⦄, a_1 ∣ a → a ≠ 0 → IsPrimePow a_1 → a_1 ∣ b → b ≠ 0 → ¬IsPrimePow a_1
rintro n han _ha hn hbn _hb -
no goals
R : Type ?u.84416
inst✝ : CommMonoidWithZero R
n✝ p : R
k a b : ℕ
hab : coprime a b
n : ℕ
han : n ∣ a
_ha : a ≠ 0
hn : IsPrimePow n
hbn : n ∣ b
_hb : b ≠ 0
⊢ False
exact hn.ne_one (Nat.eq_one_of_dvd_coprimes hab han hbn)