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∈MN
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∈MN
7 elicc2 ⊢M∈ℝ∧N∈ℝ→B∈MN↔B∈ℝ∧M≤B∧B≤N
8 4 5 7 syl2anc ⊢φ→B∈MN↔B∈ℝ∧M≤B∧B≤N
9 8 adantr ⊢φ∧x∈A∧C≤x→B∈MN↔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