MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bccmpl Structured version   Visualization version   GIF version

Theorem bccmpl 13039
Description: "Complementing" its second argument doesn't change a binary coefficient. (Contributed by NM, 21-Jun-2005.) (Revised by Mario Carneiro, 5-Mar-2014.)
Assertion
Ref Expression
bccmpl ((𝑁 ∈ ℕ0𝐾 ∈ ℤ) → (𝑁C𝐾) = (𝑁C(𝑁𝐾)))

Proof of Theorem bccmpl
StepHypRef Expression
1 bcval2 13035 . . . 4 (𝐾 ∈ (0...𝑁) → (𝑁C𝐾) = ((!‘𝑁) / ((!‘(𝑁𝐾)) · (!‘𝐾))))
2 fznn0sub2 12390 . . . . . 6 (𝐾 ∈ (0...𝑁) → (𝑁𝐾) ∈ (0...𝑁))
3 bcval2 13035 . . . . . 6 ((𝑁𝐾) ∈ (0...𝑁) → (𝑁C(𝑁𝐾)) = ((!‘𝑁) / ((!‘(𝑁 − (𝑁𝐾))) · (!‘(𝑁𝐾)))))
42, 3syl 17 . . . . 5 (𝐾 ∈ (0...𝑁) → (𝑁C(𝑁𝐾)) = ((!‘𝑁) / ((!‘(𝑁 − (𝑁𝐾))) · (!‘(𝑁𝐾)))))
5 elfznn0 12377 . . . . . . . . . . 11 ((𝑁𝐾) ∈ (0...𝑁) → (𝑁𝐾) ∈ ℕ0)
6 faccl 13013 . . . . . . . . . . 11 ((𝑁𝐾) ∈ ℕ0 → (!‘(𝑁𝐾)) ∈ ℕ)
75, 6syl 17 . . . . . . . . . 10 ((𝑁𝐾) ∈ (0...𝑁) → (!‘(𝑁𝐾)) ∈ ℕ)
87nncnd 10983 . . . . . . . . 9 ((𝑁𝐾) ∈ (0...𝑁) → (!‘(𝑁𝐾)) ∈ ℂ)
92, 8syl 17 . . . . . . . 8 (𝐾 ∈ (0...𝑁) → (!‘(𝑁𝐾)) ∈ ℂ)
10 elfznn0 12377 . . . . . . . . . 10 (𝐾 ∈ (0...𝑁) → 𝐾 ∈ ℕ0)
11 faccl 13013 . . . . . . . . . 10 (𝐾 ∈ ℕ0 → (!‘𝐾) ∈ ℕ)
1210, 11syl 17 . . . . . . . . 9 (𝐾 ∈ (0...𝑁) → (!‘𝐾) ∈ ℕ)
1312nncnd 10983 . . . . . . . 8 (𝐾 ∈ (0...𝑁) → (!‘𝐾) ∈ ℂ)
149, 13mulcomd 10008 . . . . . . 7 (𝐾 ∈ (0...𝑁) → ((!‘(𝑁𝐾)) · (!‘𝐾)) = ((!‘𝐾) · (!‘(𝑁𝐾))))
15 elfz3nn0 12378 . . . . . . . . . 10 (𝐾 ∈ (0...𝑁) → 𝑁 ∈ ℕ0)
16 elfzelz 12287 . . . . . . . . . 10 (𝐾 ∈ (0...𝑁) → 𝐾 ∈ ℤ)
17 nn0cn 11249 . . . . . . . . . . 11 (𝑁 ∈ ℕ0𝑁 ∈ ℂ)
18 zcn 11329 . . . . . . . . . . 11 (𝐾 ∈ ℤ → 𝐾 ∈ ℂ)
19 nncan 10257 . . . . . . . . . . 11 ((𝑁 ∈ ℂ ∧ 𝐾 ∈ ℂ) → (𝑁 − (𝑁𝐾)) = 𝐾)
2017, 18, 19syl2an 494 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝐾 ∈ ℤ) → (𝑁 − (𝑁𝐾)) = 𝐾)
2115, 16, 20syl2anc 692 . . . . . . . . 9 (𝐾 ∈ (0...𝑁) → (𝑁 − (𝑁𝐾)) = 𝐾)
2221fveq2d 6154 . . . . . . . 8 (𝐾 ∈ (0...𝑁) → (!‘(𝑁 − (𝑁𝐾))) = (!‘𝐾))
2322oveq1d 6622 . . . . . . 7 (𝐾 ∈ (0...𝑁) → ((!‘(𝑁 − (𝑁𝐾))) · (!‘(𝑁𝐾))) = ((!‘𝐾) · (!‘(𝑁𝐾))))
2414, 23eqtr4d 2658 . . . . . 6 (𝐾 ∈ (0...𝑁) → ((!‘(𝑁𝐾)) · (!‘𝐾)) = ((!‘(𝑁 − (𝑁𝐾))) · (!‘(𝑁𝐾))))
2524oveq2d 6623 . . . . 5 (𝐾 ∈ (0...𝑁) → ((!‘𝑁) / ((!‘(𝑁𝐾)) · (!‘𝐾))) = ((!‘𝑁) / ((!‘(𝑁 − (𝑁𝐾))) · (!‘(𝑁𝐾)))))
264, 25eqtr4d 2658 . . . 4 (𝐾 ∈ (0...𝑁) → (𝑁C(𝑁𝐾)) = ((!‘𝑁) / ((!‘(𝑁𝐾)) · (!‘𝐾))))
271, 26eqtr4d 2658 . . 3 (𝐾 ∈ (0...𝑁) → (𝑁C𝐾) = (𝑁C(𝑁𝐾)))
2827adantl 482 . 2 (((𝑁 ∈ ℕ0𝐾 ∈ ℤ) ∧ 𝐾 ∈ (0...𝑁)) → (𝑁C𝐾) = (𝑁C(𝑁𝐾)))
29 bcval3 13036 . . . 4 ((𝑁 ∈ ℕ0𝐾 ∈ ℤ ∧ ¬ 𝐾 ∈ (0...𝑁)) → (𝑁C𝐾) = 0)
30 simp1 1059 . . . . 5 ((𝑁 ∈ ℕ0𝐾 ∈ ℤ ∧ ¬ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈ ℕ0)
31 nn0z 11347 . . . . . . 7 (𝑁 ∈ ℕ0𝑁 ∈ ℤ)
32 zsubcl 11366 . . . . . . 7 ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑁𝐾) ∈ ℤ)
3331, 32sylan 488 . . . . . 6 ((𝑁 ∈ ℕ0𝐾 ∈ ℤ) → (𝑁𝐾) ∈ ℤ)
34333adant3 1079 . . . . 5 ((𝑁 ∈ ℕ0𝐾 ∈ ℤ ∧ ¬ 𝐾 ∈ (0...𝑁)) → (𝑁𝐾) ∈ ℤ)
35 fznn0sub2 12390 . . . . . . . 8 ((𝑁𝐾) ∈ (0...𝑁) → (𝑁 − (𝑁𝐾)) ∈ (0...𝑁))
3620eleq1d 2683 . . . . . . . 8 ((𝑁 ∈ ℕ0𝐾 ∈ ℤ) → ((𝑁 − (𝑁𝐾)) ∈ (0...𝑁) ↔ 𝐾 ∈ (0...𝑁)))
3735, 36syl5ib 234 . . . . . . 7 ((𝑁 ∈ ℕ0𝐾 ∈ ℤ) → ((𝑁𝐾) ∈ (0...𝑁) → 𝐾 ∈ (0...𝑁)))
3837con3d 148 . . . . . 6 ((𝑁 ∈ ℕ0𝐾 ∈ ℤ) → (¬ 𝐾 ∈ (0...𝑁) → ¬ (𝑁𝐾) ∈ (0...𝑁)))
39383impia 1258 . . . . 5 ((𝑁 ∈ ℕ0𝐾 ∈ ℤ ∧ ¬ 𝐾 ∈ (0...𝑁)) → ¬ (𝑁𝐾) ∈ (0...𝑁))
40 bcval3 13036 . . . . 5 ((𝑁 ∈ ℕ0 ∧ (𝑁𝐾) ∈ ℤ ∧ ¬ (𝑁𝐾) ∈ (0...𝑁)) → (𝑁C(𝑁𝐾)) = 0)
4130, 34, 39, 40syl3anc 1323 . . . 4 ((𝑁 ∈ ℕ0𝐾 ∈ ℤ ∧ ¬ 𝐾 ∈ (0...𝑁)) → (𝑁C(𝑁𝐾)) = 0)
4229, 41eqtr4d 2658 . . 3 ((𝑁 ∈ ℕ0𝐾 ∈ ℤ ∧ ¬ 𝐾 ∈ (0...𝑁)) → (𝑁C𝐾) = (𝑁C(𝑁𝐾)))
43423expa 1262 . 2 (((𝑁 ∈ ℕ0𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...𝑁)) → (𝑁C𝐾) = (𝑁C(𝑁𝐾)))
4428, 43pm2.61dan 831 1 ((𝑁 ∈ ℕ0𝐾 ∈ ℤ) → (𝑁C𝐾) = (𝑁C(𝑁𝐾)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384  w3a 1036   = wceq 1480  wcel 1987  cfv 5849  (class class class)co 6607  cc 9881  0cc0 9883   · cmul 9888  cmin 10213   / cdiv 10631  cn 10967  0cn0 11239  cz 11324  ...cfz 12271  !cfa 13003  Ccbc 13032
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4743  ax-nul 4751  ax-pow 4805  ax-pr 4869  ax-un 6905  ax-cnex 9939  ax-resscn 9940  ax-1cn 9941  ax-icn 9942  ax-addcl 9943  ax-addrcl 9944  ax-mulcl 9945  ax-mulrcl 9946  ax-mulcom 9947  ax-addass 9948  ax-mulass 9949  ax-distr 9950  ax-i2m1 9951  ax-1ne0 9952  ax-1rid 9953  ax-rnegex 9954  ax-rrecex 9955  ax-cnre 9956  ax-pre-lttri 9957  ax-pre-lttrn 9958  ax-pre-ltadd 9959  ax-pre-mulgt0 9960
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3188  df-sbc 3419  df-csb 3516  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-pss 3572  df-nul 3894  df-if 4061  df-pw 4134  df-sn 4151  df-pr 4153  df-tp 4155  df-op 4157  df-uni 4405  df-iun 4489  df-br 4616  df-opab 4676  df-mpt 4677  df-tr 4715  df-eprel 4987  df-id 4991  df-po 4997  df-so 4998  df-fr 5035  df-we 5037  df-xp 5082  df-rel 5083  df-cnv 5084  df-co 5085  df-dm 5086  df-rn 5087  df-res 5088  df-ima 5089  df-pred 5641  df-ord 5687  df-on 5688  df-lim 5689  df-suc 5690  df-iota 5812  df-fun 5851  df-fn 5852  df-f 5853  df-f1 5854  df-fo 5855  df-f1o 5856  df-fv 5857  df-riota 6568  df-ov 6610  df-oprab 6611  df-mpt2 6612  df-om 7016  df-1st 7116  df-2nd 7117  df-wrecs 7355  df-recs 7416  df-rdg 7454  df-er 7690  df-en 7903  df-dom 7904  df-sdom 7905  df-pnf 10023  df-mnf 10024  df-xr 10025  df-ltxr 10026  df-le 10027  df-sub 10215  df-neg 10216  df-nn 10968  df-n0 11240  df-z 11325  df-uz 11635  df-fz 12272  df-seq 12745  df-fac 13004  df-bc 13033
This theorem is referenced by:  bcnn  13042  bcnp1n  13044  bcp1m1  13050  bcnm1  13057  basellem3  24716  chtublem  24843  bcmax  24910  bcp1ctr  24911
  Copyright terms: Public domain W3C validator