Step |
Hyp |
Ref |
Expression |
1 |
|
oveq2 |
|- ( n = N -> ( 0 ... n ) = ( 0 ... N ) ) |
2 |
1
|
eleq2d |
|- ( n = N -> ( k e. ( 0 ... n ) <-> k e. ( 0 ... N ) ) ) |
3 |
|
fveq2 |
|- ( n = N -> ( ! ` n ) = ( ! ` N ) ) |
4 |
|
fvoveq1 |
|- ( n = N -> ( ! ` ( n - k ) ) = ( ! ` ( N - k ) ) ) |
5 |
4
|
oveq1d |
|- ( n = N -> ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) = ( ( ! ` ( N - k ) ) x. ( ! ` k ) ) ) |
6 |
3 5
|
oveq12d |
|- ( n = N -> ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) = ( ( ! ` N ) / ( ( ! ` ( N - k ) ) x. ( ! ` k ) ) ) ) |
7 |
2 6
|
ifbieq1d |
|- ( n = N -> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) = if ( k e. ( 0 ... N ) , ( ( ! ` N ) / ( ( ! ` ( N - k ) ) x. ( ! ` k ) ) ) , 0 ) ) |
8 |
|
eleq1 |
|- ( k = K -> ( k e. ( 0 ... N ) <-> K e. ( 0 ... N ) ) ) |
9 |
|
oveq2 |
|- ( k = K -> ( N - k ) = ( N - K ) ) |
10 |
9
|
fveq2d |
|- ( k = K -> ( ! ` ( N - k ) ) = ( ! ` ( N - K ) ) ) |
11 |
|
fveq2 |
|- ( k = K -> ( ! ` k ) = ( ! ` K ) ) |
12 |
10 11
|
oveq12d |
|- ( k = K -> ( ( ! ` ( N - k ) ) x. ( ! ` k ) ) = ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) |
13 |
12
|
oveq2d |
|- ( k = K -> ( ( ! ` N ) / ( ( ! ` ( N - k ) ) x. ( ! ` k ) ) ) = ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) ) |
14 |
8 13
|
ifbieq1d |
|- ( k = K -> if ( k e. ( 0 ... N ) , ( ( ! ` N ) / ( ( ! ` ( N - k ) ) x. ( ! ` k ) ) ) , 0 ) = if ( K e. ( 0 ... N ) , ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) , 0 ) ) |
15 |
|
df-bc |
|- _C = ( n e. NN0 , k e. ZZ |-> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) ) |
16 |
|
ovex |
|- ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) e. _V |
17 |
|
c0ex |
|- 0 e. _V |
18 |
16 17
|
ifex |
|- if ( K e. ( 0 ... N ) , ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) , 0 ) e. _V |
19 |
7 14 15 18
|
ovmpo |
|- ( ( N e. NN0 /\ K e. ZZ ) -> ( N _C K ) = if ( K e. ( 0 ... N ) , ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) , 0 ) ) |