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