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 ⊢ Ⅎ 𝑘 𝜑
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 ⊢ ( 𝜑 → 𝐻 ⇝ ( 𝐴 / 𝐵 ) )