Metamath Proof Explorer

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 ) ) ) ) )