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