This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database REAL AND COMPLEX NUMBERS Elementary limits and convergence Limits 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