Database
REAL AND COMPLEX NUMBERS
Elementary limits and convergence
Finite and infinite products
Finite products
fprodclf
Metamath Proof Explorer
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
⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐵 ∈ ℂ )