Metamath Proof Explorer


Theorem pcrec

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

Ref Expression
Assertion pcrec ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ) → ( 𝑃 pCnt ( 1 / 𝐴 ) ) = - ( 𝑃 pCnt 𝐴 ) )

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 ( ( 𝑃 ∈ ℙ ∧ ( 1 ∈ ℚ ∧ 1 ≠ 0 ) ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ) → ( 𝑃 pCnt ( 1 / 𝐴 ) ) = ( ( 𝑃 pCnt 1 ) − ( 𝑃 pCnt 𝐴 ) ) )
7 5 6 mp3an2 ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ) → ( 𝑃 pCnt ( 1 / 𝐴 ) ) = ( ( 𝑃 pCnt 1 ) − ( 𝑃 pCnt 𝐴 ) ) )
8 pc1 ( 𝑃 ∈ ℙ → ( 𝑃 pCnt 1 ) = 0 )
9 8 adantr ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ) → ( 𝑃 pCnt 1 ) = 0 )
10 9 oveq1d ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ) → ( ( 𝑃 pCnt 1 ) − ( 𝑃 pCnt 𝐴 ) ) = ( 0 − ( 𝑃 pCnt 𝐴 ) ) )
11 7 10 eqtrd ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ) → ( 𝑃 pCnt ( 1 / 𝐴 ) ) = ( 0 − ( 𝑃 pCnt 𝐴 ) ) )
12 df-neg - ( 𝑃 pCnt 𝐴 ) = ( 0 − ( 𝑃 pCnt 𝐴 ) )
13 11 12 eqtr4di ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) ) → ( 𝑃 pCnt ( 1 / 𝐴 ) ) = - ( 𝑃 pCnt 𝐴 ) )