Metamath Proof Explorer

Theorem rlimno1

Description: A function whose inverse converges to zero is unbounded. (Contributed by Mario Carneiro, 30-May-2016)

Ref Expression
Hypotheses rlimno1.1 
|- ( ph -> sup ( A , RR* , < ) = +oo )
rlimno1.2 
|- ( ph -> ( x e. A |-> ( 1 / B ) ) ~~>r 0 )
rlimno1.3 
|- ( ( ph /\ x e. A ) -> B e. CC )
rlimno1.4 
|- ( ( ph /\ x e. A ) -> B =/= 0 )
Assertion rlimno1 
|- ( ph -> -. ( x e. A |-> B ) e. O(1) )

Proof

Step Hyp Ref Expression
1 rlimno1.1 
 |-  ( ph -> sup ( A , RR* , < ) = +oo )
2 rlimno1.2 
 |-  ( ph -> ( x e. A |-> ( 1 / B ) ) ~~>r 0 )
3 rlimno1.3 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
4 rlimno1.4 
 |-  ( ( ph /\ x e. A ) -> B =/= 0 )
5 fal 
 |-  -. F.
6 3 4 reccld 
 |-  ( ( ph /\ x e. A ) -> ( 1 / B ) e. CC )
7 6 ralrimiva 
 |-  ( ph -> A. x e. A ( 1 / B ) e. CC )
8 7 adantr 
 |-  ( ( ph /\ y e. RR ) -> A. x e. A ( 1 / B ) e. CC )
9 simpr 
 |-  ( ( ph /\ y e. RR ) -> y e. RR )
10 1re 
 |-  1 e. RR
11 ifcl 
 |-  ( ( y e. RR /\ 1 e. RR ) -> if ( 1 <_ y , y , 1 ) e. RR )
12 9 10 11 sylancl 
 |-  ( ( ph /\ y e. RR ) -> if ( 1 <_ y , y , 1 ) e. RR )
13 1rp 
 |-  1 e. RR+
14 13 a1i 
 |-  ( ( ph /\ y e. RR ) -> 1 e. RR+ )
15 max1 
 |-  ( ( 1 e. RR /\ y e. RR ) -> 1 <_ if ( 1 <_ y , y , 1 ) )
16 10 9 15 sylancr 
 |-  ( ( ph /\ y e. RR ) -> 1 <_ if ( 1 <_ y , y , 1 ) )
17 12 14 16 rpgecld 
 |-  ( ( ph /\ y e. RR ) -> if ( 1 <_ y , y , 1 ) e. RR+ )
18 17 rpreccld 
 |-  ( ( ph /\ y e. RR ) -> ( 1 / if ( 1 <_ y , y , 1 ) ) e. RR+ )
19 2 adantr 
 |-  ( ( ph /\ y e. RR ) -> ( x e. A |-> ( 1 / B ) ) ~~>r 0 )
20 8 18 19 rlimi 
 |-  ( ( ph /\ y e. RR ) -> E. c e. RR A. x e. A ( c <_ x -> ( abs ` ( ( 1 / B ) - 0 ) ) < ( 1 / if ( 1 <_ y , y , 1 ) ) ) )
21 dmmptg 
 |-  ( A. x e. A ( 1 / B ) e. CC -> dom ( x e. A |-> ( 1 / B ) ) = A )
22 7 21 syl 
 |-  ( ph -> dom ( x e. A |-> ( 1 / B ) ) = A )
23 rlimss 
 |-  ( ( x e. A |-> ( 1 / B ) ) ~~>r 0 -> dom ( x e. A |-> ( 1 / B ) ) C_ RR )
24 2 23 syl 
 |-  ( ph -> dom ( x e. A |-> ( 1 / B ) ) C_ RR )
25 22 24 eqsstrrd 
 |-  ( ph -> A C_ RR )
26 25 adantr 
 |-  ( ( ph /\ y e. RR ) -> A C_ RR )
27 rexanre 
 |-  ( A C_ RR -> ( E. c e. RR A. x e. A ( c <_ x -> ( ( abs ` ( ( 1 / B ) - 0 ) ) < ( 1 / if ( 1 <_ y , y , 1 ) ) /\ ( abs ` B ) <_ y ) ) <-> ( E. c e. RR A. x e. A ( c <_ x -> ( abs ` ( ( 1 / B ) - 0 ) ) < ( 1 / if ( 1 <_ y , y , 1 ) ) ) /\ E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ y ) ) ) )
28 26 27 syl 
 |-  ( ( ph /\ y e. RR ) -> ( E. c e. RR A. x e. A ( c <_ x -> ( ( abs ` ( ( 1 / B ) - 0 ) ) < ( 1 / if ( 1 <_ y , y , 1 ) ) /\ ( abs ` B ) <_ y ) ) <-> ( E. c e. RR A. x e. A ( c <_ x -> ( abs ` ( ( 1 / B ) - 0 ) ) < ( 1 / if ( 1 <_ y , y , 1 ) ) ) /\ E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ y ) ) ) )
29 ressxr 
 |-  RR C_ RR*
30 25 29 sstrdi 
 |-  ( ph -> A C_ RR* )
31 supxrunb1 
 |-  ( A C_ RR* -> ( A. c e. RR E. x e. A c <_ x <-> sup ( A , RR* , < ) = +oo ) )
32 30 31 syl 
 |-  ( ph -> ( A. c e. RR E. x e. A c <_ x <-> sup ( A , RR* , < ) = +oo ) )
33 1 32 mpbird 
 |-  ( ph -> A. c e. RR E. x e. A c <_ x )
34 33 adantr 
 |-  ( ( ph /\ y e. RR ) -> A. c e. RR E. x e. A c <_ x )
35 r19.29 
 |-  ( ( A. c e. RR E. x e. A c <_ x /\ E. c e. RR A. x e. A ( c <_ x -> ( ( abs ` ( ( 1 / B ) - 0 ) ) < ( 1 / if ( 1 <_ y , y , 1 ) ) /\ ( abs ` B ) <_ y ) ) ) -> E. c e. RR ( E. x e. A c <_ x /\ A. x e. A ( c <_ x -> ( ( abs ` ( ( 1 / B ) - 0 ) ) < ( 1 / if ( 1 <_ y , y , 1 ) ) /\ ( abs ` B ) <_ y ) ) ) )
36 r19.29r 
 |-  ( ( E. x e. A c <_ x /\ A. x e. A ( c <_ x -> ( ( abs ` ( ( 1 / B ) - 0 ) ) < ( 1 / if ( 1 <_ y , y , 1 ) ) /\ ( abs ` B ) <_ y ) ) ) -> E. x e. A ( c <_ x /\ ( c <_ x -> ( ( abs ` ( ( 1 / B ) - 0 ) ) < ( 1 / if ( 1 <_ y , y , 1 ) ) /\ ( abs ` B ) <_ y ) ) ) )
37 3 adantlr 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> B e. CC )
38 37 adantr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ ( abs ` B ) <_ y ) -> B e. CC )
39 4 adantlr 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> B =/= 0 )
40 39 adantr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ ( abs ` B ) <_ y ) -> B =/= 0 )
41 38 40 reccld 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ ( abs ` B ) <_ y ) -> ( 1 / B ) e. CC )
42 41 subid1d 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ ( abs ` B ) <_ y ) -> ( ( 1 / B ) - 0 ) = ( 1 / B ) )
43 42 fveq2d 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ ( abs ` B ) <_ y ) -> ( abs ` ( ( 1 / B ) - 0 ) ) = ( abs ` ( 1 / B ) ) )
44 1cnd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ ( abs ` B ) <_ y ) -> 1 e. CC )
45 44 38 40 absdivd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ ( abs ` B ) <_ y ) -> ( abs ` ( 1 / B ) ) = ( ( abs ` 1 ) / ( abs ` B ) ) )
46 10 a1i 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ ( abs ` B ) <_ y ) -> 1 e. RR )
47 0le1 
 |-  0 <_ 1
48 47 a1i 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ ( abs ` B ) <_ y ) -> 0 <_ 1 )
49 46 48 absidd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ ( abs ` B ) <_ y ) -> ( abs ` 1 ) = 1 )
50 49 oveq1d 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ ( abs ` B ) <_ y ) -> ( ( abs ` 1 ) / ( abs ` B ) ) = ( 1 / ( abs ` B ) ) )
51 43 45 50 3eqtrd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ ( abs ` B ) <_ y ) -> ( abs ` ( ( 1 / B ) - 0 ) ) = ( 1 / ( abs ` B ) ) )
52 17 ad2antrr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ ( abs ` B ) <_ y ) -> if ( 1 <_ y , y , 1 ) e. RR+ )
53 52 rprecred 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ ( abs ` B ) <_ y ) -> ( 1 / if ( 1 <_ y , y , 1 ) ) e. RR )
54 37 39 absrpcld 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( abs ` B ) e. RR+ )
55 54 adantr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ ( abs ` B ) <_ y ) -> ( abs ` B ) e. RR+ )
56 55 rprecred 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ ( abs ` B ) <_ y ) -> ( 1 / ( abs ` B ) ) e. RR )
57 55 rpred 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ ( abs ` B ) <_ y ) -> ( abs ` B ) e. RR )
58 9 ad2antrr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ ( abs ` B ) <_ y ) -> y e. RR )
59 12 ad2antrr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ ( abs ` B ) <_ y ) -> if ( 1 <_ y , y , 1 ) e. RR )
60 simpr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ ( abs ` B ) <_ y ) -> ( abs ` B ) <_ y )
61 max2 
 |-  ( ( 1 e. RR /\ y e. RR ) -> y <_ if ( 1 <_ y , y , 1 ) )
62 10 58 61 sylancr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ ( abs ` B ) <_ y ) -> y <_ if ( 1 <_ y , y , 1 ) )
63 57 58 59 60 62 letrd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ ( abs ` B ) <_ y ) -> ( abs ` B ) <_ if ( 1 <_ y , y , 1 ) )
64 55 52 46 48 63 lediv2ad 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ ( abs ` B ) <_ y ) -> ( 1 / if ( 1 <_ y , y , 1 ) ) <_ ( 1 / ( abs ` B ) ) )
65 53 56 64 lensymd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ ( abs ` B ) <_ y ) -> -. ( 1 / ( abs ` B ) ) < ( 1 / if ( 1 <_ y , y , 1 ) ) )
66 51 65 eqnbrtrd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ ( abs ` B ) <_ y ) -> -. ( abs ` ( ( 1 / B ) - 0 ) ) < ( 1 / if ( 1 <_ y , y , 1 ) ) )
67 66 pm2.21d 
 |-  ( ( ( ( ph /\ y e. RR ) /\ x e. A ) /\ ( abs ` B ) <_ y ) -> ( ( abs ` ( ( 1 / B ) - 0 ) ) < ( 1 / if ( 1 <_ y , y , 1 ) ) -> F. ) )
68 67 expimpd 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( ( ( abs ` B ) <_ y /\ ( abs ` ( ( 1 / B ) - 0 ) ) < ( 1 / if ( 1 <_ y , y , 1 ) ) ) -> F. ) )
69 68 ancomsd 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( ( ( abs ` ( ( 1 / B ) - 0 ) ) < ( 1 / if ( 1 <_ y , y , 1 ) ) /\ ( abs ` B ) <_ y ) -> F. ) )
70 69 imim2d 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( ( c <_ x -> ( ( abs ` ( ( 1 / B ) - 0 ) ) < ( 1 / if ( 1 <_ y , y , 1 ) ) /\ ( abs ` B ) <_ y ) ) -> ( c <_ x -> F. ) ) )
71 70 impcomd 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( ( c <_ x /\ ( c <_ x -> ( ( abs ` ( ( 1 / B ) - 0 ) ) < ( 1 / if ( 1 <_ y , y , 1 ) ) /\ ( abs ` B ) <_ y ) ) ) -> F. ) )
72 71 rexlimdva 
 |-  ( ( ph /\ y e. RR ) -> ( E. x e. A ( c <_ x /\ ( c <_ x -> ( ( abs ` ( ( 1 / B ) - 0 ) ) < ( 1 / if ( 1 <_ y , y , 1 ) ) /\ ( abs ` B ) <_ y ) ) ) -> F. ) )
73 36 72 syl5 
 |-  ( ( ph /\ y e. RR ) -> ( ( E. x e. A c <_ x /\ A. x e. A ( c <_ x -> ( ( abs ` ( ( 1 / B ) - 0 ) ) < ( 1 / if ( 1 <_ y , y , 1 ) ) /\ ( abs ` B ) <_ y ) ) ) -> F. ) )
74 73 rexlimdvw 
 |-  ( ( ph /\ y e. RR ) -> ( E. c e. RR ( E. x e. A c <_ x /\ A. x e. A ( c <_ x -> ( ( abs ` ( ( 1 / B ) - 0 ) ) < ( 1 / if ( 1 <_ y , y , 1 ) ) /\ ( abs ` B ) <_ y ) ) ) -> F. ) )
75 35 74 syl5 
 |-  ( ( ph /\ y e. RR ) -> ( ( A. c e. RR E. x e. A c <_ x /\ E. c e. RR A. x e. A ( c <_ x -> ( ( abs ` ( ( 1 / B ) - 0 ) ) < ( 1 / if ( 1 <_ y , y , 1 ) ) /\ ( abs ` B ) <_ y ) ) ) -> F. ) )
76 34 75 mpand 
 |-  ( ( ph /\ y e. RR ) -> ( E. c e. RR A. x e. A ( c <_ x -> ( ( abs ` ( ( 1 / B ) - 0 ) ) < ( 1 / if ( 1 <_ y , y , 1 ) ) /\ ( abs ` B ) <_ y ) ) -> F. ) )
77 28 76 sylbird 
 |-  ( ( ph /\ y e. RR ) -> ( ( E. c e. RR A. x e. A ( c <_ x -> ( abs ` ( ( 1 / B ) - 0 ) ) < ( 1 / if ( 1 <_ y , y , 1 ) ) ) /\ E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ y ) ) -> F. ) )
78 20 77 mpand 
 |-  ( ( ph /\ y e. RR ) -> ( E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ y ) -> F. ) )
79 5 78 mtoi 
 |-  ( ( ph /\ y e. RR ) -> -. E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ y ) )
80 79 nrexdv 
 |-  ( ph -> -. E. y e. RR E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ y ) )
81 25 3 elo1mpt 
 |-  ( ph -> ( ( x e. A |-> B ) e. O(1) <-> E. c e. RR E. y e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ y ) ) )
82 rexcom 
 |-  ( E. c e. RR E. y e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ y ) <-> E. y e. RR E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ y ) )
83 81 82 bitrdi 
 |-  ( ph -> ( ( x e. A |-> B ) e. O(1) <-> E. y e. RR E. c e. RR A. x e. A ( c <_ x -> ( abs ` B ) <_ y ) ) )
84 80 83 mtbird 
 |-  ( ph -> -. ( x e. A |-> B ) e. O(1) )