Metamath Proof Explorer

Theorem faccl

Description: Closure of the factorial function. (Contributed by NM, 2-Dec-2004)

Ref Expression
Assertion faccl 
|- ( N e. NN0 -> ( ! ` N ) e. NN )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( j = 0 -> ( ! ` j ) = ( ! ` 0 ) )
2 1 eleq1d 
 |-  ( j = 0 -> ( ( ! ` j ) e. NN <-> ( ! ` 0 ) e. NN ) )
3 fveq2 
 |-  ( j = k -> ( ! ` j ) = ( ! ` k ) )
4 3 eleq1d 
 |-  ( j = k -> ( ( ! ` j ) e. NN <-> ( ! ` k ) e. NN ) )
5 fveq2 
 |-  ( j = ( k + 1 ) -> ( ! ` j ) = ( ! ` ( k + 1 ) ) )
6 5 eleq1d 
 |-  ( j = ( k + 1 ) -> ( ( ! ` j ) e. NN <-> ( ! ` ( k + 1 ) ) e. NN ) )
7 fveq2 
 |-  ( j = N -> ( ! ` j ) = ( ! ` N ) )
8 7 eleq1d 
 |-  ( j = N -> ( ( ! ` j ) e. NN <-> ( ! ` N ) e. NN ) )
9 fac0 
 |-  ( ! ` 0 ) = 1
10 1nn 
 |-  1 e. NN
11 9 10 eqeltri 
 |-  ( ! ` 0 ) e. NN
12 facp1 
 |-  ( k e. NN0 -> ( ! ` ( k + 1 ) ) = ( ( ! ` k ) x. ( k + 1 ) ) )
13 12 adantl 
 |-  ( ( ( ! ` k ) e. NN /\ k e. NN0 ) -> ( ! ` ( k + 1 ) ) = ( ( ! ` k ) x. ( k + 1 ) ) )
14 nn0p1nn 
 |-  ( k e. NN0 -> ( k + 1 ) e. NN )
15 nnmulcl 
 |-  ( ( ( ! ` k ) e. NN /\ ( k + 1 ) e. NN ) -> ( ( ! ` k ) x. ( k + 1 ) ) e. NN )
16 14 15 sylan2 
 |-  ( ( ( ! ` k ) e. NN /\ k e. NN0 ) -> ( ( ! ` k ) x. ( k + 1 ) ) e. NN )
17 13 16 eqeltrd 
 |-  ( ( ( ! ` k ) e. NN /\ k e. NN0 ) -> ( ! ` ( k + 1 ) ) e. NN )
18 17 expcom 
 |-  ( k e. NN0 -> ( ( ! ` k ) e. NN -> ( ! ` ( k + 1 ) ) e. NN ) )
19 2 4 6 8 11 18 nn0ind 
 |-  ( N e. NN0 -> ( ! ` N ) e. NN )