Metamath Proof Explorer

Theorem caurcvgr

Description: A Cauchy sequence of real numbers converges to its limit supremum. The third hypothesis specifies that F is a Cauchy sequence. (Contributed by Mario Carneiro, 7-May-2016) (Revised by AV, 12-Sep-2020)

Ref Expression
Hypotheses caurcvgr.1 
|- ( ph -> A C_ RR )
caurcvgr.2 
|- ( ph -> F : A --> RR )
caurcvgr.3 
|- ( ph -> sup ( A , RR* , < ) = +oo )
caurcvgr.4 
|- ( ph -> A. x e. RR+ E. j e. A A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )
Assertion caurcvgr 
|- ( ph -> F ~~>r ( limsup ` F ) )

Proof

Step Hyp Ref Expression
1 caurcvgr.1 
 |-  ( ph -> A C_ RR )
2 caurcvgr.2 
 |-  ( ph -> F : A --> RR )
3 caurcvgr.3 
 |-  ( ph -> sup ( A , RR* , < ) = +oo )
4 caurcvgr.4 
 |-  ( ph -> A. x e. RR+ E. j e. A A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )
5 1rp 
 |-  1 e. RR+
6 5 a1i 
 |-  ( ph -> 1 e. RR+ )
7 1 2 3 4 6 caucvgrlem 
 |-  ( ph -> E. j e. A ( ( limsup ` F ) e. RR /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < ( 3 x. 1 ) ) ) )
8 simpl 
 |-  ( ( ( limsup ` F ) e. RR /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < ( 3 x. 1 ) ) ) -> ( limsup ` F ) e. RR )
9 8 rexlimivw 
 |-  ( E. j e. A ( ( limsup ` F ) e. RR /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < ( 3 x. 1 ) ) ) -> ( limsup ` F ) e. RR )
10 7 9 syl 
 |-  ( ph -> ( limsup ` F ) e. RR )
11 10 recnd 
 |-  ( ph -> ( limsup ` F ) e. CC )
12 1 adantr 
 |-  ( ( ph /\ y e. RR+ ) -> A C_ RR )
13 2 adantr 
 |-  ( ( ph /\ y e. RR+ ) -> F : A --> RR )
14 3 adantr 
 |-  ( ( ph /\ y e. RR+ ) -> sup ( A , RR* , < ) = +oo )
15 4 adantr 
 |-  ( ( ph /\ y e. RR+ ) -> A. x e. RR+ E. j e. A A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )
16 simpr 
 |-  ( ( ph /\ y e. RR+ ) -> y e. RR+ )
17 3rp 
 |-  3 e. RR+
18 rpdivcl 
 |-  ( ( y e. RR+ /\ 3 e. RR+ ) -> ( y / 3 ) e. RR+ )
19 16 17 18 sylancl 
 |-  ( ( ph /\ y e. RR+ ) -> ( y / 3 ) e. RR+ )
20 12 13 14 15 19 caucvgrlem 
 |-  ( ( ph /\ y e. RR+ ) -> E. j e. A ( ( limsup ` F ) e. RR /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < ( 3 x. ( y / 3 ) ) ) ) )
21 simpr 
 |-  ( ( ( limsup ` F ) e. RR /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < ( 3 x. ( y / 3 ) ) ) ) -> A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < ( 3 x. ( y / 3 ) ) ) )
22 21 reximi 
 |-  ( E. j e. A ( ( limsup ` F ) e. RR /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < ( 3 x. ( y / 3 ) ) ) ) -> E. j e. A A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < ( 3 x. ( y / 3 ) ) ) )
23 20 22 syl 
 |-  ( ( ph /\ y e. RR+ ) -> E. j e. A A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < ( 3 x. ( y / 3 ) ) ) )
24 ssrexv 
 |-  ( A C_ RR -> ( E. j e. A A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < ( 3 x. ( y / 3 ) ) ) -> E. j e. RR A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < ( 3 x. ( y / 3 ) ) ) ) )
25 12 23 24 sylc 
 |-  ( ( ph /\ y e. RR+ ) -> E. j e. RR A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < ( 3 x. ( y / 3 ) ) ) )
26 rpcn 
 |-  ( y e. RR+ -> y e. CC )
27 26 adantl 
 |-  ( ( ph /\ y e. RR+ ) -> y e. CC )
28 3cn 
 |-  3 e. CC
29 28 a1i 
 |-  ( ( ph /\ y e. RR+ ) -> 3 e. CC )
30 3ne0 
 |-  3 =/= 0
31 30 a1i 
 |-  ( ( ph /\ y e. RR+ ) -> 3 =/= 0 )
32 27 29 31 divcan2d 
 |-  ( ( ph /\ y e. RR+ ) -> ( 3 x. ( y / 3 ) ) = y )
33 32 breq2d 
 |-  ( ( ph /\ y e. RR+ ) -> ( ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < ( 3 x. ( y / 3 ) ) <-> ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < y ) )
34 33 imbi2d 
 |-  ( ( ph /\ y e. RR+ ) -> ( ( j <_ k -> ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < ( 3 x. ( y / 3 ) ) ) <-> ( j <_ k -> ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < y ) ) )
35 34 rexralbidv 
 |-  ( ( ph /\ y e. RR+ ) -> ( E. j e. RR A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < ( 3 x. ( y / 3 ) ) ) <-> E. j e. RR A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < y ) ) )
36 25 35 mpbid 
 |-  ( ( ph /\ y e. RR+ ) -> E. j e. RR A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < y ) )
37 36 ralrimiva 
 |-  ( ph -> A. y e. RR+ E. j e. RR A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < y ) )
38 ax-resscn 
 |-  RR C_ CC
39 fss 
 |-  ( ( F : A --> RR /\ RR C_ CC ) -> F : A --> CC )
40 2 38 39 sylancl 
 |-  ( ph -> F : A --> CC )
41 eqidd 
 |-  ( ( ph /\ k e. A ) -> ( F ` k ) = ( F ` k ) )
42 40 1 41 rlim 
 |-  ( ph -> ( F ~~>r ( limsup ` F ) <-> ( ( limsup ` F ) e. CC /\ A. y e. RR+ E. j e. RR A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < y ) ) ) )
43 11 37 42 mpbir2and 
 |-  ( ph -> F ~~>r ( limsup ` F ) )