Theorem lo1mul2

Description: The product of an eventually upper bounded function and a positive eventually upper bounded function is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016)

	Ref	Expression
Hypotheses	o1add2.1	$$⊢\left(\phi \wedge x\in A\right)\to B\in V$$
	o1add2.2	$$⊢\left(\phi \wedge x\in A\right)\to C\in V$$
	lo1add.3	$$⊢\phi \to \left(x\in A⟼B\right)\in \le 𝑂\left(1\right)$$
	lo1add.4	$$⊢\phi \to \left(x\in A⟼C\right)\in \le 𝑂\left(1\right)$$
	lo1mul.5	$$⊢\left(\phi \wedge x\in A\right)\to 0\le B$$
Assertion	lo1mul2	$$⊢\phi \to \left(x\in A⟼CB\right)\in \le 𝑂\left(1\right)$$

Proof

Step	Hyp	Ref	Expression
1		o1add2.1	$$⊢\left(\phi \wedge x\in A\right)\to B\in V$$
2		o1add2.2	$$⊢\left(\phi \wedge x\in A\right)\to C\in V$$
3		lo1add.3	$$⊢\phi \to \left(x\in A⟼B\right)\in \le 𝑂\left(1\right)$$
4		lo1add.4	$$⊢\phi \to \left(x\in A⟼C\right)\in \le 𝑂\left(1\right)$$
5		lo1mul.5	$$⊢\left(\phi \wedge x\in A\right)\to 0\le B$$
6	2 4	lo1mptrcl	$$⊢\left(\phi \wedge x\in A\right)\to C\in ℝ$$
7	6	recnd	$$⊢\left(\phi \wedge x\in A\right)\to C\in ℂ$$
8	1 3	lo1mptrcl	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℝ$$
9	8	recnd	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℂ$$
10	7 9	mulcomd	$$⊢\left(\phi \wedge x\in A\right)\to CB=BC$$
11	10	mpteq2dva	$$⊢\phi \to \left(x\in A⟼CB\right)=\left(x\in A⟼BC\right)$$
12	1 2 3 4 5	lo1mul	$$⊢\phi \to \left(x\in A⟼BC\right)\in \le 𝑂\left(1\right)$$
13	11 12	eqeltrd	$$⊢\phi \to \left(x\in A⟼CB\right)\in \le 𝑂\left(1\right)$$