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 ( 𝑁 − 𝐾 ) ) )