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 φ sup A * < = +∞
rlimno1.2 φ x A 1 B 0
rlimno1.3 φ x A B
rlimno1.4 φ x A B 0
Assertion rlimno1 φ ¬ x A B 𝑂1

Proof

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