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

Definition df-fac 10440
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 12867). 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 10439 . 2  class  !
2 cc0 7588 . . . . 5  class  0
3 c1 7589 . . . . 5  class  1
42, 3cop 3500 . . . 4  class  <. 0 ,  1 >.
54csn 3497 . . 3  class  { <. 0 ,  1 >. }
6 cmul 7593 . . . 4  class  x.
7 cid 4180 . . . 4  class  _I
86, 7, 3cseq 10186 . . 3  class  seq 1
(  x.  ,  _I  )
95, 8cun 3039 . 2  class  ( {
<. 0 ,  1
>. }  u.  seq 1
(  x.  ,  _I  ) )
101, 9wceq 1316 1  wff  !  =  ( { <. 0 ,  1 >. }  u.  seq 1 (  x.  ,  _I  ) )
Colors of variables: wff set class
This definition is referenced by:  facnn  10441  fac0  10442
  Copyright terms: Public domain W3C validator