Theorem prod0

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

	Ref	Expression
Assertion	prod0	⊢ ∏ 𝑘 ∈ ∅ 𝐴 = 1

Proof

Step	Hyp	Ref	Expression
1		1z	⊢ 1 ∈ ℤ
2		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
3		id	⊢ ( 1 ∈ ℤ → 1 ∈ ℤ )
4		ax-1ne0	⊢ 1 ≠ 0
5	4	a1i	⊢ ( 1 ∈ ℤ → 1 ≠ 0 )
6	2	prodfclim1	⊢ ( 1 ∈ ℤ → seq 1 ( · , ( ℕ × { 1 } ) ) ⇝ 1 )
7		0ss	⊢ ∅ ⊆ ℕ
8	7	a1i	⊢ ( 1 ∈ ℤ → ∅ ⊆ ℕ )
9		fvconst2g	⊢ ( ( 1 ∈ ℤ ∧ 𝑘 ∈ ℕ ) → ( ( ℕ × { 1 } ) ‘ 𝑘 ) = 1 )
10		noel	⊢ ¬ 𝑘 ∈ ∅
11	10	iffalsei	⊢ if ( 𝑘 ∈ ∅ , 𝐴 , 1 ) = 1
12	9 11	eqtr4di	⊢ ( ( 1 ∈ ℤ ∧ 𝑘 ∈ ℕ ) → ( ( ℕ × { 1 } ) ‘ 𝑘 ) = if ( 𝑘 ∈ ∅ , 𝐴 , 1 ) )
13	10	pm2.21i	⊢ ( 𝑘 ∈ ∅ → 𝐴 ∈ ℂ )
14	13	adantl	⊢ ( ( 1 ∈ ℤ ∧ 𝑘 ∈ ∅ ) → 𝐴 ∈ ℂ )
15	2 3 5 6 8 12 14	zprodn0	⊢ ( 1 ∈ ℤ → ∏ 𝑘 ∈ ∅ 𝐴 = 1 )
16	1 15	ax-mp	⊢ ∏ 𝑘 ∈ ∅ 𝐴 = 1