Metamath Proof Explorer

Theorem rlimuni

Description: A real function whose domain is unbounded above converges to at most one limit. (Contributed by Mario Carneiro, 8-May-2016)

Ref Expression
Hypotheses rlimuni.1 
|- ( ph -> F : A --> CC )
rlimuni.2 
|- ( ph -> sup ( A , RR* , < ) = +oo )
rlimuni.3 
|- ( ph -> F ~~>r B )
rlimuni.4 
|- ( ph -> F ~~>r C )
Assertion rlimuni 
|- ( ph -> B = C )

Proof

Step Hyp Ref Expression
1 rlimuni.1 
 |-  ( ph -> F : A --> CC )
2 rlimuni.2 
 |-  ( ph -> sup ( A , RR* , < ) = +oo )
3 rlimuni.3 
 |-  ( ph -> F ~~>r B )
4 rlimuni.4 
 |-  ( ph -> F ~~>r C )
5 rlimcl 
 |-  ( F ~~>r B -> B e. CC )
6 3 5 syl 
 |-  ( ph -> B e. CC )
7 6 ad2antrr 
 |-  ( ( ( ph /\ j e. RR ) /\ k e. A ) -> B e. CC )
8 rlimcl 
 |-  ( F ~~>r C -> C e. CC )
9 4 8 syl 
 |-  ( ph -> C e. CC )
10 9 ad2antrr 
 |-  ( ( ( ph /\ j e. RR ) /\ k e. A ) -> C e. CC )
11 7 10 subcld 
 |-  ( ( ( ph /\ j e. RR ) /\ k e. A ) -> ( B - C ) e. CC )
12 11 abscld 
 |-  ( ( ( ph /\ j e. RR ) /\ k e. A ) -> ( abs ` ( B - C ) ) e. RR )
13 12 ltnrd 
 |-  ( ( ( ph /\ j e. RR ) /\ k e. A ) -> -. ( abs ` ( B - C ) ) < ( abs ` ( B - C ) ) )
14 1 ffvelrnda 
 |-  ( ( ph /\ k e. A ) -> ( F ` k ) e. CC )
15 14 adantlr 
 |-  ( ( ( ph /\ j e. RR ) /\ k e. A ) -> ( F ` k ) e. CC )
16 15 7 abssubd 
 |-  ( ( ( ph /\ j e. RR ) /\ k e. A ) -> ( abs ` ( ( F ` k ) - B ) ) = ( abs ` ( B - ( F ` k ) ) ) )
17 16 breq1d 
 |-  ( ( ( ph /\ j e. RR ) /\ k e. A ) -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) <-> ( abs ` ( B - ( F ` k ) ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) )
18 17 anbi1d 
 |-  ( ( ( ph /\ j e. RR ) /\ k e. A ) -> ( ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) <-> ( ( abs ` ( B - ( F ` k ) ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) )
19 abs3lem 
 |-  ( ( ( B e. CC /\ C e. CC ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( B - C ) ) e. RR ) ) -> ( ( ( abs ` ( B - ( F ` k ) ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) -> ( abs ` ( B - C ) ) < ( abs ` ( B - C ) ) ) )
20 7 10 15 12 19 syl22anc 
 |-  ( ( ( ph /\ j e. RR ) /\ k e. A ) -> ( ( ( abs ` ( B - ( F ` k ) ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) -> ( abs ` ( B - C ) ) < ( abs ` ( B - C ) ) ) )
21 18 20 sylbid 
 |-  ( ( ( ph /\ j e. RR ) /\ k e. A ) -> ( ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) -> ( abs ` ( B - C ) ) < ( abs ` ( B - C ) ) ) )
22 21 imim2d 
 |-  ( ( ( ph /\ j e. RR ) /\ k e. A ) -> ( ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) -> ( j <_ k -> ( abs ` ( B - C ) ) < ( abs ` ( B - C ) ) ) ) )
23 22 impcomd 
 |-  ( ( ( ph /\ j e. RR ) /\ k e. A ) -> ( ( j <_ k /\ ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) ) -> ( abs ` ( B - C ) ) < ( abs ` ( B - C ) ) ) )
24 13 23 mtod 
 |-  ( ( ( ph /\ j e. RR ) /\ k e. A ) -> -. ( j <_ k /\ ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) ) )
25 24 nrexdv 
 |-  ( ( ph /\ j e. RR ) -> -. E. k e. A ( j <_ k /\ ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) ) )
26 r19.29r 
 |-  ( ( E. k e. A j <_ k /\ A. k e. A ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) ) -> E. k e. A ( j <_ k /\ ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) ) )
27 25 26 nsyl 
 |-  ( ( ph /\ j e. RR ) -> -. ( E. k e. A j <_ k /\ A. k e. A ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) ) )
28 27 nrexdv 
 |-  ( ph -> -. E. j e. RR ( E. k e. A j <_ k /\ A. k e. A ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) ) )
29 1 fdmd 
 |-  ( ph -> dom F = A )
30 rlimss 
 |-  ( F ~~>r B -> dom F C_ RR )
31 3 30 syl 
 |-  ( ph -> dom F C_ RR )
32 29 31 eqsstrrd 
 |-  ( ph -> A C_ RR )
33 ressxr 
 |-  RR C_ RR*
34 32 33 sstrdi 
 |-  ( ph -> A C_ RR* )
35 supxrunb1 
 |-  ( A C_ RR* -> ( A. j e. RR E. k e. A j <_ k <-> sup ( A , RR* , < ) = +oo ) )
36 34 35 syl 
 |-  ( ph -> ( A. j e. RR E. k e. A j <_ k <-> sup ( A , RR* , < ) = +oo ) )
37 2 36 mpbird 
 |-  ( ph -> A. j e. RR E. k e. A j <_ k )
38 r19.29 
 |-  ( ( A. j e. RR E. k e. A j <_ k /\ E. j e. RR A. k e. A ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) ) -> E. j e. RR ( E. k e. A j <_ k /\ A. k e. A ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) ) )
39 38 ex 
 |-  ( A. j e. RR E. k e. A j <_ k -> ( E. j e. RR A. k e. A ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) -> E. j e. RR ( E. k e. A j <_ k /\ A. k e. A ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) ) ) )
40 37 39 syl 
 |-  ( ph -> ( E. j e. RR A. k e. A ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) -> E. j e. RR ( E. k e. A j <_ k /\ A. k e. A ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) ) ) )
41 28 40 mtod 
 |-  ( ph -> -. E. j e. RR A. k e. A ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) )
42 1 adantr 
 |-  ( ( ph /\ B =/= C ) -> F : A --> CC )
43 ffvelrn 
 |-  ( ( F : A --> CC /\ k e. A ) -> ( F ` k ) e. CC )
44 43 ralrimiva 
 |-  ( F : A --> CC -> A. k e. A ( F ` k ) e. CC )
45 42 44 syl 
 |-  ( ( ph /\ B =/= C ) -> A. k e. A ( F ` k ) e. CC )
46 6 adantr 
 |-  ( ( ph /\ B =/= C ) -> B e. CC )
47 9 adantr 
 |-  ( ( ph /\ B =/= C ) -> C e. CC )
48 46 47 subcld 
 |-  ( ( ph /\ B =/= C ) -> ( B - C ) e. CC )
49 simpr 
 |-  ( ( ph /\ B =/= C ) -> B =/= C )
50 46 47 49 subne0d 
 |-  ( ( ph /\ B =/= C ) -> ( B - C ) =/= 0 )
51 48 50 absrpcld 
 |-  ( ( ph /\ B =/= C ) -> ( abs ` ( B - C ) ) e. RR+ )
52 51 rphalfcld 
 |-  ( ( ph /\ B =/= C ) -> ( ( abs ` ( B - C ) ) / 2 ) e. RR+ )
53 42 feqmptd 
 |-  ( ( ph /\ B =/= C ) -> F = ( k e. A |-> ( F ` k ) ) )
54 3 adantr 
 |-  ( ( ph /\ B =/= C ) -> F ~~>r B )
55 53 54 eqbrtrrd 
 |-  ( ( ph /\ B =/= C ) -> ( k e. A |-> ( F ` k ) ) ~~>r B )
56 45 52 55 rlimi 
 |-  ( ( ph /\ B =/= C ) -> E. j e. RR A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) )
57 4 adantr 
 |-  ( ( ph /\ B =/= C ) -> F ~~>r C )
58 53 57 eqbrtrrd 
 |-  ( ( ph /\ B =/= C ) -> ( k e. A |-> ( F ` k ) ) ~~>r C )
59 45 52 58 rlimi 
 |-  ( ( ph /\ B =/= C ) -> E. j e. RR A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) )
60 32 adantr 
 |-  ( ( ph /\ B =/= C ) -> A C_ RR )
61 rexanre 
 |-  ( A C_ RR -> ( E. j e. RR A. k e. A ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) <-> ( E. j e. RR A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) /\ E. j e. RR A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) ) )
62 60 61 syl 
 |-  ( ( ph /\ B =/= C ) -> ( E. j e. RR A. k e. A ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) <-> ( E. j e. RR A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) /\ E. j e. RR A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) ) )
63 56 59 62 mpbir2and 
 |-  ( ( ph /\ B =/= C ) -> E. j e. RR A. k e. A ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) )
64 63 ex 
 |-  ( ph -> ( B =/= C -> E. j e. RR A. k e. A ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) ) )
65 64 necon1bd 
 |-  ( ph -> ( -. E. j e. RR A. k e. A ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) -> B = C ) )
66 41 65 mpd 
 |-  ( ph -> B = C )