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 38057
Description: Define a generalized binomial coefficient operation, which unlike df-bc 13046 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 38056 . 2 class C𝑐
2 vc . . 3 setvar 𝑐
3 vk . . 3 setvar 𝑘
4 cc 9894 . . 3 class
5 cn0 11252 . . 3 class 0
62cv 1479 . . . . 5 class 𝑐
73cv 1479 . . . . 5 class 𝑘
8 cfallfac 14679 . . . . 5 class FallFac
96, 7, 8co 6615 . . . 4 class (𝑐 FallFac 𝑘)
10 cfa 13016 . . . . 5 class !
117, 10cfv 5857 . . . 4 class (!‘𝑘)
12 cdiv 10644 . . . 4 class /
139, 11, 12co 6615 . . 3 class ((𝑐 FallFac 𝑘) / (!‘𝑘))
142, 3, 4, 5, 13cmpt2 6617 . 2 class (𝑐 ∈ ℂ, 𝑘 ∈ ℕ0 ↦ ((𝑐 FallFac 𝑘) / (!‘𝑘)))
151, 14wceq 1480 1 wff C𝑐 = (𝑐 ∈ ℂ, 𝑘 ∈ ℕ0 ↦ ((𝑐 FallFac 𝑘) / (!‘𝑘)))
Colors of variables: wff setvar class
This definition is referenced by:  bccval  38058
  Copyright terms: Public domain W3C validator