Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-fallfac Structured version   Unicode version

Definition df-fallfac 14038
 Description: Define the falling factorial function. This is the function for complex and nonnegative integers . (Contributed by Scott Fenton, 5-Jan-2018.)
Assertion
Ref Expression
df-fallfac FallFac
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-fallfac
StepHypRef Expression
1 cfallfac 14035 . 2 FallFac
2 vx . . 3
3 vn . . 3
4 cc 9536 . . 3
5 cn0 10869 . . 3
6 cc0 9538 . . . . 5
73cv 1436 . . . . . 6
8 c1 9539 . . . . . 6
9 cmin 9859 . . . . . 6
107, 8, 9co 6305 . . . . 5
11 cfz 11782 . . . . 5
126, 10, 11co 6305 . . . 4
132cv 1436 . . . . 5
14 vk . . . . . 6
1514cv 1436 . . . . 5
1613, 15, 9co 6305 . . . 4
1712, 16, 14cprod 13937 . . 3
182, 3, 4, 5, 17cmpt2 6307 . 2
191, 18wceq 1437 1 FallFac
 Colors of variables: wff setvar class This definition is referenced by:  fallfacval  14040
 Copyright terms: Public domain W3C validator