Metamath Proof Explorer

Theorem climdivf

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

Ref Expression
Hypotheses climdivf.1 ⊢Ⅎkφ
climdivf.2 ⊢Ⅎ_kF
climdivf.3 ⊢Ⅎ_kG
climdivf.4 ⊢Ⅎ_kH
climdivf.5 ⊢Z=ℤ≥M
climdivf.6 ⊢φ→M∈ℤ
climdivf.7 ⊢φ→F⇝A
climdivf.8 ⊢φ→H∈X
climdivf.9 ⊢φ→G⇝B
climdivf.10 ⊢φ→B≠0
climdivf.11 ⊢φ∧k∈Z→F⁡k∈ℂ
climdivf.12 ⊢φ∧k∈Z→G⁡k∈ℂ∖0
climdivf.13 ⊢φ∧k∈Z→H⁡k=F⁡kG⁡k
Assertion climdivf ⊢φ→H⇝AB

Proof

Step Hyp Ref Expression
1 climdivf.1 ⊢Ⅎkφ
2 climdivf.2 ⊢Ⅎ_kF
3 climdivf.3 ⊢Ⅎ_kG
4 climdivf.4 ⊢Ⅎ_kH
5 climdivf.5 ⊢Z=ℤ≥M
6 climdivf.6 ⊢φ→M∈ℤ
7 climdivf.7 ⊢φ→F⇝A
8 climdivf.8 ⊢φ→H∈X
9 climdivf.9 ⊢φ→G⇝B
10 climdivf.10 ⊢φ→B≠0
11 climdivf.11 ⊢φ∧k∈Z→F⁡k∈ℂ
12 climdivf.12 ⊢φ∧k∈Z→G⁡k∈ℂ∖0
13 climdivf.13 ⊢φ∧k∈Z→H⁡k=F⁡kG⁡k
14 nfmpt1 ⊢Ⅎ_kk∈Z⟼1G⁡k
15 simpr ⊢φ∧k∈Z→k∈Z
16 12 eldifad ⊢φ∧k∈Z→G⁡k∈ℂ
17 eldifsni ⊢G⁡k∈ℂ∖0→G⁡k≠0
18 12 17 syl ⊢φ∧k∈Z→G⁡k≠0
19 16 18 reccld ⊢φ∧k∈Z→1G⁡k∈ℂ
20 eqid ⊢k∈Z⟼1G⁡k=k∈Z⟼1G⁡k
21 20 fvmpt2 ⊢k∈Z∧1G⁡k∈ℂ→k∈Z⟼1G⁡k⁡k=1G⁡k
22 15 19 21 syl2anc ⊢φ∧k∈Z→k∈Z⟼1G⁡k⁡k=1G⁡k
23 5 fvexi ⊢Z∈V
24 23 mptex ⊢k∈Z⟼1G⁡k∈V
25 24 a1i ⊢φ→k∈Z⟼1G⁡k∈V
26 1 3 14 5 6 9 10 12 22 25 climrecf ⊢φ→k∈Z⟼1G⁡k⇝1B
27 22 19 eqeltrd ⊢φ∧k∈Z→k∈Z⟼1G⁡k⁡k∈ℂ
28 11 16 18 divrecd ⊢φ∧k∈Z→F⁡kG⁡k=F⁡k⁢1G⁡k
29 22 eqcomd ⊢φ∧k∈Z→1G⁡k=k∈Z⟼1G⁡k⁡k
30 29 oveq2d ⊢φ∧k∈Z→F⁡k⁢1G⁡k=F⁡k⁢k∈Z⟼1G⁡k⁡k
31 13 28 30 3eqtrd ⊢φ∧k∈Z→H⁡k=F⁡k⁢k∈Z⟼1G⁡k⁡k
32 1 2 14 4 5 6 7 8 26 11 27 31 climmulf ⊢φ→H⇝A⁢1B
33 climcl ⊢F⇝A→A∈ℂ
34 7 33 syl ⊢φ→A∈ℂ
35 climcl ⊢G⇝B→B∈ℂ
36 9 35 syl ⊢φ→B∈ℂ
37 34 36 10 divrecd ⊢φ→AB=A⁢1B
38 32 37 breqtrrd ⊢φ→H⇝AB