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 = ( ZZ>= ` M )
divcnvlin.2 
|- ( ph -> M e. ZZ )
divcnvlin.3 
|- ( ph -> A e. CC )
divcnvlin.4 
|- ( ph -> B e. ZZ )
divcnvlin.5 
|- ( ph -> F e. V )
divcnvlin.6 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = ( ( k + A ) / ( k + B ) ) )
Assertion divcnvlin 
|- ( ph -> F ~~> 1 )

Proof

Step Hyp Ref Expression
1 divcnvlin.1 
 |-  Z = ( ZZ>= ` M )
2 divcnvlin.2 
 |-  ( ph -> M e. ZZ )
3 divcnvlin.3 
 |-  ( ph -> A e. CC )
4 divcnvlin.4 
 |-  ( ph -> B e. ZZ )
5 divcnvlin.5 
 |-  ( ph -> F e. V )
6 divcnvlin.6 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = ( ( k + A ) / ( k + B ) ) )
7 nncn 
 |-  ( m e. NN -> m e. CC )
8 7 adantl 
 |-  ( ( ph /\ m e. NN ) -> m e. CC )
9 4 zcnd 
 |-  ( ph -> B e. CC )
10 3 9 subcld 
 |-  ( ph -> ( A - B ) e. CC )
11 10 adantr 
 |-  ( ( ph /\ m e. NN ) -> ( A - B ) e. CC )
12 nnne0 
 |-  ( m e. NN -> m =/= 0 )
13 12 adantl 
 |-  ( ( ph /\ m e. NN ) -> m =/= 0 )
14 8 11 8 13 divdird 
 |-  ( ( ph /\ m e. NN ) -> ( ( m + ( A - B ) ) / m ) = ( ( m / m ) + ( ( A - B ) / m ) ) )
15 8 13 dividd 
 |-  ( ( ph /\ m e. NN ) -> ( m / m ) = 1 )
16 15 oveq1d 
 |-  ( ( ph /\ m e. NN ) -> ( ( m / m ) + ( ( A - B ) / m ) ) = ( 1 + ( ( A - B ) / m ) ) )
17 14 16 eqtrd 
 |-  ( ( ph /\ m e. NN ) -> ( ( m + ( A - B ) ) / m ) = ( 1 + ( ( A - B ) / m ) ) )
18 17 mpteq2dva 
 |-  ( ph -> ( m e. NN |-> ( ( m + ( A - B ) ) / m ) ) = ( m e. NN |-> ( 1 + ( ( A - B ) / m ) ) ) )
19 nnuz 
 |-  NN = ( ZZ>= ` 1 )
20 1zzd 
 |-  ( ph -> 1 e. ZZ )
21 divcnv 
 |-  ( ( A - B ) e. CC -> ( m e. NN |-> ( ( A - B ) / m ) ) ~~> 0 )
22 10 21 syl 
 |-  ( ph -> ( m e. NN |-> ( ( A - B ) / m ) ) ~~> 0 )
23 1cnd 
 |-  ( ph -> 1 e. CC )
24 nnex 
 |-  NN e. _V
25 24 mptex 
 |-  ( m e. NN |-> ( 1 + ( ( A - B ) / m ) ) ) e. _V
26 25 a1i 
 |-  ( ph -> ( m e. NN |-> ( 1 + ( ( A - B ) / m ) ) ) e. _V )
27 11 8 13 divcld 
 |-  ( ( ph /\ m e. NN ) -> ( ( A - B ) / m ) e. CC )
28 27 fmpttd 
 |-  ( ph -> ( m e. NN |-> ( ( A - B ) / m ) ) : NN --> CC )
29 28 ffvelrnda 
 |-  ( ( ph /\ k e. NN ) -> ( ( m e. NN |-> ( ( A - B ) / m ) ) ` k ) e. CC )
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 e. NN |-> ( 1 + ( ( A - B ) / m ) ) ) = ( m e. NN |-> ( 1 + ( ( A - B ) / m ) ) )
33 ovex 
 |-  ( 1 + ( ( A - B ) / k ) ) e. _V
34 31 32 33 fvmpt 
 |-  ( k e. NN -> ( ( m e. NN |-> ( 1 + ( ( A - B ) / m ) ) ) ` k ) = ( 1 + ( ( A - B ) / k ) ) )
35 eqid 
 |-  ( m e. NN |-> ( ( A - B ) / m ) ) = ( m e. NN |-> ( ( A - B ) / m ) )
36 ovex 
 |-  ( ( A - B ) / k ) e. _V
37 30 35 36 fvmpt 
 |-  ( k e. NN -> ( ( m e. NN |-> ( ( A - B ) / m ) ) ` k ) = ( ( A - B ) / k ) )
38 37 oveq2d 
 |-  ( k e. NN -> ( 1 + ( ( m e. NN |-> ( ( A - B ) / m ) ) ` k ) ) = ( 1 + ( ( A - B ) / k ) ) )
39 34 38 eqtr4d 
 |-  ( k e. NN -> ( ( m e. NN |-> ( 1 + ( ( A - B ) / m ) ) ) ` k ) = ( 1 + ( ( m e. NN |-> ( ( A - B ) / m ) ) ` k ) ) )
40 39 adantl 
 |-  ( ( ph /\ k e. NN ) -> ( ( m e. NN |-> ( 1 + ( ( A - B ) / m ) ) ) ` k ) = ( 1 + ( ( m e. NN |-> ( ( A - B ) / m ) ) ` k ) ) )
41 19 20 22 23 26 29 40 climaddc2 
 |-  ( ph -> ( m e. NN |-> ( 1 + ( ( A - B ) / m ) ) ) ~~> ( 1 + 0 ) )
42 18 41 eqbrtrd 
 |-  ( ph -> ( m e. NN |-> ( ( m + ( A - B ) ) / m ) ) ~~> ( 1 + 0 ) )
43 nnssz 
 |-  NN C_ ZZ
44 resmpt 
 |-  ( NN C_ ZZ -> ( ( m e. ZZ |-> ( ( m + ( A - B ) ) / m ) ) |` NN ) = ( m e. NN |-> ( ( m + ( A - B ) ) / m ) ) )
45 43 44 ax-mp 
 |-  ( ( m e. ZZ |-> ( ( m + ( A - B ) ) / m ) ) |` NN ) = ( m e. NN |-> ( ( m + ( A - B ) ) / m ) )
46 19 reseq2i 
 |-  ( ( m e. ZZ |-> ( ( m + ( A - B ) ) / m ) ) |` NN ) = ( ( m e. ZZ |-> ( ( m + ( A - B ) ) / m ) ) |` ( ZZ>= ` 1 ) )
47 45 46 eqtr3i 
 |-  ( m e. NN |-> ( ( m + ( A - B ) ) / m ) ) = ( ( m e. ZZ |-> ( ( m + ( A - B ) ) / m ) ) |` ( ZZ>= ` 1 ) )
48 1p0e1 
 |-  ( 1 + 0 ) = 1
49 47 48 breq12i 
 |-  ( ( m e. NN |-> ( ( m + ( A - B ) ) / m ) ) ~~> ( 1 + 0 ) <-> ( ( m e. ZZ |-> ( ( m + ( A - B ) ) / m ) ) |` ( ZZ>= ` 1 ) ) ~~> 1 )
50 1z 
 |-  1 e. ZZ
51 zex 
 |-  ZZ e. _V
52 51 mptex 
 |-  ( m e. ZZ |-> ( ( m + ( A - B ) ) / m ) ) e. _V
53 climres 
 |-  ( ( 1 e. ZZ /\ ( m e. ZZ |-> ( ( m + ( A - B ) ) / m ) ) e. _V ) -> ( ( ( m e. ZZ |-> ( ( m + ( A - B ) ) / m ) ) |` ( ZZ>= ` 1 ) ) ~~> 1 <-> ( m e. ZZ |-> ( ( m + ( A - B ) ) / m ) ) ~~> 1 ) )
54 50 52 53 mp2an 
 |-  ( ( ( m e. ZZ |-> ( ( m + ( A - B ) ) / m ) ) |` ( ZZ>= ` 1 ) ) ~~> 1 <-> ( m e. ZZ |-> ( ( m + ( A - B ) ) / m ) ) ~~> 1 )
55 49 54 bitri 
 |-  ( ( m e. NN |-> ( ( m + ( A - B ) ) / m ) ) ~~> ( 1 + 0 ) <-> ( m e. ZZ |-> ( ( m + ( A - B ) ) / m ) ) ~~> 1 )
56 42 55 sylib 
 |-  ( ph -> ( m e. ZZ |-> ( ( m + ( A - B ) ) / m ) ) ~~> 1 )
57 52 a1i 
 |-  ( ph -> ( m e. ZZ |-> ( ( m + ( A - B ) ) / m ) ) e. _V )
58 eluzelz 
 |-  ( k e. ( ZZ>= ` M ) -> k e. ZZ )
59 58 1 eleq2s 
 |-  ( k e. Z -> k e. ZZ )
60 59 zcnd 
 |-  ( k e. Z -> k e. CC )
61 60 adantl 
 |-  ( ( ph /\ k e. Z ) -> k e. CC )
62 4 adantr 
 |-  ( ( ph /\ k e. Z ) -> B e. ZZ )
63 62 zcnd 
 |-  ( ( ph /\ k e. Z ) -> B e. CC )
64 3 adantr 
 |-  ( ( ph /\ k e. Z ) -> A e. CC )
65 61 63 64 ppncand 
 |-  ( ( ph /\ k e. Z ) -> ( ( k + B ) + ( A - B ) ) = ( k + A ) )
66 65 oveq1d 
 |-  ( ( ph /\ k e. Z ) -> ( ( ( k + B ) + ( A - B ) ) / ( k + B ) ) = ( ( k + A ) / ( k + B ) ) )
67 59 adantl 
 |-  ( ( ph /\ k e. Z ) -> k e. ZZ )
68 67 62 zaddcld 
 |-  ( ( ph /\ k e. Z ) -> ( k + B ) e. ZZ )
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 e. ZZ |-> ( ( m + ( A - B ) ) / m ) ) = ( m e. ZZ |-> ( ( m + ( A - B ) ) / m ) )
73 ovex 
 |-  ( ( ( k + B ) + ( A - B ) ) / ( k + B ) ) e. _V
74 71 72 73 fvmpt 
 |-  ( ( k + B ) e. ZZ -> ( ( m e. ZZ |-> ( ( m + ( A - B ) ) / m ) ) ` ( k + B ) ) = ( ( ( k + B ) + ( A - B ) ) / ( k + B ) ) )
75 68 74 syl 
 |-  ( ( ph /\ k e. Z ) -> ( ( m e. ZZ |-> ( ( m + ( A - B ) ) / m ) ) ` ( k + B ) ) = ( ( ( k + B ) + ( A - B ) ) / ( k + B ) ) )
76 66 75 6 3eqtr4d 
 |-  ( ( ph /\ k e. Z ) -> ( ( m e. ZZ |-> ( ( m + ( A - B ) ) / m ) ) ` ( k + B ) ) = ( F ` k ) )
77 1 2 4 5 57 76 climshft2 
 |-  ( ph -> ( F ~~> 1 <-> ( m e. ZZ |-> ( ( m + ( A - B ) ) / m ) ) ~~> 1 ) )
78 56 77 mpbird 
 |-  ( ph -> F ~~> 1 )