Metamath Proof Explorer


Theorem pcrec

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

Ref Expression
Assertion pcrec P A A 0 P pCnt 1 A = P pCnt A

Proof

Step Hyp Ref Expression
1 1z 1
2 zq 1 1
3 1 2 ax-mp 1
4 ax-1ne0 1 0
5 3 4 pm3.2i 1 1 0
6 pcqdiv P 1 1 0 A A 0 P pCnt 1 A = P pCnt 1 P pCnt A
7 5 6 mp3an2 P A A 0 P pCnt 1 A = P pCnt 1 P pCnt A
8 pc1 P P pCnt 1 = 0
9 8 adantr P A A 0 P pCnt 1 = 0
10 9 oveq1d P A A 0 P pCnt 1 P pCnt A = 0 P pCnt A
11 7 10 eqtrd P A A 0 P pCnt 1 A = 0 P pCnt A
12 df-neg P pCnt A = 0 P pCnt A
13 11 12 eqtr4di P A A 0 P pCnt 1 A = P pCnt A