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

Proof

Step Hyp Ref Expression
1 elnn0 ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
2 1eluzge0 1 ∈ ( ℤ ‘ 0 )
3 2 a1i ( 𝑁 ∈ ℕ → 1 ∈ ( ℤ ‘ 0 ) )
4 elnnuz ( 𝑁 ∈ ℕ ↔ 𝑁 ∈ ( ℤ ‘ 1 ) )
5 4 biimpi ( 𝑁 ∈ ℕ → 𝑁 ∈ ( ℤ ‘ 1 ) )
6 elfzuzb ( 1 ∈ ( 0 ... 𝑁 ) ↔ ( 1 ∈ ( ℤ ‘ 0 ) ∧ 𝑁 ∈ ( ℤ ‘ 1 ) ) )
7 3 5 6 sylanbrc ( 𝑁 ∈ ℕ → 1 ∈ ( 0 ... 𝑁 ) )
8 bcval2 ( 1 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 1 ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 1 ) ) · ( ! ‘ 1 ) ) ) )
9 7 8 syl ( 𝑁 ∈ ℕ → ( 𝑁 C 1 ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 1 ) ) · ( ! ‘ 1 ) ) ) )
10 facnn2 ( 𝑁 ∈ ℕ → ( ! ‘ 𝑁 ) = ( ( ! ‘ ( 𝑁 − 1 ) ) · 𝑁 ) )
11 fac1 ( ! ‘ 1 ) = 1
12 11 oveq2i ( ( ! ‘ ( 𝑁 − 1 ) ) · ( ! ‘ 1 ) ) = ( ( ! ‘ ( 𝑁 − 1 ) ) · 1 )
13 nnm1nn0 ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
14 13 faccld ( 𝑁 ∈ ℕ → ( ! ‘ ( 𝑁 − 1 ) ) ∈ ℕ )
15 14 nncnd ( 𝑁 ∈ ℕ → ( ! ‘ ( 𝑁 − 1 ) ) ∈ ℂ )
16 15 mulid1d ( 𝑁 ∈ ℕ → ( ( ! ‘ ( 𝑁 − 1 ) ) · 1 ) = ( ! ‘ ( 𝑁 − 1 ) ) )
17 12 16 eqtrid ( 𝑁 ∈ ℕ → ( ( ! ‘ ( 𝑁 − 1 ) ) · ( ! ‘ 1 ) ) = ( ! ‘ ( 𝑁 − 1 ) ) )
18 10 17 oveq12d ( 𝑁 ∈ ℕ → ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 1 ) ) · ( ! ‘ 1 ) ) ) = ( ( ( ! ‘ ( 𝑁 − 1 ) ) · 𝑁 ) / ( ! ‘ ( 𝑁 − 1 ) ) ) )
19 nncn ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
20 14 nnne0d ( 𝑁 ∈ ℕ → ( ! ‘ ( 𝑁 − 1 ) ) ≠ 0 )
21 19 15 20 divcan3d ( 𝑁 ∈ ℕ → ( ( ( ! ‘ ( 𝑁 − 1 ) ) · 𝑁 ) / ( ! ‘ ( 𝑁 − 1 ) ) ) = 𝑁 )
22 9 18 21 3eqtrd ( 𝑁 ∈ ℕ → ( 𝑁 C 1 ) = 𝑁 )
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 C 1 ) = 0 )
28 23 24 26 27 mp3an ( 0 C 1 ) = 0
29 oveq1 ( 𝑁 = 0 → ( 𝑁 C 1 ) = ( 0 C 1 ) )
30 eqeq12 ( ( ( 𝑁 C 1 ) = ( 0 C 1 ) ∧ 𝑁 = 0 ) → ( ( 𝑁 C 1 ) = 𝑁 ↔ ( 0 C 1 ) = 0 ) )
31 29 30 mpancom ( 𝑁 = 0 → ( ( 𝑁 C 1 ) = 𝑁 ↔ ( 0 C 1 ) = 0 ) )
32 28 31 mpbiri ( 𝑁 = 0 → ( 𝑁 C 1 ) = 𝑁 )
33 22 32 jaoi ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) → ( 𝑁 C 1 ) = 𝑁 )
34 1 33 sylbi ( 𝑁 ∈ ℕ0 → ( 𝑁 C 1 ) = 𝑁 )