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

Metamath Proof Explorer

Theorem bcn1

Description: Binomial coefficient: N choose 1 . (Contributed by NM, 21-Jun-2005) (Revised by Mario Carneiro, 8-Nov-2013)

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

Proof

Step Hyp Ref Expression
1 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
2 1eluzge0 
 |-  1 e. ( ZZ>= ` 0 )
3 2 a1i 
 |-  ( N e. NN -> 1 e. ( ZZ>= ` 0 ) )
4 elnnuz 
 |-  ( N e. NN <-> N e. ( ZZ>= ` 1 ) )
5 4 biimpi 
 |-  ( N e. NN -> N e. ( ZZ>= ` 1 ) )
6 elfzuzb 
 |-  ( 1 e. ( 0 ... N ) <-> ( 1 e. ( ZZ>= ` 0 ) /\ N e. ( ZZ>= ` 1 ) ) )
7 3 5 6 sylanbrc 
 |-  ( N e. NN -> 1 e. ( 0 ... N ) )
8 bcval2 
 |-  ( 1 e. ( 0 ... N ) -> ( N _C 1 ) = ( ( ! ` N ) / ( ( ! ` ( N - 1 ) ) x. ( ! ` 1 ) ) ) )
9 7 8 syl 
 |-  ( N e. NN -> ( N _C 1 ) = ( ( ! ` N ) / ( ( ! ` ( N - 1 ) ) x. ( ! ` 1 ) ) ) )
10 facnn2 
 |-  ( N e. NN -> ( ! ` N ) = ( ( ! ` ( N - 1 ) ) x. N ) )
11 fac1 
 |-  ( ! ` 1 ) = 1
12 11 oveq2i 
 |-  ( ( ! ` ( N - 1 ) ) x. ( ! ` 1 ) ) = ( ( ! ` ( N - 1 ) ) x. 1 )
13 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
14 13 faccld 
 |-  ( N e. NN -> ( ! ` ( N - 1 ) ) e. NN )
15 14 nncnd 
 |-  ( N e. NN -> ( ! ` ( N - 1 ) ) e. CC )
16 15 mulridd 
 |-  ( N e. NN -> ( ( ! ` ( N - 1 ) ) x. 1 ) = ( ! ` ( N - 1 ) ) )
17 12 16 eqtrid 
 |-  ( N e. NN -> ( ( ! ` ( N - 1 ) ) x. ( ! ` 1 ) ) = ( ! ` ( N - 1 ) ) )
18 10 17 oveq12d 
 |-  ( N e. NN -> ( ( ! ` N ) / ( ( ! ` ( N - 1 ) ) x. ( ! ` 1 ) ) ) = ( ( ( ! ` ( N - 1 ) ) x. N ) / ( ! ` ( N - 1 ) ) ) )
19 nncn 
 |-  ( N e. NN -> N e. CC )
20 14 nnne0d 
 |-  ( N e. NN -> ( ! ` ( N - 1 ) ) =/= 0 )
21 19 15 20 divcan3d 
 |-  ( N e. NN -> ( ( ( ! ` ( N - 1 ) ) x. N ) / ( ! ` ( N - 1 ) ) ) = N )
22 9 18 21 3eqtrd 
 |-  ( N e. NN -> ( N _C 1 ) = N )
23 0nn0 
 |-  0 e. NN0
24 1z 
 |-  1 e. ZZ
25 0lt1 
 |-  0 < 1
26 25 olci 
 |-  ( 1 < 0 \/ 0 < 1 )
27 bcval4 
 |-  ( ( 0 e. NN0 /\ 1 e. ZZ /\ ( 1 < 0 \/ 0 < 1 ) ) -> ( 0 _C 1 ) = 0 )
28 23 24 26 27 mp3an 
 |-  ( 0 _C 1 ) = 0
29 oveq1 
 |-  ( N = 0 -> ( N _C 1 ) = ( 0 _C 1 ) )
30 eqeq12 
 |-  ( ( ( N _C 1 ) = ( 0 _C 1 ) /\ N = 0 ) -> ( ( N _C 1 ) = N <-> ( 0 _C 1 ) = 0 ) )
31 29 30 mpancom 
 |-  ( N = 0 -> ( ( N _C 1 ) = N <-> ( 0 _C 1 ) = 0 ) )
32 28 31 mpbiri 
 |-  ( N = 0 -> ( N _C 1 ) = N )
33 22 32 jaoi 
 |-  ( ( N e. NN \/ N = 0 ) -> ( N _C 1 ) = N )
34 1 33 sylbi 
 |-  ( N e. NN0 -> ( N _C 1 ) = N )