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 ∏ 𝑘 ∈ ∅ 𝐴 = 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