Theorem pcabs

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

	Ref	Expression
Assertion	pcabs	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℚ ) → ( 𝑃 pCnt ( abs ‘ 𝐴 ) ) = ( 𝑃 pCnt 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( ( abs ‘ 𝐴 ) = 𝐴 → ( 𝑃 pCnt ( abs ‘ 𝐴 ) ) = ( 𝑃 pCnt 𝐴 ) )
2	1	a1i	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℚ ) → ( ( abs ‘ 𝐴 ) = 𝐴 → ( 𝑃 pCnt ( abs ‘ 𝐴 ) ) = ( 𝑃 pCnt 𝐴 ) ) )
3		pcneg	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℚ ) → ( 𝑃 pCnt - 𝐴 ) = ( 𝑃 pCnt 𝐴 ) )
4		oveq2	⊢ ( ( abs ‘ 𝐴 ) = - 𝐴 → ( 𝑃 pCnt ( abs ‘ 𝐴 ) ) = ( 𝑃 pCnt - 𝐴 ) )
5	4	eqeq1d	⊢ ( ( abs ‘ 𝐴 ) = - 𝐴 → ( ( 𝑃 pCnt ( abs ‘ 𝐴 ) ) = ( 𝑃 pCnt 𝐴 ) ↔ ( 𝑃 pCnt - 𝐴 ) = ( 𝑃 pCnt 𝐴 ) ) )
6	3 5	syl5ibrcom	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℚ ) → ( ( abs ‘ 𝐴 ) = - 𝐴 → ( 𝑃 pCnt ( abs ‘ 𝐴 ) ) = ( 𝑃 pCnt 𝐴 ) ) )
7		qre	⊢ ( 𝐴 ∈ ℚ → 𝐴 ∈ ℝ )
8	7	adantl	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℚ ) → 𝐴 ∈ ℝ )
9	8	absord	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℚ ) → ( ( abs ‘ 𝐴 ) = 𝐴 ∨ ( abs ‘ 𝐴 ) = - 𝐴 ) )
10	2 6 9	mpjaod	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℚ ) → ( 𝑃 pCnt ( abs ‘ 𝐴 ) ) = ( 𝑃 pCnt 𝐴 ) )