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