bcp1ctr

Description: Ratio of two central binomial coefficients. (Contributed by Mario Carneiro, 10-Mar-2014)

		Ref	Expression
	Assertion	bcp1ctr	$⊢ N \in ℕ_{0} \to (\binom{2 (N + 1)}{N + 1}) = (\binom{2 \cdot N}{N}) 2 (\frac{2 \cdot N + 1}{N + 1})$

Proof

Step	Hyp	Ref	Expression
1		2t1e2	$⊢ 2 \cdot 1 = 2$
2		df-2	$⊢ 2 = 1 + 1$
3	1 2	eqtri	$⊢ 2 \cdot 1 = 1 + 1$
4	3	oveq2i	$⊢ 2 \cdot N + 2 \cdot 1 = 2 \cdot N + 1 + 1$
5		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
6		2cn	$⊢ 2 \in ℂ$
7		ax-1cn	$⊢ 1 \in ℂ$
8		adddi	$⊢ (2 \in ℂ \land N \in ℂ \land 1 \in ℂ) \to 2 (N + 1) = 2 \cdot N + 2 \cdot 1$
9	6 7 8	mp3an13	$⊢ N \in ℂ \to 2 (N + 1) = 2 \cdot N + 2 \cdot 1$
10	5 9	syl	$⊢ N \in ℕ_{0} \to 2 (N + 1) = 2 \cdot N + 2 \cdot 1$
11		2nn0	$⊢ 2 \in ℕ_{0}$
12		nn0mulcl	$⊢ (2 \in ℕ_{0} \land N \in ℕ_{0}) \to 2 \cdot N \in ℕ_{0}$
13	11 12	mpan	$⊢ N \in ℕ_{0} \to 2 \cdot N \in ℕ_{0}$
14	13	nn0cnd	$⊢ N \in ℕ_{0} \to 2 \cdot N \in ℂ$
15		addass	$⊢ (2 \cdot N \in ℂ \land 1 \in ℂ \land 1 \in ℂ) \to 2 \cdot N + 1 + 1 = 2 \cdot N + 1 + 1$
16	7 7 15	mp3an23	$⊢ 2 \cdot N \in ℂ \to 2 \cdot N + 1 + 1 = 2 \cdot N + 1 + 1$
17	14 16	syl	$⊢ N \in ℕ_{0} \to 2 \cdot N + 1 + 1 = 2 \cdot N + 1 + 1$
18	4 10 17	3eqtr4a	$⊢ N \in ℕ_{0} \to 2 (N + 1) = 2 \cdot N + 1 + 1$
19	18	oveq1d	$⊢ N \in ℕ_{0} \to (\binom{2 (N + 1)}{N + 1}) = (\binom{2 \cdot N + 1 + 1}{N + 1})$
20		peano2nn0	$⊢ 2 \cdot N \in ℕ_{0} \to 2 \cdot N + 1 \in ℕ_{0}$
21	13 20	syl	$⊢ N \in ℕ_{0} \to 2 \cdot N + 1 \in ℕ_{0}$
22		nn0p1nn	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ$
23	22	nnzd	$⊢ N \in ℕ_{0} \to N + 1 \in ℤ$
24		bcpasc	$⊢ (2 \cdot N + 1 \in ℕ_{0} \land N + 1 \in ℤ) \to (\binom{2 \cdot N + 1}{N + 1}) + (\binom{2 \cdot N + 1}{N + 1 - 1}) = (\binom{2 \cdot N + 1 + 1}{N + 1})$
25	21 23 24	syl2anc	$⊢ N \in ℕ_{0} \to (\binom{2 \cdot N + 1}{N + 1}) + (\binom{2 \cdot N + 1}{N + 1 - 1}) = (\binom{2 \cdot N + 1 + 1}{N + 1})$
26	19 25	eqtr4d	$⊢ N \in ℕ_{0} \to (\binom{2 (N + 1)}{N + 1}) = (\binom{2 \cdot N + 1}{N + 1}) + (\binom{2 \cdot N + 1}{N + 1 - 1})$
27		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
28		bccl	$⊢ (2 \cdot N \in ℕ_{0} \land N \in ℤ) \to (\binom{2 \cdot N}{N}) \in ℕ_{0}$
29	13 27 28	syl2anc	$⊢ N \in ℕ_{0} \to (\binom{2 \cdot N}{N}) \in ℕ_{0}$
30	29	nn0cnd	$⊢ N \in ℕ_{0} \to (\binom{2 \cdot N}{N}) \in ℂ$
31		2cnd	$⊢ N \in ℕ_{0} \to 2 \in ℂ$
32	21	nn0red	$⊢ N \in ℕ_{0} \to 2 \cdot N + 1 \in ℝ$
33	32 22	nndivred	$⊢ N \in ℕ_{0} \to \frac{2 \cdot N + 1}{N + 1} \in ℝ$
34	33	recnd	$⊢ N \in ℕ_{0} \to \frac{2 \cdot N + 1}{N + 1} \in ℂ$
35	30 31 34	mul12d	$⊢ N \in ℕ_{0} \to (\binom{2 \cdot N}{N}) 2 (\frac{2 \cdot N + 1}{N + 1}) = 2 (\binom{2 \cdot N}{N}) (\frac{2 \cdot N + 1}{N + 1})$
36		1cnd	$⊢ N \in ℕ_{0} \to 1 \in ℂ$
37	14 36 5	addsubd	$⊢ N \in ℕ_{0} \to 2 \cdot N + 1 - N = 2 \cdot N - N + 1$
38	5	2timesd	$⊢ N \in ℕ_{0} \to 2 \cdot N = N + N$
39	5 5 38	mvrladdd	$⊢ N \in ℕ_{0} \to 2 \cdot N - N = N$
40	39	oveq1d	$⊢ N \in ℕ_{0} \to 2 \cdot N - N + 1 = N + 1$
41	37 40	eqtr2d	$⊢ N \in ℕ_{0} \to N + 1 = 2 \cdot N + 1 - N$
42	41	oveq2d	$⊢ N \in ℕ_{0} \to \frac{2 \cdot N + 1}{N + 1} = \frac{2 \cdot N + 1}{2 \cdot N + 1 - N}$
43	42	oveq2d	$⊢ N \in ℕ_{0} \to (\binom{2 \cdot N}{N}) (\frac{2 \cdot N + 1}{N + 1}) = (\binom{2 \cdot N}{N}) (\frac{2 \cdot N + 1}{2 \cdot N + 1 - N})$
44		fzctr	$⊢ N \in ℕ_{0} \to N \in (0 \dots 2 \cdot N)$
45		bcp1n	$⊢ N \in (0 \dots 2 \cdot N) \to (\binom{2 \cdot N + 1}{N}) = (\binom{2 \cdot N}{N}) (\frac{2 \cdot N + 1}{2 \cdot N + 1 - N})$
46	44 45	syl	$⊢ N \in ℕ_{0} \to (\binom{2 \cdot N + 1}{N}) = (\binom{2 \cdot N}{N}) (\frac{2 \cdot N + 1}{2 \cdot N + 1 - N})$
47	43 46	eqtr4d	$⊢ N \in ℕ_{0} \to (\binom{2 \cdot N}{N}) (\frac{2 \cdot N + 1}{N + 1}) = (\binom{2 \cdot N + 1}{N})$
48	47	oveq2d	$⊢ N \in ℕ_{0} \to 2 (\binom{2 \cdot N}{N}) (\frac{2 \cdot N + 1}{N + 1}) = 2 (\binom{2 \cdot N + 1}{N})$
49	35 48	eqtrd	$⊢ N \in ℕ_{0} \to (\binom{2 \cdot N}{N}) 2 (\frac{2 \cdot N + 1}{N + 1}) = 2 (\binom{2 \cdot N + 1}{N})$
50		bccmpl	$⊢ (2 \cdot N + 1 \in ℕ_{0} \land N + 1 \in ℤ) \to (\binom{2 \cdot N + 1}{N + 1}) = (\binom{2 \cdot N + 1}{2 \cdot N + 1 - (N + 1)})$
51	21 23 50	syl2anc	$⊢ N \in ℕ_{0} \to (\binom{2 \cdot N + 1}{N + 1}) = (\binom{2 \cdot N + 1}{2 \cdot N + 1 - (N + 1)})$
52	22	nncnd	$⊢ N \in ℕ_{0} \to N + 1 \in ℂ$
53	38	oveq1d	$⊢ N \in ℕ_{0} \to 2 \cdot N + 1 = N + N + 1$
54	5 5 36	addassd	$⊢ N \in ℕ_{0} \to N + N + 1 = N + N + 1$
55	53 54	eqtrd	$⊢ N \in ℕ_{0} \to 2 \cdot N + 1 = N + N + 1$
56	5 52 55	mvrraddd	$⊢ N \in ℕ_{0} \to 2 \cdot N + 1 - (N + 1) = N$
57	56	oveq2d	$⊢ N \in ℕ_{0} \to (\binom{2 \cdot N + 1}{2 \cdot N + 1 - (N + 1)}) = (\binom{2 \cdot N + 1}{N})$
58	51 57	eqtrd	$⊢ N \in ℕ_{0} \to (\binom{2 \cdot N + 1}{N + 1}) = (\binom{2 \cdot N + 1}{N})$
59		pncan	$⊢ (N \in ℂ \land 1 \in ℂ) \to N + 1 - 1 = N$
60	5 7 59	sylancl	$⊢ N \in ℕ_{0} \to N + 1 - 1 = N$
61	60	oveq2d	$⊢ N \in ℕ_{0} \to (\binom{2 \cdot N + 1}{N + 1 - 1}) = (\binom{2 \cdot N + 1}{N})$
62	58 61	oveq12d	$⊢ N \in ℕ_{0} \to (\binom{2 \cdot N + 1}{N + 1}) + (\binom{2 \cdot N + 1}{N + 1 - 1}) = (\binom{2 \cdot N + 1}{N}) + (\binom{2 \cdot N + 1}{N})$
63		bccl	$⊢ (2 \cdot N + 1 \in ℕ_{0} \land N \in ℤ) \to (\binom{2 \cdot N + 1}{N}) \in ℕ_{0}$
64	21 27 63	syl2anc	$⊢ N \in ℕ_{0} \to (\binom{2 \cdot N + 1}{N}) \in ℕ_{0}$
65	64	nn0cnd	$⊢ N \in ℕ_{0} \to (\binom{2 \cdot N + 1}{N}) \in ℂ$
66	65	2timesd	$⊢ N \in ℕ_{0} \to 2 (\binom{2 \cdot N + 1}{N}) = (\binom{2 \cdot N + 1}{N}) + (\binom{2 \cdot N + 1}{N})$
67	62 66	eqtr4d	$⊢ N \in ℕ_{0} \to (\binom{2 \cdot N + 1}{N + 1}) + (\binom{2 \cdot N + 1}{N + 1 - 1}) = 2 (\binom{2 \cdot N + 1}{N})$
68	49 67	eqtr4d	$⊢ N \in ℕ_{0} \to (\binom{2 \cdot N}{N}) 2 (\frac{2 \cdot N + 1}{N + 1}) = (\binom{2 \cdot N + 1}{N + 1}) + (\binom{2 \cdot N + 1}{N + 1 - 1})$
69	26 68	eqtr4d	$⊢ N \in ℕ_{0} \to (\binom{2 (N + 1)}{N + 1}) = (\binom{2 \cdot N}{N}) 2 (\frac{2 \cdot N + 1}{N + 1})$

Metamath Proof Explorer

Theorem bcp1ctr

Proof