Definition df-fac

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 ). In the literature, the factorial function is written as a postscript exclamation point. (Contributed by NM, 2-Dec-2004)

	Ref	Expression
Assertion	df-fac	|- ! = ( { <. 0 , 1 >. } u. seq 1 ( x. , _I ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfa	|- !
1		cc0	|- 0
2		c1	|- 1
3	1 2	cop	|- <. 0 , 1 >.
4	3	csn	|- { <. 0 , 1 >. }
5		cmul	|- x.
6		cid	|- _I
7	5 6 2	cseq	|- seq 1 ( x. , _I )
8	4 7	cun	|- ( { <. 0 , 1 >. } u. seq 1 ( x. , _I ) )
9	0 8	wceq	|- ! = ( { <. 0 , 1 >. } u. seq 1 ( x. , _I ) )