Metamath Proof Explorer

Theorem o1le

Description: Transfer eventual boundedness from a larger function to a smaller function. (Contributed by Mario Carneiro, 25-Sep-2014) (Proof shortened by Mario Carneiro, 26-May-2016)

		Ref	Expression
	Hypotheses	o1le.1	$⊢ φ \to M \in ℝ$
		o1le.2	$⊢ φ \to (x \in A ⟼ B) \in 𝑂 (1)$
		o1le.3	$⊢ (φ \land x \in A) \to B \in V$
		o1le.4	$⊢ (φ \land x \in A) \to C \in ℂ$
		o1le.5	$⊢ (φ \land (x \in A \land M \leq x)) \to \|C\| \leq \|B\|$
	Assertion	o1le	$⊢ φ \to (x \in A ⟼ C) \in 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		o1le.1	$⊢ φ \to M \in ℝ$
2		o1le.2	$⊢ φ \to (x \in A ⟼ B) \in 𝑂 (1)$
3		o1le.3	$⊢ (φ \land x \in A) \to B \in V$
4		o1le.4	$⊢ (φ \land x \in A) \to C \in ℂ$
5		o1le.5	$⊢ (φ \land (x \in A \land M \leq x)) \to \|C\| \leq \|B\|$
6	3 2	o1mptrcl	$⊢ (φ \land x \in A) \to B \in ℂ$
7	6	lo1o12	$⊢ φ \to ((x \in A ⟼ B) \in 𝑂 (1) \leftrightarrow (x \in A ⟼ \|B\|) \in \leq 𝑂 (1))$
8	2 7	mpbid	$⊢ φ \to (x \in A ⟼ \|B\|) \in \leq 𝑂 (1)$
9		fvexd	$⊢ (φ \land x \in A) \to \|B\| \in V$
10	4	abscld	$⊢ (φ \land x \in A) \to \|C\| \in ℝ$
11	1 8 9 10 5	lo1le	$⊢ φ \to (x \in A ⟼ \|C\|) \in \leq 𝑂 (1)$
12	4	lo1o12	$⊢ φ \to ((x \in A ⟼ C) \in 𝑂 (1) \leftrightarrow (x \in A ⟼ \|C\|) \in \leq 𝑂 (1))$
13	11 12	mpbird	$⊢ φ \to (x \in A ⟼ C) \in 𝑂 (1)$