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

Metamath Proof Explorer

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) )