Theorem fprodfac

Description: Factorial using product notation. (Contributed by Scott Fenton, 15-Dec-2017)

	Ref	Expression
Assertion	fprodfac	$$⊢A\in {\mathbb{N}}_0\to A!=\prod _{k=1}^{A}k$$

Proof

Step	Hyp	Ref	Expression
1		elnn0	$$⊢A\in {\mathbb{N}}_0\leftrightarrow \left(A\in \mathbb{N}\vee A=0\right)$$
2		facnn	$$⊢A\in \mathbb{N}\to A!=seq1\left(\times ,\mathrm{I}\right)\left(A\right)$$
3		vex	$$⊢k\in \mathrm{V}$$
4		fvi	$$⊢k\in \mathrm{V}\to \mathrm{I}\left(k\right)=k$$
5	3 4	mp1i	$$⊢\left(A\in \mathbb{N}\wedge k\in \left(1\dots A\right)\right)\to \mathrm{I}\left(k\right)=k$$
6		elnnuz	$$⊢A\in \mathbb{N}\leftrightarrow A\in {\mathbb{Z}}_{\ge 1}$$
7	6	biimpi	$$⊢A\in \mathbb{N}\to A\in {\mathbb{Z}}_{\ge 1}$$
8		elfznn	$$⊢k\in \left(1\dots A\right)\to k\in \mathbb{N}$$
9	8	nncnd	$$⊢k\in \left(1\dots A\right)\to k\in ℂ$$
10	9	adantl	$$⊢\left(A\in \mathbb{N}\wedge k\in \left(1\dots A\right)\right)\to k\in ℂ$$
11	5 7 10	fprodser	$$⊢A\in \mathbb{N}\to \prod _{k=1}^{A}k=seq1\left(\times ,\mathrm{I}\right)\left(A\right)$$
12	2 11	eqtr4d	$$⊢A\in \mathbb{N}\to A!=\prod _{k=1}^{A}k$$
13		prod0	$$⊢\prod _{k\in \varnothing }k=1$$
14	13	eqcomi	$$⊢1=\prod _{k\in \varnothing }k$$
15		fveq2	$$⊢A=0\to A!=0!$$
16		fac0	$$⊢0!=1$$
17	15 16	eqtrdi	$$⊢A=0\to A!=1$$
18		oveq2	$$⊢A=0\to \left(1\dots A\right)=\left(1\dots 0\right)$$
19		fz10	$$⊢\left(1\dots 0\right)=\varnothing$$
20	18 19	eqtrdi	$$⊢A=0\to \left(1\dots A\right)=\varnothing$$
21	20	prodeq1d	$$⊢A=0\to \prod _{k=1}^{A}k=\prod _{k\in \varnothing }k$$
22	14 17 21	3eqtr4a	$$⊢A=0\to A!=\prod _{k=1}^{A}k$$
23	12 22	jaoi	$$⊢\left(A\in \mathbb{N}\vee A=0\right)\to A!=\prod _{k=1}^{A}k$$
24	1 23	sylbi	$$⊢A\in {\mathbb{N}}_0\to A!=\prod _{k=1}^{A}k$$