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 e. (/) A = 1

Proof

Step Hyp Ref Expression
1 1z 
 |-  1 e. ZZ
2 nnuz 
 |-  NN = ( ZZ>= ` 1 )
3 id 
 |-  ( 1 e. ZZ -> 1 e. ZZ )
4 ax-1ne0 
 |-  1 =/= 0
5 4 a1i 
 |-  ( 1 e. ZZ -> 1 =/= 0 )
6 2 prodfclim1 
 |-  ( 1 e. ZZ -> seq 1 ( x. , ( NN X. { 1 } ) ) ~~> 1 )
7 0ss 
 |-  (/) C_ NN
8 7 a1i 
 |-  ( 1 e. ZZ -> (/) C_ NN )
9 fvconst2g 
 |-  ( ( 1 e. ZZ /\ k e. NN ) -> ( ( NN X. { 1 } ) ` k ) = 1 )
10 noel 
 |-  -. k e. (/)
11 10 iffalsei 
 |-  if ( k e. (/) , A , 1 ) = 1
12 9 11 eqtr4di 
 |-  ( ( 1 e. ZZ /\ k e. NN ) -> ( ( NN X. { 1 } ) ` k ) = if ( k e. (/) , A , 1 ) )
13 10 pm2.21i 
 |-  ( k e. (/) -> A e. CC )
14 13 adantl 
 |-  ( ( 1 e. ZZ /\ k e. (/) ) -> A e. CC )
15 2 3 5 6 8 12 14 zprodn0 
 |-  ( 1 e. ZZ -> prod_ k e. (/) A = 1 )
16 1 15 ax-mp 
 |-  prod_ k e. (/) A = 1