Metamath Proof Explorer

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 ℤ$
2 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
3 id ${⊢}1\in ℤ\to 1\in ℤ$
4 ax-1ne0 ${⊢}1\ne 0$
5 4 a1i ${⊢}1\in ℤ\to 1\ne 0$
6 2 prodfclim1 ${⊢}1\in ℤ\to seq1\left(×,\left(ℕ×\left\{1\right\}\right)\right)⇝1$
7 0ss ${⊢}\varnothing \subseteq ℕ$
8 7 a1i ${⊢}1\in ℤ\to \varnothing \subseteq ℕ$
9 fvconst2g ${⊢}\left(1\in ℤ\wedge {k}\in ℕ\right)\to \left(ℕ×\left\{1\right\}\right)\left({k}\right)=1$
10 noel ${⊢}¬{k}\in \varnothing$
11 10 iffalsei ${⊢}if\left({k}\in \varnothing ,{A},1\right)=1$
12 9 11 syl6eqr ${⊢}\left(1\in ℤ\wedge {k}\in ℕ\right)\to \left(ℕ×\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 ℤ\wedge {k}\in \varnothing \right)\to {A}\in ℂ$
15 2 3 5 6 8 12 14 zprodn0 ${⊢}1\in ℤ\to \prod _{{k}\in \varnothing }{A}=1$
16 1 15 ax-mp ${⊢}\prod _{{k}\in \varnothing }{A}=1$