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