This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 class !
1 cc0 class 0
2 c1 class 1
3 1 2 cop class 0 1
4 3 csn class 0 1
5 cmul class ×
6 cid class I
7 5 6 2 cseq class seq 1 × I
8 4 7 cun class 0 1 ∪ seq 1 × I
9 0 8 wceq wff ! = 0 1 ∪ seq 1 × I