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 ∈ ℕ0
2		facp1	⊢ ( 3 ∈ ℕ0 → ( ! ‘ ( 3 + 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 ) ) = ( 6 · 4 )
8		6t4e24	⊢ ( 6 · 4 ) = ; 2 4
9	7 8	eqtri	⊢ ( ( ! ‘ 3 ) · ( 3 + 1 ) ) = ; 2 4
10	3 5 9	3eqtr3i	⊢ ( ! ‘ 4 ) = ; 2 4