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