Metamath Proof Explorer

Theorem dvdssqf

Description: A divisor of a squarefree number is squarefree. (Contributed by Mario Carneiro, 1-Jul-2015)

Ref Expression
Assertion dvdssqf ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ B ∥ A → μ ⁡ A ≠ 0 → μ ⁡ B ≠ 0

Proof

Step Hyp Ref Expression
1 simpl3 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ B ∥ A ∧ p ∈ ℙ → B ∥ A
2 prmz ⊢ p ∈ ℙ → p ∈ ℤ
3 2 adantl ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ B ∥ A ∧ p ∈ ℙ → p ∈ ℤ
4 zsqcl ⊢ p ∈ ℤ → p 2 ∈ ℤ
5 3 4 syl ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ B ∥ A ∧ p ∈ ℙ → p 2 ∈ ℤ
6 simpl2 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ B ∥ A ∧ p ∈ ℙ → B ∈ ℕ
7 6 nnzd ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ B ∥ A ∧ p ∈ ℙ → B ∈ ℤ
8 simpl1 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ B ∥ A ∧ p ∈ ℙ → A ∈ ℕ
9 8 nnzd ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ B ∥ A ∧ p ∈ ℙ → A ∈ ℤ
10 dvdstr ⊢ p 2 ∈ ℤ ∧ B ∈ ℤ ∧ A ∈ ℤ → p 2 ∥ B ∧ B ∥ A → p 2 ∥ A
11 5 7 9 10 syl3anc ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ B ∥ A ∧ p ∈ ℙ → p 2 ∥ B ∧ B ∥ A → p 2 ∥ A
12 1 11 mpan2d ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ B ∥ A ∧ p ∈ ℙ → p 2 ∥ B → p 2 ∥ A
13 12 reximdva ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ B ∥ A → ∃ p ∈ ℙ p 2 ∥ B → ∃ p ∈ ℙ p 2 ∥ A
14 isnsqf ⊢ B ∈ ℕ → μ ⁡ B = 0 ↔ ∃ p ∈ ℙ p 2 ∥ B
15 14 3ad2ant2 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ B ∥ A → μ ⁡ B = 0 ↔ ∃ p ∈ ℙ p 2 ∥ B
16 isnsqf ⊢ A ∈ ℕ → μ ⁡ A = 0 ↔ ∃ p ∈ ℙ p 2 ∥ A
17 16 3ad2ant1 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ B ∥ A → μ ⁡ A = 0 ↔ ∃ p ∈ ℙ p 2 ∥ A
18 13 15 17 3imtr4d ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ B ∥ A → μ ⁡ B = 0 → μ ⁡ A = 0
19 18 necon3d ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ B ∥ A → μ ⁡ A ≠ 0 → μ ⁡ B ≠ 0