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

Definition df-fac 11283
Description: Define the factorial function on nonnegative integers. For example,  ( ! `  4 )  = ; 2
4 because  ( 4  x.  (
3  x.  ( 2  x.  1 ) ) )  = ; 2 4 (fac4 11290). 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  ) )

Detailed syntax breakdown of Definition df-fac
StepHypRef Expression
1 cfa 11282 . 2  class  !
2 cc0 8732 . . . . 5  class  0
3 c1 8733 . . . . 5  class  1
42, 3cop 3644 . . . 4  class  <. 0 ,  1 >.
54csn 3641 . . 3  class  { <. 0 ,  1 >. }
6 cmul 8737 . . . 4  class  x.
7 cid 4303 . . . 4  class  _I
86, 7, 3cseq 11040 . . 3  class  seq  1
(  x.  ,  _I  )
95, 8cun 3151 . 2  class  ( {
<. 0 ,  1
>. }  u.  seq  1
(  x.  ,  _I  ) )
101, 9wceq 1624 1  wff  !  =  ( { <. 0 ,  1 >. }  u.  seq  1 (  x.  ,  _I  ) )
Colors of variables: wff set class
This definition is referenced by:  facnn  11284  fac0  11285
  Copyright terms: Public domain W3C validator