This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
rlimeq.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
rlimeq.3 ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
rlimeq.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐷 ≤ 𝑥 ) ) → 𝐵 = 𝐶 )
Assertion o1eq ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝑂(1) ) )

Proof

Step Hyp Ref Expression
1 rlimeq.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
2 rlimeq.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
3 rlimeq.3 ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
4 rlimeq.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐷 ≤ 𝑥 ) ) → 𝐵 = 𝐶 )
5 1 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ 𝐵 ) ∈ ℝ )
6 2 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ 𝐶 ) ∈ ℝ )
7 4 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐷 ≤ 𝑥 ) ) → ( abs ‘ 𝐵 ) = ( abs ‘ 𝐶 ) )
8 5 6 3 7 lo1eq ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ ≤𝑂(1) ↔ ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ 𝐶 ) ) ∈ ≤𝑂(1) ) )
9 1 lo1o12 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ ≤𝑂(1) ) )
10 2 lo1o12 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ 𝐶 ) ) ∈ ≤𝑂(1) ) )
11 8 9 10 3bitr4d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝑂(1) ) )