Theorem bcval5

Description: Write out the top and bottom parts of the binomial coefficient ( N _C K ) = ( N x. ( N - 1 ) x. ... x. ( ( N - K ) + 1 ) ) / K ! explicitly. In this form, it is valid even for N < K , although it is no longer valid for nonpositive K . (Contributed by Mario Carneiro, 22-May-2014)

	Ref	Expression
Assertion	bcval5	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) → ( 𝑁 C 𝐾 ) = ( ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) / ( ! ‘ 𝐾 ) ) )

Proof

Step	Hyp	Ref	Expression
1		bcval2	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝐾 ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) )
2	1	adantl	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝐾 ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) )
3		mulcl	⊢ ( ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑘 · 𝑥 ) ∈ ℂ )
4	3	adantl	⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) ∧ ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝑘 · 𝑥 ) ∈ ℂ )
5		mulass	⊢ ( ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 𝑘 · 𝑥 ) · 𝑦 ) = ( 𝑘 · ( 𝑥 · 𝑦 ) ) )
6	5	adantl	⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) ∧ ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( ( 𝑘 · 𝑥 ) · 𝑦 ) = ( 𝑘 · ( 𝑥 · 𝑦 ) ) )
7		simplr	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 𝐾 ∈ ℕ )
8		elfzuz3	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) )
9	8	adantl	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) )
10		eluznn	⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑁 ∈ ℕ )
11	7 9 10	syl2anc	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ℕ )
12	11	adantrr	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) → 𝑁 ∈ ℕ )
13		simplr	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) → 𝐾 ∈ ℕ )
14		nnre	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
15		nnrp	⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℝ+ )
16		ltsubrp	⊢ ( ( 𝑁 ∈ ℝ ∧ 𝐾 ∈ ℝ+ ) → ( 𝑁 − 𝐾 ) < 𝑁 )
17	14 15 16	syl2an	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( 𝑁 − 𝐾 ) < 𝑁 )
18	12 13 17	syl2anc	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) → ( 𝑁 − 𝐾 ) < 𝑁 )
19	12	nnzd	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) → 𝑁 ∈ ℤ )
20		nnz	⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℤ )
21	20	ad2antlr	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) → 𝐾 ∈ ℤ )
22	19 21	zsubcld	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) → ( 𝑁 − 𝐾 ) ∈ ℤ )
23		zltp1le	⊢ ( ( ( 𝑁 − 𝐾 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑁 − 𝐾 ) < 𝑁 ↔ ( ( 𝑁 − 𝐾 ) + 1 ) ≤ 𝑁 ) )
24	22 19 23	syl2anc	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) → ( ( 𝑁 − 𝐾 ) < 𝑁 ↔ ( ( 𝑁 − 𝐾 ) + 1 ) ≤ 𝑁 ) )
25	18 24	mpbid	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) → ( ( 𝑁 − 𝐾 ) + 1 ) ≤ 𝑁 )
26	22	peano2zd	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) → ( ( 𝑁 − 𝐾 ) + 1 ) ∈ ℤ )
27		eluz	⊢ ( ( ( ( 𝑁 − 𝐾 ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∈ ( ℤ≥ ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) ↔ ( ( 𝑁 − 𝐾 ) + 1 ) ≤ 𝑁 ) )
28	26 19 27	syl2anc	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) → ( 𝑁 ∈ ( ℤ≥ ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) ↔ ( ( 𝑁 − 𝐾 ) + 1 ) ≤ 𝑁 ) )
29	25 28	mpbird	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) → 𝑁 ∈ ( ℤ≥ ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) )
30		simprr	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) → ( 𝑁 − 𝐾 ) ∈ ℕ )
31		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
32	30 31	eleqtrdi	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) → ( 𝑁 − 𝐾 ) ∈ ( ℤ≥ ‘ 1 ) )
33		fvi	⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( I ‘ 𝑘 ) = 𝑘 )
34		elfzelz	⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℤ )
35	34	zcnd	⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℂ )
36	33 35	eqeltrd	⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( I ‘ 𝑘 ) ∈ ℂ )
37	36	adantl	⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( I ‘ 𝑘 ) ∈ ℂ )
38	4 6 29 32 37	seqsplit	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) → ( seq 1 ( · , I ) ‘ 𝑁 ) = ( ( seq 1 ( · , I ) ‘ ( 𝑁 − 𝐾 ) ) · ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) ) )
39		facnn	⊢ ( 𝑁 ∈ ℕ → ( ! ‘ 𝑁 ) = ( seq 1 ( · , I ) ‘ 𝑁 ) )
40	12 39	syl	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) → ( ! ‘ 𝑁 ) = ( seq 1 ( · , I ) ‘ 𝑁 ) )
41		facnn	⊢ ( ( 𝑁 − 𝐾 ) ∈ ℕ → ( ! ‘ ( 𝑁 − 𝐾 ) ) = ( seq 1 ( · , I ) ‘ ( 𝑁 − 𝐾 ) ) )
42	30 41	syl	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) → ( ! ‘ ( 𝑁 − 𝐾 ) ) = ( seq 1 ( · , I ) ‘ ( 𝑁 − 𝐾 ) ) )
43	42	oveq1d	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) → ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) ) = ( ( seq 1 ( · , I ) ‘ ( 𝑁 − 𝐾 ) ) · ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) ) )
44	38 40 43	3eqtr4d	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) → ( ! ‘ 𝑁 ) = ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) ) )
45	44	expr	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 𝐾 ) ∈ ℕ → ( ! ‘ 𝑁 ) = ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) ) ) )
46		simpll	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ℕ0 )
47		faccl	⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ∈ ℕ )
48		nncn	⊢ ( ( ! ‘ 𝑁 ) ∈ ℕ → ( ! ‘ 𝑁 ) ∈ ℂ )
49	46 47 48	3syl	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ 𝑁 ) ∈ ℂ )
50	49	mullidd	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 1 · ( ! ‘ 𝑁 ) ) = ( ! ‘ 𝑁 ) )
51	11 39	syl	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ 𝑁 ) = ( seq 1 ( · , I ) ‘ 𝑁 ) )
52	51	oveq2d	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 1 · ( ! ‘ 𝑁 ) ) = ( 1 · ( seq 1 ( · , I ) ‘ 𝑁 ) ) )
53	50 52	eqtr3d	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ 𝑁 ) = ( 1 · ( seq 1 ( · , I ) ‘ 𝑁 ) ) )
54		fveq2	⊢ ( ( 𝑁 − 𝐾 ) = 0 → ( ! ‘ ( 𝑁 − 𝐾 ) ) = ( ! ‘ 0 ) )
55		fac0	⊢ ( ! ‘ 0 ) = 1
56	54 55	eqtrdi	⊢ ( ( 𝑁 − 𝐾 ) = 0 → ( ! ‘ ( 𝑁 − 𝐾 ) ) = 1 )
57		oveq1	⊢ ( ( 𝑁 − 𝐾 ) = 0 → ( ( 𝑁 − 𝐾 ) + 1 ) = ( 0 + 1 ) )
58		0p1e1	⊢ ( 0 + 1 ) = 1
59	57 58	eqtrdi	⊢ ( ( 𝑁 − 𝐾 ) = 0 → ( ( 𝑁 − 𝐾 ) + 1 ) = 1 )
60	59	seqeq1d	⊢ ( ( 𝑁 − 𝐾 ) = 0 → seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) = seq 1 ( · , I ) )
61	60	fveq1d	⊢ ( ( 𝑁 − 𝐾 ) = 0 → ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) = ( seq 1 ( · , I ) ‘ 𝑁 ) )
62	56 61	oveq12d	⊢ ( ( 𝑁 − 𝐾 ) = 0 → ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) ) = ( 1 · ( seq 1 ( · , I ) ‘ 𝑁 ) ) )
63	62	eqeq2d	⊢ ( ( 𝑁 − 𝐾 ) = 0 → ( ( ! ‘ 𝑁 ) = ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) ) ↔ ( ! ‘ 𝑁 ) = ( 1 · ( seq 1 ( · , I ) ‘ 𝑁 ) ) ) )
64	53 63	syl5ibrcom	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 𝐾 ) = 0 → ( ! ‘ 𝑁 ) = ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) ) ) )
65		fznn0sub	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 − 𝐾 ) ∈ ℕ0 )
66	65	adantl	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 − 𝐾 ) ∈ ℕ0 )
67		elnn0	⊢ ( ( 𝑁 − 𝐾 ) ∈ ℕ0 ↔ ( ( 𝑁 − 𝐾 ) ∈ ℕ ∨ ( 𝑁 − 𝐾 ) = 0 ) )
68	66 67	sylib	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 𝐾 ) ∈ ℕ ∨ ( 𝑁 − 𝐾 ) = 0 ) )
69	45 64 68	mpjaod	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ 𝑁 ) = ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) ) )
70	69	oveq1d	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) = ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) )
71		eqid	⊢ ( ℤ≥ ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) = ( ℤ≥ ‘ ( ( 𝑁 − 𝐾 ) + 1 ) )
72		nn0z	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
73		zsubcl	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑁 − 𝐾 ) ∈ ℤ )
74	72 20 73	syl2an	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) → ( 𝑁 − 𝐾 ) ∈ ℤ )
75	74	peano2zd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) → ( ( 𝑁 − 𝐾 ) + 1 ) ∈ ℤ )
76	75	adantr	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 𝐾 ) + 1 ) ∈ ℤ )
77		fvi	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) → ( I ‘ 𝑘 ) = 𝑘 )
78		eluzelcn	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) → 𝑘 ∈ ℂ )
79	77 78	eqeltrd	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) → ( I ‘ 𝑘 ) ∈ ℂ )
80	79	adantl	⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) ) → ( I ‘ 𝑘 ) ∈ ℂ )
81	3	adantl	⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝑘 · 𝑥 ) ∈ ℂ )
82	71 76 80 81	seqf	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) : ( ℤ≥ ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) ⟶ ℂ )
83	11 7 17	syl2anc	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 − 𝐾 ) < 𝑁 )
84	74	adantr	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 − 𝐾 ) ∈ ℤ )
85	11	nnzd	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ℤ )
86	84 85 23	syl2anc	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 𝐾 ) < 𝑁 ↔ ( ( 𝑁 − 𝐾 ) + 1 ) ≤ 𝑁 ) )
87	83 86	mpbid	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 𝐾 ) + 1 ) ≤ 𝑁 )
88	76 85 27	syl2anc	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 ∈ ( ℤ≥ ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) ↔ ( ( 𝑁 − 𝐾 ) + 1 ) ≤ 𝑁 ) )
89	87 88	mpbird	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ( ℤ≥ ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) )
90	82 89	ffvelcdmd	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) ∈ ℂ )
91		elfznn0	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ℕ0 )
92	91	adantl	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 𝐾 ∈ ℕ0 )
93	92	faccld	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ 𝐾 ) ∈ ℕ )
94	93	nncnd	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ 𝐾 ) ∈ ℂ )
95	66	faccld	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ ( 𝑁 − 𝐾 ) ) ∈ ℕ )
96	95	nncnd	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ ( 𝑁 − 𝐾 ) ) ∈ ℂ )
97	93	nnne0d	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ 𝐾 ) ≠ 0 )
98	95	nnne0d	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ ( 𝑁 − 𝐾 ) ) ≠ 0 )
99	90 94 96 97 98	divcan5d	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) = ( ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) / ( ! ‘ 𝐾 ) ) )
100	2 70 99	3eqtrd	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝐾 ) = ( ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) / ( ! ‘ 𝐾 ) ) )
101		nnnn0	⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℕ0 )
102	101	ad2antlr	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 𝐾 ∈ ℕ0 )
103		faccl	⊢ ( 𝐾 ∈ ℕ0 → ( ! ‘ 𝐾 ) ∈ ℕ )
104		nncn	⊢ ( ( ! ‘ 𝐾 ) ∈ ℕ → ( ! ‘ 𝐾 ) ∈ ℂ )
105		nnne0	⊢ ( ( ! ‘ 𝐾 ) ∈ ℕ → ( ! ‘ 𝐾 ) ≠ 0 )
106	104 105	div0d	⊢ ( ( ! ‘ 𝐾 ) ∈ ℕ → ( 0 / ( ! ‘ 𝐾 ) ) = 0 )
107	102 103 106	3syl	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 0 / ( ! ‘ 𝐾 ) ) = 0 )
108	3	adantl	⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝑘 · 𝑥 ) ∈ ℂ )
109		fvi	⊢ ( 𝑘 ∈ ( ( ( 𝑁 − 𝐾 ) + 1 ) ... 𝑁 ) → ( I ‘ 𝑘 ) = 𝑘 )
110		elfzelz	⊢ ( 𝑘 ∈ ( ( ( 𝑁 − 𝐾 ) + 1 ) ... 𝑁 ) → 𝑘 ∈ ℤ )
111	110	zcnd	⊢ ( 𝑘 ∈ ( ( ( 𝑁 − 𝐾 ) + 1 ) ... 𝑁 ) → 𝑘 ∈ ℂ )
112	109 111	eqeltrd	⊢ ( 𝑘 ∈ ( ( ( 𝑁 − 𝐾 ) + 1 ) ... 𝑁 ) → ( I ‘ 𝑘 ) ∈ ℂ )
113	112	adantl	⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 ∈ ( ( ( 𝑁 − 𝐾 ) + 1 ) ... 𝑁 ) ) → ( I ‘ 𝑘 ) ∈ ℂ )
114		mul02	⊢ ( 𝑘 ∈ ℂ → ( 0 · 𝑘 ) = 0 )
115	114	adantl	⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 ∈ ℂ ) → ( 0 · 𝑘 ) = 0 )
116		mul01	⊢ ( 𝑘 ∈ ℂ → ( 𝑘 · 0 ) = 0 )
117	116	adantl	⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 ∈ ℂ ) → ( 𝑘 · 0 ) = 0 )
118	75	adantr	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 𝐾 ) + 1 ) ∈ ℤ )
119	72	ad2antrr	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ℤ )
120		0zd	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 0 ∈ ℤ )
121		simpr	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ¬ 𝐾 ∈ ( 0 ... 𝑁 ) )
122		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
123	102 122	eleqtrdi	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 𝐾 ∈ ( ℤ≥ ‘ 0 ) )
124		elfz5	⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ( 0 ... 𝑁 ) ↔ 𝐾 ≤ 𝑁 ) )
125	123 119 124	syl2anc	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝐾 ∈ ( 0 ... 𝑁 ) ↔ 𝐾 ≤ 𝑁 ) )
126		nn0re	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
127	126	ad2antrr	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ℝ )
128		nnre	⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℝ )
129	128	ad2antlr	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 𝐾 ∈ ℝ )
130	127 129	subge0d	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 0 ≤ ( 𝑁 − 𝐾 ) ↔ 𝐾 ≤ 𝑁 ) )
131	125 130	bitr4d	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝐾 ∈ ( 0 ... 𝑁 ) ↔ 0 ≤ ( 𝑁 − 𝐾 ) ) )
132	121 131	mtbid	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ¬ 0 ≤ ( 𝑁 − 𝐾 ) )
133	74	adantr	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 − 𝐾 ) ∈ ℤ )
134	133	zred	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 − 𝐾 ) ∈ ℝ )
135		0re	⊢ 0 ∈ ℝ
136		ltnle	⊢ ( ( ( 𝑁 − 𝐾 ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( 𝑁 − 𝐾 ) < 0 ↔ ¬ 0 ≤ ( 𝑁 − 𝐾 ) ) )
137	134 135 136	sylancl	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 𝐾 ) < 0 ↔ ¬ 0 ≤ ( 𝑁 − 𝐾 ) ) )
138	132 137	mpbird	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 − 𝐾 ) < 0 )
139		0z	⊢ 0 ∈ ℤ
140		zltp1le	⊢ ( ( ( 𝑁 − 𝐾 ) ∈ ℤ ∧ 0 ∈ ℤ ) → ( ( 𝑁 − 𝐾 ) < 0 ↔ ( ( 𝑁 − 𝐾 ) + 1 ) ≤ 0 ) )
141	133 139 140	sylancl	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 𝐾 ) < 0 ↔ ( ( 𝑁 − 𝐾 ) + 1 ) ≤ 0 ) )
142	138 141	mpbid	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 𝐾 ) + 1 ) ≤ 0 )
143		nn0ge0	⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ 𝑁 )
144	143	ad2antrr	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 0 ≤ 𝑁 )
145	118 119 120 142 144	elfzd	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 0 ∈ ( ( ( 𝑁 − 𝐾 ) + 1 ) ... 𝑁 ) )
146		simpll	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ℕ0 )
147		0cn	⊢ 0 ∈ ℂ
148		fvi	⊢ ( 0 ∈ ℂ → ( I ‘ 0 ) = 0 )
149	147 148	mp1i	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( I ‘ 0 ) = 0 )
150	108 113 115 117 145 146 149	seqz	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) = 0 )
151	150	oveq1d	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) / ( ! ‘ 𝐾 ) ) = ( 0 / ( ! ‘ 𝐾 ) ) )
152		bcval3	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝐾 ) = 0 )
153	20 152	syl3an2	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝐾 ) = 0 )
154	153	3expa	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝐾 ) = 0 )
155	107 151 154	3eqtr4rd	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝐾 ) = ( ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) / ( ! ‘ 𝐾 ) ) )
156	100 155	pm2.61dan	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) → ( 𝑁 C 𝐾 ) = ( ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) / ( ! ‘ 𝐾 ) ) )