Metamath Proof Explorer


Theorem sqfpc

Description: The prime count of a squarefree number is at most 1. (Contributed by Mario Carneiro, 1-Jul-2015)

Ref Expression
Assertion sqfpc ( ( 𝐴 ∈ ℕ ∧ ( μ ‘ 𝐴 ) ≠ 0 ∧ 𝑃 ∈ ℙ ) → ( 𝑃 pCnt 𝐴 ) ≤ 1 )

Proof

Step Hyp Ref Expression
1 issqf ( 𝐴 ∈ ℕ → ( ( μ ‘ 𝐴 ) ≠ 0 ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝐴 ) ≤ 1 ) )
2 1 biimpa ( ( 𝐴 ∈ ℕ ∧ ( μ ‘ 𝐴 ) ≠ 0 ) → ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝐴 ) ≤ 1 )
3 oveq1 ( 𝑝 = 𝑃 → ( 𝑝 pCnt 𝐴 ) = ( 𝑃 pCnt 𝐴 ) )
4 3 breq1d ( 𝑝 = 𝑃 → ( ( 𝑝 pCnt 𝐴 ) ≤ 1 ↔ ( 𝑃 pCnt 𝐴 ) ≤ 1 ) )
5 4 rspccv ( ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝐴 ) ≤ 1 → ( 𝑃 ∈ ℙ → ( 𝑃 pCnt 𝐴 ) ≤ 1 ) )
6 2 5 syl ( ( 𝐴 ∈ ℕ ∧ ( μ ‘ 𝐴 ) ≠ 0 ) → ( 𝑃 ∈ ℙ → ( 𝑃 pCnt 𝐴 ) ≤ 1 ) )
7 6 3impia ( ( 𝐴 ∈ ℕ ∧ ( μ ‘ 𝐴 ) ≠ 0 ∧ 𝑃 ∈ ℙ ) → ( 𝑃 pCnt 𝐴 ) ≤ 1 )