Metamath Proof Explorer


Theorem fac4

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

Ref Expression
Assertion fac4 4!=24

Proof

Step Hyp Ref Expression
1 3nn0 30
2 facp1 303+1!=3!3+1
3 1 2 ax-mp 3+1!=3!3+1
4 3p1e4 3+1=4
5 4 fveq2i 3+1!=4!
6 fac3 3!=6
7 6 4 oveq12i 3!3+1=64
8 6t4e24 64=24
9 7 8 eqtri 3!3+1=24
10 3 5 9 3eqtr3i 4!=24