Theorem bccbc

Description: The binomial coefficient and generalized binomial coefficient are equal when their arguments are nonnegative integers. (Contributed by Steve Rodriguez, 22-Apr-2020)

	Ref	Expression
Hypotheses	bccbc.c	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	bccbc.k	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
Assertion	bccbc	⊢ ( 𝜑 → ( 𝑁 C𝑐 𝐾 ) = ( 𝑁 C 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		bccbc.c	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
2		bccbc.k	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
3	1	nn0cnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
4	3 2	bccval	⊢ ( 𝜑 → ( 𝑁 C𝑐 𝐾 ) = ( ( 𝑁 FallFac 𝐾 ) / ( ! ‘ 𝐾 ) ) )
5	4	adantr	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C𝑐 𝐾 ) = ( ( 𝑁 FallFac 𝐾 ) / ( ! ‘ 𝐾 ) ) )
6		bcfallfac	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝐾 ) = ( ( 𝑁 FallFac 𝐾 ) / ( ! ‘ 𝐾 ) ) )
7	6	adantl	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝐾 ) = ( ( 𝑁 FallFac 𝐾 ) / ( ! ‘ 𝐾 ) ) )
8	5 7	eqtr4d	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C𝑐 𝐾 ) = ( 𝑁 C 𝐾 ) )
9		nn0split	⊢ ( 𝑁 ∈ ℕ0 → ℕ0 = ( ( 0 ... 𝑁 ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) )
10	1 9	syl	⊢ ( 𝜑 → ℕ0 = ( ( 0 ... 𝑁 ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) )
11	2 10	eleqtrd	⊢ ( 𝜑 → 𝐾 ∈ ( ( 0 ... 𝑁 ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) )
12		elun	⊢ ( 𝐾 ∈ ( ( 0 ... 𝑁 ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ↔ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∨ 𝐾 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) )
13	11 12	sylib	⊢ ( 𝜑 → ( 𝐾 ∈ ( 0 ... 𝑁 ) ∨ 𝐾 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) )
14	13	orcanai	⊢ ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 𝐾 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) )
15		eluzle	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) → ( 𝑁 + 1 ) ≤ 𝐾 )
16	15	adantl	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( 𝑁 + 1 ) ≤ 𝐾 )
17	1	nn0zd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
18	2	nn0zd	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
19		zltp1le	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑁 < 𝐾 ↔ ( 𝑁 + 1 ) ≤ 𝐾 ) )
20	17 18 19	syl2anc	⊢ ( 𝜑 → ( 𝑁 < 𝐾 ↔ ( 𝑁 + 1 ) ≤ 𝐾 ) )
21	20	adantr	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( 𝑁 < 𝐾 ↔ ( 𝑁 + 1 ) ≤ 𝐾 ) )
22	16 21	mpbird	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑁 < 𝐾 )
23	14 22	syldan	⊢ ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 𝑁 < 𝐾 )
24	1	nn0ge0d	⊢ ( 𝜑 → 0 ≤ 𝑁 )
25		0zd	⊢ ( 𝜑 → 0 ∈ ℤ )
26		elfzo	⊢ ( ( 𝑁 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑁 ∈ ( 0 ..^ 𝐾 ) ↔ ( 0 ≤ 𝑁 ∧ 𝑁 < 𝐾 ) ) )
27	17 25 18 26	syl3anc	⊢ ( 𝜑 → ( 𝑁 ∈ ( 0 ..^ 𝐾 ) ↔ ( 0 ≤ 𝑁 ∧ 𝑁 < 𝐾 ) ) )
28	27	biimpar	⊢ ( ( 𝜑 ∧ ( 0 ≤ 𝑁 ∧ 𝑁 < 𝐾 ) ) → 𝑁 ∈ ( 0 ..^ 𝐾 ) )
29		fzoval	⊢ ( 𝐾 ∈ ℤ → ( 0 ..^ 𝐾 ) = ( 0 ... ( 𝐾 − 1 ) ) )
30	18 29	syl	⊢ ( 𝜑 → ( 0 ..^ 𝐾 ) = ( 0 ... ( 𝐾 − 1 ) ) )
31	30	eleq2d	⊢ ( 𝜑 → ( 𝑁 ∈ ( 0 ..^ 𝐾 ) ↔ 𝑁 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) )
32	31	biimpa	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( 0 ..^ 𝐾 ) ) → 𝑁 ∈ ( 0 ... ( 𝐾 − 1 ) ) )
33	3 2	bcc0	⊢ ( 𝜑 → ( ( 𝑁 C𝑐 𝐾 ) = 0 ↔ 𝑁 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) )
34	33	biimpar	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝑁 C𝑐 𝐾 ) = 0 )
35	32 34	syldan	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( 0 ..^ 𝐾 ) ) → ( 𝑁 C𝑐 𝐾 ) = 0 )
36	28 35	syldan	⊢ ( ( 𝜑 ∧ ( 0 ≤ 𝑁 ∧ 𝑁 < 𝐾 ) ) → ( 𝑁 C𝑐 𝐾 ) = 0 )
37	24 36	sylanr1	⊢ ( ( 𝜑 ∧ ( 𝜑 ∧ 𝑁 < 𝐾 ) ) → ( 𝑁 C𝑐 𝐾 ) = 0 )
38	37	anabss5	⊢ ( ( 𝜑 ∧ 𝑁 < 𝐾 ) → ( 𝑁 C𝑐 𝐾 ) = 0 )
39	23 38	syldan	⊢ ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C𝑐 𝐾 ) = 0 )
40	1 18	jca	⊢ ( 𝜑 → ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) )
41		bcval3	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝐾 ) = 0 )
42	41	3expa	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝐾 ) = 0 )
43	40 42	sylan	⊢ ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝐾 ) = 0 )
44	39 43	eqtr4d	⊢ ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C𝑐 𝐾 ) = ( 𝑁 C 𝐾 ) )
45	8 44	pm2.61dan	⊢ ( 𝜑 → ( 𝑁 C𝑐 𝐾 ) = ( 𝑁 C 𝐾 ) )