Theorem divlimc

Description: Limit of the quotient of two functions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	divlimc.f	$$⊢F=\left(x\in A⟼B\right)$$
	divlimc.g	$$⊢G=\left(x\in A⟼C\right)$$
	divlimc.h	$$⊢H=\left(x\in A⟼\frac{B}{C}\right)$$
	divlimc.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℂ$$
	divlimc.c	$$⊢\left(\phi \wedge x\in A\right)\to C\in \left(ℂ\setminus \left\{0\right\}\right)$$
	divlimc.x	$$⊢\phi \to X\in \left(F{lim}_{ℂ}D\right)$$
	divlimc.y	$$⊢\phi \to Y\in \left(G{lim}_{ℂ}D\right)$$
	divlimc.yne0	$$⊢\phi \to Y\ne 0$$
	divlimc.cne0	$$⊢\left(\phi \wedge x\in A\right)\to C\ne 0$$
Assertion	divlimc	$$⊢\phi \to \frac{X}{Y}\in \left(H{lim}_{ℂ}D\right)$$

Proof

Step	Hyp	Ref	Expression
1		divlimc.f	$$⊢F=\left(x\in A⟼B\right)$$
2		divlimc.g	$$⊢G=\left(x\in A⟼C\right)$$
3		divlimc.h	$$⊢H=\left(x\in A⟼\frac{B}{C}\right)$$
4		divlimc.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℂ$$
5		divlimc.c	$$⊢\left(\phi \wedge x\in A\right)\to C\in \left(ℂ\setminus \left\{0\right\}\right)$$
6		divlimc.x	$$⊢\phi \to X\in \left(F{lim}_{ℂ}D\right)$$
7		divlimc.y	$$⊢\phi \to Y\in \left(G{lim}_{ℂ}D\right)$$
8		divlimc.yne0	$$⊢\phi \to Y\ne 0$$
9		divlimc.cne0	$$⊢\left(\phi \wedge x\in A\right)\to C\ne 0$$
10		eqid	$$⊢\left(x\in A⟼\frac{1}{C}\right)=\left(x\in A⟼\frac{1}{C}\right)$$
11		eqid	$$⊢\left(x\in A⟼B\left(\frac{1}{C}\right)\right)=\left(x\in A⟼B\left(\frac{1}{C}\right)\right)$$
12	5	eldifad	$$⊢\left(\phi \wedge x\in A\right)\to C\in ℂ$$
13	12 9	reccld	$$⊢\left(\phi \wedge x\in A\right)\to \frac{1}{C}\in ℂ$$
14	2 10 5 7 8	reclimc	$$⊢\phi \to \frac{1}{Y}\in \left(\left(x\in A⟼\frac{1}{C}\right){lim}_{ℂ}D\right)$$
15	1 10 11 4 13 6 14	mullimc	$$⊢\phi \to X\left(\frac{1}{Y}\right)\in \left(\left(x\in A⟼B\left(\frac{1}{C}\right)\right){lim}_{ℂ}D\right)$$
16		limccl	$$⊢F{lim}_{ℂ}D\subseteq ℂ$$
17	16 6	sselid	$$⊢\phi \to X\in ℂ$$
18		limccl	$$⊢G{lim}_{ℂ}D\subseteq ℂ$$
19	18 7	sselid	$$⊢\phi \to Y\in ℂ$$
20	17 19 8	divrecd	$$⊢\phi \to \frac{X}{Y}=X\left(\frac{1}{Y}\right)$$
21	4 12 9	divrecd	$$⊢\left(\phi \wedge x\in A\right)\to \frac{B}{C}=B\left(\frac{1}{C}\right)$$
22	21	mpteq2dva	$$⊢\phi \to \left(x\in A⟼\frac{B}{C}\right)=\left(x\in A⟼B\left(\frac{1}{C}\right)\right)$$
23	3 22	eqtrid	$$⊢\phi \to H=\left(x\in A⟼B\left(\frac{1}{C}\right)\right)$$
24	23	oveq1d	$$⊢\phi \to H{lim}_{ℂ}D=\left(x\in A⟼B\left(\frac{1}{C}\right)\right){lim}_{ℂ}D$$
25	15 20 24	3eltr4d	$$⊢\phi \to \frac{X}{Y}\in \left(H{lim}_{ℂ}D\right)$$