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