Theorem facp2

Description: The factorial of a successor's successor. (Contributed by metakunt, 19-Apr-2024)

	Ref	Expression
Assertion	facp2	$$⊢N\in {\mathbb{N}}_0\to \left(N+2\right)!=N!\left(N+1\right)\left(N+2\right)$$

Proof

Step	Hyp	Ref	Expression
1		nn0cn	$$⊢N\in {\mathbb{N}}_0\to N\in ℂ$$
2		ax-1cn	$$⊢1\in ℂ$$
3		addass	$$⊢\left(N\in ℂ\wedge 1\in ℂ\wedge 1\in ℂ\right)\to N+1+1=N+1+1$$
4	2 2 3	mp3an23	$$⊢N\in ℂ\to N+1+1=N+1+1$$
5	1 4	syl	$$⊢N\in {\mathbb{N}}_0\to N+1+1=N+1+1$$
6		df-2	$$⊢2=1+1$$
7	6	oveq2i	$$⊢N+2=N+1+1$$
8	7	eqcomi	$$⊢N+1+1=N+2$$
9	8	a1i	$$⊢N\in {\mathbb{N}}_0\to N+1+1=N+2$$
10	5 9	eqtrd	$$⊢N\in {\mathbb{N}}_0\to N+1+1=N+2$$
11	10	fveq2d	$$⊢N\in {\mathbb{N}}_0\to \left(N+1+1\right)!=\left(N+2\right)!$$
12		peano2nn0	$$⊢N\in {\mathbb{N}}_0\to N+1\in {\mathbb{N}}_0$$
13		facp1	$$⊢N+1\in {\mathbb{N}}_0\to \left(N+1+1\right)!=\left(N+1\right)!\left(N+1+1\right)$$
14	12 13	syl	$$⊢N\in {\mathbb{N}}_0\to \left(N+1+1\right)!=\left(N+1\right)!\left(N+1+1\right)$$
15	11 14	eqtr3d	$$⊢N\in {\mathbb{N}}_0\to \left(N+2\right)!=\left(N+1\right)!\left(N+1+1\right)$$
16	10	oveq2d	$$⊢N\in {\mathbb{N}}_0\to \left(N+1\right)!\left(N+1+1\right)=\left(N+1\right)!\left(N+2\right)$$
17	15 16	eqtrd	$$⊢N\in {\mathbb{N}}_0\to \left(N+2\right)!=\left(N+1\right)!\left(N+2\right)$$
18		facp1	$$⊢N\in {\mathbb{N}}_0\to \left(N+1\right)!=N!\left(N+1\right)$$
19	18	oveq1d	$$⊢N\in {\mathbb{N}}_0\to \left(N+1\right)!\left(N+2\right)=N!\left(N+1\right)\left(N+2\right)$$
20	17 19	eqtrd	$$⊢N\in {\mathbb{N}}_0\to \left(N+2\right)!=N!\left(N+1\right)\left(N+2\right)$$
21		faccl	$$⊢N\in {\mathbb{N}}_0\to N!\in \mathbb{N}$$
22		nncn	$$⊢N!\in \mathbb{N}\to N!\in ℂ$$
23	21 22	syl	$$⊢N\in {\mathbb{N}}_0\to N!\in ℂ$$
24		nn0cn	$$⊢N+1\in {\mathbb{N}}_0\to N+1\in ℂ$$
25	12 24	syl	$$⊢N\in {\mathbb{N}}_0\to N+1\in ℂ$$
26		2cn	$$⊢2\in ℂ$$
27		addcl	$$⊢\left(N\in ℂ\wedge 2\in ℂ\right)\to N+2\in ℂ$$
28	26 27	mpan2	$$⊢N\in ℂ\to N+2\in ℂ$$
29	1 28	syl	$$⊢N\in {\mathbb{N}}_0\to N+2\in ℂ$$
30		mulass	$$⊢\left(N!\in ℂ\wedge N+1\in ℂ\wedge N+2\in ℂ\right)\to N!\left(N+1\right)\left(N+2\right)=N!\left(N+1\right)\left(N+2\right)$$
31	23 25 29 30	syl3anc	$$⊢N\in {\mathbb{N}}_0\to N!\left(N+1\right)\left(N+2\right)=N!\left(N+1\right)\left(N+2\right)$$
32	20 31	eqtrd	$$⊢N\in {\mathbb{N}}_0\to \left(N+2\right)!=N!\left(N+1\right)\left(N+2\right)$$