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 syl6eqr 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