Metamath Proof Explorer


Theorem divcncf

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

Ref Expression
Hypotheses divcncf.1 φxXA:Xcn
divcncf.2 φxXB:Xcn0
Assertion divcncf φxXAB:Xcn

Proof

Step Hyp Ref Expression
1 divcncf.1 φxXA:Xcn
2 divcncf.2 φxXB:Xcn0
3 cncff xXA:XcnxXA:X
4 1 3 syl φxXA:X
5 4 fvmptelrn φxXA
6 cncff xXB:Xcn0xXB:X0
7 2 6 syl φxXB:X0
8 7 fvmptelrn φxXB0
9 8 eldifad φxXB
10 eldifsni B0B0
11 8 10 syl φxXB0
12 5 9 11 divrecd φxXAB=A1B
13 12 mpteq2dva φxXAB=xXA1B
14 8 ralrimiva φxXB0
15 eqidd φxXB=xXB
16 eqidd φy01y=y01y
17 14 15 16 fmptcos φy01yxXB=xXB/y1y
18 csbov2g BB/y1y=1B/yy
19 9 18 syl φxXB/y1y=1B/yy
20 csbvarg BB/yy=B
21 9 20 syl φxXB/yy=B
22 21 oveq2d φxX1B/yy=1B
23 19 22 eqtrd φxXB/y1y=1B
24 23 mpteq2dva φxXB/y1y=xX1B
25 17 24 eqtr2d φxX1B=y01yxXB
26 ax-1cn 1
27 eqid y01y=y01y
28 27 cdivcncf 1y01y:0cn
29 26 28 mp1i φy01y:0cn
30 2 29 cncfco φy01yxXB:Xcn
31 25 30 eqeltrd φxX1B:Xcn
32 1 31 mulcncf φxXA1B:Xcn
33 13 32 eqeltrd φxXAB:Xcn