Metamath Proof Explorer

Theorem o1add

Description: The sum 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 o1add ⊢ F ∈ 𝑂⁡1 ∧ G ∈ 𝑂⁡1 → F + f G ∈ 𝑂⁡1

Proof

Step Hyp Ref Expression
1 readdcl ⊢ x ∈ ℝ ∧ y ∈ ℝ → x + y ∈ ℝ
2 addcl ⊢ m ∈ ℂ ∧ n ∈ ℂ → m + n ∈ ℂ
3 simp2l ⊢ x ∈ ℝ ∧ y ∈ ℝ ∧ m ∈ ℂ ∧ n ∈ ℂ ∧ m ≤ x ∧ n ≤ y → m ∈ ℂ
4 simp2r ⊢ x ∈ ℝ ∧ y ∈ ℝ ∧ m ∈ ℂ ∧ n ∈ ℂ ∧ m ≤ x ∧ n ≤ y → n ∈ ℂ
5 3 4 addcld ⊢ x ∈ ℝ ∧ y ∈ ℝ ∧ m ∈ ℂ ∧ n ∈ ℂ ∧ m ≤ x ∧ n ≤ y → m + n ∈ ℂ
6 5 abscld ⊢ x ∈ ℝ ∧ y ∈ ℝ ∧ m ∈ ℂ ∧ n ∈ ℂ ∧ m ≤ x ∧ n ≤ y → m + n ∈ ℝ
7 3 abscld ⊢ x ∈ ℝ ∧ y ∈ ℝ ∧ m ∈ ℂ ∧ n ∈ ℂ ∧ m ≤ x ∧ n ≤ y → m ∈ ℝ
8 4 abscld ⊢ x ∈ ℝ ∧ y ∈ ℝ ∧ m ∈ ℂ ∧ n ∈ ℂ ∧ m ≤ x ∧ n ≤ y → n ∈ ℝ
9 7 8 readdcld ⊢ x ∈ ℝ ∧ y ∈ ℝ ∧ m ∈ ℂ ∧ n ∈ ℂ ∧ m ≤ x ∧ n ≤ y → m + n ∈ ℝ
10 simp1l ⊢ x ∈ ℝ ∧ y ∈ ℝ ∧ m ∈ ℂ ∧ n ∈ ℂ ∧ m ≤ x ∧ n ≤ y → x ∈ ℝ
11 simp1r ⊢ x ∈ ℝ ∧ y ∈ ℝ ∧ m ∈ ℂ ∧ n ∈ ℂ ∧ m ≤ x ∧ n ≤ y → y ∈ ℝ
12 10 11 readdcld ⊢ x ∈ ℝ ∧ y ∈ ℝ ∧ m ∈ ℂ ∧ n ∈ ℂ ∧ m ≤ x ∧ n ≤ y → x + y ∈ ℝ
13 3 4 abstrid ⊢ x ∈ ℝ ∧ y ∈ ℝ ∧ m ∈ ℂ ∧ n ∈ ℂ ∧ m ≤ x ∧ n ≤ y → m + n ≤ m + n
14 simp3l ⊢ x ∈ ℝ ∧ y ∈ ℝ ∧ m ∈ ℂ ∧ n ∈ ℂ ∧ m ≤ x ∧ n ≤ y → m ≤ x
15 simp3r ⊢ x ∈ ℝ ∧ y ∈ ℝ ∧ m ∈ ℂ ∧ n ∈ ℂ ∧ m ≤ x ∧ n ≤ y → n ≤ y
16 7 8 10 11 14 15 le2addd ⊢ x ∈ ℝ ∧ y ∈ ℝ ∧ m ∈ ℂ ∧ n ∈ ℂ ∧ m ≤ x ∧ n ≤ y → m + n ≤ x + y
17 6 9 12 13 16 letrd ⊢ x ∈ ℝ ∧ y ∈ ℝ ∧ m ∈ ℂ ∧ n ∈ ℂ ∧ m ≤ x ∧ n ≤ y → m + n ≤ x + y
18 17 3expia ⊢ x ∈ ℝ ∧ y ∈ ℝ ∧ m ∈ ℂ ∧ n ∈ ℂ → m ≤ x ∧ n ≤ y → m + n ≤ x + y
19 1 2 18 o1of2 ⊢ F ∈ 𝑂⁡1 ∧ G ∈ 𝑂⁡1 → F + f G ∈ 𝑂⁡1