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