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

Definition df-fac 10031
Description: Define the factorial function on nonnegative integers. For example,  ( ! `  5 )  =  1 2 0 because  1  x.  2  x.  3  x.  4  x.  5  =  1 2 0 (ex-fac 11100). 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 >. }  u.  seq 1 (  x.  ,  _I  ,  CC ) )

Detailed syntax breakdown of Definition df-fac
StepHypRef Expression
1 cfa 10030 . 2  class  !
2 cc0 7294 . . . . 5  class  0
3 c1 7295 . . . . 5  class  1
42, 3cop 3434 . . . 4  class  <. 0 ,  1 >.
54csn 3431 . . 3  class  { <. 0 ,  1 >. }
6 cmul 7299 . . . 4  class  x.
7 cc 7292 . . . 4  class  CC
8 cid 4089 . . . 4  class  _I
96, 7, 8, 3cseq 9779 . . 3  class  seq 1
(  x.  ,  _I  ,  CC )
105, 9cun 2986 . 2  class  ( {
<. 0 ,  1
>. }  u.  seq 1
(  x.  ,  _I  ,  CC ) )
111, 10wceq 1287 1  wff  !  =  ( { <. 0 ,  1 >. }  u.  seq 1 (  x.  ,  _I  ,  CC ) )
Colors of variables: wff set class
This definition is referenced by:  facnn  10032  fac0  10033
  Copyright terms: Public domain W3C validator