This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 mulridd ⊢ ( 𝑁 ∈ ℕ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 )