ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-fac GIF version

Definition df-fac 10134
Description: Define the factorial function on nonnegative integers. For example, (!‘5) = 120 because 1 · 2 · 3 · 4 · 5 = 120 (ex-fac 11655). In the literature, the factorial function is written as a postscript exclamation point. (Contributed by NM, 2-Dec-2004.)
Assertion
Ref Expression
df-fac ! = ({⟨0, 1⟩} ∪ seq1( · , I , ℂ))

Detailed syntax breakdown of Definition df-fac
StepHypRef Expression
1 cfa 10133 . 2 class !
2 cc0 7350 . . . . 5 class 0
3 c1 7351 . . . . 5 class 1
42, 3cop 3449 . . . 4 class ⟨0, 1⟩
54csn 3446 . . 3 class {⟨0, 1⟩}
6 cmul 7355 . . . 4 class ·
7 cc 7348 . . . 4 class
8 cid 4115 . . . 4 class I
96, 7, 8, 3cseq4 9851 . . 3 class seq1( · , I , ℂ)
105, 9cun 2997 . 2 class ({⟨0, 1⟩} ∪ seq1( · , I , ℂ))
111, 10wceq 1289 1 wff ! = ({⟨0, 1⟩} ∪ seq1( · , I , ℂ))
Colors of variables: wff set class
This definition is referenced by:  facnn  10135  fac0  10136
  Copyright terms: Public domain W3C validator