Metamath Proof Explorer

Theorem fac4

Description: The factorial of 4. (Contributed by Mario Carneiro, 18-Jun-2015)

Ref Expression
Assertion fac4 
|- ( ! ` 4 ) = ; 2 4

Proof

Step Hyp Ref Expression
1 3nn0 
 |-  3 e. NN0
2 facp1 
 |-  ( 3 e. NN0 -> ( ! ` ( 3 + 1 ) ) = ( ( ! ` 3 ) x. ( 3 + 1 ) ) )
3 1 2 ax-mp 
 |-  ( ! ` ( 3 + 1 ) ) = ( ( ! ` 3 ) x. ( 3 + 1 ) )
4 3p1e4 
 |-  ( 3 + 1 ) = 4
5 4 fveq2i 
 |-  ( ! ` ( 3 + 1 ) ) = ( ! ` 4 )
6 fac3 
 |-  ( ! ` 3 ) = 6
7 6 4 oveq12i 
 |-  ( ( ! ` 3 ) x. ( 3 + 1 ) ) = ( 6 x. 4 )
8 6t4e24 
 |-  ( 6 x. 4 ) = ; 2 4
9 7 8 eqtri 
 |-  ( ( ! ` 3 ) x. ( 3 + 1 ) ) = ; 2 4
10 3 5 9 3eqtr3i 
 |-  ( ! ` 4 ) = ; 2 4