pcrec

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

		Ref	Expression
	Assertion	pcrec	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0)) \to P pCnt (\frac{1}{A}) = - (P pCnt A)$

Step	Hyp	Ref	Expression
1		1z	$⊢ 1 \in ℤ$
2		zq	$⊢ 1 \in ℤ \to 1 \in ℚ$
3	1 2	ax-mp	$⊢ 1 \in ℚ$
4		ax-1ne0	$⊢ 1 \neq 0$
5	3 4	pm3.2i	$⊢ (1 \in ℚ \land 1 \neq 0)$
6		pcqdiv	$⊢ (P \in ℙ \land (1 \in ℚ \land 1 \neq 0) \land (A \in ℚ \land A \neq 0)) \to P pCnt (\frac{1}{A}) = (P pCnt 1) - (P pCnt A)$
7	5 6	mp3an2	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0)) \to P pCnt (\frac{1}{A}) = (P pCnt 1) - (P pCnt A)$
8		pc1	$⊢ P \in ℙ \to P pCnt 1 = 0$
9	8	adantr	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0)) \to P pCnt 1 = 0$
10	9	oveq1d	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0)) \to (P pCnt 1) - (P pCnt A) = 0 - (P pCnt A)$
11	7 10	eqtrd	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0)) \to P pCnt (\frac{1}{A}) = 0 - (P pCnt A)$
12		df-neg	$⊢ - (P pCnt A) = 0 - (P pCnt A)$
13	11 12	eqtr4di	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0)) \to P pCnt (\frac{1}{A}) = - (P pCnt A)$

Metamath Proof Explorer