Metamath Proof Explorer

Theorem facp1

Description: The factorial of a successor. (Contributed by NM, 2-Dec-2004) (Revised by Mario Carneiro, 13-Jul-2013)

Ref Expression
Assertion facp1 
|- ( N e. NN0 -> ( ! ` ( N + 1 ) ) = ( ( ! ` N ) x. ( N + 1 ) ) )

Proof

Step Hyp Ref Expression
1 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
2 peano2nn 
 |-  ( N e. NN -> ( N + 1 ) e. NN )
3 facnn 
 |-  ( ( N + 1 ) e. NN -> ( ! ` ( N + 1 ) ) = ( seq 1 ( x. , _I ) ` ( N + 1 ) ) )
4 2 3 syl 
 |-  ( N e. NN -> ( ! ` ( N + 1 ) ) = ( seq 1 ( x. , _I ) ` ( N + 1 ) ) )
5 ovex 
 |-  ( N + 1 ) e. _V
6 fvi 
 |-  ( ( N + 1 ) e. _V -> ( _I ` ( N + 1 ) ) = ( N + 1 ) )
7 5 6 ax-mp 
 |-  ( _I ` ( N + 1 ) ) = ( N + 1 )
8 7 oveq2i 
 |-  ( ( seq 1 ( x. , _I ) ` N ) x. ( _I ` ( N + 1 ) ) ) = ( ( seq 1 ( x. , _I ) ` N ) x. ( N + 1 ) )
9 seqp1 
 |-  ( N e. ( ZZ>= ` 1 ) -> ( seq 1 ( x. , _I ) ` ( N + 1 ) ) = ( ( seq 1 ( x. , _I ) ` N ) x. ( _I ` ( N + 1 ) ) ) )
10 nnuz 
 |-  NN = ( ZZ>= ` 1 )
11 9 10 eleq2s 
 |-  ( N e. NN -> ( seq 1 ( x. , _I ) ` ( N + 1 ) ) = ( ( seq 1 ( x. , _I ) ` N ) x. ( _I ` ( N + 1 ) ) ) )
12 facnn 
 |-  ( N e. NN -> ( ! ` N ) = ( seq 1 ( x. , _I ) ` N ) )
13 12 oveq1d 
 |-  ( N e. NN -> ( ( ! ` N ) x. ( N + 1 ) ) = ( ( seq 1 ( x. , _I ) ` N ) x. ( N + 1 ) ) )
14 8 11 13 3eqtr4a 
 |-  ( N e. NN -> ( seq 1 ( x. , _I ) ` ( N + 1 ) ) = ( ( ! ` N ) x. ( N + 1 ) ) )
15 4 14 eqtrd 
 |-  ( N e. NN -> ( ! ` ( N + 1 ) ) = ( ( ! ` N ) x. ( N + 1 ) ) )
16 0p1e1 
 |-  ( 0 + 1 ) = 1
17 16 fveq2i 
 |-  ( ! ` ( 0 + 1 ) ) = ( ! ` 1 )
18 fac1 
 |-  ( ! ` 1 ) = 1
19 17 18 eqtri 
 |-  ( ! ` ( 0 + 1 ) ) = 1
20 fvoveq1 
 |-  ( N = 0 -> ( ! ` ( N + 1 ) ) = ( ! ` ( 0 + 1 ) ) )
21 fveq2 
 |-  ( N = 0 -> ( ! ` N ) = ( ! ` 0 ) )
22 oveq1 
 |-  ( N = 0 -> ( N + 1 ) = ( 0 + 1 ) )
23 21 22 oveq12d 
 |-  ( N = 0 -> ( ( ! ` N ) x. ( N + 1 ) ) = ( ( ! ` 0 ) x. ( 0 + 1 ) ) )
24 fac0 
 |-  ( ! ` 0 ) = 1
25 24 16 oveq12i 
 |-  ( ( ! ` 0 ) x. ( 0 + 1 ) ) = ( 1 x. 1 )
26 1t1e1 
 |-  ( 1 x. 1 ) = 1
27 25 26 eqtri 
 |-  ( ( ! ` 0 ) x. ( 0 + 1 ) ) = 1
28 23 27 eqtrdi 
 |-  ( N = 0 -> ( ( ! ` N ) x. ( N + 1 ) ) = 1 )
29 19 20 28 3eqtr4a 
 |-  ( N = 0 -> ( ! ` ( N + 1 ) ) = ( ( ! ` N ) x. ( N + 1 ) ) )
30 15 29 jaoi 
 |-  ( ( N e. NN \/ N = 0 ) -> ( ! ` ( N + 1 ) ) = ( ( ! ` N ) x. ( N + 1 ) ) )
31 1 30 sylbi 
 |-  ( N e. NN0 -> ( ! ` ( N + 1 ) ) = ( ( ! ` N ) x. ( N + 1 ) ) )