Theorem ex-fac

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

	Ref	Expression
Assertion	ex-fac	$$⊢5!=120$$

Proof

Step	Hyp	Ref	Expression
1		df-5	$$⊢5=4+1$$
2	1	fveq2i	$$⊢5!=\left(4+1\right)!$$
3		4nn0	$$⊢4\in {\mathbb{N}}_0$$
4		facp1	$$⊢4\in {\mathbb{N}}_0\to \left(4+1\right)!=4!\left(4+1\right)$$
5	3 4	ax-mp	$$⊢\left(4+1\right)!=4!\left(4+1\right)$$
6	2 5	eqtri	$$⊢5!=4!\left(4+1\right)$$
7		fac4	$$⊢4!=24$$
8		4p1e5	$$⊢4+1=5$$
9	7 8	oveq12i	$$⊢4!\left(4+1\right)=24\cdot 5$$
10		5nn0	$$⊢5\in {\mathbb{N}}_0$$
11		2nn0	$$⊢2\in {\mathbb{N}}_0$$
12		eqid	$$⊢24=24$$
13		0nn0	$$⊢0\in {\mathbb{N}}_0$$
14		1nn0	$$⊢1\in {\mathbb{N}}_0$$
15		5cn	$$⊢5\in ℂ$$
16		2cn	$$⊢2\in ℂ$$
17		5t2e10	$$⊢5\cdot 2=10$$
18	15 16 17	mulcomli	$$⊢2\cdot 5=10$$
19	16	addlidi	$$⊢0+2=2$$
20	14 13 11 18 19	decaddi	$$⊢2\cdot 5+2=12$$
21		4cn	$$⊢4\in ℂ$$
22		5t4e20	$$⊢5\cdot 4=20$$
23	15 21 22	mulcomli	$$⊢4\cdot 5=20$$
24	10 11 3 12 13 11 20 23	decmul1c	$$⊢24\cdot 5=120$$
25	9 24	eqtri	$$⊢4!\left(4+1\right)=120$$
26	6 25	eqtri	$$⊢5!=120$$