Metamath Proof Explorer

Theorem o1eq

Description: Two functions that are eventually equal to one another are eventually bounded if one of them is. (Contributed by Mario Carneiro, 26-May-2016)

Ref Expression
Hypotheses rlimeq.1 ⊢ φ ∧ x ∈ A → B ∈ ℂ
rlimeq.2 ⊢ φ ∧ x ∈ A → C ∈ ℂ
rlimeq.3 ⊢ φ → D ∈ ℝ
rlimeq.4 ⊢ φ ∧ x ∈ A ∧ D ≤ x → B = C
Assertion o1eq ⊢ φ → x ∈ A ⟼ B ∈ 𝑂⁡1 ↔ x ∈ A ⟼ C ∈ 𝑂⁡1

Proof

Step Hyp Ref Expression
1 rlimeq.1 ⊢ φ ∧ x ∈ A → B ∈ ℂ
2 rlimeq.2 ⊢ φ ∧ x ∈ A → C ∈ ℂ
3 rlimeq.3 ⊢ φ → D ∈ ℝ
4 rlimeq.4 ⊢ φ ∧ x ∈ A ∧ D ≤ x → B = C
5 1 abscld ⊢ φ ∧ x ∈ A → B ∈ ℝ
6 2 abscld ⊢ φ ∧ x ∈ A → C ∈ ℝ
7 4 fveq2d ⊢ φ ∧ x ∈ A ∧ D ≤ x → B = C
8 5 6 3 7 lo1eq ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1 ↔ x ∈ A ⟼ C ∈ ≤𝑂⁡1
9 1 lo1o12 ⊢ φ → x ∈ A ⟼ B ∈ 𝑂⁡1 ↔ x ∈ A ⟼ B ∈ ≤𝑂⁡1
10 2 lo1o12 ⊢ φ → x ∈ A ⟼ C ∈ 𝑂⁡1 ↔ x ∈ A ⟼ C ∈ ≤𝑂⁡1
11 8 9 10 3bitr4d ⊢ φ → x ∈ A ⟼ B ∈ 𝑂⁡1 ↔ x ∈ A ⟼ C ∈ 𝑂⁡1