pcid

Description: The prime count of a prime power. (Contributed by Mario Carneiro, 9-Sep-2014)

		Ref	Expression
	Assertion	pcid	$⊢ (P \in ℙ \land A \in ℤ) \to P pCnt P^{A} = A$

Proof

Step	Hyp	Ref	Expression
1		elznn0nn	$⊢ A \in ℤ \leftrightarrow (A \in ℕ_{0} \lor (A \in ℝ \land - A \in ℕ))$
2		pcidlem	$⊢ (P \in ℙ \land A \in ℕ_{0}) \to P pCnt P^{A} = A$
3		prmnn	$⊢ P \in ℙ \to P \in ℕ$
4	3	adantr	$⊢ (P \in ℙ \land (A \in ℝ \land - A \in ℕ)) \to P \in ℕ$
5	4	nncnd	$⊢ (P \in ℙ \land (A \in ℝ \land - A \in ℕ)) \to P \in ℂ$
6		simprl	$⊢ (P \in ℙ \land (A \in ℝ \land - A \in ℕ)) \to A \in ℝ$
7	6	recnd	$⊢ (P \in ℙ \land (A \in ℝ \land - A \in ℕ)) \to A \in ℂ$
8		nnnn0	$⊢ - A \in ℕ \to - A \in ℕ_{0}$
9	8	ad2antll	$⊢ (P \in ℙ \land (A \in ℝ \land - A \in ℕ)) \to - A \in ℕ_{0}$
10		expneg2	$⊢ (P \in ℂ \land A \in ℂ \land - A \in ℕ_{0}) \to P^{A} = \frac{1}{P^{- A}}$
11	5 7 9 10	syl3anc	$⊢ (P \in ℙ \land (A \in ℝ \land - A \in ℕ)) \to P^{A} = \frac{1}{P^{- A}}$
12	11	oveq2d	$⊢ (P \in ℙ \land (A \in ℝ \land - A \in ℕ)) \to P pCnt P^{A} = P pCnt (\frac{1}{P^{- A}})$
13		simpl	$⊢ (P \in ℙ \land (A \in ℝ \land - A \in ℕ)) \to P \in ℙ$
14		1zzd	$⊢ (P \in ℙ \land (A \in ℝ \land - A \in ℕ)) \to 1 \in ℤ$
15		ax-1ne0	$⊢ 1 \neq 0$
16	15	a1i	$⊢ (P \in ℙ \land (A \in ℝ \land - A \in ℕ)) \to 1 \neq 0$
17	4 9	nnexpcld	$⊢ (P \in ℙ \land (A \in ℝ \land - A \in ℕ)) \to P^{- A} \in ℕ$
18		pcdiv	$⊢ (P \in ℙ \land (1 \in ℤ \land 1 \neq 0) \land P^{- A} \in ℕ) \to P pCnt (\frac{1}{P^{- A}}) = (P pCnt 1) - (P pCnt P^{- A})$
19	13 14 16 17 18	syl121anc	$⊢ (P \in ℙ \land (A \in ℝ \land - A \in ℕ)) \to P pCnt (\frac{1}{P^{- A}}) = (P pCnt 1) - (P pCnt P^{- A})$
20		pc1	$⊢ P \in ℙ \to P pCnt 1 = 0$
21	20	adantr	$⊢ (P \in ℙ \land (A \in ℝ \land - A \in ℕ)) \to P pCnt 1 = 0$
22		pcidlem	$⊢ (P \in ℙ \land - A \in ℕ_{0}) \to P pCnt P^{- A} = - A$
23	9 22	syldan	$⊢ (P \in ℙ \land (A \in ℝ \land - A \in ℕ)) \to P pCnt P^{- A} = - A$
24	21 23	oveq12d	$⊢ (P \in ℙ \land (A \in ℝ \land - A \in ℕ)) \to (P pCnt 1) - (P pCnt P^{- A}) = 0 - (- A)$
25		df-neg	$⊢ - (- A) = 0 - (- A)$
26	7	negnegd	$⊢ (P \in ℙ \land (A \in ℝ \land - A \in ℕ)) \to - (- A) = A$
27	25 26	eqtr3id	$⊢ (P \in ℙ \land (A \in ℝ \land - A \in ℕ)) \to 0 - (- A) = A$
28	24 27	eqtrd	$⊢ (P \in ℙ \land (A \in ℝ \land - A \in ℕ)) \to (P pCnt 1) - (P pCnt P^{- A}) = A$
29	19 28	eqtrd	$⊢ (P \in ℙ \land (A \in ℝ \land - A \in ℕ)) \to P pCnt (\frac{1}{P^{- A}}) = A$
30	12 29	eqtrd	$⊢ (P \in ℙ \land (A \in ℝ \land - A \in ℕ)) \to P pCnt P^{A} = A$
31	2 30	jaodan	$⊢ (P \in ℙ \land (A \in ℕ_{0} \lor (A \in ℝ \land - A \in ℕ))) \to P pCnt P^{A} = A$
32	1 31	sylan2b	$⊢ (P \in ℙ \land A \in ℤ) \to P pCnt P^{A} = A$

Metamath Proof Explorer

Theorem pcid

Proof