Step |
Hyp |
Ref |
Expression |
1 |
|
2nn |
⊢ 2 ∈ ℕ |
2 |
|
nnmulcl |
⊢ ( ( 2 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 2 · 𝑁 ) ∈ ℕ ) |
3 |
1 2
|
mpan |
⊢ ( 𝑁 ∈ ℕ → ( 2 · 𝑁 ) ∈ ℕ ) |
4 |
3
|
adantr |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ) → ( 2 · 𝑁 ) ∈ ℕ ) |
5 |
|
nnnn0 |
⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 ) |
6 |
|
fzctr |
⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ( 0 ... ( 2 · 𝑁 ) ) ) |
7 |
5 6
|
syl |
⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ( 0 ... ( 2 · 𝑁 ) ) ) |
8 |
7
|
adantr |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ) → 𝑁 ∈ ( 0 ... ( 2 · 𝑁 ) ) ) |
9 |
|
simpr |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ) → 𝑃 ∈ ℙ ) |
10 |
|
pcbc |
⊢ ( ( ( 2 · 𝑁 ) ∈ ℕ ∧ 𝑁 ∈ ( 0 ... ( 2 · 𝑁 ) ) ∧ 𝑃 ∈ ℙ ) → ( 𝑃 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) = Σ 𝑘 ∈ ( 1 ... ( 2 · 𝑁 ) ) ( ( ⌊ ‘ ( ( 2 · 𝑁 ) / ( 𝑃 ↑ 𝑘 ) ) ) − ( ( ⌊ ‘ ( ( ( 2 · 𝑁 ) − 𝑁 ) / ( 𝑃 ↑ 𝑘 ) ) ) + ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) ) ) ) |
11 |
4 8 9 10
|
syl3anc |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ) → ( 𝑃 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) = Σ 𝑘 ∈ ( 1 ... ( 2 · 𝑁 ) ) ( ( ⌊ ‘ ( ( 2 · 𝑁 ) / ( 𝑃 ↑ 𝑘 ) ) ) − ( ( ⌊ ‘ ( ( ( 2 · 𝑁 ) − 𝑁 ) / ( 𝑃 ↑ 𝑘 ) ) ) + ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) ) ) ) |
12 |
|
nncn |
⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ ) |
13 |
12
|
2timesd |
⊢ ( 𝑁 ∈ ℕ → ( 2 · 𝑁 ) = ( 𝑁 + 𝑁 ) ) |
14 |
12 12 13
|
mvrladdd |
⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 𝑁 ) − 𝑁 ) = 𝑁 ) |
15 |
14
|
fvoveq1d |
⊢ ( 𝑁 ∈ ℕ → ( ⌊ ‘ ( ( ( 2 · 𝑁 ) − 𝑁 ) / ( 𝑃 ↑ 𝑘 ) ) ) = ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) ) |
16 |
15
|
oveq1d |
⊢ ( 𝑁 ∈ ℕ → ( ( ⌊ ‘ ( ( ( 2 · 𝑁 ) − 𝑁 ) / ( 𝑃 ↑ 𝑘 ) ) ) + ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) ) = ( ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) + ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) ) ) |
17 |
16
|
ad2antrr |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( 2 · 𝑁 ) ) ) → ( ( ⌊ ‘ ( ( ( 2 · 𝑁 ) − 𝑁 ) / ( 𝑃 ↑ 𝑘 ) ) ) + ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) ) = ( ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) + ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) ) ) |
18 |
|
nnre |
⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ ) |
19 |
18
|
ad2antrr |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( 2 · 𝑁 ) ) ) → 𝑁 ∈ ℝ ) |
20 |
|
prmnn |
⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ ) |
21 |
20
|
adantl |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ) → 𝑃 ∈ ℕ ) |
22 |
|
elfznn |
⊢ ( 𝑘 ∈ ( 1 ... ( 2 · 𝑁 ) ) → 𝑘 ∈ ℕ ) |
23 |
22
|
nnnn0d |
⊢ ( 𝑘 ∈ ( 1 ... ( 2 · 𝑁 ) ) → 𝑘 ∈ ℕ0 ) |
24 |
|
nnexpcl |
⊢ ( ( 𝑃 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑃 ↑ 𝑘 ) ∈ ℕ ) |
25 |
21 23 24
|
syl2an |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( 2 · 𝑁 ) ) ) → ( 𝑃 ↑ 𝑘 ) ∈ ℕ ) |
26 |
19 25
|
nndivred |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( 2 · 𝑁 ) ) ) → ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ∈ ℝ ) |
27 |
26
|
flcld |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( 2 · 𝑁 ) ) ) → ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) ∈ ℤ ) |
28 |
27
|
zcnd |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( 2 · 𝑁 ) ) ) → ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) ∈ ℂ ) |
29 |
28
|
2timesd |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( 2 · 𝑁 ) ) ) → ( 2 · ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) ) = ( ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) + ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) ) ) |
30 |
17 29
|
eqtr4d |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( 2 · 𝑁 ) ) ) → ( ( ⌊ ‘ ( ( ( 2 · 𝑁 ) − 𝑁 ) / ( 𝑃 ↑ 𝑘 ) ) ) + ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) ) = ( 2 · ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) ) ) |
31 |
30
|
oveq2d |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( 2 · 𝑁 ) ) ) → ( ( ⌊ ‘ ( ( 2 · 𝑁 ) / ( 𝑃 ↑ 𝑘 ) ) ) − ( ( ⌊ ‘ ( ( ( 2 · 𝑁 ) − 𝑁 ) / ( 𝑃 ↑ 𝑘 ) ) ) + ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) ) ) = ( ( ⌊ ‘ ( ( 2 · 𝑁 ) / ( 𝑃 ↑ 𝑘 ) ) ) − ( 2 · ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) ) ) ) |
32 |
31
|
sumeq2dv |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ) → Σ 𝑘 ∈ ( 1 ... ( 2 · 𝑁 ) ) ( ( ⌊ ‘ ( ( 2 · 𝑁 ) / ( 𝑃 ↑ 𝑘 ) ) ) − ( ( ⌊ ‘ ( ( ( 2 · 𝑁 ) − 𝑁 ) / ( 𝑃 ↑ 𝑘 ) ) ) + ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) ) ) = Σ 𝑘 ∈ ( 1 ... ( 2 · 𝑁 ) ) ( ( ⌊ ‘ ( ( 2 · 𝑁 ) / ( 𝑃 ↑ 𝑘 ) ) ) − ( 2 · ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) ) ) ) |
33 |
11 32
|
eqtrd |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ) → ( 𝑃 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) = Σ 𝑘 ∈ ( 1 ... ( 2 · 𝑁 ) ) ( ( ⌊ ‘ ( ( 2 · 𝑁 ) / ( 𝑃 ↑ 𝑘 ) ) ) − ( 2 · ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) ) ) ) |