Metamath Proof Explorer

Theorem fprodcl

Description: Closure of a finite product of complex numbers. (Contributed by Scott Fenton, 14-Dec-2017)

Ref Expression
Hypotheses fprodcl.1 φ A Fin
fprodcl.2 φ k A B
Assertion fprodcl φ k A B


Step Hyp Ref Expression
1 fprodcl.1 φ A Fin
2 fprodcl.2 φ k A B
3 ssidd φ
4 mulcl x y x y
5 4 adantl φ x y x y
6 1cnd φ 1
7 3 5 1 2 6 fprodcllem φ k A B