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 | |- F/ k ph |
|
fprodclf.a | |- ( ph -> A e. Fin ) |
||
fprodclf.b | |- ( ( ph /\ k e. A ) -> B e. CC ) |
||
Assertion | fprodclf | |- ( ph -> prod_ k e. A B e. CC ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fprodclf.kph | |- F/ k ph |
|
2 | fprodclf.a | |- ( ph -> A e. Fin ) |
|
3 | fprodclf.b | |- ( ( ph /\ k e. A ) -> B e. CC ) |
|
4 | ssidd | |- ( ph -> CC C_ CC ) |
|
5 | mulcl | |- ( ( x e. CC /\ y e. CC ) -> ( x x. y ) e. CC ) |
|
6 | 5 | adantl | |- ( ( ph /\ ( x e. CC /\ y e. CC ) ) -> ( x x. y ) e. CC ) |
7 | 1cnd | |- ( ph -> 1 e. CC ) |
|
8 | 1 4 6 2 3 7 | fprodcllemf | |- ( ph -> prod_ k e. A B e. CC ) |