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
|
syl5eqr |
⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℝ ∧ - 𝐴 ∈ ℕ ) ) → ( 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 ( 𝑃 ↑ 𝐴 ) ) = 𝐴 ) |