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

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