Metamath Proof Explorer

Theorem rlimclim

Description: A sequence on an upper integer set converges in the real sense iff it converges in the integer sense. (Contributed by Mario Carneiro, 16-Sep-2014)

Ref Expression
Hypotheses rlimclim.1 
|- Z = ( ZZ>= ` M )
rlimclim.2 
|- ( ph -> M e. ZZ )
rlimclim.3 
|- ( ph -> F : Z --> CC )
Assertion rlimclim 
|- ( ph -> ( F ~~>r A <-> F ~~> A ) )

Proof

Step Hyp Ref Expression
1 rlimclim.1 
 |-  Z = ( ZZ>= ` M )
2 rlimclim.2 
 |-  ( ph -> M e. ZZ )
3 rlimclim.3 
 |-  ( ph -> F : Z --> CC )
4 2 adantr 
 |-  ( ( ph /\ F ~~>r A ) -> M e. ZZ )
5 simpr 
 |-  ( ( ph /\ F ~~>r A ) -> F ~~>r A )
6 fdm 
 |-  ( F : Z --> CC -> dom F = Z )
7 eqimss2 
 |-  ( dom F = Z -> Z C_ dom F )
8 3 6 7 3syl 
 |-  ( ph -> Z C_ dom F )
9 8 adantr 
 |-  ( ( ph /\ F ~~>r A ) -> Z C_ dom F )
10 1 4 5 9 rlimclim1 
 |-  ( ( ph /\ F ~~>r A ) -> F ~~> A )
11 climcl 
 |-  ( F ~~> A -> A e. CC )
12 11 adantl 
 |-  ( ( ph /\ F ~~> A ) -> A e. CC )
13 2 ad2antrr 
 |-  ( ( ( ph /\ F ~~> A ) /\ y e. RR+ ) -> M e. ZZ )
14 simpr 
 |-  ( ( ( ph /\ F ~~> A ) /\ y e. RR+ ) -> y e. RR+ )
15 eqidd 
 |-  ( ( ( ( ph /\ F ~~> A ) /\ y e. RR+ ) /\ k e. Z ) -> ( F ` k ) = ( F ` k ) )
16 simplr 
 |-  ( ( ( ph /\ F ~~> A ) /\ y e. RR+ ) -> F ~~> A )
17 1 13 14 15 16 climi2 
 |-  ( ( ( ph /\ F ~~> A ) /\ y e. RR+ ) -> E. z e. Z A. k e. ( ZZ>= ` z ) ( abs ` ( ( F ` k ) - A ) ) < y )
18 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
19 1 18 eqsstri 
 |-  Z C_ ZZ
20 zssre 
 |-  ZZ C_ RR
21 19 20 sstri 
 |-  Z C_ RR
22 fveq2 
 |-  ( k = w -> ( F ` k ) = ( F ` w ) )
23 22 fvoveq1d 
 |-  ( k = w -> ( abs ` ( ( F ` k ) - A ) ) = ( abs ` ( ( F ` w ) - A ) ) )
24 23 breq1d 
 |-  ( k = w -> ( ( abs ` ( ( F ` k ) - A ) ) < y <-> ( abs ` ( ( F ` w ) - A ) ) < y ) )
25 simplrr 
 |-  ( ( ( ( ( ph /\ F ~~> A ) /\ y e. RR+ ) /\ ( z e. Z /\ A. k e. ( ZZ>= ` z ) ( abs ` ( ( F ` k ) - A ) ) < y ) ) /\ ( w e. Z /\ z <_ w ) ) -> A. k e. ( ZZ>= ` z ) ( abs ` ( ( F ` k ) - A ) ) < y )
26 simplrl 
 |-  ( ( ( ( ( ph /\ F ~~> A ) /\ y e. RR+ ) /\ ( z e. Z /\ A. k e. ( ZZ>= ` z ) ( abs ` ( ( F ` k ) - A ) ) < y ) ) /\ ( w e. Z /\ z <_ w ) ) -> z e. Z )
27 19 26 sseldi 
 |-  ( ( ( ( ( ph /\ F ~~> A ) /\ y e. RR+ ) /\ ( z e. Z /\ A. k e. ( ZZ>= ` z ) ( abs ` ( ( F ` k ) - A ) ) < y ) ) /\ ( w e. Z /\ z <_ w ) ) -> z e. ZZ )
28 simprl 
 |-  ( ( ( ( ( ph /\ F ~~> A ) /\ y e. RR+ ) /\ ( z e. Z /\ A. k e. ( ZZ>= ` z ) ( abs ` ( ( F ` k ) - A ) ) < y ) ) /\ ( w e. Z /\ z <_ w ) ) -> w e. Z )
29 19 28 sseldi 
 |-  ( ( ( ( ( ph /\ F ~~> A ) /\ y e. RR+ ) /\ ( z e. Z /\ A. k e. ( ZZ>= ` z ) ( abs ` ( ( F ` k ) - A ) ) < y ) ) /\ ( w e. Z /\ z <_ w ) ) -> w e. ZZ )
30 simprr 
 |-  ( ( ( ( ( ph /\ F ~~> A ) /\ y e. RR+ ) /\ ( z e. Z /\ A. k e. ( ZZ>= ` z ) ( abs ` ( ( F ` k ) - A ) ) < y ) ) /\ ( w e. Z /\ z <_ w ) ) -> z <_ w )
31 eluz2 
 |-  ( w e. ( ZZ>= ` z ) <-> ( z e. ZZ /\ w e. ZZ /\ z <_ w ) )
32 27 29 30 31 syl3anbrc 
 |-  ( ( ( ( ( ph /\ F ~~> A ) /\ y e. RR+ ) /\ ( z e. Z /\ A. k e. ( ZZ>= ` z ) ( abs ` ( ( F ` k ) - A ) ) < y ) ) /\ ( w e. Z /\ z <_ w ) ) -> w e. ( ZZ>= ` z ) )
33 24 25 32 rspcdva 
 |-  ( ( ( ( ( ph /\ F ~~> A ) /\ y e. RR+ ) /\ ( z e. Z /\ A. k e. ( ZZ>= ` z ) ( abs ` ( ( F ` k ) - A ) ) < y ) ) /\ ( w e. Z /\ z <_ w ) ) -> ( abs ` ( ( F ` w ) - A ) ) < y )
34 33 expr 
 |-  ( ( ( ( ( ph /\ F ~~> A ) /\ y e. RR+ ) /\ ( z e. Z /\ A. k e. ( ZZ>= ` z ) ( abs ` ( ( F ` k ) - A ) ) < y ) ) /\ w e. Z ) -> ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) )
35 34 ralrimiva 
 |-  ( ( ( ( ph /\ F ~~> A ) /\ y e. RR+ ) /\ ( z e. Z /\ A. k e. ( ZZ>= ` z ) ( abs ` ( ( F ` k ) - A ) ) < y ) ) -> A. w e. Z ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) )
36 35 expr 
 |-  ( ( ( ( ph /\ F ~~> A ) /\ y e. RR+ ) /\ z e. Z ) -> ( A. k e. ( ZZ>= ` z ) ( abs ` ( ( F ` k ) - A ) ) < y -> A. w e. Z ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) ) )
37 36 reximdva 
 |-  ( ( ( ph /\ F ~~> A ) /\ y e. RR+ ) -> ( E. z e. Z A. k e. ( ZZ>= ` z ) ( abs ` ( ( F ` k ) - A ) ) < y -> E. z e. Z A. w e. Z ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) ) )
38 ssrexv 
 |-  ( Z C_ RR -> ( E. z e. Z A. w e. Z ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) -> E. z e. RR A. w e. Z ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) ) )
39 21 37 38 mpsylsyld 
 |-  ( ( ( ph /\ F ~~> A ) /\ y e. RR+ ) -> ( E. z e. Z A. k e. ( ZZ>= ` z ) ( abs ` ( ( F ` k ) - A ) ) < y -> E. z e. RR A. w e. Z ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) ) )
40 17 39 mpd 
 |-  ( ( ( ph /\ F ~~> A ) /\ y e. RR+ ) -> E. z e. RR A. w e. Z ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) )
41 40 ralrimiva 
 |-  ( ( ph /\ F ~~> A ) -> A. y e. RR+ E. z e. RR A. w e. Z ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) )
42 3 adantr 
 |-  ( ( ph /\ F ~~> A ) -> F : Z --> CC )
43 21 a1i 
 |-  ( ( ph /\ F ~~> A ) -> Z C_ RR )
44 eqidd 
 |-  ( ( ( ph /\ F ~~> A ) /\ w e. Z ) -> ( F ` w ) = ( F ` w ) )
45 42 43 44 rlim 
 |-  ( ( ph /\ F ~~> A ) -> ( F ~~>r A <-> ( A e. CC /\ A. y e. RR+ E. z e. RR A. w e. Z ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) ) ) )
46 12 41 45 mpbir2and 
 |-  ( ( ph /\ F ~~> A ) -> F ~~>r A )
47 10 46 impbida 
 |-  ( ph -> ( F ~~>r A <-> F ~~> A ) )