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