Metamath Proof Explorer

Theorem divcnvshft

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

Ref Expression
Hypotheses divcnvshft.1 
|- Z = ( ZZ>= ` M )
divcnvshft.2 
|- ( ph -> M e. ZZ )
divcnvshft.3 
|- ( ph -> A e. CC )
divcnvshft.4 
|- ( ph -> B e. ZZ )
divcnvshft.5 
|- ( ph -> F e. V )
divcnvshft.6 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = ( A / ( k + B ) ) )
Assertion divcnvshft 
|- ( ph -> F ~~> 0 )

Proof

Step Hyp Ref Expression
1 divcnvshft.1 
 |-  Z = ( ZZ>= ` M )
2 divcnvshft.2 
 |-  ( ph -> M e. ZZ )
3 divcnvshft.3 
 |-  ( ph -> A e. CC )
4 divcnvshft.4 
 |-  ( ph -> B e. ZZ )
5 divcnvshft.5 
 |-  ( ph -> F e. V )
6 divcnvshft.6 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = ( A / ( k + B ) ) )
7 divcnv 
 |-  ( A e. CC -> ( m e. NN |-> ( A / m ) ) ~~> 0 )
8 3 7 syl 
 |-  ( ph -> ( m e. NN |-> ( A / m ) ) ~~> 0 )
9 nnssz 
 |-  NN C_ ZZ
10 resmpt 
 |-  ( NN C_ ZZ -> ( ( m e. ZZ |-> ( A / m ) ) |` NN ) = ( m e. NN |-> ( A / m ) ) )
11 9 10 ax-mp 
 |-  ( ( m e. ZZ |-> ( A / m ) ) |` NN ) = ( m e. NN |-> ( A / m ) )
12 nnuz 
 |-  NN = ( ZZ>= ` 1 )
13 12 reseq2i 
 |-  ( ( m e. ZZ |-> ( A / m ) ) |` NN ) = ( ( m e. ZZ |-> ( A / m ) ) |` ( ZZ>= ` 1 ) )
14 11 13 eqtr3i 
 |-  ( m e. NN |-> ( A / m ) ) = ( ( m e. ZZ |-> ( A / m ) ) |` ( ZZ>= ` 1 ) )
15 14 breq1i 
 |-  ( ( m e. NN |-> ( A / m ) ) ~~> 0 <-> ( ( m e. ZZ |-> ( A / m ) ) |` ( ZZ>= ` 1 ) ) ~~> 0 )
16 1z 
 |-  1 e. ZZ
17 zex 
 |-  ZZ e. _V
18 17 mptex 
 |-  ( m e. ZZ |-> ( A / m ) ) e. _V
19 climres 
 |-  ( ( 1 e. ZZ /\ ( m e. ZZ |-> ( A / m ) ) e. _V ) -> ( ( ( m e. ZZ |-> ( A / m ) ) |` ( ZZ>= ` 1 ) ) ~~> 0 <-> ( m e. ZZ |-> ( A / m ) ) ~~> 0 ) )
20 16 18 19 mp2an 
 |-  ( ( ( m e. ZZ |-> ( A / m ) ) |` ( ZZ>= ` 1 ) ) ~~> 0 <-> ( m e. ZZ |-> ( A / m ) ) ~~> 0 )
21 15 20 bitri 
 |-  ( ( m e. NN |-> ( A / m ) ) ~~> 0 <-> ( m e. ZZ |-> ( A / m ) ) ~~> 0 )
22 8 21 sylib 
 |-  ( ph -> ( m e. ZZ |-> ( A / m ) ) ~~> 0 )
23 18 a1i 
 |-  ( ph -> ( m e. ZZ |-> ( A / m ) ) e. _V )
24 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
25 1 24 eqsstri 
 |-  Z C_ ZZ
26 25 sseli 
 |-  ( k e. Z -> k e. ZZ )
27 26 adantl 
 |-  ( ( ph /\ k e. Z ) -> k e. ZZ )
28 4 adantr 
 |-  ( ( ph /\ k e. Z ) -> B e. ZZ )
29 27 28 zaddcld 
 |-  ( ( ph /\ k e. Z ) -> ( k + B ) e. ZZ )
30 oveq2 
 |-  ( m = ( k + B ) -> ( A / m ) = ( A / ( k + B ) ) )
31 eqid 
 |-  ( m e. ZZ |-> ( A / m ) ) = ( m e. ZZ |-> ( A / m ) )
32 ovex 
 |-  ( A / ( k + B ) ) e. _V
33 30 31 32 fvmpt 
 |-  ( ( k + B ) e. ZZ -> ( ( m e. ZZ |-> ( A / m ) ) ` ( k + B ) ) = ( A / ( k + B ) ) )
34 29 33 syl 
 |-  ( ( ph /\ k e. Z ) -> ( ( m e. ZZ |-> ( A / m ) ) ` ( k + B ) ) = ( A / ( k + B ) ) )
35 34 6 eqtr4d 
 |-  ( ( ph /\ k e. Z ) -> ( ( m e. ZZ |-> ( A / m ) ) ` ( k + B ) ) = ( F ` k ) )
36 1 2 4 5 23 35 climshft2 
 |-  ( ph -> ( F ~~> 0 <-> ( m e. ZZ |-> ( A / m ) ) ~~> 0 ) )
37 22 36 mpbird 
 |-  ( ph -> F ~~> 0 )