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 ⊢ A ∈ ℕ ∧ μ ⁡ A ≠ 0 ∧ P ∈ ℙ → P pCnt A ≤ 1

Proof

Step Hyp Ref Expression
1 issqf ⊢ A ∈ ℕ → μ ⁡ A ≠ 0 ↔ ∀ p ∈ ℙ p pCnt A ≤ 1
2 1 biimpa ⊢ A ∈ ℕ ∧ μ ⁡ A ≠ 0 → ∀ p ∈ ℙ p pCnt A ≤ 1
3 oveq1 ⊢ p = P → p pCnt A = P pCnt A
4 3 breq1d ⊢ p = P → p pCnt A ≤ 1 ↔ P pCnt A ≤ 1
5 4 rspccv ⊢ ∀ p ∈ ℙ p pCnt A ≤ 1 → P ∈ ℙ → P pCnt A ≤ 1
6 2 5 syl ⊢ A ∈ ℕ ∧ μ ⁡ A ≠ 0 → P ∈ ℙ → P pCnt A ≤ 1
7 6 3impia ⊢ A ∈ ℕ ∧ μ ⁡ A ≠ 0 ∧ P ∈ ℙ → P pCnt A ≤ 1