Metamath Proof Explorer

Theorem o1lo12

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

Ref Expression
Hypotheses o1lo1.1 ⊢ φ ∧ x ∈ A → B ∈ ℝ
o1lo12.2 ⊢ φ → M ∈ ℝ
o1lo12.3 ⊢ φ ∧ x ∈ A → M ≤ B
Assertion o1lo12 ⊢ φ → x ∈ A ⟼ B ∈ 𝑂⁡1 ↔ x ∈ A ⟼ B ∈ ≤𝑂⁡1

Proof

Step Hyp Ref Expression
1 o1lo1.1 ⊢ φ ∧ x ∈ A → B ∈ ℝ
2 o1lo12.2 ⊢ φ → M ∈ ℝ
3 o1lo12.3 ⊢ φ ∧ x ∈ A → M ≤ B
4 o1dm ⊢ x ∈ A ⟼ B ∈ 𝑂⁡1 → dom ⁡ x ∈ A ⟼ B ⊆ ℝ
5 4 a1i ⊢ φ → x ∈ A ⟼ B ∈ 𝑂⁡1 → dom ⁡ x ∈ A ⟼ B ⊆ ℝ
6 lo1dm ⊢ x ∈ A ⟼ B ∈ ≤𝑂⁡1 → dom ⁡ x ∈ A ⟼ B ⊆ ℝ
7 6 a1i ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1 → dom ⁡ x ∈ A ⟼ B ⊆ ℝ
8 1 ralrimiva ⊢ φ → ∀ x ∈ A B ∈ ℝ
9 dmmptg ⊢ ∀ x ∈ A B ∈ ℝ → dom ⁡ x ∈ A ⟼ B = A
10 8 9 syl ⊢ φ → dom ⁡ x ∈ A ⟼ B = A
11 10 sseq1d ⊢ φ → dom ⁡ x ∈ A ⟼ B ⊆ ℝ ↔ A ⊆ ℝ
12 simpr ⊢ φ ∧ A ⊆ ℝ → A ⊆ ℝ
13 1 renegcld ⊢ φ ∧ x ∈ A → − B ∈ ℝ
14 13 adantlr ⊢ φ ∧ A ⊆ ℝ ∧ x ∈ A → − B ∈ ℝ
15 2 adantr ⊢ φ ∧ A ⊆ ℝ → M ∈ ℝ
16 15 renegcld ⊢ φ ∧ A ⊆ ℝ → − M ∈ ℝ
17 2 adantr ⊢ φ ∧ x ∈ A → M ∈ ℝ
18 17 1 lenegd ⊢ φ ∧ x ∈ A → M ≤ B ↔ − B ≤ − M
19 3 18 mpbid ⊢ φ ∧ x ∈ A → − B ≤ − M
20 19 ad2ant2r ⊢ φ ∧ A ⊆ ℝ ∧ x ∈ A ∧ M ≤ x → − B ≤ − M
21 12 14 15 16 20 ello1d ⊢ φ ∧ A ⊆ ℝ → x ∈ A ⟼ − B ∈ ≤𝑂⁡1
22 1 o1lo1 ⊢ φ → x ∈ A ⟼ B ∈ 𝑂⁡1 ↔ x ∈ A ⟼ B ∈ ≤𝑂⁡1 ∧ x ∈ A ⟼ − B ∈ ≤𝑂⁡1
23 22 rbaibd ⊢ φ ∧ x ∈ A ⟼ − B ∈ ≤𝑂⁡1 → x ∈ A ⟼ B ∈ 𝑂⁡1 ↔ x ∈ A ⟼ B ∈ ≤𝑂⁡1
24 21 23 syldan ⊢ φ ∧ A ⊆ ℝ → x ∈ A ⟼ B ∈ 𝑂⁡1 ↔ x ∈ A ⟼ B ∈ ≤𝑂⁡1
25 24 ex ⊢ φ → A ⊆ ℝ → x ∈ A ⟼ B ∈ 𝑂⁡1 ↔ x ∈ A ⟼ B ∈ ≤𝑂⁡1
26 11 25 sylbid ⊢ φ → dom ⁡ x ∈ A ⟼ B ⊆ ℝ → x ∈ A ⟼ B ∈ 𝑂⁡1 ↔ x ∈ A ⟼ B ∈ ≤𝑂⁡1
27 5 7 26 pm5.21ndd ⊢ φ → x ∈ A ⟼ B ∈ 𝑂⁡1 ↔ x ∈ A ⟼ B ∈ ≤𝑂⁡1