This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem divcnvshft

Description: Limit of a ratio function. (Contributed by Scott Fenton, 16-Dec-2017)

Ref Expression
Hypotheses divcnvshft.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
divcnvshft.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
divcnvshft.3 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
divcnvshft.4 ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
divcnvshft.5 ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
divcnvshft.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐴 / ( 𝑘 + 𝐵 ) ) )
Assertion divcnvshft ( 𝜑 → 𝐹 ⇝ 0 )

Proof

Step Hyp Ref Expression
1 divcnvshft.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 divcnvshft.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 divcnvshft.3 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
4 divcnvshft.4 ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
5 divcnvshft.5 ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
6 divcnvshft.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐴 / ( 𝑘 + 𝐵 ) ) )
7 divcnv ⊢ ( 𝐴 ∈ ℂ → ( 𝑚 ∈ ℕ ↦ ( 𝐴 / 𝑚 ) ) ⇝ 0 )
8 3 7 syl ⊢ ( 𝜑 → ( 𝑚 ∈ ℕ ↦ ( 𝐴 / 𝑚 ) ) ⇝ 0 )
9 nnssz ⊢ ℕ ⊆ ℤ
10 resmpt ⊢ ( ℕ ⊆ ℤ → ( ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ↾ ℕ ) = ( 𝑚 ∈ ℕ ↦ ( 𝐴 / 𝑚 ) ) )
11 9 10 ax-mp ⊢ ( ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ↾ ℕ ) = ( 𝑚 ∈ ℕ ↦ ( 𝐴 / 𝑚 ) )
12 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
13 12 reseq2i ⊢ ( ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ↾ ℕ ) = ( ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ↾ ( ℤ≥ ‘ 1 ) )
14 11 13 eqtr3i ⊢ ( 𝑚 ∈ ℕ ↦ ( 𝐴 / 𝑚 ) ) = ( ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ↾ ( ℤ≥ ‘ 1 ) )
15 14 breq1i ⊢ ( ( 𝑚 ∈ ℕ ↦ ( 𝐴 / 𝑚 ) ) ⇝ 0 ↔ ( ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ↾ ( ℤ≥ ‘ 1 ) ) ⇝ 0 )
16 1z ⊢ 1 ∈ ℤ
17 zex ⊢ ℤ ∈ V
18 17 mptex ⊢ ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ∈ V
19 climres ⊢ ( ( 1 ∈ ℤ ∧ ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ∈ V ) → ( ( ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ↾ ( ℤ≥ ‘ 1 ) ) ⇝ 0 ↔ ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ⇝ 0 ) )
20 16 18 19 mp2an ⊢ ( ( ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ↾ ( ℤ≥ ‘ 1 ) ) ⇝ 0 ↔ ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ⇝ 0 )
21 15 20 bitri ⊢ ( ( 𝑚 ∈ ℕ ↦ ( 𝐴 / 𝑚 ) ) ⇝ 0 ↔ ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ⇝ 0 )
22 8 21 sylib ⊢ ( 𝜑 → ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ⇝ 0 )
23 18 a1i ⊢ ( 𝜑 → ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ∈ V )
24 uzssz ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
25 1 24 eqsstri ⊢ 𝑍 ⊆ ℤ
26 25 sseli ⊢ ( 𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ )
27 26 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ ℤ )
28 4 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℤ )
29 27 28 zaddcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑘 + 𝐵 ) ∈ ℤ )
30 oveq2 ⊢ ( 𝑚 = ( 𝑘 + 𝐵 ) → ( 𝐴 / 𝑚 ) = ( 𝐴 / ( 𝑘 + 𝐵 ) ) )
31 eqid ⊢ ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) = ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) )
32 ovex ⊢ ( 𝐴 / ( 𝑘 + 𝐵 ) ) ∈ V
33 30 31 32 fvmpt ⊢ ( ( 𝑘 + 𝐵 ) ∈ ℤ → ( ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ‘ ( 𝑘 + 𝐵 ) ) = ( 𝐴 / ( 𝑘 + 𝐵 ) ) )
34 29 33 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ‘ ( 𝑘 + 𝐵 ) ) = ( 𝐴 / ( 𝑘 + 𝐵 ) ) )
35 34 6 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ‘ ( 𝑘 + 𝐵 ) ) = ( 𝐹 ‘ 𝑘 ) )
36 1 2 4 5 23 35 climshft2 ⊢ ( 𝜑 → ( 𝐹 ⇝ 0 ↔ ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ⇝ 0 ) )
37 22 36 mpbird ⊢ ( 𝜑 → 𝐹 ⇝ 0 )