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 ⟩ } ∪ seq 1 ( · , 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	⊢ ·
6		cid	⊢ I
7	5 6 2	cseq	⊢ seq 1 ( · , I )
8	4 7	cun	⊢ ( { ⟨ 0 , 1 ⟩ } ∪ seq 1 ( · , I ) )
9	0 8	wceq	⊢ ! = ( { ⟨ 0 , 1 ⟩ } ∪ seq 1 ( · , I ) )