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) )

Metamath Proof Explorer

Theorem icco1

Proof