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 ( ( 𝜑𝑥𝐴 ) → 𝐵𝑉 )
o1add2.2 ( ( 𝜑𝑥𝐴 ) → 𝐶𝑉 )
lo1add.3 ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ ≤𝑂(1) )
lo1add.4 ( 𝜑 → ( 𝑥𝐴𝐶 ) ∈ ≤𝑂(1) )
lo1mul.5 ( ( 𝜑𝑥𝐴 ) → 0 ≤ 𝐵 )
Assertion lo1mul2 ( 𝜑 → ( 𝑥𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∈ ≤𝑂(1) )

Proof

Step Hyp Ref Expression
1 o1add2.1 ( ( 𝜑𝑥𝐴 ) → 𝐵𝑉 )
2 o1add2.2 ( ( 𝜑𝑥𝐴 ) → 𝐶𝑉 )
3 lo1add.3 ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ ≤𝑂(1) )
4 lo1add.4 ( 𝜑 → ( 𝑥𝐴𝐶 ) ∈ ≤𝑂(1) )
5 lo1mul.5 ( ( 𝜑𝑥𝐴 ) → 0 ≤ 𝐵 )
6 2 4 lo1mptrcl ( ( 𝜑𝑥𝐴 ) → 𝐶 ∈ ℝ )
7 6 recnd ( ( 𝜑𝑥𝐴 ) → 𝐶 ∈ ℂ )
8 1 3 lo1mptrcl ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℝ )
9 8 recnd ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℂ )
10 7 9 mulcomd ( ( 𝜑𝑥𝐴 ) → ( 𝐶 · 𝐵 ) = ( 𝐵 · 𝐶 ) )
11 10 mpteq2dva ( 𝜑 → ( 𝑥𝐴 ↦ ( 𝐶 · 𝐵 ) ) = ( 𝑥𝐴 ↦ ( 𝐵 · 𝐶 ) ) )
12 1 2 3 4 5 lo1mul ( 𝜑 → ( 𝑥𝐴 ↦ ( 𝐵 · 𝐶 ) ) ∈ ≤𝑂(1) )
13 11 12 eqeltrd ( 𝜑 → ( 𝑥𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∈ ≤𝑂(1) )