# 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 ) ) )`
` |-  ( ( ( ! ` k ) e. NN /\ k e. NN0 ) -> ( ! ` ( k + 1 ) ) = ( ( ! ` k ) x. ( k + 1 ) ) )`
` |-  ( k e. NN0 -> ( k + 1 ) e. NN )`
` |-  ( ( ( ! ` k ) e. NN /\ ( k + 1 ) e. NN ) -> ( ( ! ` k ) x. ( k + 1 ) ) e. NN )`
` |-  ( ( ( ! ` k ) e. NN /\ k e. NN0 ) -> ( ( ! ` k ) x. ( k + 1 ) ) e. NN )`
` |-  ( ( ( ! ` k ) e. NN /\ k e. NN0 ) -> ( ! ` ( k + 1 ) ) e. NN )`
` |-  ( k e. NN0 -> ( ( ! ` k ) e. NN -> ( ! ` ( k + 1 ) ) e. NN ) )`
` |-  ( N e. NN0 -> ( ! ` N ) e. NN )`