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	|- ( ( ph /\ x e. A ) -> B e. V )
	o1add2.2	|- ( ( ph /\ x e. A ) -> C e. V )
	lo1add.3	|- ( ph -> ( x e. A |-> B ) e. <_O(1) )
	lo1add.4	|- ( ph -> ( x e. A |-> C ) e. <_O(1) )
	lo1mul.5	|- ( ( ph /\ x e. A ) -> 0 <_ B )
Assertion	lo1mul2	|- ( ph -> ( x e. A |-> ( C x. B ) ) e. <_O(1) )

Proof

Step	Hyp	Ref	Expression
1		o1add2.1	|- ( ( ph /\ x e. A ) -> B e. V )
2		o1add2.2	|- ( ( ph /\ x e. A ) -> C e. V )
3		lo1add.3	|- ( ph -> ( x e. A |-> B ) e. <_O(1) )
4		lo1add.4	|- ( ph -> ( x e. A |-> C ) e. <_O(1) )
5		lo1mul.5	|- ( ( ph /\ x e. A ) -> 0 <_ B )
6	2 4	lo1mptrcl	|- ( ( ph /\ x e. A ) -> C e. RR )
7	6	recnd	|- ( ( ph /\ x e. A ) -> C e. CC )
8	1 3	lo1mptrcl	|- ( ( ph /\ x e. A ) -> B e. RR )
9	8	recnd	|- ( ( ph /\ x e. A ) -> B e. CC )
10	7 9	mulcomd	|- ( ( ph /\ x e. A ) -> ( C x. B ) = ( B x. C ) )
11	10	mpteq2dva	|- ( ph -> ( x e. A |-> ( C x. B ) ) = ( x e. A |-> ( B x. C ) ) )
12	1 2 3 4 5	lo1mul	|- ( ph -> ( x e. A |-> ( B x. C ) ) e. <_O(1) )
13	11 12	eqeltrd	|- ( ph -> ( x e. A |-> ( C x. B ) ) e. <_O(1) )