# Metamath Proof Explorer

## Theorem pcid

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

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

### Proof

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