This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pcid

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

Ref Expression
Assertion pcid ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) = 𝐴 )

Proof

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