Theorem climdivf

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

	Ref	Expression
Hypotheses	climdivf.1	⊢ Ⅎ 𝑘 𝜑
	climdivf.2	⊢ Ⅎ 𝑘 𝐹
	climdivf.3	⊢ Ⅎ 𝑘 𝐺
	climdivf.4	⊢ Ⅎ 𝑘 𝐻
	climdivf.5	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	climdivf.6	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	climdivf.7	⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
	climdivf.8	⊢ ( 𝜑 → 𝐻 ∈ 𝑋 )
	climdivf.9	⊢ ( 𝜑 → 𝐺 ⇝ 𝐵 )
	climdivf.10	⊢ ( 𝜑 → 𝐵 ≠ 0 )
	climdivf.11	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
	climdivf.12	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ( ℂ ∖ { 0 } ) )
	climdivf.13	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) / ( 𝐺 ‘ 𝑘 ) ) )
Assertion	climdivf	⊢ ( 𝜑 → 𝐻 ⇝ ( 𝐴 / 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		climdivf.1	⊢ Ⅎ 𝑘 𝜑
2		climdivf.2	⊢ Ⅎ 𝑘 𝐹
3		climdivf.3	⊢ Ⅎ 𝑘 𝐺
4		climdivf.4	⊢ Ⅎ 𝑘 𝐻
5		climdivf.5	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
6		climdivf.6	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
7		climdivf.7	⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
8		climdivf.8	⊢ ( 𝜑 → 𝐻 ∈ 𝑋 )
9		climdivf.9	⊢ ( 𝜑 → 𝐺 ⇝ 𝐵 )
10		climdivf.10	⊢ ( 𝜑 → 𝐵 ≠ 0 )
11		climdivf.11	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
12		climdivf.12	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ( ℂ ∖ { 0 } ) )
13		climdivf.13	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) / ( 𝐺 ‘ 𝑘 ) ) )
14		nfmpt1	⊢ Ⅎ 𝑘 ( 𝑘 ∈ 𝑍 ↦ ( 1 / ( 𝐺 ‘ 𝑘 ) ) )
15		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ 𝑍 )
16	12	eldifad	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
17		eldifsni	⊢ ( ( 𝐺 ‘ 𝑘 ) ∈ ( ℂ ∖ { 0 } ) → ( 𝐺 ‘ 𝑘 ) ≠ 0 )
18	12 17	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ≠ 0 )
19	16 18	reccld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 1 / ( 𝐺 ‘ 𝑘 ) ) ∈ ℂ )
20		eqid	⊢ ( 𝑘 ∈ 𝑍 ↦ ( 1 / ( 𝐺 ‘ 𝑘 ) ) ) = ( 𝑘 ∈ 𝑍 ↦ ( 1 / ( 𝐺 ‘ 𝑘 ) ) )
21	20	fvmpt2	⊢ ( ( 𝑘 ∈ 𝑍 ∧ ( 1 / ( 𝐺 ‘ 𝑘 ) ) ∈ ℂ ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 1 / ( 𝐺 ‘ 𝑘 ) ) ) ‘ 𝑘 ) = ( 1 / ( 𝐺 ‘ 𝑘 ) ) )
22	15 19 21	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 1 / ( 𝐺 ‘ 𝑘 ) ) ) ‘ 𝑘 ) = ( 1 / ( 𝐺 ‘ 𝑘 ) ) )
23	5	fvexi	⊢ 𝑍 ∈ V
24	23	mptex	⊢ ( 𝑘 ∈ 𝑍 ↦ ( 1 / ( 𝐺 ‘ 𝑘 ) ) ) ∈ V
25	24	a1i	⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 1 / ( 𝐺 ‘ 𝑘 ) ) ) ∈ V )
26	1 3 14 5 6 9 10 12 22 25	climrecf	⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 1 / ( 𝐺 ‘ 𝑘 ) ) ) ⇝ ( 1 / 𝐵 ) )
27	22 19	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 1 / ( 𝐺 ‘ 𝑘 ) ) ) ‘ 𝑘 ) ∈ ℂ )
28	11 16 18	divrecd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑘 ) / ( 𝐺 ‘ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑘 ) · ( 1 / ( 𝐺 ‘ 𝑘 ) ) ) )
29	22	eqcomd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 1 / ( 𝐺 ‘ 𝑘 ) ) = ( ( 𝑘 ∈ 𝑍 ↦ ( 1 / ( 𝐺 ‘ 𝑘 ) ) ) ‘ 𝑘 ) )
30	29	oveq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑘 ) · ( 1 / ( 𝐺 ‘ 𝑘 ) ) ) = ( ( 𝐹 ‘ 𝑘 ) · ( ( 𝑘 ∈ 𝑍 ↦ ( 1 / ( 𝐺 ‘ 𝑘 ) ) ) ‘ 𝑘 ) ) )
31	13 28 30	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) · ( ( 𝑘 ∈ 𝑍 ↦ ( 1 / ( 𝐺 ‘ 𝑘 ) ) ) ‘ 𝑘 ) ) )
32	1 2 14 4 5 6 7 8 26 11 27 31	climmulf	⊢ ( 𝜑 → 𝐻 ⇝ ( 𝐴 · ( 1 / 𝐵 ) ) )
33		climcl	⊢ ( 𝐹 ⇝ 𝐴 → 𝐴 ∈ ℂ )
34	7 33	syl	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
35		climcl	⊢ ( 𝐺 ⇝ 𝐵 → 𝐵 ∈ ℂ )
36	9 35	syl	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
37	34 36 10	divrecd	⊢ ( 𝜑 → ( 𝐴 / 𝐵 ) = ( 𝐴 · ( 1 / 𝐵 ) ) )
38	32 37	breqtrrd	⊢ ( 𝜑 → 𝐻 ⇝ ( 𝐴 / 𝐵 ) )