Theorem bcval5 12094

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.)

Assertion

Ref	Expression
bcval5	|- ( ( N e. NN0 /\ K e. NN ) -> ( N _C K ) = ( ( seq ( ( N - K ) + 1 ) ( x. , _I ) ` N ) / ( ! ` K ) ) )

Proof of Theorem bcval5

Dummy variables x k y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		bcval2 12081	. . . 4 |- ( K e. ( 0 ... N ) -> ( N _C K ) = ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) )
2	1	adantl 466	. . 3 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( N _C K ) = ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) )
3		mulcl 9366	. . . . . . . . 9 |- ( ( k e. CC /\ x e. CC ) -> ( k x. x ) e. CC )
4	3	adantl 466	. . . . . . . 8 |- ( ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) /\ ( k e. CC /\ x e. CC ) ) -> ( k x. x ) e. CC )
5		mulass 9370	. . . . . . . . 9 |- ( ( k e. CC /\ x e. CC /\ y e. CC ) -> ( ( k x. x ) x. y ) = ( k x. ( x x. y ) ) )
6	5	adantl 466	. . . . . . . 8 |- ( ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) /\ ( k e. CC /\ x e. CC /\ y e. CC ) ) -> ( ( k x. x ) x. y ) = ( k x. ( x x. y ) ) )
7		simplr 754	. . . . . . . . . . . . 13 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> K e. NN )
8		elfzuz3 11450	. . . . . . . . . . . . . 14 |- ( K e. ( 0 ... N ) -> N e. ( ZZ>= ` K ) )
9	8	adantl 466	. . . . . . . . . . . . 13 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> N e. ( ZZ>= ` K ) )
10		eluznn 10925	. . . . . . . . . . . . 13 |- ( ( K e. NN /\ N e. ( ZZ>= ` K ) ) -> N e. NN )
11	7, 9, 10	syl2anc 661	. . . . . . . . . . . 12 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> N e. NN )
12	11	adantrr 716	. . . . . . . . . . 11 |- ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> N e. NN )
13		simplr 754	. . . . . . . . . . 11 |- ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> K e. NN )
14		nnre 10329	. . . . . . . . . . . 12 |- ( N e. NN -> N e. RR )
15		nnrp 11000	. . . . . . . . . . . 12 |- ( K e. NN -> K e. RR+ )
16		ltsubrp 11022	. . . . . . . . . . . 12 |- ( ( N e. RR /\ K e. RR+ ) -> ( N - K ) < N )
17	14, 15, 16	syl2an 477	. . . . . . . . . . 11 |- ( ( N e. NN /\ K e. NN ) -> ( N - K ) < N )
18	12, 13, 17	syl2anc 661	. . . . . . . . . 10 |- ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> ( N - K ) < N )
19	12	nnzd 10746	. . . . . . . . . . . 12 |- ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> N e. ZZ )
20		nnz 10668	. . . . . . . . . . . . 13 |- ( K e. NN -> K e. ZZ )
21	20	ad2antlr 726	. . . . . . . . . . . 12 |- ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> K e. ZZ )
22	19, 21	zsubcld 10752	. . . . . . . . . . 11 |- ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> ( N - K ) e. ZZ )
23		zltp1le 10694	. . . . . . . . . . 11 |- ( ( ( N - K ) e. ZZ /\ N e. ZZ ) -> ( ( N - K ) < N <-> ( ( N - K ) + 1 ) <_ N ) )
24	22, 19, 23	syl2anc 661	. . . . . . . . . 10 |- ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> ( ( N - K ) < N <-> ( ( N - K ) + 1 ) <_ N ) )
25	18, 24	mpbid 210	. . . . . . . . 9 |- ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> ( ( N - K ) + 1 ) <_ N )
26	22	peano2zd 10750	. . . . . . . . . 10 |- ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> ( ( N - K ) + 1 ) e. ZZ )
27		eluz 10874	. . . . . . . . . 10 |- ( ( ( ( N - K ) + 1 ) e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` ( ( N - K ) + 1 ) ) <-> ( ( N - K ) + 1 ) <_ N ) )
28	26, 19, 27	syl2anc 661	. . . . . . . . 9 |- ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> ( N e. ( ZZ>= ` ( ( N - K ) + 1 ) ) <-> ( ( N - K ) + 1 ) <_ N ) )
29	25, 28	mpbird 232	. . . . . . . 8 |- ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> N e. ( ZZ>= ` ( ( N - K ) + 1 ) ) )
30		simprr 756	. . . . . . . . 9 |- ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> ( N - K ) e. NN )
31		nnuz 10896	. . . . . . . . 9 |- NN = ( ZZ>= ` 1 )
32	30, 31	syl6eleq 2533	. . . . . . . 8 |- ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> ( N - K ) e. ( ZZ>= ` 1 ) )
33		fvi 5748	. . . . . . . . . 10 |- ( k e. ( 1 ... N ) -> ( _I ` k ) = k )
34		elfzelz 11453	. . . . . . . . . . 11 |- ( k e. ( 1 ... N ) -> k e. ZZ )
35	34	zcnd 10748	. . . . . . . . . 10 |- ( k e. ( 1 ... N ) -> k e. CC )
36	33, 35	eqeltrd 2517	. . . . . . . . 9 |- ( k e. ( 1 ... N ) -> ( _I ` k ) e. CC )
37	36	adantl 466	. . . . . . . 8 |- ( ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) /\ k e. ( 1 ... N ) ) -> ( _I ` k ) e. CC )
38	4, 6, 29, 32, 37	seqsplit 11839	. . . . . . 7 |- ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> ( seq 1 ( x. , _I ) ` N ) = ( ( seq 1 ( x. , _I ) ` ( N - K ) ) x. ( seq ( ( N - K ) + 1 ) ( x. , _I ) ` N ) ) )
39		facnn 12053	. . . . . . . 8 |- ( N e. NN -> ( ! ` N ) = ( seq 1 ( x. , _I ) ` N ) )
40	12, 39	syl 16	. . . . . . 7 |- ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> ( ! ` N ) = ( seq 1 ( x. , _I ) ` N ) )
41		facnn 12053	. . . . . . . . 9 |- ( ( N - K ) e. NN -> ( ! ` ( N - K ) ) = ( seq 1 ( x. , _I ) ` ( N - K ) ) )
42	30, 41	syl 16	. . . . . . . 8 |- ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> ( ! ` ( N - K ) ) = ( seq 1 ( x. , _I ) ` ( N - K ) ) )
43	42	oveq1d 6106	. . . . . . 7 |- ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> ( ( ! ` ( N - K ) ) x. ( seq ( ( N - K ) + 1 ) ( x. , _I ) ` N ) ) = ( ( seq 1 ( x. , _I ) ` ( N - K ) ) x. ( seq ( ( N - K ) + 1 ) ( x. , _I ) ` N ) ) )
44	38, 40, 43	3eqtr4d 2485	. . . . . 6 |- ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> ( ! ` N ) = ( ( ! ` ( N - K ) ) x. ( seq ( ( N - K ) + 1 ) ( x. , _I ) ` N ) ) )
45	44	expr 615	. . . . 5 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ( N - K ) e. NN -> ( ! ` N ) = ( ( ! ` ( N - K ) ) x. ( seq ( ( N - K ) + 1 ) ( x. , _I ) ` N ) ) ) )
46		simpll 753	. . . . . . . . 9 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> N e. NN0 )
47		faccl 12061	. . . . . . . . 9 |- ( N e. NN0 -> ( ! ` N ) e. NN )
48		nncn 10330	. . . . . . . . 9 |- ( ( ! ` N ) e. NN -> ( ! ` N ) e. CC )
49	46, 47, 48	3syl 20	. . . . . . . 8 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ! ` N ) e. CC )
50	49	mulid2d 9404	. . . . . . 7 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( 1 x. ( ! ` N ) ) = ( ! ` N ) )
51	11, 39	syl 16	. . . . . . . 8 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ! ` N ) = ( seq 1 ( x. , _I ) ` N ) )
52	51	oveq2d 6107	. . . . . . 7 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( 1 x. ( ! ` N ) ) = ( 1 x. ( seq 1 ( x. , _I ) ` N ) ) )
53	50, 52	eqtr3d 2477	. . . . . 6 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ! ` N ) = ( 1 x. ( seq 1 ( x. , _I ) ` N ) ) )
54		fveq2 5691	. . . . . . . . 9 |- ( ( N - K ) = 0 -> ( ! ` ( N - K ) ) = ( ! ` 0 ) )
55		fac0 12054	. . . . . . . . 9 |- ( ! ` 0 ) = 1
56	54, 55	syl6eq 2491	. . . . . . . 8 |- ( ( N - K ) = 0 -> ( ! ` ( N - K ) ) = 1 )
57		oveq1 6098	. . . . . . . . . . 11 |- ( ( N - K ) = 0 -> ( ( N - K ) + 1 ) = ( 0 + 1 ) )
58		0p1e1 10433	. . . . . . . . . . 11 |- ( 0 + 1 ) = 1
59	57, 58	syl6eq 2491	. . . . . . . . . 10 |- ( ( N - K ) = 0 -> ( ( N - K ) + 1 ) = 1 )
60	59	seqeq1d 11812	. . . . . . . . 9 |- ( ( N - K ) = 0 -> seq ( ( N - K ) + 1 ) ( x. , _I ) = seq 1 ( x. , _I ) )
61	60	fveq1d 5693	. . . . . . . 8 |- ( ( N - K ) = 0 -> ( seq ( ( N - K ) + 1 ) ( x. , _I ) ` N ) = ( seq 1 ( x. , _I ) ` N ) )
62	56, 61	oveq12d 6109	. . . . . . 7 |- ( ( N - K ) = 0 -> ( ( ! ` ( N - K ) ) x. ( seq ( ( N - K ) + 1 ) ( x. , _I ) ` N ) ) = ( 1 x. ( seq 1 ( x. , _I ) ` N ) ) )
63	62	eqeq2d 2454	. . . . . 6 |- ( ( N - K ) = 0 -> ( ( ! ` N ) = ( ( ! ` ( N - K ) ) x. ( seq ( ( N - K ) + 1 ) ( x. , _I ) ` N ) ) <-> ( ! ` N ) = ( 1 x. ( seq 1 ( x. , _I ) ` N ) ) ) )
64	53, 63	syl5ibrcom 222	. . . . 5 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ( N - K ) = 0 -> ( ! ` N ) = ( ( ! ` ( N - K ) ) x. ( seq ( ( N - K ) + 1 ) ( x. , _I ) ` N ) ) ) )
65		fznn0sub 11487	. . . . . . 7 |- ( K e. ( 0 ... N ) -> ( N - K ) e. NN0 )
66	65	adantl 466	. . . . . 6 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( N - K ) e. NN0 )
67		elnn0 10581	. . . . . 6 |- ( ( N - K ) e. NN0 <-> ( ( N - K ) e. NN \/ ( N - K ) = 0 ) )
68	66, 67	sylib 196	. . . . 5 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ( N - K ) e. NN \/ ( N - K ) = 0 ) )
69	45, 64, 68	mpjaod 381	. . . 4 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ! ` N ) = ( ( ! ` ( N - K ) ) x. ( seq ( ( N - K ) + 1 ) ( x. , _I ) ` N ) ) )
70	69	oveq1d 6106	. . 3 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) = ( ( ( ! ` ( N - K ) ) x. ( seq ( ( N - K ) + 1 ) ( x. , _I ) ` N ) ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) )
71		eqid 2443	. . . . . 6 |- ( ZZ>= ` ( ( N - K ) + 1 ) ) = ( ZZ>= ` ( ( N - K ) + 1 ) )
72		nn0z 10669	. . . . . . . . 9 |- ( N e. NN0 -> N e. ZZ )
73		zsubcl 10687	. . . . . . . . 9 |- ( ( N e. ZZ /\ K e. ZZ ) -> ( N - K ) e. ZZ )
74	72, 20, 73	syl2an 477	. . . . . . . 8 |- ( ( N e. NN0 /\ K e. NN ) -> ( N - K ) e. ZZ )
75	74	peano2zd 10750	. . . . . . 7 |- ( ( N e. NN0 /\ K e. NN ) -> ( ( N - K ) + 1 ) e. ZZ )
76	75	adantr 465	. . . . . 6 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ( N - K ) + 1 ) e. ZZ )
77		fvi 5748	. . . . . . . 8 |- ( k e. ( ZZ>= ` ( ( N - K ) + 1 ) ) -> ( _I ` k ) = k )
78		eluzelz 10870	. . . . . . . . 9 |- ( k e. ( ZZ>= ` ( ( N - K ) + 1 ) ) -> k e. ZZ )
79	78	zcnd 10748	. . . . . . . 8 |- ( k e. ( ZZ>= ` ( ( N - K ) + 1 ) ) -> k e. CC )
80	77, 79	eqeltrd 2517	. . . . . . 7 |- ( k e. ( ZZ>= ` ( ( N - K ) + 1 ) ) -> ( _I ` k ) e. CC )
81	80	adantl 466	. . . . . 6 |- ( ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) /\ k e. ( ZZ>= ` ( ( N - K ) + 1 ) ) ) -> ( _I ` k ) e. CC )
82	3	adantl 466	. . . . . 6 |- ( ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) /\ ( k e. CC /\ x e. CC ) ) -> ( k x. x ) e. CC )
83	71, 76, 81, 82	seqf 11827	. . . . 5 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> seq ( ( N - K ) + 1 ) ( x. , _I ) : ( ZZ>= ` ( ( N - K ) + 1 ) ) --> CC )
84	11, 7, 17	syl2anc 661	. . . . . . 7 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( N - K ) < N )
85	74	adantr 465	. . . . . . . 8 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( N - K ) e. ZZ )
86	11	nnzd 10746	. . . . . . . 8 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> N e. ZZ )
87	85, 86, 23	syl2anc 661	. . . . . . 7 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ( N - K ) < N <-> ( ( N - K ) + 1 ) <_ N ) )
88	84, 87	mpbid 210	. . . . . 6 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ( N - K ) + 1 ) <_ N )
89	76, 86, 27	syl2anc 661	. . . . . 6 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( N e. ( ZZ>= ` ( ( N - K ) + 1 ) ) <-> ( ( N - K ) + 1 ) <_ N ) )
90	88, 89	mpbird 232	. . . . 5 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> N e. ( ZZ>= ` ( ( N - K ) + 1 ) ) )
91	83, 90	ffvelrnd 5844	. . . 4 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( seq ( ( N - K ) + 1 ) ( x. , _I ) ` N ) e. CC )
92		elfznn0 11481	. . . . . . 7 |- ( K e. ( 0 ... N ) -> K e. NN0 )
93	92	adantl 466	. . . . . 6 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> K e. NN0 )
94		faccl 12061	. . . . . 6 |- ( K e. NN0 -> ( ! ` K ) e. NN )
95	93, 94	syl 16	. . . . 5 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ! ` K ) e. NN )
96	95	nncnd 10338	. . . 4 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ! ` K ) e. CC )
97		faccl 12061	. . . . . 6 |- ( ( N - K ) e. NN0 -> ( ! ` ( N - K ) ) e. NN )
98	66, 97	syl 16	. . . . 5 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ! ` ( N - K ) ) e. NN )
99	98	nncnd 10338	. . . 4 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ! ` ( N - K ) ) e. CC )
100	95	nnne0d 10366	. . . 4 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ! ` K ) =/= 0 )
101	98	nnne0d 10366	. . . 4 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ! ` ( N - K ) ) =/= 0 )
102	91, 96, 99, 100, 101	divcan5d 10133	. . 3 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ( ( ! ` ( N - K ) ) x. ( seq ( ( N - K ) + 1 ) ( x. , _I ) ` N ) ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) = ( ( seq ( ( N - K ) + 1 ) ( x. , _I ) ` N ) / ( ! ` K ) ) )
103	2, 70, 102	3eqtrd 2479	. 2 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( N _C K ) = ( ( seq ( ( N - K ) + 1 ) ( x. , _I ) ` N ) / ( ! ` K ) ) )
104		nnnn0 10586	. . . . 5 |- ( K e. NN -> K e. NN0 )
105	104	ad2antlr 726	. . . 4 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> K e. NN0 )
106		nncn 10330	. . . . 5 |- ( ( ! ` K ) e. NN -> ( ! ` K ) e. CC )
107		nnne0 10354	. . . . 5 |- ( ( ! ` K ) e. NN -> ( ! ` K ) =/= 0 )
108	106, 107	div0d 10106	. . . 4 |- ( ( ! ` K ) e. NN -> ( 0 / ( ! ` K ) ) = 0 )
109	105, 94, 108	3syl 20	. . 3 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( 0 / ( ! ` K ) ) = 0 )
110	3	adantl 466	. . . . 5 |- ( ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) /\ ( k e. CC /\ x e. CC ) ) -> ( k x. x ) e. CC )
111		fvi 5748	. . . . . . 7 |- ( k e. ( ( ( N - K ) + 1 ) ... N ) -> ( _I ` k ) = k )
112		elfzelz 11453	. . . . . . . 8 |- ( k e. ( ( ( N - K ) + 1 ) ... N ) -> k e. ZZ )
113	112	zcnd 10748	. . . . . . 7 |- ( k e. ( ( ( N - K ) + 1 ) ... N ) -> k e. CC )
114	111, 113	eqeltrd 2517	. . . . . 6 |- ( k e. ( ( ( N - K ) + 1 ) ... N ) -> ( _I ` k ) e. CC )
115	114	adantl 466	. . . . 5 |- ( ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) /\ k e. ( ( ( N - K ) + 1 ) ... N ) ) -> ( _I ` k ) e. CC )
116		mul02 9547	. . . . . 6 |- ( k e. CC -> ( 0 x. k ) = 0 )
117	116	adantl 466	. . . . 5 |- ( ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) /\ k e. CC ) -> ( 0 x. k ) = 0 )
118		mul01 9548	. . . . . 6 |- ( k e. CC -> ( k x. 0 ) = 0 )
119	118	adantl 466	. . . . 5 |- ( ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) /\ k e. CC ) -> ( k x. 0 ) = 0 )
120		simpr 461	. . . . . . . . 9 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> -. K e. ( 0 ... N ) )
121		nn0uz 10895	. . . . . . . . . . . 12 |- NN0 = ( ZZ>= ` 0 )
122	105, 121	syl6eleq 2533	. . . . . . . . . . 11 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> K e. ( ZZ>= ` 0 ) )
123	72	ad2antrr 725	. . . . . . . . . . 11 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> N e. ZZ )
124		elfz5 11445	. . . . . . . . . . 11 |- ( ( K e. ( ZZ>= ` 0 ) /\ N e. ZZ ) -> ( K e. ( 0 ... N ) <-> K <_ N ) )
125	122, 123, 124	syl2anc 661	. . . . . . . . . 10 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( K e. ( 0 ... N ) <-> K <_ N ) )
126		nn0re 10588	. . . . . . . . . . . 12 |- ( N e. NN0 -> N e. RR )
127	126	ad2antrr 725	. . . . . . . . . . 11 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> N e. RR )
128		nnre 10329	. . . . . . . . . . . 12 |- ( K e. NN -> K e. RR )
129	128	ad2antlr 726	. . . . . . . . . . 11 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> K e. RR )
130	127, 129	subge0d 9929	. . . . . . . . . 10 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( 0 <_ ( N - K ) <-> K <_ N ) )
131	125, 130	bitr4d 256	. . . . . . . . 9 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( K e. ( 0 ... N ) <-> 0 <_ ( N - K ) ) )
132	120, 131	mtbid 300	. . . . . . . 8 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> -. 0 <_ ( N - K ) )
133	74	adantr 465	. . . . . . . . . 10 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( N - K ) e. ZZ )
134	133	zred 10747	. . . . . . . . 9 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( N - K ) e. RR )
135		0re 9386	. . . . . . . . 9 |- 0 e. RR
136		ltnle 9454	. . . . . . . . 9 |- ( ( ( N - K ) e. RR /\ 0 e. RR ) -> ( ( N - K ) < 0 <-> -. 0 <_ ( N - K ) ) )
137	134, 135, 136	sylancl 662	. . . . . . . 8 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( ( N - K ) < 0 <-> -. 0 <_ ( N - K ) ) )
138	132, 137	mpbird 232	. . . . . . 7 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( N - K ) < 0 )
139		0z 10657	. . . . . . . 8 |- 0 e. ZZ
140		zltp1le 10694	. . . . . . . 8 |- ( ( ( N - K ) e. ZZ /\ 0 e. ZZ ) -> ( ( N - K ) < 0 <-> ( ( N - K ) + 1 ) <_ 0 ) )
141	133, 139, 140	sylancl 662	. . . . . . 7 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( ( N - K ) < 0 <-> ( ( N - K ) + 1 ) <_ 0 ) )
142	138, 141	mpbid 210	. . . . . 6 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( ( N - K ) + 1 ) <_ 0 )
143		nn0ge0 10605	. . . . . . 7 |- ( N e. NN0 -> 0 <_ N )
144	143	ad2antrr 725	. . . . . 6 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> 0 <_ N )
145		0zd 10658	. . . . . . 7 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> 0 e. ZZ )
146	75	adantr 465	. . . . . . 7 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( ( N - K ) + 1 ) e. ZZ )
147		elfz 11443	. . . . . . 7 |- ( ( 0 e. ZZ /\ ( ( N - K ) + 1 ) e. ZZ /\ N e. ZZ ) -> ( 0 e. ( ( ( N - K ) + 1 ) ... N ) <-> ( ( ( N - K ) + 1 ) <_ 0 /\ 0 <_ N ) ) )
148	145, 146, 123, 147	syl3anc 1218	. . . . . 6 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( 0 e. ( ( ( N - K ) + 1 ) ... N ) <-> ( ( ( N - K ) + 1 ) <_ 0 /\ 0 <_ N ) ) )
149	142, 144, 148	mpbir2and 913	. . . . 5 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> 0 e. ( ( ( N - K ) + 1 ) ... N ) )
150		simpll 753	. . . . 5 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> N e. NN0 )
151		0cn 9378	. . . . . 6 |- 0 e. CC
152		fvi 5748	. . . . . 6 |- ( 0 e. CC -> ( _I ` 0 ) = 0 )
153	151, 152	mp1i 12	. . . . 5 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( _I ` 0 ) = 0 )
154	110, 115, 117, 119, 149, 150, 153	seqz 11854	. . . 4 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( seq ( ( N - K ) + 1 ) ( x. , _I ) ` N ) = 0 )
155	154	oveq1d 6106	. . 3 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( ( seq ( ( N - K ) + 1 ) ( x. , _I ) ` N ) / ( ! ` K ) ) = ( 0 / ( ! ` K ) ) )
156		bcval3 12082	. . . . 5 |- ( ( N e. NN0 /\ K e. ZZ /\ -. K e. ( 0 ... N ) ) -> ( N _C K ) = 0 )
157	20, 156	syl3an2 1252	. . . 4 |- ( ( N e. NN0 /\ K e. NN /\ -. K e. ( 0 ... N ) ) -> ( N _C K ) = 0 )
158	157	3expa 1187	. . 3 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( N _C K ) = 0 )
159	109, 155, 158	3eqtr4rd 2486	. 2 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( N _C K ) = ( ( seq ( ( N - K ) + 1 ) ( x. , _I ) ` N ) / ( ! ` K ) ) )
160	103, 159	pm2.61dan 789	1 |- ( ( N e. NN0 /\ K e. NN ) -> ( N _C K ) = ( ( seq ( ( N - K ) + 1 ) ( x. , _I ) ` N ) / ( ! ` K ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   \/ wo 368   /\ wa 369   /\ w3a 965   = wceq 1369   e. wcel 1756   class class class wbr 4292   _I cid 4631   ` cfv 5418  (class class class)co 6091   CCcc 9280   RRcr 9281   0cc0 9282   1c1 9283   + caddc 9285   x. cmul 9287   < clt 9418   <_ cle 9419   - cmin 9595   / cdiv 9993   NNcn 10322   NN0cn0 10579   ZZcz 10646   ZZ>=cuz 10861   RR+crp 10991   ...cfz 11437   seqcseq 11806   !cfa 12051   _C cbc 12078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4413  ax-nul 4421  ax-pow 4470  ax-pr 4531  ax-un 6372  ax-cnex 9338  ax-resscn 9339  ax-1cn 9340  ax-icn 9341  ax-addcl 9342  ax-addrcl 9343  ax-mulcl 9344  ax-mulrcl 9345  ax-mulcom 9346  ax-addass 9347  ax-mulass 9348  ax-distr 9349  ax-i2m1 9350  ax-1ne0 9351  ax-1rid 9352  ax-rnegex 9353  ax-rrecex 9354  ax-cnre 9355  ax-pre-lttri 9356  ax-pre-lttrn 9357  ax-pre-ltadd 9358  ax-pre-mulgt0 9359

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-nel 2609  df-ral 2720  df-rex 2721  df-reu 2722  df-rmo 2723  df-rab 2724  df-v 2974  df-sbc 3187  df-csb 3289  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-pss 3344  df-nul 3638  df-if 3792  df-pw 3862  df-sn 3878  df-pr 3880  df-tp 3882  df-op 3884  df-uni 4092  df-iun 4173  df-br 4293  df-opab 4351  df-mpt 4352  df-tr 4386  df-eprel 4632  df-id 4636  df-po 4641  df-so 4642  df-fr 4679  df-we 4681  df-ord 4722  df-on 4723  df-lim 4724  df-suc 4725  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-ima 4853  df-iota 5381  df-fun 5420  df-fn 5421  df-f 5422  df-f1 5423  df-fo 5424  df-f1o 5425  df-fv 5426  df-riota 6052  df-ov 6094  df-oprab 6095  df-mpt2 6096  df-om 6477  df-1st 6577  df-2nd 6578  df-recs 6832  df-rdg 6866  df-er 7101  df-en 7311  df-dom 7312  df-sdom 7313  df-pnf 9420  df-mnf 9421  df-xr 9422  df-ltxr 9423  df-le 9424  df-sub 9597  df-neg 9598  df-div 9994  df-nn 10323  df-n0 10580  df-z 10647  df-uz 10862  df-rp 10992  df-fz 11438  df-seq 11807  df-fac 12052  df-bc 12079

This theorem is referenced by:  bcn2  12095