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 ( 𝑃𝐴 ) ) = 𝐴 )