Metamath Proof Explorer


Theorem fprodclf

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

Ref Expression
Hypotheses fprodclf.kph 𝑘 𝜑
fprodclf.a ( 𝜑𝐴 ∈ Fin )
fprodclf.b ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ℂ )
Assertion fprodclf ( 𝜑 → ∏ 𝑘𝐴 𝐵 ∈ ℂ )

Proof

Step Hyp Ref Expression
1 fprodclf.kph 𝑘 𝜑
2 fprodclf.a ( 𝜑𝐴 ∈ Fin )
3 fprodclf.b ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ℂ )
4 ssidd ( 𝜑 → ℂ ⊆ ℂ )
5 mulcl ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
6 5 adantl ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
7 1cnd ( 𝜑 → 1 ∈ ℂ )
8 1 4 6 2 3 7 fprodcllemf ( 𝜑 → ∏ 𝑘𝐴 𝐵 ∈ ℂ )