Definition df-fac 7135

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 7134	. 2 class !
2		cc0 5388	. . . . 5 class 0
3		c1 5389	. . . . 5 class 1
4	2, 3	cop 2469	. . . 4 class <.0, 1>.
5	4	csn 2467	. . 3 class {<.0, 1>.}
6		cmul 5393	. . . 4 class x.
7		cid 2909	. . . . 5 class I
8		cn 5450	. . . . 5 class NN
9	7, 8	cres 3253	. . . 4 class (I |` NN)
10		cseq1 6672	. . . 4 class seq1
11	6, 9, 10	co 4021	. . 3 class ( x. seq1 (I |` NN))
12	5, 11	cun 2097	. 2 class ({<.0, 1>.} u. ( x. seq1 (I |` NN)))
13	1, 12	wceq 992	1 wff ! = ({<.0, 1>.} u. ( x. seq1 (I |` NN)))

This definition is referenced by:  facnn 7136  fac0 7137

Copyright terms: Public domain