This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ∏ k ∈ ∅ A = 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 ∈ ℤ ∧ k ∈ ℕ → ℕ × 1 ⁡ k = 1
10 noel ⊢ ¬ k ∈ ∅
11 10 iffalsei ⊢ if k ∈ ∅ A 1 = 1
12 9 11 eqtr4di ⊢ 1 ∈ ℤ ∧ k ∈ ℕ → ℕ × 1 ⁡ k = if k ∈ ∅ A 1
13 10 pm2.21i ⊢ k ∈ ∅ → A ∈ ℂ
14 13 adantl ⊢ 1 ∈ ℤ ∧ k ∈ ∅ → A ∈ ℂ
15 2 3 5 6 8 12 14 zprodn0 ⊢ 1 ∈ ℤ → ∏ k ∈ ∅ A = 1
16 1 15 ax-mp ⊢ ∏ k ∈ ∅ A = 1