This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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