Theorem pcabs

Description: The prime count of an absolute value. (Contributed by Mario Carneiro, 13-Mar-2014)

	Ref	Expression
Assertion	pcabs	$$⊢\left(P\in \mathbb{P}\wedge A\in \mathbb{Q}\right)\to P\mathrm{pCnt}\left|A\right|=P\mathrm{pCnt}A$$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢\left|A\right|=A\to P\mathrm{pCnt}\left|A\right|=P\mathrm{pCnt}A$$
2	1	a1i	$$⊢\left(P\in \mathbb{P}\wedge A\in \mathbb{Q}\right)\to \left(\left|A\right|=A\to P\mathrm{pCnt}\left|A\right|=P\mathrm{pCnt}A\right)$$
3		pcneg	$$⊢\left(P\in \mathbb{P}\wedge A\in \mathbb{Q}\right)\to P\mathrm{pCnt}\left(-A\right)=P\mathrm{pCnt}A$$
4		oveq2	$$⊢\left|A\right|=-A\to P\mathrm{pCnt}\left|A\right|=P\mathrm{pCnt}\left(-A\right)$$
5	4	eqeq1d	$$⊢\left|A\right|=-A\to \left(P\mathrm{pCnt}\left|A\right|=P\mathrm{pCnt}A\leftrightarrow P\mathrm{pCnt}\left(-A\right)=P\mathrm{pCnt}A\right)$$
6	3 5	syl5ibrcom	$$⊢\left(P\in \mathbb{P}\wedge A\in \mathbb{Q}\right)\to \left(\left|A\right|=-A\to P\mathrm{pCnt}\left|A\right|=P\mathrm{pCnt}A\right)$$
7		qre	$$⊢A\in \mathbb{Q}\to A\in ℝ$$
8	7	adantl	$$⊢\left(P\in \mathbb{P}\wedge A\in \mathbb{Q}\right)\to A\in ℝ$$
9	8	absord	$$⊢\left(P\in \mathbb{P}\wedge A\in \mathbb{Q}\right)\to \left(\left|A\right|=A\vee \left|A\right|=-A\right)$$
10	2 6 9	mpjaod	$$⊢\left(P\in \mathbb{P}\wedge A\in \mathbb{Q}\right)\to P\mathrm{pCnt}\left|A\right|=P\mathrm{pCnt}A$$