Metamath Proof Explorer

Theorem bccmpl

Description: "Complementing" its second argument doesn't change a binary coefficient. (Contributed by NM, 21-Jun-2005) (Revised by Mario Carneiro, 5-Mar-2014)

Ref Expression
Assertion bccmpl 
|- ( ( N e. NN0 /\ K e. ZZ ) -> ( N _C K ) = ( N _C ( N - K ) ) )

Proof

Step Hyp Ref Expression
1 bcval2 
 |-  ( K e. ( 0 ... N ) -> ( N _C K ) = ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) )
2 fznn0sub2 
 |-  ( K e. ( 0 ... N ) -> ( N - K ) e. ( 0 ... N ) )
3 bcval2 
 |-  ( ( N - K ) e. ( 0 ... N ) -> ( N _C ( N - K ) ) = ( ( ! ` N ) / ( ( ! ` ( N - ( N - K ) ) ) x. ( ! ` ( N - K ) ) ) ) )
4 2 3 syl 
 |-  ( K e. ( 0 ... N ) -> ( N _C ( N - K ) ) = ( ( ! ` N ) / ( ( ! ` ( N - ( N - K ) ) ) x. ( ! ` ( N - K ) ) ) ) )
5 elfznn0 
 |-  ( ( N - K ) e. ( 0 ... N ) -> ( N - K ) e. NN0 )
6 5 faccld 
 |-  ( ( N - K ) e. ( 0 ... N ) -> ( ! ` ( N - K ) ) e. NN )
7 6 nncnd 
 |-  ( ( N - K ) e. ( 0 ... N ) -> ( ! ` ( N - K ) ) e. CC )
8 2 7 syl 
 |-  ( K e. ( 0 ... N ) -> ( ! ` ( N - K ) ) e. CC )
9 elfznn0 
 |-  ( K e. ( 0 ... N ) -> K e. NN0 )
10 9 faccld 
 |-  ( K e. ( 0 ... N ) -> ( ! ` K ) e. NN )
11 10 nncnd 
 |-  ( K e. ( 0 ... N ) -> ( ! ` K ) e. CC )
12 8 11 mulcomd 
 |-  ( K e. ( 0 ... N ) -> ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) = ( ( ! ` K ) x. ( ! ` ( N - K ) ) ) )
13 elfz3nn0 
 |-  ( K e. ( 0 ... N ) -> N e. NN0 )
14 elfzelz 
 |-  ( K e. ( 0 ... N ) -> K e. ZZ )
15 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
16 zcn 
 |-  ( K e. ZZ -> K e. CC )
17 nncan 
 |-  ( ( N e. CC /\ K e. CC ) -> ( N - ( N - K ) ) = K )
18 15 16 17 syl2an 
 |-  ( ( N e. NN0 /\ K e. ZZ ) -> ( N - ( N - K ) ) = K )
19 13 14 18 syl2anc 
 |-  ( K e. ( 0 ... N ) -> ( N - ( N - K ) ) = K )
20 19 fveq2d 
 |-  ( K e. ( 0 ... N ) -> ( ! ` ( N - ( N - K ) ) ) = ( ! ` K ) )
21 20 oveq1d 
 |-  ( K e. ( 0 ... N ) -> ( ( ! ` ( N - ( N - K ) ) ) x. ( ! ` ( N - K ) ) ) = ( ( ! ` K ) x. ( ! ` ( N - K ) ) ) )
22 12 21 eqtr4d 
 |-  ( K e. ( 0 ... N ) -> ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) = ( ( ! ` ( N - ( N - K ) ) ) x. ( ! ` ( N - K ) ) ) )
23 22 oveq2d 
 |-  ( K e. ( 0 ... N ) -> ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) = ( ( ! ` N ) / ( ( ! ` ( N - ( N - K ) ) ) x. ( ! ` ( N - K ) ) ) ) )
24 4 23 eqtr4d 
 |-  ( K e. ( 0 ... N ) -> ( N _C ( N - K ) ) = ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) )
25 1 24 eqtr4d 
 |-  ( K e. ( 0 ... N ) -> ( N _C K ) = ( N _C ( N - K ) ) )
26 25 adantl 
 |-  ( ( ( N e. NN0 /\ K e. ZZ ) /\ K e. ( 0 ... N ) ) -> ( N _C K ) = ( N _C ( N - K ) ) )
27 bcval3 
 |-  ( ( N e. NN0 /\ K e. ZZ /\ -. K e. ( 0 ... N ) ) -> ( N _C K ) = 0 )
28 simp1 
 |-  ( ( N e. NN0 /\ K e. ZZ /\ -. K e. ( 0 ... N ) ) -> N e. NN0 )
29 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
30 zsubcl 
 |-  ( ( N e. ZZ /\ K e. ZZ ) -> ( N - K ) e. ZZ )
31 29 30 sylan 
 |-  ( ( N e. NN0 /\ K e. ZZ ) -> ( N - K ) e. ZZ )
32 31 3adant3 
 |-  ( ( N e. NN0 /\ K e. ZZ /\ -. K e. ( 0 ... N ) ) -> ( N - K ) e. ZZ )
33 fznn0sub2 
 |-  ( ( N - K ) e. ( 0 ... N ) -> ( N - ( N - K ) ) e. ( 0 ... N ) )
34 18 eleq1d 
 |-  ( ( N e. NN0 /\ K e. ZZ ) -> ( ( N - ( N - K ) ) e. ( 0 ... N ) <-> K e. ( 0 ... N ) ) )
35 33 34 imbitrid 
 |-  ( ( N e. NN0 /\ K e. ZZ ) -> ( ( N - K ) e. ( 0 ... N ) -> K e. ( 0 ... N ) ) )
36 35 con3d 
 |-  ( ( N e. NN0 /\ K e. ZZ ) -> ( -. K e. ( 0 ... N ) -> -. ( N - K ) e. ( 0 ... N ) ) )
37 36 3impia 
 |-  ( ( N e. NN0 /\ K e. ZZ /\ -. K e. ( 0 ... N ) ) -> -. ( N - K ) e. ( 0 ... N ) )
38 bcval3 
 |-  ( ( N e. NN0 /\ ( N - K ) e. ZZ /\ -. ( N - K ) e. ( 0 ... N ) ) -> ( N _C ( N - K ) ) = 0 )
39 28 32 37 38 syl3anc 
 |-  ( ( N e. NN0 /\ K e. ZZ /\ -. K e. ( 0 ... N ) ) -> ( N _C ( N - K ) ) = 0 )
40 27 39 eqtr4d 
 |-  ( ( N e. NN0 /\ K e. ZZ /\ -. K e. ( 0 ... N ) ) -> ( N _C K ) = ( N _C ( N - K ) ) )
41 40 3expa 
 |-  ( ( ( N e. NN0 /\ K e. ZZ ) /\ -. K e. ( 0 ... N ) ) -> ( N _C K ) = ( N _C ( N - K ) ) )
42 26 41 pm2.61dan 
 |-  ( ( N e. NN0 /\ K e. ZZ ) -> ( N _C K ) = ( N _C ( N - K ) ) )