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