Metamath Proof Explorer

Theorem o1sub

Description: The difference 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 o1sub ⊢F∈𝑂⁡1∧G∈𝑂⁡1→F−fG∈𝑂⁡1

Proof

Step Hyp Ref Expression
1 readdcl ⊢x∈ℝ∧y∈ℝ→x+y∈ℝ
2 subcl ⊢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 subcld ⊢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 abs2dif2d ⊢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−fG∈𝑂⁡1