pcbcctr

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

		Ref	Expression
	Assertion	pcbcctr	$⊢ (N \in ℕ \land P \in ℙ) \to P pCnt (\binom{2 \cdot N}{N}) = \sum_{k = 1}^{2 \cdot N} (⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋)$

Proof

Step	Hyp	Ref	Expression
1		2nn	$⊢ 2 \in ℕ$
2		nnmulcl	$⊢ (2 \in ℕ \land N \in ℕ) \to 2 \cdot N \in ℕ$
3	1 2	mpan	$⊢ N \in ℕ \to 2 \cdot N \in ℕ$
4	3	adantr	$⊢ (N \in ℕ \land P \in ℙ) \to 2 \cdot N \in ℕ$
5		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
6		fzctr	$⊢ N \in ℕ_{0} \to N \in (0 \dots 2 \cdot N)$
7	5 6	syl	$⊢ N \in ℕ \to N \in (0 \dots 2 \cdot N)$
8	7	adantr	$⊢ (N \in ℕ \land P \in ℙ) \to N \in (0 \dots 2 \cdot N)$
9		simpr	$⊢ (N \in ℕ \land P \in ℙ) \to P \in ℙ$
10		pcbc	$⊢ (2 \cdot N \in ℕ \land N \in (0 \dots 2 \cdot N) \land P \in ℙ) \to P pCnt (\binom{2 \cdot N}{N}) = \sum_{k = 1}^{2 \cdot N} (⌊\frac{2 \cdot N}{P^{k}}⌋ - (⌊\frac{2 \cdot N - N}{P^{k}}⌋ + ⌊\frac{N}{P^{k}}⌋))$
11	4 8 9 10	syl3anc	$⊢ (N \in ℕ \land P \in ℙ) \to P pCnt (\binom{2 \cdot N}{N}) = \sum_{k = 1}^{2 \cdot N} (⌊\frac{2 \cdot N}{P^{k}}⌋ - (⌊\frac{2 \cdot N - N}{P^{k}}⌋ + ⌊\frac{N}{P^{k}}⌋))$
12		nncn	$⊢ N \in ℕ \to N \in ℂ$
13	12	2timesd	$⊢ N \in ℕ \to 2 \cdot N = N + N$
14	12 12 13	mvrladdd	$⊢ N \in ℕ \to 2 \cdot N - N = N$
15	14	fvoveq1d	$⊢ N \in ℕ \to ⌊\frac{2 \cdot N - N}{P^{k}}⌋ = ⌊\frac{N}{P^{k}}⌋$
16	15	oveq1d	$⊢ N \in ℕ \to ⌊\frac{2 \cdot N - N}{P^{k}}⌋ + ⌊\frac{N}{P^{k}}⌋ = ⌊\frac{N}{P^{k}}⌋ + ⌊\frac{N}{P^{k}}⌋$
17	16	ad2antrr	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to ⌊\frac{2 \cdot N - N}{P^{k}}⌋ + ⌊\frac{N}{P^{k}}⌋ = ⌊\frac{N}{P^{k}}⌋ + ⌊\frac{N}{P^{k}}⌋$
18		nnre	$⊢ N \in ℕ \to N \in ℝ$
19	18	ad2antrr	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to N \in ℝ$
20		prmnn	$⊢ P \in ℙ \to P \in ℕ$
21	20	adantl	$⊢ (N \in ℕ \land P \in ℙ) \to P \in ℕ$
22		elfznn	$⊢ k \in (1 \dots 2 \cdot N) \to k \in ℕ$
23	22	nnnn0d	$⊢ k \in (1 \dots 2 \cdot N) \to k \in ℕ_{0}$
24		nnexpcl	$⊢ (P \in ℕ \land k \in ℕ_{0}) \to P^{k} \in ℕ$
25	21 23 24	syl2an	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to P^{k} \in ℕ$
26	19 25	nndivred	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to \frac{N}{P^{k}} \in ℝ$
27	26	flcld	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to ⌊\frac{N}{P^{k}}⌋ \in ℤ$
28	27	zcnd	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to ⌊\frac{N}{P^{k}}⌋ \in ℂ$
29	28	2timesd	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to 2 ⌊\frac{N}{P^{k}}⌋ = ⌊\frac{N}{P^{k}}⌋ + ⌊\frac{N}{P^{k}}⌋$
30	17 29	eqtr4d	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to ⌊\frac{2 \cdot N - N}{P^{k}}⌋ + ⌊\frac{N}{P^{k}}⌋ = 2 ⌊\frac{N}{P^{k}}⌋$
31	30	oveq2d	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to ⌊\frac{2 \cdot N}{P^{k}}⌋ - (⌊\frac{2 \cdot N - N}{P^{k}}⌋ + ⌊\frac{N}{P^{k}}⌋) = ⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋$
32	31	sumeq2dv	$⊢ (N \in ℕ \land P \in ℙ) \to \sum_{k = 1}^{2 \cdot N} (⌊\frac{2 \cdot N}{P^{k}}⌋ - (⌊\frac{2 \cdot N - N}{P^{k}}⌋ + ⌊\frac{N}{P^{k}}⌋)) = \sum_{k = 1}^{2 \cdot N} (⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋)$
33	11 32	eqtrd	$⊢ (N \in ℕ \land P \in ℙ) \to P pCnt (\binom{2 \cdot N}{N}) = \sum_{k = 1}^{2 \cdot N} (⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋)$

Metamath Proof Explorer

Theorem pcbcctr

Proof