# Metamath Proof Explorer

## Theorem cdivcncf

Description: Division with a constant numerator is continuous. (Contributed by Mario Carneiro, 28-Dec-2016)

Ref Expression
Hypothesis cdivcncf.1 ${⊢}{F}=\left({x}\in \left(ℂ\setminus \left\{0\right\}\right)⟼\frac{{A}}{{x}}\right)$
Assertion cdivcncf ${⊢}{A}\in ℂ\to {F}:\left(ℂ\setminus \left\{0\right\}\right)\underset{cn}{⟶}ℂ$

### Proof

Step Hyp Ref Expression
1 cdivcncf.1 ${⊢}{F}=\left({x}\in \left(ℂ\setminus \left\{0\right\}\right)⟼\frac{{A}}{{x}}\right)$
2 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
3 2 cnfldtopon ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$
4 3 a1i ${⊢}{A}\in ℂ\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$
5 difss ${⊢}ℂ\setminus \left\{0\right\}\subseteq ℂ$
6 resttopon ${⊢}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\wedge ℂ\setminus \left\{0\right\}\subseteq ℂ\right)\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)\in \mathrm{TopOn}\left(ℂ\setminus \left\{0\right\}\right)$
7 4 5 6 sylancl ${⊢}{A}\in ℂ\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)\in \mathrm{TopOn}\left(ℂ\setminus \left\{0\right\}\right)$
8 id ${⊢}{A}\in ℂ\to {A}\in ℂ$
9 7 4 8 cnmptc ${⊢}{A}\in ℂ\to \left({x}\in \left(ℂ\setminus \left\{0\right\}\right)⟼{A}\right)\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
10 7 cnmptid ${⊢}{A}\in ℂ\to \left({x}\in \left(ℂ\setminus \left\{0\right\}\right)⟼{x}\right)\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)\right)\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)\right)\right)$
11 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)$
12 2 11 divcn ${⊢}÷\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
13 12 a1i ${⊢}{A}\in ℂ\to ÷\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
14 7 9 10 13 cnmpt12f ${⊢}{A}\in ℂ\to \left({x}\in \left(ℂ\setminus \left\{0\right\}\right)⟼\frac{{A}}{{x}}\right)\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
15 ssid ${⊢}ℂ\subseteq ℂ$
16 3 toponrestid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℂ$
17 2 11 16 cncfcn
18 5 15 17 mp2an
19 14 1 18 3eltr4g ${⊢}{A}\in ℂ\to {F}:\left(ℂ\setminus \left\{0\right\}\right)\underset{cn}{⟶}ℂ$