Theorem ex-fac

Description: Example for df-fac . (Contributed by AV, 4-Sep-2021)

	Ref	Expression
Assertion	ex-fac	⊢ ( ! ‘ 5 ) = ; ; 1 2 0

Proof

Step	Hyp	Ref	Expression
1		df-5	⊢ 5 = ( 4 + 1 )
2	1	fveq2i	⊢ ( ! ‘ 5 ) = ( ! ‘ ( 4 + 1 ) )
3		4nn0	⊢ 4 ∈ ℕ0
4		facp1	⊢ ( 4 ∈ ℕ0 → ( ! ‘ ( 4 + 1 ) ) = ( ( ! ‘ 4 ) · ( 4 + 1 ) ) )
5	3 4	ax-mp	⊢ ( ! ‘ ( 4 + 1 ) ) = ( ( ! ‘ 4 ) · ( 4 + 1 ) )
6	2 5	eqtri	⊢ ( ! ‘ 5 ) = ( ( ! ‘ 4 ) · ( 4 + 1 ) )
7		fac4	⊢ ( ! ‘ 4 ) = ; 2 4
8		4p1e5	⊢ ( 4 + 1 ) = 5
9	7 8	oveq12i	⊢ ( ( ! ‘ 4 ) · ( 4 + 1 ) ) = ( ; 2 4 · 5 )
10		5nn0	⊢ 5 ∈ ℕ0
11		2nn0	⊢ 2 ∈ ℕ0
12		eqid	⊢ ; 2 4 = ; 2 4
13		0nn0	⊢ 0 ∈ ℕ0
14		1nn0	⊢ 1 ∈ ℕ0
15		5cn	⊢ 5 ∈ ℂ
16		2cn	⊢ 2 ∈ ℂ
17		5t2e10	⊢ ( 5 · 2 ) = ; 1 0
18	15 16 17	mulcomli	⊢ ( 2 · 5 ) = ; 1 0
19	16	addid2i	⊢ ( 0 + 2 ) = 2
20	14 13 11 18 19	decaddi	⊢ ( ( 2 · 5 ) + 2 ) = ; 1 2
21		4cn	⊢ 4 ∈ ℂ
22		5t4e20	⊢ ( 5 · 4 ) = ; 2 0
23	15 21 22	mulcomli	⊢ ( 4 · 5 ) = ; 2 0
24	10 11 3 12 13 11 20 23	decmul1c	⊢ ( ; 2 4 · 5 ) = ; ; 1 2 0
25	9 24	eqtri	⊢ ( ( ! ‘ 4 ) · ( 4 + 1 ) ) = ; ; 1 2 0
26	6 25	eqtri	⊢ ( ! ‘ 5 ) = ; ; 1 2 0