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

Metamath Proof Explorer

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