Metamath Proof Explorer


Theorem fzctr

Description: Lemma for theorems about the central binomial coefficient. (Contributed by Mario Carneiro, 8-Mar-2014) (Revised by Mario Carneiro, 2-Aug-2014)

Ref Expression
Assertion fzctr
|- ( N e. NN0 -> N e. ( 0 ... ( 2 x. N ) ) )

Proof

Step Hyp Ref Expression
1 nn0ge0
 |-  ( N e. NN0 -> 0 <_ N )
2 nn0re
 |-  ( N e. NN0 -> N e. RR )
3 nn0addge1
 |-  ( ( N e. RR /\ N e. NN0 ) -> N <_ ( N + N ) )
4 2 3 mpancom
 |-  ( N e. NN0 -> N <_ ( N + N ) )
5 nn0cn
 |-  ( N e. NN0 -> N e. CC )
6 5 2timesd
 |-  ( N e. NN0 -> ( 2 x. N ) = ( N + N ) )
7 4 6 breqtrrd
 |-  ( N e. NN0 -> N <_ ( 2 x. N ) )
8 nn0z
 |-  ( N e. NN0 -> N e. ZZ )
9 0zd
 |-  ( N e. NN0 -> 0 e. ZZ )
10 2z
 |-  2 e. ZZ
11 zmulcl
 |-  ( ( 2 e. ZZ /\ N e. ZZ ) -> ( 2 x. N ) e. ZZ )
12 10 8 11 sylancr
 |-  ( N e. NN0 -> ( 2 x. N ) e. ZZ )
13 elfz
 |-  ( ( N e. ZZ /\ 0 e. ZZ /\ ( 2 x. N ) e. ZZ ) -> ( N e. ( 0 ... ( 2 x. N ) ) <-> ( 0 <_ N /\ N <_ ( 2 x. N ) ) ) )
14 8 9 12 13 syl3anc
 |-  ( N e. NN0 -> ( N e. ( 0 ... ( 2 x. N ) ) <-> ( 0 <_ N /\ N <_ ( 2 x. N ) ) ) )
15 1 7 14 mpbir2and
 |-  ( N e. NN0 -> N e. ( 0 ... ( 2 x. N ) ) )