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	$$⊢\left(A\in \mathbb{N}\wedge \mu \left(A\right)\ne 0\wedge P\in \mathbb{P}\right)\to P\mathrm{pCnt}A\le 1$$

Proof

Step	Hyp	Ref	Expression
1		issqf	$$⊢A\in \mathbb{N}\to \left(\mu \left(A\right)\ne 0\leftrightarrow \forall p\in \mathbb{P}p\mathrm{pCnt}A\le 1\right)$$
2	1	biimpa	$$⊢\left(A\in \mathbb{N}\wedge \mu \left(A\right)\ne 0\right)\to \forall p\in \mathbb{P}p\mathrm{pCnt}A\le 1$$
3		oveq1	$$⊢p=P\to p\mathrm{pCnt}A=P\mathrm{pCnt}A$$
4	3	breq1d	$$⊢p=P\to \left(p\mathrm{pCnt}A\le 1\leftrightarrow P\mathrm{pCnt}A\le 1\right)$$
5	4	rspccv	$$⊢\forall p\in \mathbb{P}p\mathrm{pCnt}A\le 1\to \left(P\in \mathbb{P}\to P\mathrm{pCnt}A\le 1\right)$$
6	2 5	syl	$$⊢\left(A\in \mathbb{N}\wedge \mu \left(A\right)\ne 0\right)\to \left(P\in \mathbb{P}\to P\mathrm{pCnt}A\le 1\right)$$
7	6	3impia	$$⊢\left(A\in \mathbb{N}\wedge \mu \left(A\right)\ne 0\wedge P\in \mathbb{P}\right)\to P\mathrm{pCnt}A\le 1$$