Metamath Proof Explorer

Theorem icco1

Description: Derive eventual boundedness from separate upper and lower eventual bounds. (Contributed by Mario Carneiro, 15-Apr-2016)

Ref Expression
Hypotheses icco1.1 ⊢ φ → A ⊆ ℝ
icco1.2 ⊢ φ ∧ x ∈ A → B ∈ ℝ
icco1.3 ⊢ φ → C ∈ ℝ
icco1.4 ⊢ φ → M ∈ ℝ
icco1.5 ⊢ φ → N ∈ ℝ
icco1.6 ⊢ φ ∧ x ∈ A ∧ C ≤ x → B ∈ M N
Assertion icco1 ⊢ φ → x ∈ A ⟼ B ∈ 𝑂⁡1

Proof

Step Hyp Ref Expression
1 icco1.1 ⊢ φ → A ⊆ ℝ
2 icco1.2 ⊢ φ ∧ x ∈ A → B ∈ ℝ
3 icco1.3 ⊢ φ → C ∈ ℝ
4 icco1.4 ⊢ φ → M ∈ ℝ
5 icco1.5 ⊢ φ → N ∈ ℝ
6 icco1.6 ⊢ φ ∧ x ∈ A ∧ C ≤ x → B ∈ M N
7 elicc2 ⊢ M ∈ ℝ ∧ N ∈ ℝ → B ∈ M N ↔ B ∈ ℝ ∧ M ≤ B ∧ B ≤ N
8 4 5 7 syl2anc ⊢ φ → B ∈ M N ↔ B ∈ ℝ ∧ M ≤ B ∧ B ≤ N
9 8 adantr ⊢ φ ∧ x ∈ A ∧ C ≤ x → B ∈ M N ↔ B ∈ ℝ ∧ M ≤ B ∧ B ≤ N
10 6 9 mpbid ⊢ φ ∧ x ∈ A ∧ C ≤ x → B ∈ ℝ ∧ M ≤ B ∧ B ≤ N
11 10 simp3d ⊢ φ ∧ x ∈ A ∧ C ≤ x → B ≤ N
12 1 2 3 5 11 ello1d ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1
13 2 renegcld ⊢ φ ∧ x ∈ A → − B ∈ ℝ
14 4 renegcld ⊢ φ → − M ∈ ℝ
15 10 simp2d ⊢ φ ∧ x ∈ A ∧ C ≤ x → M ≤ B
16 4 adantr ⊢ φ ∧ x ∈ A ∧ C ≤ x → M ∈ ℝ
17 2 adantrr ⊢ φ ∧ x ∈ A ∧ C ≤ x → B ∈ ℝ
18 16 17 lenegd ⊢ φ ∧ x ∈ A ∧ C ≤ x → M ≤ B ↔ − B ≤ − M
19 15 18 mpbid ⊢ φ ∧ x ∈ A ∧ C ≤ x → − B ≤ − M
20 1 13 3 14 19 ello1d ⊢ φ → x ∈ A ⟼ − B ∈ ≤𝑂⁡1
21 2 o1lo1 ⊢ φ → x ∈ A ⟼ B ∈ 𝑂⁡1 ↔ x ∈ A ⟼ B ∈ ≤𝑂⁡1 ∧ x ∈ A ⟼ − B ∈ ≤𝑂⁡1
22 12 20 21 mpbir2and ⊢ φ → x ∈ A ⟼ B ∈ 𝑂⁡1