Metamath Proof Explorer

Theorem mumullem1

Description: Lemma for mumul . A multiple of a non-squarefree number is non-squarefree. (Contributed by Mario Carneiro, 3-Oct-2014)

Ref Expression
Assertion mumullem1 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ μ ⁡ A = 0 → μ ⁡ A ⁢ B = 0

Proof

Step Hyp Ref Expression
1 prmz ⊢ p ∈ ℙ → p ∈ ℤ
2 1 adantl ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ p ∈ ℙ → p ∈ ℤ
3 zsqcl ⊢ p ∈ ℤ → p 2 ∈ ℤ
4 2 3 syl ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ p ∈ ℙ → p 2 ∈ ℤ
5 nnz ⊢ A ∈ ℕ → A ∈ ℤ
6 5 ad2antrr ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ p ∈ ℙ → A ∈ ℤ
7 nnz ⊢ B ∈ ℕ → B ∈ ℤ
8 7 ad2antlr ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ p ∈ ℙ → B ∈ ℤ
9 dvdsmultr1 ⊢ p 2 ∈ ℤ ∧ A ∈ ℤ ∧ B ∈ ℤ → p 2 ∥ A → p 2 ∥ A ⁢ B
10 4 6 8 9 syl3anc ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ p ∈ ℙ → p 2 ∥ A → p 2 ∥ A ⁢ B
11 10 reximdva ⊢ A ∈ ℕ ∧ B ∈ ℕ → ∃ p ∈ ℙ p 2 ∥ A → ∃ p ∈ ℙ p 2 ∥ A ⁢ B
12 isnsqf ⊢ A ∈ ℕ → μ ⁡ A = 0 ↔ ∃ p ∈ ℙ p 2 ∥ A
13 12 adantr ⊢ A ∈ ℕ ∧ B ∈ ℕ → μ ⁡ A = 0 ↔ ∃ p ∈ ℙ p 2 ∥ A
14 nnmulcl ⊢ A ∈ ℕ ∧ B ∈ ℕ → A ⁢ B ∈ ℕ
15 isnsqf ⊢ A ⁢ B ∈ ℕ → μ ⁡ A ⁢ B = 0 ↔ ∃ p ∈ ℙ p 2 ∥ A ⁢ B
16 14 15 syl ⊢ A ∈ ℕ ∧ B ∈ ℕ → μ ⁡ A ⁢ B = 0 ↔ ∃ p ∈ ℙ p 2 ∥ A ⁢ B
17 11 13 16 3imtr4d ⊢ A ∈ ℕ ∧ B ∈ ℕ → μ ⁡ A = 0 → μ ⁡ A ⁢ B = 0
18 17 imp ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ μ ⁡ A = 0 → μ ⁡ A ⁢ B = 0