Theorem prod0

Description: A product over the empty set is one. (Contributed by Scott Fenton, 5-Dec-2017)

	Ref	Expression
Assertion	prod0	$$⊢\prod _{k\in \varnothing }A=1$$

Proof

Step	Hyp	Ref	Expression
1		1z	$$⊢1\in \mathbb{Z}$$
2		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
3		id	$$⊢1\in \mathbb{Z}\to 1\in \mathbb{Z}$$
4		ax-1ne0	$$⊢1\ne 0$$
5	4	a1i	$$⊢1\in \mathbb{Z}\to 1\ne 0$$
6	2	prodfclim1	$$⊢1\in \mathbb{Z}\to seq1\left(\times ,\left(\mathbb{N}\times \left\{1\right\}\right)\right)⇝1$$
7		0ss	$$⊢\varnothing \subseteq \mathbb{N}$$
8	7	a1i	$$⊢1\in \mathbb{Z}\to \varnothing \subseteq \mathbb{N}$$
9		fvconst2g	$$⊢\left(1\in \mathbb{Z}\wedge k\in \mathbb{N}\right)\to \left(\mathbb{N}\times \left\{1\right\}\right)\left(k\right)=1$$
10		noel	$$⊢\neg k\in \varnothing$$
11	10	iffalsei	$$⊢if\left(k\in \varnothing ,A,1\right)=1$$
12	9 11	eqtr4di	$$⊢\left(1\in \mathbb{Z}\wedge k\in \mathbb{N}\right)\to \left(\mathbb{N}\times \left\{1\right\}\right)\left(k\right)=if\left(k\in \varnothing ,A,1\right)$$
13	10	pm2.21i	$$⊢k\in \varnothing \to A\in ℂ$$
14	13	adantl	$$⊢\left(1\in \mathbb{Z}\wedge k\in \varnothing \right)\to A\in ℂ$$
15	2 3 5 6 8 12 14	zprodn0	$$⊢1\in \mathbb{Z}\to \prod _{k\in \varnothing }A=1$$
16	1 15	ax-mp	$$⊢\prod _{k\in \varnothing }A=1$$