Metamath Proof Explorer

Theorem pcrec

Description: Prime power of a reciprocal. (Contributed by Mario Carneiro, 10-Aug-2015)

Ref Expression
Assertion pcrec 
|- ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) -> ( P pCnt ( 1 / A ) ) = -u ( P pCnt A ) )

Proof

Step Hyp Ref Expression
1 1z 
 |-  1 e. ZZ
2 zq 
 |-  ( 1 e. ZZ -> 1 e. QQ )
3 1 2 ax-mp 
 |-  1 e. QQ
4 ax-1ne0 
 |-  1 =/= 0
5 3 4 pm3.2i 
 |-  ( 1 e. QQ /\ 1 =/= 0 )
6 pcqdiv 
 |-  ( ( P e. Prime /\ ( 1 e. QQ /\ 1 =/= 0 ) /\ ( A e. QQ /\ A =/= 0 ) ) -> ( P pCnt ( 1 / A ) ) = ( ( P pCnt 1 ) - ( P pCnt A ) ) )
7 5 6 mp3an2 
 |-  ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) -> ( P pCnt ( 1 / A ) ) = ( ( P pCnt 1 ) - ( P pCnt A ) ) )
8 pc1 
 |-  ( P e. Prime -> ( P pCnt 1 ) = 0 )
9 8 adantr 
 |-  ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) -> ( P pCnt 1 ) = 0 )
10 9 oveq1d 
 |-  ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) -> ( ( P pCnt 1 ) - ( P pCnt A ) ) = ( 0 - ( P pCnt A ) ) )
11 7 10 eqtrd 
 |-  ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) -> ( P pCnt ( 1 / A ) ) = ( 0 - ( P pCnt A ) ) )
12 df-neg 
 |-  -u ( P pCnt A ) = ( 0 - ( P pCnt A ) )
13 11 12 eqtr4di 
 |-  ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) -> ( P pCnt ( 1 / A ) ) = -u ( P pCnt A ) )