Theorem ibcval5 10232

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 Jim Kingdon, 6-Nov-2021.)

Assertion

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

Proof of Theorem ibcval5

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

Step	Hyp	Ref	Expression
1		bcval2 10219	. . . 4 |- ( K e. ( 0 ... N ) -> ( N _C K ) = ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) )
2	1	adantl 272	. . 3 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( N _C K ) = ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) )
3		simprl 499	. . . . . . . . 9 |- ( ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) /\ ( k e. CC /\ x e. CC ) ) -> k e. CC )
4		simprr 500	. . . . . . . . 9 |- ( ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) /\ ( k e. CC /\ x e. CC ) ) -> x e. CC )
5	3, 4	mulcld 7569	. . . . . . . 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 )
6		simpr1 950	. . . . . . . . 9 |- ( ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) /\ ( k e. CC /\ x e. CC /\ y e. CC ) ) -> k e. CC )
7		simpr2 951	. . . . . . . . 9 |- ( ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) /\ ( k e. CC /\ x e. CC /\ y e. CC ) ) -> x e. CC )
8		simpr3 952	. . . . . . . . 9 |- ( ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) /\ ( k e. CC /\ x e. CC /\ y e. CC ) ) -> y e. CC )
9	6, 7, 8	mulassd 7572	. . . . . . . 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 ) ) )
10		simpll 497	. . . . . . . . . . . . 13 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> N e. NN0 )
11	10	nn0zd 8927	. . . . . . . . . . . 12 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> N e. ZZ )
12		simplr 498	. . . . . . . . . . . . 13 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> K e. NN )
13	12	nnzd 8928	. . . . . . . . . . . 12 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> K e. ZZ )
14	11, 13	zsubcld 8934	. . . . . . . . . . 11 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( N - K ) e. ZZ )
15	14	peano2zd 8932	. . . . . . . . . 10 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ( N - K ) + 1 ) e. ZZ )
16		1red 7564	. . . . . . . . . . . 12 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> 1 e. RR )
17	12	nnred 8496	. . . . . . . . . . . 12 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> K e. RR )
18	10	nn0red 8788	. . . . . . . . . . . 12 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> N e. RR )
19	12	nnge1d 8526	. . . . . . . . . . . 12 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> 1 <_ K )
20	16, 17, 18, 19	lesub2dd 8100	. . . . . . . . . . 11 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( N - K ) <_ ( N - 1 ) )
21	14	zred 8929	. . . . . . . . . . . 12 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( N - K ) e. RR )
22		leaddsub 7977	. . . . . . . . . . . 12 |- ( ( ( N - K ) e. RR /\ 1 e. RR /\ N e. RR ) -> ( ( ( N - K ) + 1 ) <_ N <-> ( N - K ) <_ ( N - 1 ) ) )
23	21, 16, 18, 22	syl3anc 1175	. . . . . . . . . . 11 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ( ( N - K ) + 1 ) <_ N <-> ( N - K ) <_ ( N - 1 ) ) )
24	20, 23	mpbird 166	. . . . . . . . . 10 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ( N - K ) + 1 ) <_ N )
25		eluz2 9086	. . . . . . . . . 10 |- ( N e. ( ZZ>= ` ( ( N - K ) + 1 ) ) <-> ( ( ( N - K ) + 1 ) e. ZZ /\ N e. ZZ /\ ( ( N - K ) + 1 ) <_ N ) )
26	15, 11, 24, 25	syl3anbrc 1128	. . . . . . . . 9 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> N e. ( ZZ>= ` ( ( N - K ) + 1 ) ) )
27	26	adantrr 464	. . . . . . . 8 |- ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> N e. ( ZZ>= ` ( ( N - K ) + 1 ) ) )
28		simprr 500	. . . . . . . . 9 |- ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> ( N - K ) e. NN )
29		nnuz 9115	. . . . . . . . 9 |- NN = ( ZZ>= ` 1 )
30	28, 29	syl6eleq 2181	. . . . . . . 8 |- ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> ( N - K ) e. ( ZZ>= ` 1 ) )
31		vex 2623	. . . . . . . . . 10 |- k e. _V
32		fvi 5374	. . . . . . . . . 10 |- ( k e. _V -> ( _I ` k ) = k )
33	31, 32	ax-mp 7	. . . . . . . . 9 |- ( _I ` k ) = k
34		eluzelcn 9091	. . . . . . . . . 10 |- ( k e. ( ZZ>= ` 1 ) -> k e. CC )
35	34	adantl 272	. . . . . . . . 9 |- ( ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) /\ k e. ( ZZ>= ` 1 ) ) -> k e. CC )
36	33, 35	syl5eqel 2175	. . . . . . . 8 |- ( ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) /\ k e. ( ZZ>= ` 1 ) ) -> ( _I ` k ) e. CC )
37	5, 9, 27, 30, 36	iseqsplit 9969	. . . . . . 7 |- ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> ( seq 1 ( x. , _I , CC ) ` N ) = ( ( seq 1 ( x. , _I , CC ) ` ( N - K ) ) x. ( seq ( ( N - K ) + 1 ) ( x. , _I , CC ) ` N ) ) )
38		elfzuz3 9498	. . . . . . . . . . 11 |- ( K e. ( 0 ... N ) -> N e. ( ZZ>= ` K ) )
39	38	adantl 272	. . . . . . . . . 10 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> N e. ( ZZ>= ` K ) )
40		eluznn 9148	. . . . . . . . . 10 |- ( ( K e. NN /\ N e. ( ZZ>= ` K ) ) -> N e. NN )
41	12, 39, 40	syl2anc 404	. . . . . . . . 9 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> N e. NN )
42	41	adantrr 464	. . . . . . . 8 |- ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> N e. NN )
43		facnn 10196	. . . . . . . 8 |- ( N e. NN -> ( ! ` N ) = ( seq 1 ( x. , _I , CC ) ` N ) )
44	42, 43	syl 14	. . . . . . 7 |- ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> ( ! ` N ) = ( seq 1 ( x. , _I , CC ) ` N ) )
45		facnn 10196	. . . . . . . . 9 |- ( ( N - K ) e. NN -> ( ! ` ( N - K ) ) = ( seq 1 ( x. , _I , CC ) ` ( N - K ) ) )
46	28, 45	syl 14	. . . . . . . 8 |- ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> ( ! ` ( N - K ) ) = ( seq 1 ( x. , _I , CC ) ` ( N - K ) ) )
47	46	oveq1d 5681	. . . . . . 7 |- ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> ( ( ! ` ( N - K ) ) x. ( seq ( ( N - K ) + 1 ) ( x. , _I , CC ) ` N ) ) = ( ( seq 1 ( x. , _I , CC ) ` ( N - K ) ) x. ( seq ( ( N - K ) + 1 ) ( x. , _I , CC ) ` N ) ) )
48	37, 44, 47	3eqtr4d 2131	. . . . . 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 , CC ) ` N ) ) )
49	48	expr 368	. . . . 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 , CC ) ` N ) ) ) )
50	10	faccld 10205	. . . . . . . . 9 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ! ` N ) e. NN )
51	50	nncnd 8497	. . . . . . . 8 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ! ` N ) e. CC )
52	51	mulid2d 7567	. . . . . . 7 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( 1 x. ( ! ` N ) ) = ( ! ` N ) )
53	41, 43	syl 14	. . . . . . . 8 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ! ` N ) = ( seq 1 ( x. , _I , CC ) ` N ) )
54	53	oveq2d 5682	. . . . . . 7 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( 1 x. ( ! ` N ) ) = ( 1 x. ( seq 1 ( x. , _I , CC ) ` N ) ) )
55	52, 54	eqtr3d 2123	. . . . . 6 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ! ` N ) = ( 1 x. ( seq 1 ( x. , _I , CC ) ` N ) ) )
56		fveq2 5318	. . . . . . . . 9 |- ( ( N - K ) = 0 -> ( ! ` ( N - K ) ) = ( ! ` 0 ) )
57		fac0 10197	. . . . . . . . 9 |- ( ! ` 0 ) = 1
58	56, 57	syl6eq 2137	. . . . . . . 8 |- ( ( N - K ) = 0 -> ( ! ` ( N - K ) ) = 1 )
59		oveq1 5673	. . . . . . . . . . 11 |- ( ( N - K ) = 0 -> ( ( N - K ) + 1 ) = ( 0 + 1 ) )
60		0p1e1 8597	. . . . . . . . . . 11 |- ( 0 + 1 ) = 1
61	59, 60	syl6eq 2137	. . . . . . . . . 10 |- ( ( N - K ) = 0 -> ( ( N - K ) + 1 ) = 1 )
62		iseqeq1 9919	. . . . . . . . . 10 |- ( ( ( N - K ) + 1 ) = 1 -> seq ( ( N - K ) + 1 ) ( x. , _I , CC ) = seq 1 ( x. , _I , CC ) )
63	61, 62	syl 14	. . . . . . . . 9 |- ( ( N - K ) = 0 -> seq ( ( N - K ) + 1 ) ( x. , _I , CC ) = seq 1 ( x. , _I , CC ) )
64	63	fveq1d 5320	. . . . . . . 8 |- ( ( N - K ) = 0 -> ( seq ( ( N - K ) + 1 ) ( x. , _I , CC ) ` N ) = ( seq 1 ( x. , _I , CC ) ` N ) )
65	58, 64	oveq12d 5684	. . . . . . 7 |- ( ( N - K ) = 0 -> ( ( ! ` ( N - K ) ) x. ( seq ( ( N - K ) + 1 ) ( x. , _I , CC ) ` N ) ) = ( 1 x. ( seq 1 ( x. , _I , CC ) ` N ) ) )
66	65	eqeq2d 2100	. . . . . 6 |- ( ( N - K ) = 0 -> ( ( ! ` N ) = ( ( ! ` ( N - K ) ) x. ( seq ( ( N - K ) + 1 ) ( x. , _I , CC ) ` N ) ) <-> ( ! ` N ) = ( 1 x. ( seq 1 ( x. , _I , CC ) ` N ) ) ) )
67	55, 66	syl5ibrcom 156	. . . . 5 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ( N - K ) = 0 -> ( ! ` N ) = ( ( ! ` ( N - K ) ) x. ( seq ( ( N - K ) + 1 ) ( x. , _I , CC ) ` N ) ) ) )
68		fznn0sub 9532	. . . . . . 7 |- ( K e. ( 0 ... N ) -> ( N - K ) e. NN0 )
69	68	adantl 272	. . . . . 6 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( N - K ) e. NN0 )
70		elnn0 8736	. . . . . 6 |- ( ( N - K ) e. NN0 <-> ( ( N - K ) e. NN \/ ( N - K ) = 0 ) )
71	69, 70	sylib 121	. . . . 5 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ( N - K ) e. NN \/ ( N - K ) = 0 ) )
72	49, 67, 71	mpjaod 674	. . . 4 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ! ` N ) = ( ( ! ` ( N - K ) ) x. ( seq ( ( N - K ) + 1 ) ( x. , _I , CC ) ` N ) ) )
73	72	oveq1d 5681	. . 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 , CC ) ` N ) ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) )
74		vex 2623	. . . . . . 7 |- f e. _V
75		fvi 5374	. . . . . . 7 |- ( f e. _V -> ( _I ` f ) = f )
76	74, 75	ax-mp 7	. . . . . 6 |- ( _I ` f ) = f
77		eluzelcn 9091	. . . . . . 7 |- ( f e. ( ZZ>= ` ( ( N - K ) + 1 ) ) -> f e. CC )
78	77	adantl 272	. . . . . 6 |- ( ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) /\ f e. ( ZZ>= ` ( ( N - K ) + 1 ) ) ) -> f e. CC )
79	76, 78	syl5eqel 2175	. . . . 5 |- ( ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) /\ f e. ( ZZ>= ` ( ( N - K ) + 1 ) ) ) -> ( _I ` f ) e. CC )
80		mulcl 7530	. . . . . 6 |- ( ( f e. CC /\ g e. CC ) -> ( f x. g ) e. CC )
81	80	adantl 272	. . . . 5 |- ( ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) /\ ( f e. CC /\ g e. CC ) ) -> ( f x. g ) e. CC )
82	26, 79, 81	iseqcl 9942	. . . 4 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( seq ( ( N - K ) + 1 ) ( x. , _I , CC ) ` N ) e. CC )
83	12	nnnn0d 8787	. . . . . 6 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> K e. NN0 )
84	83	faccld 10205	. . . . 5 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ! ` K ) e. NN )
85	84	nncnd 8497	. . . 4 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ! ` K ) e. CC )
86	69	faccld 10205	. . . . 5 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ! ` ( N - K ) ) e. NN )
87	86	nncnd 8497	. . . 4 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ! ` ( N - K ) ) e. CC )
88	84	nnap0d 8529	. . . 4 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ! ` K ) # 0 )
89	86	nnap0d 8529	. . . 4 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ! ` ( N - K ) ) # 0 )
90	82, 85, 87, 88, 89	divcanap5d 8345	. . 3 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ( ( ! ` ( N - K ) ) x. ( seq ( ( N - K ) + 1 ) ( x. , _I , CC ) ` N ) ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) = ( ( seq ( ( N - K ) + 1 ) ( x. , _I , CC ) ` N ) / ( ! ` K ) ) )
91	2, 73, 90	3eqtrd 2125	. 2 |- ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( N _C K ) = ( ( seq ( ( N - K ) + 1 ) ( x. , _I , CC ) ` N ) / ( ! ` K ) ) )
92		simplr 498	. . . . . . 7 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> K e. NN )
93	92	nnnn0d 8787	. . . . . 6 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> K e. NN0 )
94	93	faccld 10205	. . . . 5 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( ! ` K ) e. NN )
95	94	nncnd 8497	. . . 4 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( ! ` K ) e. CC )
96	94	nnap0d 8529	. . . 4 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( ! ` K ) # 0 )
97	95, 96	div0apd 8315	. . 3 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( 0 / ( ! ` K ) ) = 0 )
98		mulcl 7530	. . . . . 6 |- ( ( k e. CC /\ x e. CC ) -> ( k x. x ) e. CC )
99	98	adantl 272	. . . . 5 |- ( ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) /\ ( k e. CC /\ x e. CC ) ) -> ( k x. x ) e. CC )
100		eluzelcn 9091	. . . . . . 7 |- ( k e. ( ZZ>= ` ( ( N - K ) + 1 ) ) -> k e. CC )
101	100	adantl 272	. . . . . 6 |- ( ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) /\ k e. ( ZZ>= ` ( ( N - K ) + 1 ) ) ) -> k e. CC )
102	33, 101	syl5eqel 2175	. . . . 5 |- ( ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) /\ k e. ( ZZ>= ` ( ( N - K ) + 1 ) ) ) -> ( _I ` k ) e. CC )
103		cnex 7527	. . . . . 6 |- CC e. _V
104	103	a1i 9	. . . . 5 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> CC e. _V )
105		simpr 109	. . . . . 6 |- ( ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) /\ k e. CC ) -> k e. CC )
106	105	mul02d 7931	. . . . 5 |- ( ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) /\ k e. CC ) -> ( 0 x. k ) = 0 )
107	105	mul01d 7932	. . . . 5 |- ( ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) /\ k e. CC ) -> ( k x. 0 ) = 0 )
108		simpr 109	. . . . . . . . 9 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> -. K e. ( 0 ... N ) )
109		nn0uz 9114	. . . . . . . . . . . 12 |- NN0 = ( ZZ>= ` 0 )
110	93, 109	syl6eleq 2181	. . . . . . . . . . 11 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> K e. ( ZZ>= ` 0 ) )
111		simpll 497	. . . . . . . . . . . 12 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> N e. NN0 )
112	111	nn0zd 8927	. . . . . . . . . . 11 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> N e. ZZ )
113		elfz5 9493	. . . . . . . . . . 11 |- ( ( K e. ( ZZ>= ` 0 ) /\ N e. ZZ ) -> ( K e. ( 0 ... N ) <-> K <_ N ) )
114	110, 112, 113	syl2anc 404	. . . . . . . . . 10 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( K e. ( 0 ... N ) <-> K <_ N ) )
115		nn0re 8743	. . . . . . . . . . . 12 |- ( N e. NN0 -> N e. RR )
116	115	ad2antrr 473	. . . . . . . . . . 11 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> N e. RR )
117		nnre 8490	. . . . . . . . . . . 12 |- ( K e. NN -> K e. RR )
118	117	ad2antlr 474	. . . . . . . . . . 11 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> K e. RR )
119	116, 118	subge0d 8073	. . . . . . . . . 10 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( 0 <_ ( N - K ) <-> K <_ N ) )
120	114, 119	bitr4d 190	. . . . . . . . 9 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( K e. ( 0 ... N ) <-> 0 <_ ( N - K ) ) )
121	108, 120	mtbid 633	. . . . . . . 8 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> -. 0 <_ ( N - K ) )
122		simpl 108	. . . . . . . . . . . 12 |- ( ( N e. NN0 /\ K e. NN ) -> N e. NN0 )
123	122	nn0zd 8927	. . . . . . . . . . 11 |- ( ( N e. NN0 /\ K e. NN ) -> N e. ZZ )
124		simpr 109	. . . . . . . . . . . 12 |- ( ( N e. NN0 /\ K e. NN ) -> K e. NN )
125	124	nnzd 8928	. . . . . . . . . . 11 |- ( ( N e. NN0 /\ K e. NN ) -> K e. ZZ )
126	123, 125	zsubcld 8934	. . . . . . . . . 10 |- ( ( N e. NN0 /\ K e. NN ) -> ( N - K ) e. ZZ )
127	126	adantr 271	. . . . . . . . 9 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( N - K ) e. ZZ )
128		0z 8822	. . . . . . . . 9 |- 0 e. ZZ
129		zltnle 8857	. . . . . . . . 9 |- ( ( ( N - K ) e. ZZ /\ 0 e. ZZ ) -> ( ( N - K ) < 0 <-> -. 0 <_ ( N - K ) ) )
130	127, 128, 129	sylancl 405	. . . . . . . 8 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( ( N - K ) < 0 <-> -. 0 <_ ( N - K ) ) )
131	121, 130	mpbird 166	. . . . . . 7 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( N - K ) < 0 )
132		zltp1le 8865	. . . . . . . 8 |- ( ( ( N - K ) e. ZZ /\ 0 e. ZZ ) -> ( ( N - K ) < 0 <-> ( ( N - K ) + 1 ) <_ 0 ) )
133	127, 128, 132	sylancl 405	. . . . . . 7 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( ( N - K ) < 0 <-> ( ( N - K ) + 1 ) <_ 0 ) )
134	131, 133	mpbid 146	. . . . . 6 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( ( N - K ) + 1 ) <_ 0 )
135		nn0ge0 8759	. . . . . . 7 |- ( N e. NN0 -> 0 <_ N )
136	135	ad2antrr 473	. . . . . 6 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> 0 <_ N )
137		0zd 8823	. . . . . . 7 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> 0 e. ZZ )
138	127	peano2zd 8932	. . . . . . 7 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( ( N - K ) + 1 ) e. ZZ )
139		elfz 9491	. . . . . . 7 |- ( ( 0 e. ZZ /\ ( ( N - K ) + 1 ) e. ZZ /\ N e. ZZ ) -> ( 0 e. ( ( ( N - K ) + 1 ) ... N ) <-> ( ( ( N - K ) + 1 ) <_ 0 /\ 0 <_ N ) ) )
140	137, 138, 112, 139	syl3anc 1175	. . . . . 6 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( 0 e. ( ( ( N - K ) + 1 ) ... N ) <-> ( ( ( N - K ) + 1 ) <_ 0 /\ 0 <_ N ) ) )
141	134, 136, 140	mpbir2and 891	. . . . 5 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> 0 e. ( ( ( N - K ) + 1 ) ... N ) )
142		elex 2631	. . . . . 6 |- ( N e. NN0 -> N e. _V )
143	142	ad2antrr 473	. . . . 5 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> N e. _V )
144		0cn 7541	. . . . . 6 |- 0 e. CC
145		fvi 5374	. . . . . 6 |- ( 0 e. CC -> ( _I ` 0 ) = 0 )
146	144, 145	mp1i 10	. . . . 5 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( _I ` 0 ) = 0 )
147	99, 102, 104, 106, 107, 141, 143, 146	iseqz 10004	. . . 4 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( seq ( ( N - K ) + 1 ) ( x. , _I , CC ) ` N ) = 0 )
148	147	oveq1d 5681	. . 3 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( ( seq ( ( N - K ) + 1 ) ( x. , _I , CC ) ` N ) / ( ! ` K ) ) = ( 0 / ( ! ` K ) ) )
149		nnz 8830	. . . . 5 |- ( K e. NN -> K e. ZZ )
150		bcval3 10220	. . . . 5 |- ( ( N e. NN0 /\ K e. ZZ /\ -. K e. ( 0 ... N ) ) -> ( N _C K ) = 0 )
151	149, 150	syl3an2 1209	. . . 4 |- ( ( N e. NN0 /\ K e. NN /\ -. K e. ( 0 ... N ) ) -> ( N _C K ) = 0 )
152	151	3expa 1144	. . 3 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( N _C K ) = 0 )
153	97, 148, 152	3eqtr4rd 2132	. 2 |- ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( N _C K ) = ( ( seq ( ( N - K ) + 1 ) ( x. , _I , CC ) ` N ) / ( ! ` K ) ) )
154		0zd 8823	. . . 4 |- ( ( N e. NN0 /\ K e. NN ) -> 0 e. ZZ )
155		fzdcel 9515	. . . 4 |- ( ( K e. ZZ /\ 0 e. ZZ /\ N e. ZZ ) -> DECID K e. ( 0 ... N ) )
156	125, 154, 123, 155	syl3anc 1175	. . 3 |- ( ( N e. NN0 /\ K e. NN ) -> DECID K e. ( 0 ... N ) )
157		exmiddc 783	. . 3 |- (DECID K e. ( 0 ... N ) -> ( K e. ( 0 ... N ) \/ -. K e. ( 0 ... N ) ) )
158	156, 157	syl 14	. 2 |- ( ( N e. NN0 /\ K e. NN ) -> ( K e. ( 0 ... N ) \/ -. K e. ( 0 ... N ) ) )
159	91, 153, 158	mpjaodan 748	1 |- ( ( N e. NN0 /\ K e. NN ) -> ( N _C K ) = ( ( seq ( ( N - K ) + 1 ) ( x. , _I , CC ) ` N ) / ( ! ` K ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103   <-> wb 104   \/ wo 665  DECID wdc 781   /\ w3a 925   = wceq 1290   e. wcel 1439   _Vcvv 2620   class class class wbr 3851   _I cid 4124   ` cfv 5028  (class class class)co 5666   CCcc 7409   RRcr 7410   0cc0 7411   1c1 7412   + caddc 7414   x. cmul 7416   < clt 7583   <_ cle 7584   - cmin 7714   / cdiv 8200   NNcn 8483   NN0cn0 8734   ZZcz 8811   ZZ>=cuz 9080   ...cfz 9485   seqcseq4 9912   !cfa 10194   _C cbc 10216

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 580  ax-in2 581  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-13 1450  ax-14 1451  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-coll 3960  ax-sep 3963  ax-nul 3971  ax-pow 4015  ax-pr 4045  ax-un 4269  ax-setind 4366  ax-iinf 4416  ax-cnex 7497  ax-resscn 7498  ax-1cn 7499  ax-1re 7500  ax-icn 7501  ax-addcl 7502  ax-addrcl 7503  ax-mulcl 7504  ax-mulrcl 7505  ax-addcom 7506  ax-mulcom 7507  ax-addass 7508  ax-mulass 7509  ax-distr 7510  ax-i2m1 7511  ax-0lt1 7512  ax-1rid 7513  ax-0id 7514  ax-rnegex 7515  ax-precex 7516  ax-cnre 7517  ax-pre-ltirr 7518  ax-pre-ltwlin 7519  ax-pre-lttrn 7520  ax-pre-apti 7521  ax-pre-ltadd 7522  ax-pre-mulgt0 7523  ax-pre-mulext 7524

This theorem depends on definitions:  df-bi 116  df-dc 782  df-3or 926  df-3an 927  df-tru 1293  df-fal 1296  df-nf 1396  df-sb 1694  df-eu 1952  df-mo 1953  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ne 2257  df-nel 2352  df-ral 2365  df-rex 2366  df-reu 2367  df-rmo 2368  df-rab 2369  df-v 2622  df-sbc 2842  df-csb 2935  df-dif 3002  df-un 3004  df-in 3006  df-ss 3013  df-nul 3288  df-if 3398  df-pw 3435  df-sn 3456  df-pr 3457  df-op 3459  df-uni 3660  df-int 3695  df-iun 3738  df-br 3852  df-opab 3906  df-mpt 3907  df-tr 3943  df-id 4129  df-po 4132  df-iso 4133  df-iord 4202  df-on 4204  df-ilim 4205  df-suc 4207  df-iom 4419  df-xp 4458  df-rel 4459  df-cnv 4460  df-co 4461  df-dm 4462  df-rn 4463  df-res 4464  df-ima 4465  df-iota 4993  df-fun 5030  df-fn 5031  df-f 5032  df-f1 5033  df-fo 5034  df-f1o 5035  df-fv 5036  df-riota 5622  df-ov 5669  df-oprab 5670  df-mpt2 5671  df-1st 5925  df-2nd 5926  df-recs 6084  df-frec 6170  df-pnf 7585  df-mnf 7586  df-xr 7587  df-ltxr 7588  df-le 7589  df-sub 7716  df-neg 7717  df-reap 8113  df-ap 8120  df-div 8201  df-inn 8484  df-n0 8735  df-z 8812  df-uz 9081  df-q 9166  df-fz 9486  df-iseq 9914  df-fac 10195  df-bc 10217

This theorem is referenced by:  bcn2  10233