This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pcabs

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

Ref Expression
Assertion pcabs ⊢ P ∈ ℙ ∧ A ∈ ℚ → P pCnt A = P pCnt A

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ A = A → P pCnt A = P pCnt A
2 1 a1i ⊢ P ∈ ℙ ∧ A ∈ ℚ → A = A → P pCnt A = P pCnt A
3 pcneg ⊢ P ∈ ℙ ∧ A ∈ ℚ → P pCnt − A = P pCnt A
4 oveq2 ⊢ A = − A → P pCnt A = P pCnt − A
5 4 eqeq1d ⊢ A = − A → P pCnt A = P pCnt A ↔ P pCnt − A = P pCnt A
6 3 5 syl5ibrcom ⊢ P ∈ ℙ ∧ A ∈ ℚ → A = − A → P pCnt A = P pCnt A
7 qre ⊢ A ∈ ℚ → A ∈ ℝ
8 7 adantl ⊢ P ∈ ℙ ∧ A ∈ ℚ → A ∈ ℝ
9 8 absord ⊢ P ∈ ℙ ∧ A ∈ ℚ → A = A ∨ A = − A
10 2 6 9 mpjaod ⊢ P ∈ ℙ ∧ A ∈ ℚ → P pCnt A = P pCnt A