Metamath Proof Explorer

Theorem bcn0

Description: N choose 0 is 1. Remark in Gleason p. 296. (Contributed by NM, 17-Jun-2005) (Revised by Mario Carneiro, 8-Nov-2013)

Ref Expression
Assertion bcn0 
|- ( N e. NN0 -> ( N _C 0 ) = 1 )

Proof

Step Hyp Ref Expression
1 0elfz 
 |-  ( N e. NN0 -> 0 e. ( 0 ... N ) )
2 bcval2 
 |-  ( 0 e. ( 0 ... N ) -> ( N _C 0 ) = ( ( ! ` N ) / ( ( ! ` ( N - 0 ) ) x. ( ! ` 0 ) ) ) )
3 1 2 syl 
 |-  ( N e. NN0 -> ( N _C 0 ) = ( ( ! ` N ) / ( ( ! ` ( N - 0 ) ) x. ( ! ` 0 ) ) ) )
4 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
5 4 subid1d 
 |-  ( N e. NN0 -> ( N - 0 ) = N )
6 5 fveq2d 
 |-  ( N e. NN0 -> ( ! ` ( N - 0 ) ) = ( ! ` N ) )
7 fac0 
 |-  ( ! ` 0 ) = 1
8 oveq12 
 |-  ( ( ( ! ` ( N - 0 ) ) = ( ! ` N ) /\ ( ! ` 0 ) = 1 ) -> ( ( ! ` ( N - 0 ) ) x. ( ! ` 0 ) ) = ( ( ! ` N ) x. 1 ) )
9 6 7 8 sylancl 
 |-  ( N e. NN0 -> ( ( ! ` ( N - 0 ) ) x. ( ! ` 0 ) ) = ( ( ! ` N ) x. 1 ) )
10 faccl 
 |-  ( N e. NN0 -> ( ! ` N ) e. NN )
11 10 nncnd 
 |-  ( N e. NN0 -> ( ! ` N ) e. CC )
12 11 mulridd 
 |-  ( N e. NN0 -> ( ( ! ` N ) x. 1 ) = ( ! ` N ) )
13 9 12 eqtrd 
 |-  ( N e. NN0 -> ( ( ! ` ( N - 0 ) ) x. ( ! ` 0 ) ) = ( ! ` N ) )
14 13 oveq2d 
 |-  ( N e. NN0 -> ( ( ! ` N ) / ( ( ! ` ( N - 0 ) ) x. ( ! ` 0 ) ) ) = ( ( ! ` N ) / ( ! ` N ) ) )
15 facne0 
 |-  ( N e. NN0 -> ( ! ` N ) =/= 0 )
16 11 15 dividd 
 |-  ( N e. NN0 -> ( ( ! ` N ) / ( ! ` N ) ) = 1 )
17 14 16 eqtrd 
 |-  ( N e. NN0 -> ( ( ! ` N ) / ( ( ! ` ( N - 0 ) ) x. ( ! ` 0 ) ) ) = 1 )
18 3 17 eqtrd 
 |-  ( N e. NN0 -> ( N _C 0 ) = 1 )