m n : ℕ
hmn : coprime m n
⊢ (∀ (x : ℕ), Prime x → ¬x ^ 2 ∣ m * n) ↔ ∀ (x : ℕ), Prime x → ¬x ^ 2 ∣ m ∧ ¬x ^ 2 ∣ n
m n : ℕ
hmn : coprime m n
⊢ Squarefree (m * n) ↔ Squarefree m ∧ Squarefree n
simp only [squarefree_iff_prime_squarefree, ← sq, ← forall_and]
m n : ℕ
hmn : coprime m n
p : ℕ
hp : Prime p
⊢ ¬p ^ 2 ∣ m * n ↔ ¬p ^ 2 ∣ m ∧ ¬p ^ 2 ∣ n
m n : ℕ
hmn : coprime m n
⊢ (∀ (x : ℕ), Prime x → ¬x ^ 2 ∣ m * n) ↔ ∀ (x : ℕ), Prime x → ¬x ^ 2 ∣ m ∧ ¬x ^ 2 ∣ n
refine' ball_congr fun p hp => _
no goals
m n : ℕ
hmn : coprime m n
p : ℕ
hp : Prime p
⊢ ¬p ^ 2 ∣ m * n ↔ ¬p ^ 2 ∣ m ∧ ¬p ^ 2 ∣ n
simp only [hmn.isPrimePow_dvd_mul (hp.isPrimePow.pow two_ne_zero), not_or]