Metamath Proof Explorer

Theorem facp2

Description: The factorial of a successor's successor. (Contributed by metakunt, 19-Apr-2024)

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

Proof

Step Hyp Ref Expression
1 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
2 ax-1cn 
 |-  1 e. CC
3 addass 
 |-  ( ( N e. CC /\ 1 e. CC /\ 1 e. CC ) -> ( ( N + 1 ) + 1 ) = ( N + ( 1 + 1 ) ) )
4 2 2 3 mp3an23 
 |-  ( N e. CC -> ( ( N + 1 ) + 1 ) = ( N + ( 1 + 1 ) ) )
5 1 4 syl 
 |-  ( N e. NN0 -> ( ( N + 1 ) + 1 ) = ( N + ( 1 + 1 ) ) )
6 df-2 
 |-  2 = ( 1 + 1 )
7 6 oveq2i 
 |-  ( N + 2 ) = ( N + ( 1 + 1 ) )
8 7 eqcomi 
 |-  ( N + ( 1 + 1 ) ) = ( N + 2 )
9 8 a1i 
 |-  ( N e. NN0 -> ( N + ( 1 + 1 ) ) = ( N + 2 ) )
10 5 9 eqtrd 
 |-  ( N e. NN0 -> ( ( N + 1 ) + 1 ) = ( N + 2 ) )
11 10 fveq2d 
 |-  ( N e. NN0 -> ( ! ` ( ( N + 1 ) + 1 ) ) = ( ! ` ( N + 2 ) ) )
12 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
13 facp1 
 |-  ( ( N + 1 ) e. NN0 -> ( ! ` ( ( N + 1 ) + 1 ) ) = ( ( ! ` ( N + 1 ) ) x. ( ( N + 1 ) + 1 ) ) )
14 12 13 syl 
 |-  ( N e. NN0 -> ( ! ` ( ( N + 1 ) + 1 ) ) = ( ( ! ` ( N + 1 ) ) x. ( ( N + 1 ) + 1 ) ) )
15 11 14 eqtr3d 
 |-  ( N e. NN0 -> ( ! ` ( N + 2 ) ) = ( ( ! ` ( N + 1 ) ) x. ( ( N + 1 ) + 1 ) ) )
16 10 oveq2d 
 |-  ( N e. NN0 -> ( ( ! ` ( N + 1 ) ) x. ( ( N + 1 ) + 1 ) ) = ( ( ! ` ( N + 1 ) ) x. ( N + 2 ) ) )
17 15 16 eqtrd 
 |-  ( N e. NN0 -> ( ! ` ( N + 2 ) ) = ( ( ! ` ( N + 1 ) ) x. ( N + 2 ) ) )
18 facp1 
 |-  ( N e. NN0 -> ( ! ` ( N + 1 ) ) = ( ( ! ` N ) x. ( N + 1 ) ) )
19 18 oveq1d 
 |-  ( N e. NN0 -> ( ( ! ` ( N + 1 ) ) x. ( N + 2 ) ) = ( ( ( ! ` N ) x. ( N + 1 ) ) x. ( N + 2 ) ) )
20 17 19 eqtrd 
 |-  ( N e. NN0 -> ( ! ` ( N + 2 ) ) = ( ( ( ! ` N ) x. ( N + 1 ) ) x. ( N + 2 ) ) )
21 faccl 
 |-  ( N e. NN0 -> ( ! ` N ) e. NN )
22 nncn 
 |-  ( ( ! ` N ) e. NN -> ( ! ` N ) e. CC )
23 21 22 syl 
 |-  ( N e. NN0 -> ( ! ` N ) e. CC )
24 nn0cn 
 |-  ( ( N + 1 ) e. NN0 -> ( N + 1 ) e. CC )
25 12 24 syl 
 |-  ( N e. NN0 -> ( N + 1 ) e. CC )
26 2cn 
 |-  2 e. CC
27 addcl 
 |-  ( ( N e. CC /\ 2 e. CC ) -> ( N + 2 ) e. CC )
28 26 27 mpan2 
 |-  ( N e. CC -> ( N + 2 ) e. CC )
29 1 28 syl 
 |-  ( N e. NN0 -> ( N + 2 ) e. CC )
30 mulass 
 |-  ( ( ( ! ` N ) e. CC /\ ( N + 1 ) e. CC /\ ( N + 2 ) e. CC ) -> ( ( ( ! ` N ) x. ( N + 1 ) ) x. ( N + 2 ) ) = ( ( ! ` N ) x. ( ( N + 1 ) x. ( N + 2 ) ) ) )
31 23 25 29 30 syl3anc 
 |-  ( N e. NN0 -> ( ( ( ! ` N ) x. ( N + 1 ) ) x. ( N + 2 ) ) = ( ( ! ` N ) x. ( ( N + 1 ) x. ( N + 2 ) ) ) )
32 20 31 eqtrd 
 |-  ( N e. NN0 -> ( ! ` ( N + 2 ) ) = ( ( ! ` N ) x. ( ( N + 1 ) x. ( N + 2 ) ) ) )