Theorem bcnn

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

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

Proof

Step	Hyp	Ref	Expression
1		0z	⊢ 0 ∈ ℤ
2		bccmpl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 0 ∈ ℤ ) → ( 𝑁 C 0 ) = ( 𝑁 C ( 𝑁 − 0 ) ) )
3	1 2	mpan2	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 C 0 ) = ( 𝑁 C ( 𝑁 − 0 ) ) )
4		bcn0	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 C 0 ) = 1 )
5		nn0cn	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
6	5	subid1d	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 − 0 ) = 𝑁 )
7	6	oveq2d	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 C ( 𝑁 − 0 ) ) = ( 𝑁 C 𝑁 ) )
8	3 4 7	3eqtr3rd	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 C 𝑁 ) = 1 )