Metamath Proof Explorer

Theorem caurcvg

Description: A Cauchy sequence of real numbers converges to its limit supremum. The fourth hypothesis specifies that F is a Cauchy sequence. (Contributed by NM, 4-Apr-2005) (Revised by AV, 12-Sep-2020)

Ref Expression
Hypotheses caurcvg.1 
|- Z = ( ZZ>= ` M )
caurcvg.3 
|- ( ph -> F : Z --> RR )
caurcvg.4 
|- ( ph -> A. x e. RR+ E. m e. Z A. k e. ( ZZ>= ` m ) ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x )
Assertion caurcvg 
|- ( ph -> F ~~> ( limsup ` F ) )

Proof

Step Hyp Ref Expression
1 caurcvg.1 
 |-  Z = ( ZZ>= ` M )
2 caurcvg.3 
 |-  ( ph -> F : Z --> RR )
3 caurcvg.4 
 |-  ( ph -> A. x e. RR+ E. m e. Z A. k e. ( ZZ>= ` m ) ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x )
4 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
5 1 4 eqsstri 
 |-  Z C_ ZZ
6 zssre 
 |-  ZZ C_ RR
7 5 6 sstri 
 |-  Z C_ RR
8 7 a1i 
 |-  ( ph -> Z C_ RR )
9 1rp 
 |-  1 e. RR+
10 9 ne0ii 
 |-  RR+ =/= (/)
11 r19.2z 
 |-  ( ( RR+ =/= (/) /\ A. x e. RR+ E. m e. Z A. k e. ( ZZ>= ` m ) ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x ) -> E. x e. RR+ E. m e. Z A. k e. ( ZZ>= ` m ) ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x )
12 10 3 11 sylancr 
 |-  ( ph -> E. x e. RR+ E. m e. Z A. k e. ( ZZ>= ` m ) ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x )
13 eluzel2 
 |-  ( m e. ( ZZ>= ` M ) -> M e. ZZ )
14 13 1 eleq2s 
 |-  ( m e. Z -> M e. ZZ )
15 1 uzsup 
 |-  ( M e. ZZ -> sup ( Z , RR* , < ) = +oo )
16 14 15 syl 
 |-  ( m e. Z -> sup ( Z , RR* , < ) = +oo )
17 16 a1d 
 |-  ( m e. Z -> ( A. k e. ( ZZ>= ` m ) ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x -> sup ( Z , RR* , < ) = +oo ) )
18 17 rexlimiv 
 |-  ( E. m e. Z A. k e. ( ZZ>= ` m ) ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x -> sup ( Z , RR* , < ) = +oo )
19 18 rexlimivw 
 |-  ( E. x e. RR+ E. m e. Z A. k e. ( ZZ>= ` m ) ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x -> sup ( Z , RR* , < ) = +oo )
20 12 19 syl 
 |-  ( ph -> sup ( Z , RR* , < ) = +oo )
21 5 sseli 
 |-  ( m e. Z -> m e. ZZ )
22 5 sseli 
 |-  ( k e. Z -> k e. ZZ )
23 eluz 
 |-  ( ( m e. ZZ /\ k e. ZZ ) -> ( k e. ( ZZ>= ` m ) <-> m <_ k ) )
24 21 22 23 syl2an 
 |-  ( ( m e. Z /\ k e. Z ) -> ( k e. ( ZZ>= ` m ) <-> m <_ k ) )
25 24 biimprd 
 |-  ( ( m e. Z /\ k e. Z ) -> ( m <_ k -> k e. ( ZZ>= ` m ) ) )
26 25 expimpd 
 |-  ( m e. Z -> ( ( k e. Z /\ m <_ k ) -> k e. ( ZZ>= ` m ) ) )
27 26 imim1d 
 |-  ( m e. Z -> ( ( k e. ( ZZ>= ` m ) -> ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x ) -> ( ( k e. Z /\ m <_ k ) -> ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x ) ) )
28 27 exp4a 
 |-  ( m e. Z -> ( ( k e. ( ZZ>= ` m ) -> ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x ) -> ( k e. Z -> ( m <_ k -> ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x ) ) ) )
29 28 ralimdv2 
 |-  ( m e. Z -> ( A. k e. ( ZZ>= ` m ) ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x -> A. k e. Z ( m <_ k -> ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x ) ) )
30 29 reximia 
 |-  ( E. m e. Z A. k e. ( ZZ>= ` m ) ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x -> E. m e. Z A. k e. Z ( m <_ k -> ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x ) )
31 30 ralimi 
 |-  ( A. x e. RR+ E. m e. Z A. k e. ( ZZ>= ` m ) ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x -> A. x e. RR+ E. m e. Z A. k e. Z ( m <_ k -> ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x ) )
32 3 31 syl 
 |-  ( ph -> A. x e. RR+ E. m e. Z A. k e. Z ( m <_ k -> ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x ) )
33 8 2 20 32 caurcvgr 
 |-  ( ph -> F ~~>r ( limsup ` F ) )
34 14 a1d 
 |-  ( m e. Z -> ( A. k e. ( ZZ>= ` m ) ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x -> M e. ZZ ) )
35 34 rexlimiv 
 |-  ( E. m e. Z A. k e. ( ZZ>= ` m ) ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x -> M e. ZZ )
36 35 rexlimivw 
 |-  ( E. x e. RR+ E. m e. Z A. k e. ( ZZ>= ` m ) ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x -> M e. ZZ )
37 12 36 syl 
 |-  ( ph -> M e. ZZ )
38 ax-resscn 
 |-  RR C_ CC
39 fss 
 |-  ( ( F : Z --> RR /\ RR C_ CC ) -> F : Z --> CC )
40 2 38 39 sylancl 
 |-  ( ph -> F : Z --> CC )
41 1 37 40 rlimclim 
 |-  ( ph -> ( F ~~>r ( limsup ` F ) <-> F ~~> ( limsup ` F ) ) )
42 33 41 mpbid 
 |-  ( ph -> F ~~> ( limsup ` F ) )