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 ⊢ !
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 ) )