Theorem divcncf

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

	Ref	Expression
Hypotheses	divcncf.1	$$⊢\phi \to \left(x\in X⟼A\right):X\underset{cn}{⟶}ℂ$$
	divcncf.2	$$⊢\phi \to \left(x\in X⟼B\right):X\underset{cn}{⟶}\left(ℂ\setminus \left\{0\right\}\right)$$
Assertion	divcncf	$$⊢\phi \to \left(x\in X⟼\frac{A}{B}\right):X\underset{cn}{⟶}ℂ$$

Proof

Step	Hyp	Ref	Expression
1		divcncf.1	$$⊢\phi \to \left(x\in X⟼A\right):X\underset{cn}{⟶}ℂ$$
2		divcncf.2	$$⊢\phi \to \left(x\in X⟼B\right):X\underset{cn}{⟶}\left(ℂ\setminus \left\{0\right\}\right)$$
3		cncff	$$⊢\left(x\in X⟼A\right):X\underset{cn}{⟶}ℂ\to \left(x\in X⟼A\right):X⟶ℂ$$
4	1 3	syl	$$⊢\phi \to \left(x\in X⟼A\right):X⟶ℂ$$
5	4	fvmptelcdm	$$⊢\left(\phi \wedge x\in X\right)\to A\in ℂ$$
6		cncff	$$⊢\left(x\in X⟼B\right):X\underset{cn}{⟶}\left(ℂ\setminus \left\{0\right\}\right)\to \left(x\in X⟼B\right):X⟶ℂ\setminus \left\{0\right\}$$
7	2 6	syl	$$⊢\phi \to \left(x\in X⟼B\right):X⟶ℂ\setminus \left\{0\right\}$$
8	7	fvmptelcdm	$$⊢\left(\phi \wedge x\in X\right)\to B\in \left(ℂ\setminus \left\{0\right\}\right)$$
9	8	eldifad	$$⊢\left(\phi \wedge x\in X\right)\to B\in ℂ$$
10		eldifsni	$$⊢B\in \left(ℂ\setminus \left\{0\right\}\right)\to B\ne 0$$
11	8 10	syl	$$⊢\left(\phi \wedge x\in X\right)\to B\ne 0$$
12	5 9 11	divrecd	$$⊢\left(\phi \wedge x\in X\right)\to \frac{A}{B}=A\left(\frac{1}{B}\right)$$
13	12	mpteq2dva	$$⊢\phi \to \left(x\in X⟼\frac{A}{B}\right)=\left(x\in X⟼A\left(\frac{1}{B}\right)\right)$$
14	8	ralrimiva	$$⊢\phi \to \forall x\in XB\in \left(ℂ\setminus \left\{0\right\}\right)$$
15		eqidd	$$⊢\phi \to \left(x\in X⟼B\right)=\left(x\in X⟼B\right)$$
16		eqidd	$$⊢\phi \to \left(y\in \left(ℂ\setminus \left\{0\right\}\right)⟼\frac{1}{y}\right)=\left(y\in \left(ℂ\setminus \left\{0\right\}\right)⟼\frac{1}{y}\right)$$
17	14 15 16	fmptcos	$$⊢\phi \to \left(y\in \left(ℂ\setminus \left\{0\right\}\right)⟼\frac{1}{y}\right)\circ \left(x\in X⟼B\right)=\left(x\in X⟼⦋B/y⦌\left(\frac{1}{y}\right)\right)$$
18		csbov2g	$$⊢B\in ℂ\to ⦋B/y⦌\left(\frac{1}{y}\right)=\frac{1}{⦋B/y⦌y}$$
19	9 18	syl	$$⊢\left(\phi \wedge x\in X\right)\to ⦋B/y⦌\left(\frac{1}{y}\right)=\frac{1}{⦋B/y⦌y}$$
20		csbvarg	$$⊢B\in ℂ\to ⦋B/y⦌y=B$$
21	9 20	syl	$$⊢\left(\phi \wedge x\in X\right)\to ⦋B/y⦌y=B$$
22	21	oveq2d	$$⊢\left(\phi \wedge x\in X\right)\to \frac{1}{⦋B/y⦌y}=\frac{1}{B}$$
23	19 22	eqtrd	$$⊢\left(\phi \wedge x\in X\right)\to ⦋B/y⦌\left(\frac{1}{y}\right)=\frac{1}{B}$$
24	23	mpteq2dva	$$⊢\phi \to \left(x\in X⟼⦋B/y⦌\left(\frac{1}{y}\right)\right)=\left(x\in X⟼\frac{1}{B}\right)$$
25	17 24	eqtr2d	$$⊢\phi \to \left(x\in X⟼\frac{1}{B}\right)=\left(y\in \left(ℂ\setminus \left\{0\right\}\right)⟼\frac{1}{y}\right)\circ \left(x\in X⟼B\right)$$
26		ax-1cn	$$⊢1\in ℂ$$
27		eqid	$$⊢\left(y\in \left(ℂ\setminus \left\{0\right\}\right)⟼\frac{1}{y}\right)=\left(y\in \left(ℂ\setminus \left\{0\right\}\right)⟼\frac{1}{y}\right)$$
28	27	cdivcncf	$$⊢1\in ℂ\to \left(y\in \left(ℂ\setminus \left\{0\right\}\right)⟼\frac{1}{y}\right):\left(ℂ\setminus \left\{0\right\}\right)\underset{cn}{⟶}ℂ$$
29	26 28	mp1i	$$⊢\phi \to \left(y\in \left(ℂ\setminus \left\{0\right\}\right)⟼\frac{1}{y}\right):\left(ℂ\setminus \left\{0\right\}\right)\underset{cn}{⟶}ℂ$$
30	2 29	cncfco	$$⊢\phi \to \left(\left(y\in \left(ℂ\setminus \left\{0\right\}\right)⟼\frac{1}{y}\right)\circ \left(x\in X⟼B\right)\right):X\underset{cn}{⟶}ℂ$$
31	25 30	eqeltrd	$$⊢\phi \to \left(x\in X⟼\frac{1}{B}\right):X\underset{cn}{⟶}ℂ$$
32	1 31	mulcncf	$$⊢\phi \to \left(x\in X⟼A\left(\frac{1}{B}\right)\right):X\underset{cn}{⟶}ℂ$$
33	13 32	eqeltrd	$$⊢\phi \to \left(x\in X⟼\frac{A}{B}\right):X\underset{cn}{⟶}ℂ$$