Metamath Proof Explorer

Theorem pcid

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

Ref Expression
Assertion pcid ⊢ P ∈ ℙ ∧ A ∈ ℤ → P pCnt P A = A

Proof

Step Hyp Ref Expression
1 elznn0nn ⊢ A ∈ ℤ ↔ A ∈ ℕ 0 ∨ A ∈ ℝ ∧ − A ∈ ℕ
2 pcidlem ⊢ P ∈ ℙ ∧ A ∈ ℕ 0 → P pCnt P A = A
3 prmnn ⊢ P ∈ ℙ → P ∈ ℕ
4 3 adantr ⊢ P ∈ ℙ ∧ A ∈ ℝ ∧ − A ∈ ℕ → P ∈ ℕ
5 4 nncnd ⊢ P ∈ ℙ ∧ A ∈ ℝ ∧ − A ∈ ℕ → P ∈ ℂ
6 simprl ⊢ P ∈ ℙ ∧ A ∈ ℝ ∧ − A ∈ ℕ → A ∈ ℝ
7 6 recnd ⊢ P ∈ ℙ ∧ A ∈ ℝ ∧ − A ∈ ℕ → A ∈ ℂ
8 nnnn0 ⊢ − A ∈ ℕ → − A ∈ ℕ 0
9 8 ad2antll ⊢ P ∈ ℙ ∧ A ∈ ℝ ∧ − A ∈ ℕ → − A ∈ ℕ 0
10 expneg2 ⊢ P ∈ ℂ ∧ A ∈ ℂ ∧ − A ∈ ℕ 0 → P A = 1 P − A
11 5 7 9 10 syl3anc ⊢ P ∈ ℙ ∧ A ∈ ℝ ∧ − A ∈ ℕ → P A = 1 P − A
12 11 oveq2d ⊢ P ∈ ℙ ∧ A ∈ ℝ ∧ − A ∈ ℕ → P pCnt P A = P pCnt 1 P − A
13 simpl ⊢ P ∈ ℙ ∧ A ∈ ℝ ∧ − A ∈ ℕ → P ∈ ℙ
14 1zzd ⊢ P ∈ ℙ ∧ A ∈ ℝ ∧ − A ∈ ℕ → 1 ∈ ℤ
15 ax-1ne0 ⊢ 1 ≠ 0
16 15 a1i ⊢ P ∈ ℙ ∧ A ∈ ℝ ∧ − A ∈ ℕ → 1 ≠ 0
17 4 9 nnexpcld ⊢ P ∈ ℙ ∧ A ∈ ℝ ∧ − A ∈ ℕ → P − A ∈ ℕ
18 pcdiv ⊢ P ∈ ℙ ∧ 1 ∈ ℤ ∧ 1 ≠ 0 ∧ P − A ∈ ℕ → P pCnt 1 P − A = P pCnt 1 − P pCnt P − A
19 13 14 16 17 18 syl121anc ⊢ P ∈ ℙ ∧ A ∈ ℝ ∧ − A ∈ ℕ → P pCnt 1 P − A = P pCnt 1 − P pCnt P − A
20 pc1 ⊢ P ∈ ℙ → P pCnt 1 = 0
21 20 adantr ⊢ P ∈ ℙ ∧ A ∈ ℝ ∧ − A ∈ ℕ → P pCnt 1 = 0
22 pcidlem ⊢ P ∈ ℙ ∧ − A ∈ ℕ 0 → P pCnt P − A = − A
23 9 22 syldan ⊢ P ∈ ℙ ∧ A ∈ ℝ ∧ − A ∈ ℕ → P pCnt P − A = − A
24 21 23 oveq12d ⊢ P ∈ ℙ ∧ A ∈ ℝ ∧ − A ∈ ℕ → P pCnt 1 − P pCnt P − A = 0 − − A
25 df-neg ⊢ − − A = 0 − − A
26 7 negnegd ⊢ P ∈ ℙ ∧ A ∈ ℝ ∧ − A ∈ ℕ → − − A = A
27 25 26 eqtr3id ⊢ P ∈ ℙ ∧ A ∈ ℝ ∧ − A ∈ ℕ → 0 − − A = A
28 24 27 eqtrd ⊢ P ∈ ℙ ∧ A ∈ ℝ ∧ − A ∈ ℕ → P pCnt 1 − P pCnt P − A = A
29 19 28 eqtrd ⊢ P ∈ ℙ ∧ A ∈ ℝ ∧ − A ∈ ℕ → P pCnt 1 P − A = A
30 12 29 eqtrd ⊢ P ∈ ℙ ∧ A ∈ ℝ ∧ − A ∈ ℕ → P pCnt P A = A
31 2 30 jaodan ⊢ P ∈ ℙ ∧ A ∈ ℕ 0 ∨ A ∈ ℝ ∧ − A ∈ ℕ → P pCnt P A = A
32 1 31 sylan2b ⊢ P ∈ ℙ ∧ A ∈ ℤ → P pCnt P A = A