Definition df-fac 9653

Description: Define the factorial function on nonnegative integers. For example, (!‘5) = 120 because 1 · 2 · 3 · 4 · 5 = 120 (ex-fac 10565). 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⟩} ∪ seq1( · , I , ℂ))

Detailed syntax breakdown of Definition df-fac

Step	Hyp	Ref	Expression
1		cfa 9652	. 2 class !
2		cc0 6981	. . . . 5 class 0
3		c1 6982	. . . . 5 class 1
4	2, 3	cop 3401	. . . 4 class ⟨0, 1⟩
5	4	csn 3398	. . 3 class {⟨0, 1⟩}
6		cmul 6986	. . . 4 class ·
7		cc 6979	. . . 4 class ℂ
8		cid 4043	. . . 4 class I
9	6, 7, 8, 3	cseq 9431	. . 3 class seq1( · , I , ℂ)
10	5, 9	cun 2971	. 2 class ({⟨0, 1⟩} ∪ seq1( · , I , ℂ))
11	1, 10	wceq 1284	1 wff ! = ({⟨0, 1⟩} ∪ seq1( · , I , ℂ))

This definition is referenced by:  facnn  9654  fac0  9655