Theorem climdivf

Description: Limit of the ratio of two converging sequences. (Contributed by Glauco Siliprandi, 29-Jun-2017)

	Ref	Expression
Hypotheses	climdivf.1	$$⊢Ⅎk\phi$$
	climdivf.2	$$⊢\underset{\_}{Ⅎ}kF$$
	climdivf.3	$$⊢\underset{\_}{Ⅎ}kG$$
	climdivf.4	$$⊢\underset{\_}{Ⅎ}kH$$
	climdivf.5	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	climdivf.6	$$⊢\phi \to M\in \mathbb{Z}$$
	climdivf.7	$$⊢\phi \to F⇝A$$
	climdivf.8	$$⊢\phi \to H\in X$$
	climdivf.9	$$⊢\phi \to G⇝B$$
	climdivf.10	$$⊢\phi \to B\ne 0$$
	climdivf.11	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℂ$$
	climdivf.12	$$⊢\left(\phi \wedge k\in Z\right)\to G\left(k\right)\in \left(ℂ\setminus \left\{0\right\}\right)$$
	climdivf.13	$$⊢\left(\phi \wedge k\in Z\right)\to H\left(k\right)=\frac{F\left(k\right)}{G\left(k\right)}$$
Assertion	climdivf	$$⊢\phi \to H⇝\left(\frac{A}{B}\right)$$

Proof

Step	Hyp	Ref	Expression
1		climdivf.1	$$⊢Ⅎk\phi$$
2		climdivf.2	$$⊢\underset{\_}{Ⅎ}kF$$
3		climdivf.3	$$⊢\underset{\_}{Ⅎ}kG$$
4		climdivf.4	$$⊢\underset{\_}{Ⅎ}kH$$
5		climdivf.5	$$⊢Z={\mathbb{Z}}_{\ge M}$$
6		climdivf.6	$$⊢\phi \to M\in \mathbb{Z}$$
7		climdivf.7	$$⊢\phi \to F⇝A$$
8		climdivf.8	$$⊢\phi \to H\in X$$
9		climdivf.9	$$⊢\phi \to G⇝B$$
10		climdivf.10	$$⊢\phi \to B\ne 0$$
11		climdivf.11	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℂ$$
12		climdivf.12	$$⊢\left(\phi \wedge k\in Z\right)\to G\left(k\right)\in \left(ℂ\setminus \left\{0\right\}\right)$$
13		climdivf.13	$$⊢\left(\phi \wedge k\in Z\right)\to H\left(k\right)=\frac{F\left(k\right)}{G\left(k\right)}$$
14		nfmpt1	$$⊢\underset{\_}{Ⅎ}k\left(k\in Z⟼\frac{1}{G\left(k\right)}\right)$$
15		simpr	$$⊢\left(\phi \wedge k\in Z\right)\to k\in Z$$
16	12	eldifad	$$⊢\left(\phi \wedge k\in Z\right)\to G\left(k\right)\in ℂ$$
17		eldifsni	$$⊢G\left(k\right)\in \left(ℂ\setminus \left\{0\right\}\right)\to G\left(k\right)\ne 0$$
18	12 17	syl	$$⊢\left(\phi \wedge k\in Z\right)\to G\left(k\right)\ne 0$$
19	16 18	reccld	$$⊢\left(\phi \wedge k\in Z\right)\to \frac{1}{G\left(k\right)}\in ℂ$$
20		eqid	$$⊢\left(k\in Z⟼\frac{1}{G\left(k\right)}\right)=\left(k\in Z⟼\frac{1}{G\left(k\right)}\right)$$
21	20	fvmpt2	$$⊢\left(k\in Z\wedge \frac{1}{G\left(k\right)}\in ℂ\right)\to \left(k\in Z⟼\frac{1}{G\left(k\right)}\right)\left(k\right)=\frac{1}{G\left(k\right)}$$
22	15 19 21	syl2anc	$$⊢\left(\phi \wedge k\in Z\right)\to \left(k\in Z⟼\frac{1}{G\left(k\right)}\right)\left(k\right)=\frac{1}{G\left(k\right)}$$
23	5	fvexi	$$⊢Z\in \mathrm{V}$$
24	23	mptex	$$⊢\left(k\in Z⟼\frac{1}{G\left(k\right)}\right)\in \mathrm{V}$$
25	24	a1i	$$⊢\phi \to \left(k\in Z⟼\frac{1}{G\left(k\right)}\right)\in \mathrm{V}$$
26	1 3 14 5 6 9 10 12 22 25	climrecf	$$⊢\phi \to \left(k\in Z⟼\frac{1}{G\left(k\right)}\right)⇝\left(\frac{1}{B}\right)$$
27	22 19	eqeltrd	$$⊢\left(\phi \wedge k\in Z\right)\to \left(k\in Z⟼\frac{1}{G\left(k\right)}\right)\left(k\right)\in ℂ$$
28	11 16 18	divrecd	$$⊢\left(\phi \wedge k\in Z\right)\to \frac{F\left(k\right)}{G\left(k\right)}=F\left(k\right)\left(\frac{1}{G\left(k\right)}\right)$$
29	22	eqcomd	$$⊢\left(\phi \wedge k\in Z\right)\to \frac{1}{G\left(k\right)}=\left(k\in Z⟼\frac{1}{G\left(k\right)}\right)\left(k\right)$$
30	29	oveq2d	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\left(\frac{1}{G\left(k\right)}\right)=F\left(k\right)\left(k\in Z⟼\frac{1}{G\left(k\right)}\right)\left(k\right)$$
31	13 28 30	3eqtrd	$$⊢\left(\phi \wedge k\in Z\right)\to H\left(k\right)=F\left(k\right)\left(k\in Z⟼\frac{1}{G\left(k\right)}\right)\left(k\right)$$
32	1 2 14 4 5 6 7 8 26 11 27 31	climmulf	$$⊢\phi \to H⇝A\left(\frac{1}{B}\right)$$
33		climcl	$$⊢F⇝A\to A\in ℂ$$
34	7 33	syl	$$⊢\phi \to A\in ℂ$$
35		climcl	$$⊢G⇝B\to B\in ℂ$$
36	9 35	syl	$$⊢\phi \to B\in ℂ$$
37	34 36 10	divrecd	$$⊢\phi \to \frac{A}{B}=A\left(\frac{1}{B}\right)$$
38	32 37	breqtrrd	$$⊢\phi \to H⇝\left(\frac{A}{B}\right)$$