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 ⊢ φ ∧ x ∈ A → B ∈ V
o1add2.2 ⊢ φ ∧ x ∈ A → C ∈ V
lo1add.3 ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1
lo1add.4 ⊢ φ → x ∈ A ⟼ C ∈ ≤𝑂⁡1
lo1mul.5 ⊢ φ ∧ x ∈ A → 0 ≤ B
Assertion lo1mul2 ⊢ φ → x ∈ A ⟼ C ⁢ B ∈ ≤𝑂⁡1

Proof

Step Hyp Ref Expression
1 o1add2.1 ⊢ φ ∧ x ∈ A → B ∈ V
2 o1add2.2 ⊢ φ ∧ x ∈ A → C ∈ V
3 lo1add.3 ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1
4 lo1add.4 ⊢ φ → x ∈ A ⟼ C ∈ ≤𝑂⁡1
5 lo1mul.5 ⊢ φ ∧ x ∈ A → 0 ≤ B
6 2 4 lo1mptrcl ⊢ φ ∧ x ∈ A → C ∈ ℝ
7 6 recnd ⊢ φ ∧ x ∈ A → C ∈ ℂ
8 1 3 lo1mptrcl ⊢ φ ∧ x ∈ A → B ∈ ℝ
9 8 recnd ⊢ φ ∧ x ∈ A → B ∈ ℂ
10 7 9 mulcomd ⊢ φ ∧ x ∈ A → C ⁢ B = B ⁢ C
11 10 mpteq2dva ⊢ φ → x ∈ A ⟼ C ⁢ B = x ∈ A ⟼ B ⁢ C
12 1 2 3 4 5 lo1mul ⊢ φ → x ∈ A ⟼ B ⁢ C ∈ ≤𝑂⁡1
13 11 12 eqeltrd ⊢ φ → x ∈ A ⟼ C ⁢ B ∈ ≤𝑂⁡1