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 ⊢φ→supAℝ*<=+∞
rlimno1.2 ⊢φ→x∈A⟼1B⇝ℝ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 ⊢φ→supAℝ*<=+∞
2 rlimno1.2 ⊢φ→x∈A⟼1B⇝ℝ0
3 rlimno1.3 ⊢φ∧x∈A→B∈ℂ
4 rlimno1.4 ⊢φ∧x∈A→B≠0
5 fal ⊢¬⊥
6 3 4 reccld ⊢φ∧x∈A→1B∈ℂ
7 6 ralrimiva ⊢φ→∀x∈A1B∈ℂ
8 7 adantr ⊢φ∧y∈ℝ→∀x∈A1B∈ℂ
9 simpr ⊢φ∧y∈ℝ→y∈ℝ
10 1re ⊢1∈ℝ
11 ifcl ⊢y∈ℝ∧1∈ℝ→if1≤yy1∈ℝ
12 9 10 11 sylancl ⊢φ∧y∈ℝ→if1≤yy1∈ℝ
13 1rp ⊢1∈ℝ+
14 13 a1i ⊢φ∧y∈ℝ→1∈ℝ+
15 max1 ⊢1∈ℝ∧y∈ℝ→1≤if1≤yy1
16 10 9 15 sylancr ⊢φ∧y∈ℝ→1≤if1≤yy1
17 12 14 16 rpgecld ⊢φ∧y∈ℝ→if1≤yy1∈ℝ+
18 17 rpreccld ⊢φ∧y∈ℝ→1if1≤yy1∈ℝ+
19 2 adantr ⊢φ∧y∈ℝ→x∈A⟼1B⇝ℝ0
20 8 18 19 rlimi ⊢φ∧y∈ℝ→∃c∈ℝ∀x∈Ac≤x→1B−0<1if1≤yy1
21 dmmptg ⊢∀x∈A1B∈ℂ→dom⁡x∈A⟼1B=A
22 7 21 syl ⊢φ→dom⁡x∈A⟼1B=A
23 rlimss ⊢x∈A⟼1B⇝ℝ0→dom⁡x∈A⟼1B⊆ℝ
24 2 23 syl ⊢φ→dom⁡x∈A⟼1B⊆ℝ
25 22 24 eqsstrrd ⊢φ→A⊆ℝ
26 25 adantr ⊢φ∧y∈ℝ→A⊆ℝ
27 rexanre ⊢A⊆ℝ→∃c∈ℝ∀x∈Ac≤x→1B−0<1if1≤yy1∧B≤y↔∃c∈ℝ∀x∈Ac≤x→1B−0<1if1≤yy1∧∃c∈ℝ∀x∈Ac≤x→B≤y
28 26 27 syl ⊢φ∧y∈ℝ→∃c∈ℝ∀x∈Ac≤x→1B−0<1if1≤yy1∧B≤y↔∃c∈ℝ∀x∈Ac≤x→1B−0<1if1≤yy1∧∃c∈ℝ∀x∈Ac≤x→B≤y
29 ressxr ⊢ℝ⊆ℝ*
30 25 29 sstrdi ⊢φ→A⊆ℝ*
31 supxrunb1 ⊢A⊆ℝ*→∀c∈ℝ∃x∈Ac≤x↔supAℝ*<=+∞
32 30 31 syl ⊢φ→∀c∈ℝ∃x∈Ac≤x↔supAℝ*<=+∞
33 1 32 mpbird ⊢φ→∀c∈ℝ∃x∈Ac≤x
34 33 adantr ⊢φ∧y∈ℝ→∀c∈ℝ∃x∈Ac≤x
35 r19.29 ⊢∀c∈ℝ∃x∈Ac≤x∧∃c∈ℝ∀x∈Ac≤x→1B−0<1if1≤yy1∧B≤y→∃c∈ℝ∃x∈Ac≤x∧∀x∈Ac≤x→1B−0<1if1≤yy1∧B≤y
36 r19.29r ⊢∃x∈Ac≤x∧∀x∈Ac≤x→1B−0<1if1≤yy1∧B≤y→∃x∈Ac≤x∧c≤x→1B−0<1if1≤yy1∧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→1B∈ℂ
42 41 subid1d ⊢φ∧y∈ℝ∧x∈A∧B≤y→1B−0=1B
43 42 fveq2d ⊢φ∧y∈ℝ∧x∈A∧B≤y→1B−0=1B
44 1cnd ⊢φ∧y∈ℝ∧x∈A∧B≤y→1∈ℂ
45 44 38 40 absdivd ⊢φ∧y∈ℝ∧x∈A∧B≤y→1B=1B
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→1B=1B
51 43 45 50 3eqtrd ⊢φ∧y∈ℝ∧x∈A∧B≤y→1B−0=1B
52 17 ad2antrr ⊢φ∧y∈ℝ∧x∈A∧B≤y→if1≤yy1∈ℝ+
53 52 rprecred ⊢φ∧y∈ℝ∧x∈A∧B≤y→1if1≤yy1∈ℝ
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→1B∈ℝ
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→if1≤yy1∈ℝ
60 simpr ⊢φ∧y∈ℝ∧x∈A∧B≤y→B≤y
61 max2 ⊢1∈ℝ∧y∈ℝ→y≤if1≤yy1
62 10 58 61 sylancr ⊢φ∧y∈ℝ∧x∈A∧B≤y→y≤if1≤yy1
63 57 58 59 60 62 letrd ⊢φ∧y∈ℝ∧x∈A∧B≤y→B≤if1≤yy1
64 55 52 46 48 63 lediv2ad ⊢φ∧y∈ℝ∧x∈A∧B≤y→1if1≤yy1≤1B
65 53 56 64 lensymd ⊢φ∧y∈ℝ∧x∈A∧B≤y→¬1B<1if1≤yy1
66 51 65 eqnbrtrd ⊢φ∧y∈ℝ∧x∈A∧B≤y→¬1B−0<1if1≤yy1
67 66 pm2.21d ⊢φ∧y∈ℝ∧x∈A∧B≤y→1B−0<1if1≤yy1→⊥
68 67 expimpd ⊢φ∧y∈ℝ∧x∈A→B≤y∧1B−0<1if1≤yy1→⊥
69 68 ancomsd ⊢φ∧y∈ℝ∧x∈A→1B−0<1if1≤yy1∧B≤y→⊥
70 69 imim2d ⊢φ∧y∈ℝ∧x∈A→c≤x→1B−0<1if1≤yy1∧B≤y→c≤x→⊥
71 70 impcomd ⊢φ∧y∈ℝ∧x∈A→c≤x∧c≤x→1B−0<1if1≤yy1∧B≤y→⊥
72 71 rexlimdva ⊢φ∧y∈ℝ→∃x∈Ac≤x∧c≤x→1B−0<1if1≤yy1∧B≤y→⊥
73 36 72 syl5 ⊢φ∧y∈ℝ→∃x∈Ac≤x∧∀x∈Ac≤x→1B−0<1if1≤yy1∧B≤y→⊥
74 73 rexlimdvw ⊢φ∧y∈ℝ→∃c∈ℝ∃x∈Ac≤x∧∀x∈Ac≤x→1B−0<1if1≤yy1∧B≤y→⊥
75 35 74 syl5 ⊢φ∧y∈ℝ→∀c∈ℝ∃x∈Ac≤x∧∃c∈ℝ∀x∈Ac≤x→1B−0<1if1≤yy1∧B≤y→⊥
76 34 75 mpand ⊢φ∧y∈ℝ→∃c∈ℝ∀x∈Ac≤x→1B−0<1if1≤yy1∧B≤y→⊥
77 28 76 sylbird ⊢φ∧y∈ℝ→∃c∈ℝ∀x∈Ac≤x→1B−0<1if1≤yy1∧∃c∈ℝ∀x∈Ac≤x→B≤y→⊥
78 20 77 mpand ⊢φ∧y∈ℝ→∃c∈ℝ∀x∈Ac≤x→B≤y→⊥
79 5 78 mtoi ⊢φ∧y∈ℝ→¬∃c∈ℝ∀x∈Ac≤x→B≤y
80 79 nrexdv ⊢φ→¬∃y∈ℝ∃c∈ℝ∀x∈Ac≤x→B≤y
81 25 3 elo1mpt ⊢φ→x∈A⟼B∈𝑂⁡1↔∃c∈ℝ∃y∈ℝ∀x∈Ac≤x→B≤y
82 rexcom ⊢∃c∈ℝ∃y∈ℝ∀x∈Ac≤x→B≤y↔∃y∈ℝ∃c∈ℝ∀x∈Ac≤x→B≤y
83 81 82 bitrdi ⊢φ→x∈A⟼B∈𝑂⁡1↔∃y∈ℝ∃c∈ℝ∀x∈Ac≤x→B≤y
84 80 83 mtbird ⊢φ→¬x∈A⟼B∈𝑂⁡1