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

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

Proof

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