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

Definition df-fac 11289
Description: Define the factorial function on nonnegative integers. For example,  ( ! `  4 )  = ; 2
4 because  ( 4  x.  (
3  x.  ( 2  x.  1 ) ) )  = ; 2 4 (fac4 11296). 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 11288 . 2  class  !
2 cc0 8737 . . . . 5  class  0
3 c1 8738 . . . . 5  class  1
42, 3cop 3643 . . . 4  class  <. 0 ,  1 >.
54csn 3640 . . 3  class  { <. 0 ,  1 >. }
6 cmul 8742 . . . 4  class  x.
7 cid 4304 . . . 4  class  _I
86, 7, 3cseq 11046 . . 3  class  seq  1
(  x.  ,  _I  )
95, 8cun 3150 . 2  class  ( {
<. 0 ,  1
>. }  u.  seq  1
(  x.  ,  _I  ) )
101, 9wceq 1623 1  wff  !  =  ( { <. 0 ,  1 >. }  u.  seq  1 (  x.  ,  _I  ) )
Colors of variables: wff set class
This definition is referenced by:  facnn  11290  fac0  11291
  Copyright terms: Public domain W3C validator