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 ( 𝑁 ∈ ℕ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 mulridd ⊢ ( 𝑁 ∈ ℕ → ( ( ! ‘ ( 𝑁 − 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 ) = 𝑁 )