Theorem facnn

Description: Value of the factorial function for positive integers. (Contributed by NM, 2-Dec-2004) (Revised by Mario Carneiro, 13-Jul-2013)

	Ref	Expression
Assertion	facnn	|- ( N e. NN -> ( ! ` N ) = ( seq 1 ( x. , _I ) ` N ) )

Proof

Step	Hyp	Ref	Expression
1		c0ex	|- 0 e. _V
2	1	a1i	|- ( N e. ( NN0 \ { 0 } ) -> 0 e. _V )
3		1ex	|- 1 e. _V
4	3	a1i	|- ( N e. ( NN0 \ { 0 } ) -> 1 e. _V )
5		df-fac	|- ! = ( { <. 0 , 1 >. } u. seq 1 ( x. , _I ) )
6		nnuz	|- NN = ( ZZ>= ` 1 )
7		dfn2	|- NN = ( NN0 \ { 0 } )
8	6 7	eqtr3i	|- ( ZZ>= ` 1 ) = ( NN0 \ { 0 } )
9	8	reseq2i	|- ( seq 1 ( x. , _I ) |` ( ZZ>= ` 1 ) ) = ( seq 1 ( x. , _I ) |` ( NN0 \ { 0 } ) )
10		1z	|- 1 e. ZZ
11		seqfn	|- ( 1 e. ZZ -> seq 1 ( x. , _I ) Fn ( ZZ>= ` 1 ) )
12		fnresdm	|- ( seq 1 ( x. , _I ) Fn ( ZZ>= ` 1 ) -> ( seq 1 ( x. , _I ) |` ( ZZ>= ` 1 ) ) = seq 1 ( x. , _I ) )
13	10 11 12	mp2b	|- ( seq 1 ( x. , _I ) |` ( ZZ>= ` 1 ) ) = seq 1 ( x. , _I )
14	9 13	eqtr3i	|- ( seq 1 ( x. , _I ) |` ( NN0 \ { 0 } ) ) = seq 1 ( x. , _I )
15	14	uneq2i	|- ( { <. 0 , 1 >. } u. ( seq 1 ( x. , _I ) |` ( NN0 \ { 0 } ) ) ) = ( { <. 0 , 1 >. } u. seq 1 ( x. , _I ) )
16	5 15	eqtr4i	|- ! = ( { <. 0 , 1 >. } u. ( seq 1 ( x. , _I ) |` ( NN0 \ { 0 } ) ) )
17		id	|- ( N e. ( NN0 \ { 0 } ) -> N e. ( NN0 \ { 0 } ) )
18	2 4 16 17	fvsnun2	|- ( N e. ( NN0 \ { 0 } ) -> ( ! ` N ) = ( seq 1 ( x. , _I ) ` N ) )
19	18 7	eleq2s	|- ( N e. NN -> ( ! ` N ) = ( seq 1 ( x. , _I ) ` N ) )