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 ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℚ ) → ( 𝑃 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 𝐴 ) )