# 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 × f G ∈ 𝑂⁡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 × f G ∈ 𝑂⁡1$