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 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
divcnvlin.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
divcnvlin.3 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
divcnvlin.4 ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
divcnvlin.5 ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
divcnvlin.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( ( 𝑘 + 𝐴 ) / ( 𝑘 + 𝐵 ) ) )
Assertion divcnvlin ( 𝜑 → 𝐹 ⇝ 1 )

Proof

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