Theorem divcncff

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

	Ref	Expression
Hypotheses	divcncff.f	$$⊢\phi \to F:X\underset{cn}{⟶}ℂ$$
	divcncff.g	$$⊢\phi \to G:X\underset{cn}{⟶}\left(ℂ\setminus \left\{0\right\}\right)$$
Assertion	divcncff	$$⊢\phi \to \left(F{÷}_{f}G\right):X\underset{cn}{⟶}ℂ$$

Proof

Step	Hyp	Ref	Expression
1		divcncff.f	$$⊢\phi \to F:X\underset{cn}{⟶}ℂ$$
2		divcncff.g	$$⊢\phi \to G:X\underset{cn}{⟶}\left(ℂ\setminus \left\{0\right\}\right)$$
3		cncfrss	$$⊢F:X\underset{cn}{⟶}ℂ\to X\subseteq ℂ$$
4		cnex	$$⊢ℂ\in \mathrm{V}$$
5	4	ssex	$$⊢X\subseteq ℂ\to X\in \mathrm{V}$$
6	1 3 5	3syl	$$⊢\phi \to X\in \mathrm{V}$$
7		cncff	$$⊢F:X\underset{cn}{⟶}ℂ\to F:X⟶ℂ$$
8	1 7	syl	$$⊢\phi \to F:X⟶ℂ$$
9	8	ffvelrnda	$$⊢\left(\phi \wedge x\in X\right)\to F\left(x\right)\in ℂ$$
10		cncff	$$⊢G:X\underset{cn}{⟶}\left(ℂ\setminus \left\{0\right\}\right)\to G:X⟶ℂ\setminus \left\{0\right\}$$
11	2 10	syl	$$⊢\phi \to G:X⟶ℂ\setminus \left\{0\right\}$$
12	11	ffvelrnda	$$⊢\left(\phi \wedge x\in X\right)\to G\left(x\right)\in \left(ℂ\setminus \left\{0\right\}\right)$$
13	8	feqmptd	$$⊢\phi \to F=\left(x\in X⟼F\left(x\right)\right)$$
14	11	feqmptd	$$⊢\phi \to G=\left(x\in X⟼G\left(x\right)\right)$$
15	6 9 12 13 14	offval2	$$⊢\phi \to F{÷}_{f}G=\left(x\in X⟼\frac{F\left(x\right)}{G\left(x\right)}\right)$$
16	13 1	eqeltrrd	$$⊢\phi \to \left(x\in X⟼F\left(x\right)\right):X\underset{cn}{⟶}ℂ$$
17	14 2	eqeltrrd	$$⊢\phi \to \left(x\in X⟼G\left(x\right)\right):X\underset{cn}{⟶}\left(ℂ\setminus \left\{0\right\}\right)$$
18	16 17	divcncf	$$⊢\phi \to \left(x\in X⟼\frac{F\left(x\right)}{G\left(x\right)}\right):X\underset{cn}{⟶}ℂ$$
19	15 18	eqeltrd	$$⊢\phi \to \left(F{÷}_{f}G\right):X\underset{cn}{⟶}ℂ$$