Definition df-fac 6932

Description: Define the factorial function on nonnegative integers. In the literature, the factorial function is written as a postscript exclamation point.

Assertion

Ref	Expression
df-fac	|- ! = ({<.0, 1>.} u. ( x. seq1 (I |` NN)))

Detailed syntax breakdown of Definition df-fac

Step	Hyp	Ref	Expression
1		cfa 6931	. 2 class !
2		cc0 5234	. . . . 5 class 0
3		c1 5235	. . . . 5 class 1
4	2, 3	cop 2411	. . . 4 class <.0, 1>.
5	4	csn 2409	. . 3 class {<.0, 1>.}
6		cmul 5239	. . . 4 class x.
7		cid 2831	. . . . 5 class I
8		cn 5296	. . . . 5 class NN
9	7, 8	cres 3172	. . . 4 class (I |` NN)
10		cseq1 6307	. . . 4 class seq1
11	6, 9, 10	co 3963	. . 3 class ( x. seq1 (I |` NN))
12	5, 11	cun 2045	. 2 class ({<.0, 1>.} u. ( x. seq1 (I |` NN)))
13	1, 12	wceq 956	1 wff ! = ({<.0, 1>.} u. ( x. seq1 (I |` NN)))

This definition is referenced by:  facnnt 6933  fac0 6934

Copyright terms: Public domain