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){\upharpoonright }_{𝑡}\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){\upharpoonright }_{𝑡}\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){\upharpoonright }_{𝑡}\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){\upharpoonright }_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)\right)\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)\right)\right)$$
11		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)$$
12	2 11	divcn	$$⊢÷\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\times }_t\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}\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){\times }_t\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}\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){\upharpoonright }_{𝑡}\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){\upharpoonright }_{𝑡}ℂ$$
17	2 11 16	cncfcn	$$⊢\left(ℂ\setminus \left\{0\right\}\subseteq ℂ\wedge ℂ\subseteq ℂ\right)\to \left(ℂ\setminus \left\{0\right\}\right)\underset{cn}{⟶}ℂ=\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
18	5 15 17	mp2an	$$⊢\left(ℂ\setminus \left\{0\right\}\right)\underset{cn}{⟶}ℂ=\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}\left(ℂ\setminus \left\{0\right\}\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
19	14 1 18	3eltr4g	$$⊢A\in ℂ\to F:\left(ℂ\setminus \left\{0\right\}\right)\underset{cn}{⟶}ℂ$$