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