Metamath Proof Explorer


Theorem pcbcctr

Description: Prime count of a central binomial coefficient. (Contributed by Mario Carneiro, 12-Mar-2014)

Ref Expression
Assertion pcbcctr ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ) → ( 𝑃 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) = Σ 𝑘 ∈ ( 1 ... ( 2 · 𝑁 ) ) ( ( ⌊ ‘ ( ( 2 · 𝑁 ) / ( 𝑃𝑘 ) ) ) − ( 2 · ( ⌊ ‘ ( 𝑁 / ( 𝑃𝑘 ) ) ) ) ) )

Proof

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 · ( ⌊ ‘ ( 𝑁 / ( 𝑃𝑘 ) ) ) ) ) )