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 N0(N1)=N

Proof

Step Hyp Ref Expression
1 elnn0 N0NN=0
2 1eluzge0 10
3 2 a1i N10
4 elnnuz NN1
5 4 biimpi NN1
6 elfzuzb 10N10N1
7 3 5 6 sylanbrc N10N
8 bcval2 10N(N1)=N!N1!1!
9 7 8 syl N(N1)=N!N1!1!
10 facnn2 NN!=N1! N
11 fac1 1!=1
12 11 oveq2i N1!1!=N1!1
13 nnm1nn0 NN10
14 13 faccld NN1!
15 14 nncnd NN1!
16 15 mulid1d NN1!1=N1!
17 12 16 eqtrid NN1!1!=N1!
18 10 17 oveq12d NN!N1!1!=N1! NN1!
19 nncn NN
20 14 nnne0d NN1!0
21 19 15 20 divcan3d NN1! NN1!=N
22 9 18 21 3eqtrd N(N1)=N
23 0nn0 00
24 1z 1
25 0lt1 0<1
26 25 olci 1<00<1
27 bcval4 0011<00<1(01)=0
28 23 24 26 27 mp3an (01)=0
29 oveq1 N=0(N1)=(01)
30 eqeq12 (N1)=(01)N=0(N1)=N(01)=0
31 29 30 mpancom N=0(N1)=N(01)=0
32 28 31 mpbiri N=0(N1)=N
33 22 32 jaoi NN=0(N1)=N
34 1 33 sylbi N0(N1)=N