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	$⊢ (φ \land x \in A) \to B \in ℂ$
		rlimeq.2	$⊢ (φ \land x \in A) \to C \in ℂ$
		rlimeq.3	$⊢ φ \to D \in ℝ$
		rlimeq.4	$⊢ (φ \land (x \in A \land D \leq x)) \to B = C$
	Assertion	o1eq	$⊢ φ \to ((x \in A ⟼ B) \in 𝑂 (1) \leftrightarrow (x \in A ⟼ C) \in 𝑂 (1))$

Proof

Step	Hyp	Ref	Expression
1		rlimeq.1	$⊢ (φ \land x \in A) \to B \in ℂ$
2		rlimeq.2	$⊢ (φ \land x \in A) \to C \in ℂ$
3		rlimeq.3	$⊢ φ \to D \in ℝ$
4		rlimeq.4	$⊢ (φ \land (x \in A \land D \leq x)) \to B = C$
5	1	abscld	$⊢ (φ \land x \in A) \to \|B\| \in ℝ$
6	2	abscld	$⊢ (φ \land x \in A) \to \|C\| \in ℝ$
7	4	fveq2d	$⊢ (φ \land (x \in A \land D \leq x)) \to \|B\| = \|C\|$
8	5 6 3 7	lo1eq	$⊢ φ \to ((x \in A ⟼ \|B\|) \in \leq 𝑂 (1) \leftrightarrow (x \in A ⟼ \|C\|) \in \leq 𝑂 (1))$
9	1	lo1o12	$⊢ φ \to ((x \in A ⟼ B) \in 𝑂 (1) \leftrightarrow (x \in A ⟼ \|B\|) \in \leq 𝑂 (1))$
10	2	lo1o12	$⊢ φ \to ((x \in A ⟼ C) \in 𝑂 (1) \leftrightarrow (x \in A ⟼ \|C\|) \in \leq 𝑂 (1))$
11	8 9 10	3bitr4d	$⊢ φ \to ((x \in A ⟼ B) \in 𝑂 (1) \leftrightarrow (x \in A ⟼ C) \in 𝑂 (1))$