Metamath Proof Explorer

Theorem divcnvlin

Description: Limit of the ratio of two linear functions. (Contributed by Scott Fenton, 17-Dec-2017)

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

Proof

Step Hyp Ref Expression
1 divcnvlin.1 ⊢ Z = ℤ ≥ M
2 divcnvlin.2 ⊢ φ → M ∈ ℤ
3 divcnvlin.3 ⊢ φ → A ∈ ℂ
4 divcnvlin.4 ⊢ φ → B ∈ ℤ
5 divcnvlin.5 ⊢ φ → F ∈ V
6 divcnvlin.6 ⊢ φ ∧ k ∈ Z → F ⁡ k = k + A k + B
7 nncn ⊢ m ∈ ℕ → m ∈ ℂ
8 7 adantl ⊢ φ ∧ m ∈ ℕ → m ∈ ℂ
9 4 zcnd ⊢ φ → B ∈ ℂ
10 3 9 subcld ⊢ φ → A − B ∈ ℂ
11 10 adantr ⊢ φ ∧ m ∈ ℕ → A − B ∈ ℂ
12 nnne0 ⊢ m ∈ ℕ → m ≠ 0
13 12 adantl ⊢ φ ∧ m ∈ ℕ → m ≠ 0
14 8 11 8 13 divdird ⊢ φ ∧ m ∈ ℕ → m + A - B m = m m + A − B m
15 8 13 dividd ⊢ φ ∧ m ∈ ℕ → m m = 1
16 15 oveq1d ⊢ φ ∧ m ∈ ℕ → m m + A − B m = 1 + A − B m
17 14 16 eqtrd ⊢ φ ∧ m ∈ ℕ → m + A - B m = 1 + A − B m
18 17 mpteq2dva ⊢ φ → m ∈ ℕ ⟼ m + A - B m = m ∈ ℕ ⟼ 1 + A − B m
19 nnuz ⊢ ℕ = ℤ ≥ 1
20 1zzd ⊢ φ → 1 ∈ ℤ
21 divcnv ⊢ A − B ∈ ℂ → m ∈ ℕ ⟼ A − B m ⇝ 0
22 10 21 syl ⊢ φ → m ∈ ℕ ⟼ A − B m ⇝ 0
23 1cnd ⊢ φ → 1 ∈ ℂ
24 nnex ⊢ ℕ ∈ V
25 24 mptex ⊢ m ∈ ℕ ⟼ 1 + A − B m ∈ V
26 25 a1i ⊢ φ → m ∈ ℕ ⟼ 1 + A − B m ∈ V
27 11 8 13 divcld ⊢ φ ∧ m ∈ ℕ → A − B m ∈ ℂ
28 27 fmpttd ⊢ φ → m ∈ ℕ ⟼ A − B m : ℕ ⟶ ℂ
29 28 ffvelcdmda ⊢ φ ∧ k ∈ ℕ → m ∈ ℕ ⟼ A − B m ⁡ k ∈ ℂ
30 oveq2 ⊢ m = k → A − B m = A − B k
31 30 oveq2d ⊢ m = k → 1 + A − B m = 1 + A − B k
32 eqid ⊢ m ∈ ℕ ⟼ 1 + A − B m = m ∈ ℕ ⟼ 1 + A − B m
33 ovex ⊢ 1 + A − B k ∈ V
34 31 32 33 fvmpt ⊢ k ∈ ℕ → m ∈ ℕ ⟼ 1 + A − B m ⁡ k = 1 + A − B k
35 eqid ⊢ m ∈ ℕ ⟼ A − B m = m ∈ ℕ ⟼ A − B m
36 ovex ⊢ A − B k ∈ V
37 30 35 36 fvmpt ⊢ k ∈ ℕ → m ∈ ℕ ⟼ A − B m ⁡ k = A − B k
38 37 oveq2d ⊢ k ∈ ℕ → 1 + m ∈ ℕ ⟼ A − B m ⁡ k = 1 + A − B k
39 34 38 eqtr4d ⊢ k ∈ ℕ → m ∈ ℕ ⟼ 1 + A − B m ⁡ k = 1 + m ∈ ℕ ⟼ A − B m ⁡ k
40 39 adantl ⊢ φ ∧ k ∈ ℕ → m ∈ ℕ ⟼ 1 + A − B m ⁡ k = 1 + m ∈ ℕ ⟼ A − B m ⁡ k
41 19 20 22 23 26 29 40 climaddc2 ⊢ φ → m ∈ ℕ ⟼ 1 + A − B m ⇝ 1 + 0
42 18 41 eqbrtrd ⊢ φ → m ∈ ℕ ⟼ m + A - B m ⇝ 1 + 0
43 nnssz ⊢ ℕ ⊆ ℤ
44 resmpt ⊢ ℕ ⊆ ℤ → m ∈ ℤ ⟼ m + A - B m ↾ ℕ = m ∈ ℕ ⟼ m + A - B m
45 43 44 ax-mp ⊢ m ∈ ℤ ⟼ m + A - B m ↾ ℕ = m ∈ ℕ ⟼ m + A - B m
46 19 reseq2i ⊢ m ∈ ℤ ⟼ m + A - B m ↾ ℕ = m ∈ ℤ ⟼ m + A - B m ↾ ℤ ≥ 1
47 45 46 eqtr3i ⊢ m ∈ ℕ ⟼ m + A - B m = m ∈ ℤ ⟼ m + A - B m ↾ ℤ ≥ 1
48 1p0e1 ⊢ 1 + 0 = 1
49 47 48 breq12i ⊢ m ∈ ℕ ⟼ m + A - B m ⇝ 1 + 0 ↔ m ∈ ℤ ⟼ m + A - B m ↾ ℤ ≥ 1 ⇝ 1
50 1z ⊢ 1 ∈ ℤ
51 zex ⊢ ℤ ∈ V
52 51 mptex ⊢ m ∈ ℤ ⟼ m + A - B m ∈ V
53 climres ⊢ 1 ∈ ℤ ∧ m ∈ ℤ ⟼ m + A - B m ∈ V → m ∈ ℤ ⟼ m + A - B m ↾ ℤ ≥ 1 ⇝ 1 ↔ m ∈ ℤ ⟼ m + A - B m ⇝ 1
54 50 52 53 mp2an ⊢ m ∈ ℤ ⟼ m + A - B m ↾ ℤ ≥ 1 ⇝ 1 ↔ m ∈ ℤ ⟼ m + A - B m ⇝ 1
55 49 54 bitri ⊢ m ∈ ℕ ⟼ m + A - B m ⇝ 1 + 0 ↔ m ∈ ℤ ⟼ m + A - B m ⇝ 1
56 42 55 sylib ⊢ φ → m ∈ ℤ ⟼ m + A - B m ⇝ 1
57 52 a1i ⊢ φ → m ∈ ℤ ⟼ m + A - B m ∈ V
58 eluzelz ⊢ k ∈ ℤ ≥ M → k ∈ ℤ
59 58 1 eleq2s ⊢ k ∈ Z → k ∈ ℤ
60 59 zcnd ⊢ k ∈ Z → k ∈ ℂ
61 60 adantl ⊢ φ ∧ k ∈ Z → k ∈ ℂ
62 4 adantr ⊢ φ ∧ k ∈ Z → B ∈ ℤ
63 62 zcnd ⊢ φ ∧ k ∈ Z → B ∈ ℂ
64 3 adantr ⊢ φ ∧ k ∈ Z → A ∈ ℂ
65 61 63 64 ppncand ⊢ φ ∧ k ∈ Z → k + B + A − B = k + A
66 65 oveq1d ⊢ φ ∧ k ∈ Z → k + B + A − B k + B = k + A k + B
67 59 adantl ⊢ φ ∧ k ∈ Z → k ∈ ℤ
68 67 62 zaddcld ⊢ φ ∧ k ∈ Z → k + B ∈ ℤ
69 oveq1 ⊢ m = k + B → m + A - B = k + B + A − B
70 id ⊢ m = k + B → m = k + B
71 69 70 oveq12d ⊢ m = k + B → m + A - B m = k + B + A − B k + B
72 eqid ⊢ m ∈ ℤ ⟼ m + A - B m = m ∈ ℤ ⟼ m + A - B m
73 ovex ⊢ k + B + A − B k + B ∈ V
74 71 72 73 fvmpt ⊢ k + B ∈ ℤ → m ∈ ℤ ⟼ m + A - B m ⁡ k + B = k + B + A − B k + B
75 68 74 syl ⊢ φ ∧ k ∈ Z → m ∈ ℤ ⟼ m + A - B m ⁡ k + B = k + B + A − B k + B
76 66 75 6 3eqtr4d ⊢ φ ∧ k ∈ Z → m ∈ ℤ ⟼ m + A - B m ⁡ k + B = F ⁡ k
77 1 2 4 5 57 76 climshft2 ⊢ φ → F ⇝ 1 ↔ m ∈ ℤ ⟼ m + A - B m ⇝ 1
78 56 77 mpbird ⊢ φ → F ⇝ 1