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 ( ๐‘ โˆˆ โ„•0 โ†’ ๐‘ โˆˆ ( 0 ... ( 2 ยท ๐‘ ) ) )

Proof

Step Hyp Ref Expression
1 nn0ge0 โŠข ( ๐‘ โˆˆ โ„•0 โ†’ 0 โ‰ค ๐‘ )
2 nn0re โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ๐‘ โˆˆ โ„ )
3 nn0addge1 โŠข ( ( ๐‘ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„•0 ) โ†’ ๐‘ โ‰ค ( ๐‘ + ๐‘ ) )
4 2 3 mpancom โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ๐‘ โ‰ค ( ๐‘ + ๐‘ ) )
5 nn0cn โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ๐‘ โˆˆ โ„‚ )
6 5 2timesd โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( 2 ยท ๐‘ ) = ( ๐‘ + ๐‘ ) )
7 4 6 breqtrrd โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ๐‘ โ‰ค ( 2 ยท ๐‘ ) )
8 nn0z โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ๐‘ โˆˆ โ„ค )
9 0zd โŠข ( ๐‘ โˆˆ โ„•0 โ†’ 0 โˆˆ โ„ค )
10 2z โŠข 2 โˆˆ โ„ค
11 zmulcl โŠข ( ( 2 โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( 2 ยท ๐‘ ) โˆˆ โ„ค )
12 10 8 11 sylancr โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( 2 ยท ๐‘ ) โˆˆ โ„ค )
13 elfz โŠข ( ( ๐‘ โˆˆ โ„ค โˆง 0 โˆˆ โ„ค โˆง ( 2 ยท ๐‘ ) โˆˆ โ„ค ) โ†’ ( ๐‘ โˆˆ ( 0 ... ( 2 ยท ๐‘ ) ) โ†” ( 0 โ‰ค ๐‘ โˆง ๐‘ โ‰ค ( 2 ยท ๐‘ ) ) ) )
14 8 9 12 13 syl3anc โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( ๐‘ โˆˆ ( 0 ... ( 2 ยท ๐‘ ) ) โ†” ( 0 โ‰ค ๐‘ โˆง ๐‘ โ‰ค ( 2 ยท ๐‘ ) ) ) )
15 1 7 14 mpbir2and โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ๐‘ โˆˆ ( 0 ... ( 2 ยท ๐‘ ) ) )