Description: The quotient of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | divcncf.1 | |
|
divcncf.2 | |
||
Assertion | divcncf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | divcncf.1 | |
|
2 | divcncf.2 | |
|
3 | cncff | |
|
4 | 1 3 | syl | |
5 | 4 | fvmptelrn | |
6 | cncff | |
|
7 | 2 6 | syl | |
8 | 7 | fvmptelrn | |
9 | 8 | eldifad | |
10 | eldifsni | |
|
11 | 8 10 | syl | |
12 | 5 9 11 | divrecd | |
13 | 12 | mpteq2dva | |
14 | 8 | ralrimiva | |
15 | eqidd | |
|
16 | eqidd | |
|
17 | 14 15 16 | fmptcos | |
18 | csbov2g | |
|
19 | 9 18 | syl | |
20 | csbvarg | |
|
21 | 9 20 | syl | |
22 | 21 | oveq2d | |
23 | 19 22 | eqtrd | |
24 | 23 | mpteq2dva | |
25 | 17 24 | eqtr2d | |
26 | ax-1cn | |
|
27 | eqid | |
|
28 | 27 | cdivcncf | |
29 | 26 28 | mp1i | |
30 | 2 29 | cncfco | |
31 | 25 30 | eqeltrd | |
32 | 1 31 | mulcncf | |
33 | 13 32 | eqeltrd | |