Metamath Proof Explorer


Theorem mulcncff

Description: The multiplication of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses mulcncff.f φ F : X cn
mulcncff.g φ G : X cn
Assertion mulcncff φ F × f G : X cn

Proof

Step Hyp Ref Expression
1 mulcncff.f φ F : X cn
2 mulcncff.g φ G : X cn
3 cncfrss F : X cn X
4 cnex V
5 4 ssex X X V
6 1 3 5 3syl φ X V
7 cncff F : X cn F : X
8 1 7 syl φ F : X
9 8 ffvelrnda φ x X F x
10 cncff G : X cn G : X
11 2 10 syl φ G : X
12 11 ffvelrnda φ x X G x
13 8 feqmptd φ F = x X F x
14 11 feqmptd φ G = x X G x
15 6 9 12 13 14 offval2 φ F × f G = x X F x G x
16 13 1 eqeltrrd φ x X F x : X cn
17 14 2 eqeltrrd φ x X G x : X cn
18 16 17 mulcncf φ x X F x G x : X cn
19 15 18 eqeltrd φ F × f G : X cn