Metamath Proof Explorer

Theorem o1mul

Description: The product of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014) (Proof shortened by Fan Zheng, 14-Jul-2016)

Ref Expression
Assertion o1mul ⊢F∈𝑂⁡1∧G∈𝑂⁡1→F×fG∈𝑂⁡1

Proof

Step Hyp Ref Expression
1 remulcl ⊢m∈ℝ∧n∈ℝ→m⁢n∈ℝ
2 mulcl ⊢x∈ℂ∧y∈ℂ→x⁢y∈ℂ
3 simp2l ⊢m∈ℝ∧n∈ℝ∧x∈ℂ∧y∈ℂ∧x≤m∧y≤n→x∈ℂ
4 simp2r ⊢m∈ℝ∧n∈ℝ∧x∈ℂ∧y∈ℂ∧x≤m∧y≤n→y∈ℂ
5 3 4 absmuld ⊢m∈ℝ∧n∈ℝ∧x∈ℂ∧y∈ℂ∧x≤m∧y≤n→x⁢y=x⁢y
6 3 abscld ⊢m∈ℝ∧n∈ℝ∧x∈ℂ∧y∈ℂ∧x≤m∧y≤n→x∈ℝ
7 simp1l ⊢m∈ℝ∧n∈ℝ∧x∈ℂ∧y∈ℂ∧x≤m∧y≤n→m∈ℝ
8 4 abscld ⊢m∈ℝ∧n∈ℝ∧x∈ℂ∧y∈ℂ∧x≤m∧y≤n→y∈ℝ
9 simp1r ⊢m∈ℝ∧n∈ℝ∧x∈ℂ∧y∈ℂ∧x≤m∧y≤n→n∈ℝ
10 3 absge0d ⊢m∈ℝ∧n∈ℝ∧x∈ℂ∧y∈ℂ∧x≤m∧y≤n→0≤x
11 4 absge0d ⊢m∈ℝ∧n∈ℝ∧x∈ℂ∧y∈ℂ∧x≤m∧y≤n→0≤y
12 simp3l ⊢m∈ℝ∧n∈ℝ∧x∈ℂ∧y∈ℂ∧x≤m∧y≤n→x≤m
13 simp3r ⊢m∈ℝ∧n∈ℝ∧x∈ℂ∧y∈ℂ∧x≤m∧y≤n→y≤n
14 6 7 8 9 10 11 12 13 lemul12ad ⊢m∈ℝ∧n∈ℝ∧x∈ℂ∧y∈ℂ∧x≤m∧y≤n→x⁢y≤m⁢n
15 5 14 eqbrtrd ⊢m∈ℝ∧n∈ℝ∧x∈ℂ∧y∈ℂ∧x≤m∧y≤n→x⁢y≤m⁢n
16 15 3expia ⊢m∈ℝ∧n∈ℝ∧x∈ℂ∧y∈ℂ→x≤m∧y≤n→x⁢y≤m⁢n
17 1 2 16 o1of2 ⊢F∈𝑂⁡1∧G∈𝑂⁡1→F×fG∈𝑂⁡1