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 e. Prime /\ A e. QQ ) -> ( P pCnt ( abs ` A ) ) = ( P pCnt A ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( ( abs ` A ) = A -> ( P pCnt ( abs ` A ) ) = ( P pCnt A ) )
2 1 a1i 
 |-  ( ( P e. Prime /\ A e. QQ ) -> ( ( abs ` A ) = A -> ( P pCnt ( abs ` A ) ) = ( P pCnt A ) ) )
3 pcneg 
 |-  ( ( P e. Prime /\ A e. QQ ) -> ( P pCnt -u A ) = ( P pCnt A ) )
4 oveq2 
 |-  ( ( abs ` A ) = -u A -> ( P pCnt ( abs ` A ) ) = ( P pCnt -u A ) )
5 4 eqeq1d 
 |-  ( ( abs ` A ) = -u A -> ( ( P pCnt ( abs ` A ) ) = ( P pCnt A ) <-> ( P pCnt -u A ) = ( P pCnt A ) ) )
6 3 5 syl5ibrcom 
 |-  ( ( P e. Prime /\ A e. QQ ) -> ( ( abs ` A ) = -u A -> ( P pCnt ( abs ` A ) ) = ( P pCnt A ) ) )
7 qre 
 |-  ( A e. QQ -> A e. RR )
8 7 adantl 
 |-  ( ( P e. Prime /\ A e. QQ ) -> A e. RR )
9 8 absord 
 |-  ( ( P e. Prime /\ A e. QQ ) -> ( ( abs ` A ) = A \/ ( abs ` A ) = -u A ) )
10 2 6 9 mpjaod 
 |-  ( ( P e. Prime /\ A e. QQ ) -> ( P pCnt ( abs ` A ) ) = ( P pCnt A ) )