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 ( ( 𝑁 ∈ ℕ0𝐾 ∈ ℤ ) → ( 𝑁 C 𝐾 ) = ( 𝑁 C ( 𝑁𝐾 ) ) )

Proof

Step Hyp Ref Expression
1 bcval2 ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝐾 ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) )
2 fznn0sub2 ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁𝐾 ) ∈ ( 0 ... 𝑁 ) )
3 bcval2 ( ( 𝑁𝐾 ) ∈ ( 0 ... 𝑁 ) → ( 𝑁 C ( 𝑁𝐾 ) ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − ( 𝑁𝐾 ) ) ) · ( ! ‘ ( 𝑁𝐾 ) ) ) ) )
4 2 3 syl ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C ( 𝑁𝐾 ) ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − ( 𝑁𝐾 ) ) ) · ( ! ‘ ( 𝑁𝐾 ) ) ) ) )
5 elfznn0 ( ( 𝑁𝐾 ) ∈ ( 0 ... 𝑁 ) → ( 𝑁𝐾 ) ∈ ℕ0 )
6 5 faccld ( ( 𝑁𝐾 ) ∈ ( 0 ... 𝑁 ) → ( ! ‘ ( 𝑁𝐾 ) ) ∈ ℕ )
7 6 nncnd ( ( 𝑁𝐾 ) ∈ ( 0 ... 𝑁 ) → ( ! ‘ ( 𝑁𝐾 ) ) ∈ ℂ )
8 2 7 syl ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ! ‘ ( 𝑁𝐾 ) ) ∈ ℂ )
9 elfznn0 ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ℕ0 )
10 9 faccld ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ! ‘ 𝐾 ) ∈ ℕ )
11 10 nncnd ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ! ‘ 𝐾 ) ∈ ℂ )
12 8 11 mulcomd ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( ! ‘ ( 𝑁𝐾 ) ) · ( ! ‘ 𝐾 ) ) = ( ( ! ‘ 𝐾 ) · ( ! ‘ ( 𝑁𝐾 ) ) ) )
13 elfz3nn0 ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℕ0 )
14 elfzelz ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ℤ )
15 nn0cn ( 𝑁 ∈ ℕ0𝑁 ∈ ℂ )
16 zcn ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ )
17 nncan ( ( 𝑁 ∈ ℂ ∧ 𝐾 ∈ ℂ ) → ( 𝑁 − ( 𝑁𝐾 ) ) = 𝐾 )
18 15 16 17 syl2an ( ( 𝑁 ∈ ℕ0𝐾 ∈ ℤ ) → ( 𝑁 − ( 𝑁𝐾 ) ) = 𝐾 )
19 13 14 18 syl2anc ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 − ( 𝑁𝐾 ) ) = 𝐾 )
20 19 fveq2d ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ! ‘ ( 𝑁 − ( 𝑁𝐾 ) ) ) = ( ! ‘ 𝐾 ) )
21 20 oveq1d ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( ! ‘ ( 𝑁 − ( 𝑁𝐾 ) ) ) · ( ! ‘ ( 𝑁𝐾 ) ) ) = ( ( ! ‘ 𝐾 ) · ( ! ‘ ( 𝑁𝐾 ) ) ) )
22 12 21 eqtr4d ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( ! ‘ ( 𝑁𝐾 ) ) · ( ! ‘ 𝐾 ) ) = ( ( ! ‘ ( 𝑁 − ( 𝑁𝐾 ) ) ) · ( ! ‘ ( 𝑁𝐾 ) ) ) )
23 22 oveq2d ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − ( 𝑁𝐾 ) ) ) · ( ! ‘ ( 𝑁𝐾 ) ) ) ) )
24 4 23 eqtr4d ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C ( 𝑁𝐾 ) ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) )
25 1 24 eqtr4d ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝐾 ) = ( 𝑁 C ( 𝑁𝐾 ) ) )
26 25 adantl ( ( ( 𝑁 ∈ ℕ0𝐾 ∈ ℤ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝐾 ) = ( 𝑁 C ( 𝑁𝐾 ) ) )
27 bcval3 ( ( 𝑁 ∈ ℕ0𝐾 ∈ ℤ ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝐾 ) = 0 )
28 simp1 ( ( 𝑁 ∈ ℕ0𝐾 ∈ ℤ ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ℕ0 )
29 nn0z ( 𝑁 ∈ ℕ0𝑁 ∈ ℤ )
30 zsubcl ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑁𝐾 ) ∈ ℤ )
31 29 30 sylan ( ( 𝑁 ∈ ℕ0𝐾 ∈ ℤ ) → ( 𝑁𝐾 ) ∈ ℤ )
32 31 3adant3 ( ( 𝑁 ∈ ℕ0𝐾 ∈ ℤ ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁𝐾 ) ∈ ℤ )
33 fznn0sub2 ( ( 𝑁𝐾 ) ∈ ( 0 ... 𝑁 ) → ( 𝑁 − ( 𝑁𝐾 ) ) ∈ ( 0 ... 𝑁 ) )
34 18 eleq1d ( ( 𝑁 ∈ ℕ0𝐾 ∈ ℤ ) → ( ( 𝑁 − ( 𝑁𝐾 ) ) ∈ ( 0 ... 𝑁 ) ↔ 𝐾 ∈ ( 0 ... 𝑁 ) ) )
35 33 34 syl5ib ( ( 𝑁 ∈ ℕ0𝐾 ∈ ℤ ) → ( ( 𝑁𝐾 ) ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ( 0 ... 𝑁 ) ) )
36 35 con3d ( ( 𝑁 ∈ ℕ0𝐾 ∈ ℤ ) → ( ¬ 𝐾 ∈ ( 0 ... 𝑁 ) → ¬ ( 𝑁𝐾 ) ∈ ( 0 ... 𝑁 ) ) )
37 36 3impia ( ( 𝑁 ∈ ℕ0𝐾 ∈ ℤ ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ¬ ( 𝑁𝐾 ) ∈ ( 0 ... 𝑁 ) )
38 bcval3 ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁𝐾 ) ∈ ℤ ∧ ¬ ( 𝑁𝐾 ) ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C ( 𝑁𝐾 ) ) = 0 )
39 28 32 37 38 syl3anc ( ( 𝑁 ∈ ℕ0𝐾 ∈ ℤ ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C ( 𝑁𝐾 ) ) = 0 )
40 27 39 eqtr4d ( ( 𝑁 ∈ ℕ0𝐾 ∈ ℤ ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝐾 ) = ( 𝑁 C ( 𝑁𝐾 ) ) )
41 40 3expa ( ( ( 𝑁 ∈ ℕ0𝐾 ∈ ℤ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝐾 ) = ( 𝑁 C ( 𝑁𝐾 ) ) )
42 26 41 pm2.61dan ( ( 𝑁 ∈ ℕ0𝐾 ∈ ℤ ) → ( 𝑁 C 𝐾 ) = ( 𝑁 C ( 𝑁𝐾 ) ) )