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 ∈ ℕ 0 → ( N 1 ) = N

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ N ∈ ℕ 0 ↔ N ∈ ℕ ∨ N = 0
2 1eluzge0 ⊢ 1 ∈ ℤ ≥ 0
3 2 a1i ⊢ N ∈ ℕ → 1 ∈ ℤ ≥ 0
4 elnnuz ⊢ N ∈ ℕ ↔ N ∈ ℤ ≥ 1
5 4 biimpi ⊢ N ∈ ℕ → N ∈ ℤ ≥ 1
6 elfzuzb ⊢ 1 ∈ 0 … N ↔ 1 ∈ ℤ ≥ 0 ∧ N ∈ ℤ ≥ 1
7 3 5 6 sylanbrc ⊢ N ∈ ℕ → 1 ∈ 0 … N
8 bcval2 ⊢ 1 ∈ 0 … N → ( N 1 ) = N ! N − 1 ! ⁢ 1 !
9 7 8 syl ⊢ N ∈ ℕ → ( N 1 ) = N ! N − 1 ! ⁢ 1 !
10 facnn2 ⊢ N ∈ ℕ → N ! = N − 1 ! ⋅ N
11 fac1 ⊢ 1 ! = 1
12 11 oveq2i ⊢ N − 1 ! ⁢ 1 ! = N − 1 ! ⋅ 1
13 nnm1nn0 ⊢ N ∈ ℕ → N − 1 ∈ ℕ 0
14 13 faccld ⊢ N ∈ ℕ → N − 1 ! ∈ ℕ
15 14 nncnd ⊢ N ∈ ℕ → N − 1 ! ∈ ℂ
16 15 mulridd ⊢ N ∈ ℕ → N − 1 ! ⋅ 1 = N − 1 !
17 12 16 eqtrid ⊢ N ∈ ℕ → N − 1 ! ⁢ 1 ! = N − 1 !
18 10 17 oveq12d ⊢ N ∈ ℕ → N ! N − 1 ! ⁢ 1 ! = N − 1 ! ⋅ N N − 1 !
19 nncn ⊢ N ∈ ℕ → N ∈ ℂ
20 14 nnne0d ⊢ N ∈ ℕ → N − 1 ! ≠ 0
21 19 15 20 divcan3d ⊢ N ∈ ℕ → N − 1 ! ⋅ N N − 1 ! = N
22 9 18 21 3eqtrd ⊢ N ∈ ℕ → ( N 1 ) = N
23 0nn0 ⊢ 0 ∈ ℕ 0
24 1z ⊢ 1 ∈ ℤ
25 0lt1 ⊢ 0 < 1
26 25 olci ⊢ 1 < 0 ∨ 0 < 1
27 bcval4 ⊢ 0 ∈ ℕ 0 ∧ 1 ∈ ℤ ∧ 1 < 0 ∨ 0 < 1 → ( 0 1 ) = 0
28 23 24 26 27 mp3an ⊢ ( 0 1 ) = 0
29 oveq1 ⊢ N = 0 → ( N 1 ) = ( 0 1 )
30 eqeq12 ⊢ ( N 1 ) = ( 0 1 ) ∧ N = 0 → ( N 1 ) = N ↔ ( 0 1 ) = 0
31 29 30 mpancom ⊢ N = 0 → ( N 1 ) = N ↔ ( 0 1 ) = 0
32 28 31 mpbiri ⊢ N = 0 → ( N 1 ) = N
33 22 32 jaoi ⊢ N ∈ ℕ ∨ N = 0 → ( N 1 ) = N
34 1 33 sylbi ⊢ N ∈ ℕ 0 → ( N 1 ) = N