Metamath Proof Explorer

Theorem bcp1ctr

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

Ref Expression
Assertion bcp1ctr 
|- ( N e. NN0 -> ( ( 2 x. ( N + 1 ) ) _C ( N + 1 ) ) = ( ( ( 2 x. N ) _C N ) x. ( 2 x. ( ( ( 2 x. N ) + 1 ) / ( N + 1 ) ) ) ) )

Proof

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