Metamath Proof Explorer

Theorem o1lo1

Description: A real function is eventually bounded iff it is eventually lower bounded and eventually upper bounded. (Contributed by Mario Carneiro, 25-May-2016)

Ref Expression
Hypothesis o1lo1.1 ⊢ φ ∧ x ∈ A → B ∈ ℝ
Assertion o1lo1 ⊢ φ → x ∈ A ⟼ B ∈ 𝑂⁡1 ↔ x ∈ A ⟼ B ∈ ≤𝑂⁡1 ∧ x ∈ A ⟼ − B ∈ ≤𝑂⁡1

Proof

Step Hyp Ref Expression
1 o1lo1.1 ⊢ φ ∧ x ∈ A → B ∈ ℝ
2 o1dm ⊢ x ∈ A ⟼ B ∈ 𝑂⁡1 → dom ⁡ x ∈ A ⟼ B ⊆ ℝ
3 2 a1i ⊢ φ → x ∈ A ⟼ B ∈ 𝑂⁡1 → dom ⁡ x ∈ A ⟼ B ⊆ ℝ
4 lo1dm ⊢ x ∈ A ⟼ B ∈ ≤𝑂⁡1 → dom ⁡ x ∈ A ⟼ B ⊆ ℝ
5 4 adantr ⊢ x ∈ A ⟼ B ∈ ≤𝑂⁡1 ∧ x ∈ A ⟼ − B ∈ ≤𝑂⁡1 → dom ⁡ x ∈ A ⟼ B ⊆ ℝ
6 5 a1i ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1 ∧ x ∈ A ⟼ − B ∈ ≤𝑂⁡1 → dom ⁡ x ∈ A ⟼ B ⊆ ℝ
7 1 ralrimiva ⊢ φ → ∀ x ∈ A B ∈ ℝ
8 dmmptg ⊢ ∀ x ∈ A B ∈ ℝ → dom ⁡ x ∈ A ⟼ B = A
9 7 8 syl ⊢ φ → dom ⁡ x ∈ A ⟼ B = A
10 9 sseq1d ⊢ φ → dom ⁡ x ∈ A ⟼ B ⊆ ℝ ↔ A ⊆ ℝ
11 simpr ⊢ φ ∧ A ⊆ ℝ ∧ m ∈ ℝ → m ∈ ℝ
12 1 adantlr ⊢ φ ∧ A ⊆ ℝ ∧ x ∈ A → B ∈ ℝ
13 12 adantlr ⊢ φ ∧ A ⊆ ℝ ∧ m ∈ ℝ ∧ x ∈ A → B ∈ ℝ
14 simplr ⊢ φ ∧ A ⊆ ℝ ∧ m ∈ ℝ ∧ x ∈ A → m ∈ ℝ
15 13 14 absled ⊢ φ ∧ A ⊆ ℝ ∧ m ∈ ℝ ∧ x ∈ A → B ≤ m ↔ − m ≤ B ∧ B ≤ m
16 ancom ⊢ − m ≤ B ∧ B ≤ m ↔ B ≤ m ∧ − m ≤ B
17 lenegcon1 ⊢ m ∈ ℝ ∧ B ∈ ℝ → − m ≤ B ↔ − B ≤ m
18 14 13 17 syl2anc ⊢ φ ∧ A ⊆ ℝ ∧ m ∈ ℝ ∧ x ∈ A → − m ≤ B ↔ − B ≤ m
19 18 anbi2d ⊢ φ ∧ A ⊆ ℝ ∧ m ∈ ℝ ∧ x ∈ A → B ≤ m ∧ − m ≤ B ↔ B ≤ m ∧ − B ≤ m
20 16 19 syl5bb ⊢ φ ∧ A ⊆ ℝ ∧ m ∈ ℝ ∧ x ∈ A → − m ≤ B ∧ B ≤ m ↔ B ≤ m ∧ − B ≤ m
21 15 20 bitrd ⊢ φ ∧ A ⊆ ℝ ∧ m ∈ ℝ ∧ x ∈ A → B ≤ m ↔ B ≤ m ∧ − B ≤ m
22 21 imbi2d ⊢ φ ∧ A ⊆ ℝ ∧ m ∈ ℝ ∧ x ∈ A → c ≤ x → B ≤ m ↔ c ≤ x → B ≤ m ∧ − B ≤ m
23 22 ralbidva ⊢ φ ∧ A ⊆ ℝ ∧ m ∈ ℝ → ∀ x ∈ A c ≤ x → B ≤ m ↔ ∀ x ∈ A c ≤ x → B ≤ m ∧ − B ≤ m
24 23 rexbidv ⊢ φ ∧ A ⊆ ℝ ∧ m ∈ ℝ → ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ↔ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ∧ − B ≤ m
25 24 biimpd ⊢ φ ∧ A ⊆ ℝ ∧ m ∈ ℝ → ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m → ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ∧ − B ≤ m
26 breq2 ⊢ n = m → B ≤ n ↔ B ≤ m
27 26 anbi1d ⊢ n = m → B ≤ n ∧ − B ≤ p ↔ B ≤ m ∧ − B ≤ p
28 27 imbi2d ⊢ n = m → c ≤ x → B ≤ n ∧ − B ≤ p ↔ c ≤ x → B ≤ m ∧ − B ≤ p
29 28 rexralbidv ⊢ n = m → ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ n ∧ − B ≤ p ↔ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ∧ − B ≤ p
30 breq2 ⊢ p = m → − B ≤ p ↔ − B ≤ m
31 30 anbi2d ⊢ p = m → B ≤ m ∧ − B ≤ p ↔ B ≤ m ∧ − B ≤ m
32 31 imbi2d ⊢ p = m → c ≤ x → B ≤ m ∧ − B ≤ p ↔ c ≤ x → B ≤ m ∧ − B ≤ m
33 32 rexralbidv ⊢ p = m → ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ∧ − B ≤ p ↔ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ∧ − B ≤ m
34 29 33 rspc2ev ⊢ m ∈ ℝ ∧ m ∈ ℝ ∧ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ∧ − B ≤ m → ∃ n ∈ ℝ ∃ p ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ n ∧ − B ≤ p
35 34 3anidm12 ⊢ m ∈ ℝ ∧ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ∧ − B ≤ m → ∃ n ∈ ℝ ∃ p ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ n ∧ − B ≤ p
36 11 25 35 syl6an ⊢ φ ∧ A ⊆ ℝ ∧ m ∈ ℝ → ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m → ∃ n ∈ ℝ ∃ p ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ n ∧ − B ≤ p
37 36 rexlimdva ⊢ φ ∧ A ⊆ ℝ → ∃ m ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m → ∃ n ∈ ℝ ∃ p ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ n ∧ − B ≤ p
38 simplrr ⊢ φ ∧ A ⊆ ℝ ∧ n ∈ ℝ ∧ p ∈ ℝ ∧ n ≤ p → p ∈ ℝ
39 simplrl ⊢ φ ∧ A ⊆ ℝ ∧ n ∈ ℝ ∧ p ∈ ℝ ∧ ¬ n ≤ p → n ∈ ℝ
40 38 39 ifclda ⊢ φ ∧ A ⊆ ℝ ∧ n ∈ ℝ ∧ p ∈ ℝ → if n ≤ p p n ∈ ℝ
41 max2 ⊢ n ∈ ℝ ∧ p ∈ ℝ → p ≤ if n ≤ p p n
42 41 ad2antlr ⊢ φ ∧ A ⊆ ℝ ∧ n ∈ ℝ ∧ p ∈ ℝ ∧ x ∈ A → p ≤ if n ≤ p p n
43 12 adantlr ⊢ φ ∧ A ⊆ ℝ ∧ n ∈ ℝ ∧ p ∈ ℝ ∧ x ∈ A → B ∈ ℝ
44 43 renegcld ⊢ φ ∧ A ⊆ ℝ ∧ n ∈ ℝ ∧ p ∈ ℝ ∧ x ∈ A → − B ∈ ℝ
45 simplrr ⊢ φ ∧ A ⊆ ℝ ∧ n ∈ ℝ ∧ p ∈ ℝ ∧ x ∈ A → p ∈ ℝ
46 simplrl ⊢ φ ∧ A ⊆ ℝ ∧ n ∈ ℝ ∧ p ∈ ℝ ∧ x ∈ A → n ∈ ℝ
47 45 46 ifcld ⊢ φ ∧ A ⊆ ℝ ∧ n ∈ ℝ ∧ p ∈ ℝ ∧ x ∈ A → if n ≤ p p n ∈ ℝ
48 letr ⊢ − B ∈ ℝ ∧ p ∈ ℝ ∧ if n ≤ p p n ∈ ℝ → − B ≤ p ∧ p ≤ if n ≤ p p n → − B ≤ if n ≤ p p n
49 44 45 47 48 syl3anc ⊢ φ ∧ A ⊆ ℝ ∧ n ∈ ℝ ∧ p ∈ ℝ ∧ x ∈ A → − B ≤ p ∧ p ≤ if n ≤ p p n → − B ≤ if n ≤ p p n
50 42 49 mpan2d ⊢ φ ∧ A ⊆ ℝ ∧ n ∈ ℝ ∧ p ∈ ℝ ∧ x ∈ A → − B ≤ p → − B ≤ if n ≤ p p n
51 lenegcon1 ⊢ B ∈ ℝ ∧ if n ≤ p p n ∈ ℝ → − B ≤ if n ≤ p p n ↔ − if n ≤ p p n ≤ B
52 43 47 51 syl2anc ⊢ φ ∧ A ⊆ ℝ ∧ n ∈ ℝ ∧ p ∈ ℝ ∧ x ∈ A → − B ≤ if n ≤ p p n ↔ − if n ≤ p p n ≤ B
53 50 52 sylibd ⊢ φ ∧ A ⊆ ℝ ∧ n ∈ ℝ ∧ p ∈ ℝ ∧ x ∈ A → − B ≤ p → − if n ≤ p p n ≤ B
54 max1 ⊢ n ∈ ℝ ∧ p ∈ ℝ → n ≤ if n ≤ p p n
55 54 ad2antlr ⊢ φ ∧ A ⊆ ℝ ∧ n ∈ ℝ ∧ p ∈ ℝ ∧ x ∈ A → n ≤ if n ≤ p p n
56 letr ⊢ B ∈ ℝ ∧ n ∈ ℝ ∧ if n ≤ p p n ∈ ℝ → B ≤ n ∧ n ≤ if n ≤ p p n → B ≤ if n ≤ p p n
57 43 46 47 56 syl3anc ⊢ φ ∧ A ⊆ ℝ ∧ n ∈ ℝ ∧ p ∈ ℝ ∧ x ∈ A → B ≤ n ∧ n ≤ if n ≤ p p n → B ≤ if n ≤ p p n
58 55 57 mpan2d ⊢ φ ∧ A ⊆ ℝ ∧ n ∈ ℝ ∧ p ∈ ℝ ∧ x ∈ A → B ≤ n → B ≤ if n ≤ p p n
59 53 58 anim12d ⊢ φ ∧ A ⊆ ℝ ∧ n ∈ ℝ ∧ p ∈ ℝ ∧ x ∈ A → − B ≤ p ∧ B ≤ n → − if n ≤ p p n ≤ B ∧ B ≤ if n ≤ p p n
60 59 ancomsd ⊢ φ ∧ A ⊆ ℝ ∧ n ∈ ℝ ∧ p ∈ ℝ ∧ x ∈ A → B ≤ n ∧ − B ≤ p → − if n ≤ p p n ≤ B ∧ B ≤ if n ≤ p p n
61 43 47 absled ⊢ φ ∧ A ⊆ ℝ ∧ n ∈ ℝ ∧ p ∈ ℝ ∧ x ∈ A → B ≤ if n ≤ p p n ↔ − if n ≤ p p n ≤ B ∧ B ≤ if n ≤ p p n
62 60 61 sylibrd ⊢ φ ∧ A ⊆ ℝ ∧ n ∈ ℝ ∧ p ∈ ℝ ∧ x ∈ A → B ≤ n ∧ − B ≤ p → B ≤ if n ≤ p p n
63 62 imim2d ⊢ φ ∧ A ⊆ ℝ ∧ n ∈ ℝ ∧ p ∈ ℝ ∧ x ∈ A → c ≤ x → B ≤ n ∧ − B ≤ p → c ≤ x → B ≤ if n ≤ p p n
64 63 ralimdva ⊢ φ ∧ A ⊆ ℝ ∧ n ∈ ℝ ∧ p ∈ ℝ → ∀ x ∈ A c ≤ x → B ≤ n ∧ − B ≤ p → ∀ x ∈ A c ≤ x → B ≤ if n ≤ p p n
65 64 reximdv ⊢ φ ∧ A ⊆ ℝ ∧ n ∈ ℝ ∧ p ∈ ℝ → ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ n ∧ − B ≤ p → ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ if n ≤ p p n
66 breq2 ⊢ m = if n ≤ p p n → B ≤ m ↔ B ≤ if n ≤ p p n
67 66 imbi2d ⊢ m = if n ≤ p p n → c ≤ x → B ≤ m ↔ c ≤ x → B ≤ if n ≤ p p n
68 67 rexralbidv ⊢ m = if n ≤ p p n → ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ↔ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ if n ≤ p p n
69 68 rspcev ⊢ if n ≤ p p n ∈ ℝ ∧ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ if n ≤ p p n → ∃ m ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m
70 40 65 69 syl6an ⊢ φ ∧ A ⊆ ℝ ∧ n ∈ ℝ ∧ p ∈ ℝ → ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ n ∧ − B ≤ p → ∃ m ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m
71 70 rexlimdvva ⊢ φ ∧ A ⊆ ℝ → ∃ n ∈ ℝ ∃ p ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ n ∧ − B ≤ p → ∃ m ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m
72 37 71 impbid ⊢ φ ∧ A ⊆ ℝ → ∃ m ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ↔ ∃ n ∈ ℝ ∃ p ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ n ∧ − B ≤ p
73 rexanre ⊢ A ⊆ ℝ → ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ n ∧ − B ≤ p ↔ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ n ∧ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → − B ≤ p
74 73 adantl ⊢ φ ∧ A ⊆ ℝ → ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ n ∧ − B ≤ p ↔ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ n ∧ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → − B ≤ p
75 74 2rexbidv ⊢ φ ∧ A ⊆ ℝ → ∃ n ∈ ℝ ∃ p ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ n ∧ − B ≤ p ↔ ∃ n ∈ ℝ ∃ p ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ n ∧ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → − B ≤ p
76 72 75 bitrd ⊢ φ ∧ A ⊆ ℝ → ∃ m ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ↔ ∃ n ∈ ℝ ∃ p ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ n ∧ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → − B ≤ p
77 reeanv ⊢ ∃ n ∈ ℝ ∃ p ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ n ∧ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → − B ≤ p ↔ ∃ n ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ n ∧ ∃ p ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → − B ≤ p
78 76 77 bitrdi ⊢ φ ∧ A ⊆ ℝ → ∃ m ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ↔ ∃ n ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ n ∧ ∃ p ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → − B ≤ p
79 rexcom ⊢ ∃ c ∈ ℝ ∃ m ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ↔ ∃ m ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m
80 rexcom ⊢ ∃ c ∈ ℝ ∃ n ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ n ↔ ∃ n ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ n
81 rexcom ⊢ ∃ c ∈ ℝ ∃ p ∈ ℝ ∀ x ∈ A c ≤ x → − B ≤ p ↔ ∃ p ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → − B ≤ p
82 80 81 anbi12i ⊢ ∃ c ∈ ℝ ∃ n ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ n ∧ ∃ c ∈ ℝ ∃ p ∈ ℝ ∀ x ∈ A c ≤ x → − B ≤ p ↔ ∃ n ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ n ∧ ∃ p ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → − B ≤ p
83 78 79 82 3bitr4g ⊢ φ ∧ A ⊆ ℝ → ∃ c ∈ ℝ ∃ m ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ↔ ∃ c ∈ ℝ ∃ n ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ n ∧ ∃ c ∈ ℝ ∃ p ∈ ℝ ∀ x ∈ A c ≤ x → − B ≤ p
84 simpr ⊢ φ ∧ A ⊆ ℝ → A ⊆ ℝ
85 12 recnd ⊢ φ ∧ A ⊆ ℝ ∧ x ∈ A → B ∈ ℂ
86 84 85 elo1mpt ⊢ φ ∧ A ⊆ ℝ → x ∈ A ⟼ B ∈ 𝑂⁡1 ↔ ∃ c ∈ ℝ ∃ m ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m
87 84 12 ello1mpt ⊢ φ ∧ A ⊆ ℝ → x ∈ A ⟼ B ∈ ≤𝑂⁡1 ↔ ∃ c ∈ ℝ ∃ n ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ n
88 12 renegcld ⊢ φ ∧ A ⊆ ℝ ∧ x ∈ A → − B ∈ ℝ
89 84 88 ello1mpt ⊢ φ ∧ A ⊆ ℝ → x ∈ A ⟼ − B ∈ ≤𝑂⁡1 ↔ ∃ c ∈ ℝ ∃ p ∈ ℝ ∀ x ∈ A c ≤ x → − B ≤ p
90 87 89 anbi12d ⊢ φ ∧ A ⊆ ℝ → x ∈ A ⟼ B ∈ ≤𝑂⁡1 ∧ x ∈ A ⟼ − B ∈ ≤𝑂⁡1 ↔ ∃ c ∈ ℝ ∃ n ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ n ∧ ∃ c ∈ ℝ ∃ p ∈ ℝ ∀ x ∈ A c ≤ x → − B ≤ p
91 83 86 90 3bitr4d ⊢ φ ∧ A ⊆ ℝ → x ∈ A ⟼ B ∈ 𝑂⁡1 ↔ x ∈ A ⟼ B ∈ ≤𝑂⁡1 ∧ x ∈ A ⟼ − B ∈ ≤𝑂⁡1
92 91 ex ⊢ φ → A ⊆ ℝ → x ∈ A ⟼ B ∈ 𝑂⁡1 ↔ x ∈ A ⟼ B ∈ ≤𝑂⁡1 ∧ x ∈ A ⟼ − B ∈ ≤𝑂⁡1
93 10 92 sylbid ⊢ φ → dom ⁡ x ∈ A ⟼ B ⊆ ℝ → x ∈ A ⟼ B ∈ 𝑂⁡1 ↔ x ∈ A ⟼ B ∈ ≤𝑂⁡1 ∧ x ∈ A ⟼ − B ∈ ≤𝑂⁡1
94 3 6 93 pm5.21ndd ⊢ φ → x ∈ A ⟼ B ∈ 𝑂⁡1 ↔ x ∈ A ⟼ B ∈ ≤𝑂⁡1 ∧ x ∈ A ⟼ − B ∈ ≤𝑂⁡1