This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ( μ ‘ 𝐴 ) = 0 ) → ( μ ‘ ( 𝐴 · 𝐵 ) ) = 0 )

Proof

Step Hyp Ref Expression
1 prmz ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℤ )
2 1 adantl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℤ )
3 zsqcl ⊢ ( 𝑝 ∈ ℤ → ( 𝑝 ↑ 2 ) ∈ ℤ )
4 2 3 syl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ↑ 2 ) ∈ ℤ )
5 nnz ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℤ )
6 5 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) → 𝐴 ∈ ℤ )
7 nnz ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℤ )
8 7 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) → 𝐵 ∈ ℤ )
9 dvdsmultr1 ⊢ ( ( ( 𝑝 ↑ 2 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝑝 ↑ 2 ) ∥ 𝐴 → ( 𝑝 ↑ 2 ) ∥ ( 𝐴 · 𝐵 ) ) )
10 4 6 8 9 syl3anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 ↑ 2 ) ∥ 𝐴 → ( 𝑝 ↑ 2 ) ∥ ( 𝐴 · 𝐵 ) ) )
11 10 reximdva ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝐴 → ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ ( 𝐴 · 𝐵 ) ) )
12 isnsqf ⊢ ( 𝐴 ∈ ℕ → ( ( μ ‘ 𝐴 ) = 0 ↔ ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝐴 ) )
13 12 adantr ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( μ ‘ 𝐴 ) = 0 ↔ ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝐴 ) )
14 nnmulcl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 · 𝐵 ) ∈ ℕ )
15 isnsqf ⊢ ( ( 𝐴 · 𝐵 ) ∈ ℕ → ( ( μ ‘ ( 𝐴 · 𝐵 ) ) = 0 ↔ ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ ( 𝐴 · 𝐵 ) ) )
16 14 15 syl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( μ ‘ ( 𝐴 · 𝐵 ) ) = 0 ↔ ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ ( 𝐴 · 𝐵 ) ) )
17 11 13 16 3imtr4d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( μ ‘ 𝐴 ) = 0 → ( μ ‘ ( 𝐴 · 𝐵 ) ) = 0 ) )
18 17 imp ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ( μ ‘ 𝐴 ) = 0 ) → ( μ ‘ ( 𝐴 · 𝐵 ) ) = 0 )