Theorem bcp1ctr

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

	Ref	Expression
Assertion	bcp1ctr	⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 · ( 𝑁 + 1 ) ) C ( 𝑁 + 1 ) ) = ( ( ( 2 · 𝑁 ) C 𝑁 ) · ( 2 · ( ( ( 2 · 𝑁 ) + 1 ) / ( 𝑁 + 1 ) ) ) ) )

Proof

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