Theorem facnn2

Description: Value of the factorial function expressed recursively. (Contributed by NM, 2-Dec-2004)

	Ref	Expression
Assertion	facnn2	$$⊢N\in \mathbb{N}\to N!=\left(N-1\right)!\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$

Proof

Step	Hyp	Ref	Expression
1		elnnnn0	$$⊢N\in \mathbb{N}\leftrightarrow \left(N\in ℂ\wedge N-1\in {\mathbb{N}}_0\right)$$
2		facp1	$$⊢N-1\in {\mathbb{N}}_0\to \left(N-1+1\right)!=\left(N-1\right)!\left(N-1+1\right)$$
3	2	adantl	$$⊢\left(N\in ℂ\wedge N-1\in {\mathbb{N}}_0\right)\to \left(N-1+1\right)!=\left(N-1\right)!\left(N-1+1\right)$$
4		npcan1	$$⊢N\in ℂ\to N-1+1=N$$
5	4	fveq2d	$$⊢N\in ℂ\to \left(N-1+1\right)!=N!$$
6	5	adantr	$$⊢\left(N\in ℂ\wedge N-1\in {\mathbb{N}}_0\right)\to \left(N-1+1\right)!=N!$$
7	4	oveq2d	$$⊢N\in ℂ\to \left(N-1\right)!\left(N-1+1\right)=\left(N-1\right)!\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
8	7	adantr	$$⊢\left(N\in ℂ\wedge N-1\in {\mathbb{N}}_0\right)\to \left(N-1\right)!\left(N-1+1\right)=\left(N-1\right)!\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
9	3 6 8	3eqtr3d	$$⊢\left(N\in ℂ\wedge N-1\in {\mathbb{N}}_0\right)\to N!=\left(N-1\right)!\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
10	1 9	sylbi	$$⊢N\in \mathbb{N}\to N!=\left(N-1\right)!\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$