Users' Mathboxes Mathbox for Steve Rodriguez < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bcc Structured version   Visualization version   GIF version

Definition df-bcc 40856
Description: Define a generalized binomial coefficient operation, which unlike df-bc 13647 allows complex numbers for the first argument. (Contributed by Steve Rodriguez, 22-Apr-2020.)
Assertion
Ref Expression
df-bcc C𝑐 = (𝑐 ∈ ℂ, 𝑘 ∈ ℕ0 ↦ ((𝑐 FallFac 𝑘) / (!‘𝑘)))
Distinct variable group:   𝑘,𝑐

Detailed syntax breakdown of Definition df-bcc
StepHypRef Expression
1 cbcc 40855 . 2 class C𝑐
2 vc . . 3 setvar 𝑐
3 vk . . 3 setvar 𝑘
4 cc 10512 . . 3 class
5 cn0 11875 . . 3 class 0
62cv 1537 . . . . 5 class 𝑐
73cv 1537 . . . . 5 class 𝑘
8 cfallfac 15337 . . . . 5 class FallFac
96, 7, 8co 7130 . . . 4 class (𝑐 FallFac 𝑘)
10 cfa 13617 . . . . 5 class !
117, 10cfv 6328 . . . 4 class (!‘𝑘)
12 cdiv 11274 . . . 4 class /
139, 11, 12co 7130 . . 3 class ((𝑐 FallFac 𝑘) / (!‘𝑘))
142, 3, 4, 5, 13cmpo 7132 . 2 class (𝑐 ∈ ℂ, 𝑘 ∈ ℕ0 ↦ ((𝑐 FallFac 𝑘) / (!‘𝑘)))
151, 14wceq 1538 1 wff C𝑐 = (𝑐 ∈ ℂ, 𝑘 ∈ ℕ0 ↦ ((𝑐 FallFac 𝑘) / (!‘𝑘)))
Colors of variables: wff setvar class
This definition is referenced by:  bccval  40857
  Copyright terms: Public domain W3C validator