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

Definition df-fac 12354
Description: Define the factorial function on nonnegative integers. For example, because (fac4 12361). In the literature, the factorial function is written as a postscript exclamation point. (Contributed by NM, 2-Dec-2004.)
Assertion
Ref Expression
df-fac

Detailed syntax breakdown of Definition df-fac
StepHypRef Expression
1 cfa 12353 . 2
2 cc0 9513 . . . . 5
3 c1 9514 . . . . 5
42, 3cop 4035 . . . 4
54csn 4029 . . 3
6 cmul 9518 . . . 4
7 cid 4795 . . . 4
86, 7, 3cseq 12107 . . 3
95, 8cun 3473 . 2
101, 9wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  facnn  12355  fac0  12356
  Copyright terms: Public domain W3C validator