This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐴 ) )