Theorem bcn0

Description: N choose 0 is 1. Remark in Gleason p. 296. (Contributed by NM, 17-Jun-2005) (Revised by Mario Carneiro, 8-Nov-2013)

	Ref	Expression
Assertion	bcn0	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 C 0 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		0elfz	⊢ ( 𝑁 ∈ ℕ0 → 0 ∈ ( 0 ... 𝑁 ) )
2		bcval2	⊢ ( 0 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 0 ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 0 ) ) · ( ! ‘ 0 ) ) ) )
3	1 2	syl	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 C 0 ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 0 ) ) · ( ! ‘ 0 ) ) ) )
4		nn0cn	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
5	4	subid1d	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 − 0 ) = 𝑁 )
6	5	fveq2d	⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ ( 𝑁 − 0 ) ) = ( ! ‘ 𝑁 ) )
7		fac0	⊢ ( ! ‘ 0 ) = 1
8		oveq12	⊢ ( ( ( ! ‘ ( 𝑁 − 0 ) ) = ( ! ‘ 𝑁 ) ∧ ( ! ‘ 0 ) = 1 ) → ( ( ! ‘ ( 𝑁 − 0 ) ) · ( ! ‘ 0 ) ) = ( ( ! ‘ 𝑁 ) · 1 ) )
9	6 7 8	sylancl	⊢ ( 𝑁 ∈ ℕ0 → ( ( ! ‘ ( 𝑁 − 0 ) ) · ( ! ‘ 0 ) ) = ( ( ! ‘ 𝑁 ) · 1 ) )
10		faccl	⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ∈ ℕ )
11	10	nncnd	⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ∈ ℂ )
12	11	mulid1d	⊢ ( 𝑁 ∈ ℕ0 → ( ( ! ‘ 𝑁 ) · 1 ) = ( ! ‘ 𝑁 ) )
13	9 12	eqtrd	⊢ ( 𝑁 ∈ ℕ0 → ( ( ! ‘ ( 𝑁 − 0 ) ) · ( ! ‘ 0 ) ) = ( ! ‘ 𝑁 ) )
14	13	oveq2d	⊢ ( 𝑁 ∈ ℕ0 → ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 0 ) ) · ( ! ‘ 0 ) ) ) = ( ( ! ‘ 𝑁 ) / ( ! ‘ 𝑁 ) ) )
15		facne0	⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ≠ 0 )
16	11 15	dividd	⊢ ( 𝑁 ∈ ℕ0 → ( ( ! ‘ 𝑁 ) / ( ! ‘ 𝑁 ) ) = 1 )
17	14 16	eqtrd	⊢ ( 𝑁 ∈ ℕ0 → ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 0 ) ) · ( ! ‘ 0 ) ) ) = 1 )
18	3 17	eqtrd	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 C 0 ) = 1 )