Metamath Proof Explorer


Theorem fprodreclf

Description: Closure of a finite product of real numbers. A version of fprodrecl using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses fprodreclf.kph โŠข โ„ฒ ๐‘˜ ๐œ‘
fprodcl.a โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ Fin )
fprodrecl.b โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐ด ) โ†’ ๐ต โˆˆ โ„ )
Assertion fprodreclf ( ๐œ‘ โ†’ โˆ ๐‘˜ โˆˆ ๐ด ๐ต โˆˆ โ„ )

Proof

Step Hyp Ref Expression
1 fprodreclf.kph โŠข โ„ฒ ๐‘˜ ๐œ‘
2 fprodcl.a โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ Fin )
3 fprodrecl.b โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐ด ) โ†’ ๐ต โˆˆ โ„ )
4 ax-resscn โŠข โ„ โІ โ„‚
5 4 a1i โŠข ( ๐œ‘ โ†’ โ„ โІ โ„‚ )
6 remulcl โŠข ( ( ๐‘ฅ โˆˆ โ„ โˆง ๐‘ฆ โˆˆ โ„ ) โ†’ ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ โ„ )
7 6 adantl โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„ โˆง ๐‘ฆ โˆˆ โ„ ) ) โ†’ ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ โ„ )
8 1red โŠข ( ๐œ‘ โ†’ 1 โˆˆ โ„ )
9 1 5 7 2 3 8 fprodcllemf โŠข ( ๐œ‘ โ†’ โˆ ๐‘˜ โˆˆ ๐ด ๐ต โˆˆ โ„ )