Metamath Proof Explorer

Theorem divcnvshft

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

Ref Expression
Hypotheses divcnvshft.1 ⊢ Z = ℤ ≥ M
divcnvshft.2 ⊢ φ → M ∈ ℤ
divcnvshft.3 ⊢ φ → A ∈ ℂ
divcnvshft.4 ⊢ φ → B ∈ ℤ
divcnvshft.5 ⊢ φ → F ∈ V
divcnvshft.6 ⊢ φ ∧ k ∈ Z → F ⁡ k = A k + B
Assertion divcnvshft ⊢ φ → F ⇝ 0

Proof

Step Hyp Ref Expression
1 divcnvshft.1 ⊢ Z = ℤ ≥ M
2 divcnvshft.2 ⊢ φ → M ∈ ℤ
3 divcnvshft.3 ⊢ φ → A ∈ ℂ
4 divcnvshft.4 ⊢ φ → B ∈ ℤ
5 divcnvshft.5 ⊢ φ → F ∈ V
6 divcnvshft.6 ⊢ φ ∧ k ∈ Z → F ⁡ k = A k + B
7 divcnv ⊢ A ∈ ℂ → m ∈ ℕ ⟼ A m ⇝ 0
8 3 7 syl ⊢ φ → m ∈ ℕ ⟼ A m ⇝ 0
9 nnssz ⊢ ℕ ⊆ ℤ
10 resmpt ⊢ ℕ ⊆ ℤ → m ∈ ℤ ⟼ A m ↾ ℕ = m ∈ ℕ ⟼ A m
11 9 10 ax-mp ⊢ m ∈ ℤ ⟼ A m ↾ ℕ = m ∈ ℕ ⟼ A m
12 nnuz ⊢ ℕ = ℤ ≥ 1
13 12 reseq2i ⊢ m ∈ ℤ ⟼ A m ↾ ℕ = m ∈ ℤ ⟼ A m ↾ ℤ ≥ 1
14 11 13 eqtr3i ⊢ m ∈ ℕ ⟼ A m = m ∈ ℤ ⟼ A m ↾ ℤ ≥ 1
15 14 breq1i ⊢ m ∈ ℕ ⟼ A m ⇝ 0 ↔ m ∈ ℤ ⟼ A m ↾ ℤ ≥ 1 ⇝ 0
16 1z ⊢ 1 ∈ ℤ
17 zex ⊢ ℤ ∈ V
18 17 mptex ⊢ m ∈ ℤ ⟼ A m ∈ V
19 climres ⊢ 1 ∈ ℤ ∧ m ∈ ℤ ⟼ A m ∈ V → m ∈ ℤ ⟼ A m ↾ ℤ ≥ 1 ⇝ 0 ↔ m ∈ ℤ ⟼ A m ⇝ 0
20 16 18 19 mp2an ⊢ m ∈ ℤ ⟼ A m ↾ ℤ ≥ 1 ⇝ 0 ↔ m ∈ ℤ ⟼ A m ⇝ 0
21 15 20 bitri ⊢ m ∈ ℕ ⟼ A m ⇝ 0 ↔ m ∈ ℤ ⟼ A m ⇝ 0
22 8 21 sylib ⊢ φ → m ∈ ℤ ⟼ A m ⇝ 0
23 18 a1i ⊢ φ → m ∈ ℤ ⟼ A m ∈ V
24 uzssz ⊢ ℤ ≥ M ⊆ ℤ
25 1 24 eqsstri ⊢ Z ⊆ ℤ
26 25 sseli ⊢ k ∈ Z → k ∈ ℤ
27 26 adantl ⊢ φ ∧ k ∈ Z → k ∈ ℤ
28 4 adantr ⊢ φ ∧ k ∈ Z → B ∈ ℤ
29 27 28 zaddcld ⊢ φ ∧ k ∈ Z → k + B ∈ ℤ
30 oveq2 ⊢ m = k + B → A m = A k + B
31 eqid ⊢ m ∈ ℤ ⟼ A m = m ∈ ℤ ⟼ A m
32 ovex ⊢ A k + B ∈ V
33 30 31 32 fvmpt ⊢ k + B ∈ ℤ → m ∈ ℤ ⟼ A m ⁡ k + B = A k + B
34 29 33 syl ⊢ φ ∧ k ∈ Z → m ∈ ℤ ⟼ A m ⁡ k + B = A k + B
35 34 6 eqtr4d ⊢ φ ∧ k ∈ Z → m ∈ ℤ ⟼ A m ⁡ k + B = F ⁡ k
36 1 2 4 5 23 35 climshft2 ⊢ φ → F ⇝ 0 ↔ m ∈ ℤ ⟼ A m ⇝ 0
37 22 36 mpbird ⊢ φ → F ⇝ 0