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 )