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 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
icco1.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
icco1.3 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
icco1.4 ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
icco1.5 ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
icco1.6 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐶 ≤ 𝑥 ) ) → 𝐵 ∈ ( 𝑀 [,] 𝑁 ) )
Assertion icco1 ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) )

Proof

Step Hyp Ref Expression
1 icco1.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2 icco1.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
3 icco1.3 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4 icco1.4 ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
5 icco1.5 ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
6 icco1.6 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐶 ≤ 𝑥 ) ) → 𝐵 ∈ ( 𝑀 [,] 𝑁 ) )
7 elicc2 ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝐵 ∈ ( 𝑀 [,] 𝑁 ) ↔ ( 𝐵 ∈ ℝ ∧ 𝑀 ≤ 𝐵 ∧ 𝐵 ≤ 𝑁 ) ) )
8 4 5 7 syl2anc ⊢ ( 𝜑 → ( 𝐵 ∈ ( 𝑀 [,] 𝑁 ) ↔ ( 𝐵 ∈ ℝ ∧ 𝑀 ≤ 𝐵 ∧ 𝐵 ≤ 𝑁 ) ) )
9 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐶 ≤ 𝑥 ) ) → ( 𝐵 ∈ ( 𝑀 [,] 𝑁 ) ↔ ( 𝐵 ∈ ℝ ∧ 𝑀 ≤ 𝐵 ∧ 𝐵 ≤ 𝑁 ) ) )
10 6 9 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐶 ≤ 𝑥 ) ) → ( 𝐵 ∈ ℝ ∧ 𝑀 ≤ 𝐵 ∧ 𝐵 ≤ 𝑁 ) )
11 10 simp3d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐶 ≤ 𝑥 ) ) → 𝐵 ≤ 𝑁 )
12 1 2 3 5 11 ello1d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) )
13 2 renegcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - 𝐵 ∈ ℝ )
14 4 renegcld ⊢ ( 𝜑 → - 𝑀 ∈ ℝ )
15 10 simp2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐶 ≤ 𝑥 ) ) → 𝑀 ≤ 𝐵 )
16 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐶 ≤ 𝑥 ) ) → 𝑀 ∈ ℝ )
17 2 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐶 ≤ 𝑥 ) ) → 𝐵 ∈ ℝ )
18 16 17 lenegd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐶 ≤ 𝑥 ) ) → ( 𝑀 ≤ 𝐵 ↔ - 𝐵 ≤ - 𝑀 ) )
19 15 18 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐶 ≤ 𝑥 ) ) → - 𝐵 ≤ - 𝑀 )
20 1 13 3 14 19 ello1d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ∈ ≤𝑂(1) )
21 2 o1lo1 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ∧ ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ∈ ≤𝑂(1) ) ) )
22 12 20 21 mpbir2and ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) )