# Metamath Proof Explorer

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 ${⊢}\left({F}\in 𝑂\left(1\right)\wedge {G}\in 𝑂\left(1\right)\right)\to {F}{+}_{f}{G}\in 𝑂\left(1\right)$

### Proof

Step Hyp Ref Expression
1 readdcl ${⊢}\left({x}\in ℝ\wedge {y}\in ℝ\right)\to {x}+{y}\in ℝ$
2 addcl ${⊢}\left({m}\in ℂ\wedge {n}\in ℂ\right)\to {m}+{n}\in ℂ$
3 simp2l ${⊢}\left(\left({x}\in ℝ\wedge {y}\in ℝ\right)\wedge \left({m}\in ℂ\wedge {n}\in ℂ\right)\wedge \left(\left|{m}\right|\le {x}\wedge \left|{n}\right|\le {y}\right)\right)\to {m}\in ℂ$
4 simp2r ${⊢}\left(\left({x}\in ℝ\wedge {y}\in ℝ\right)\wedge \left({m}\in ℂ\wedge {n}\in ℂ\right)\wedge \left(\left|{m}\right|\le {x}\wedge \left|{n}\right|\le {y}\right)\right)\to {n}\in ℂ$
5 3 4 addcld ${⊢}\left(\left({x}\in ℝ\wedge {y}\in ℝ\right)\wedge \left({m}\in ℂ\wedge {n}\in ℂ\right)\wedge \left(\left|{m}\right|\le {x}\wedge \left|{n}\right|\le {y}\right)\right)\to {m}+{n}\in ℂ$
6 5 abscld ${⊢}\left(\left({x}\in ℝ\wedge {y}\in ℝ\right)\wedge \left({m}\in ℂ\wedge {n}\in ℂ\right)\wedge \left(\left|{m}\right|\le {x}\wedge \left|{n}\right|\le {y}\right)\right)\to \left|{m}+{n}\right|\in ℝ$
7 3 abscld ${⊢}\left(\left({x}\in ℝ\wedge {y}\in ℝ\right)\wedge \left({m}\in ℂ\wedge {n}\in ℂ\right)\wedge \left(\left|{m}\right|\le {x}\wedge \left|{n}\right|\le {y}\right)\right)\to \left|{m}\right|\in ℝ$
8 4 abscld ${⊢}\left(\left({x}\in ℝ\wedge {y}\in ℝ\right)\wedge \left({m}\in ℂ\wedge {n}\in ℂ\right)\wedge \left(\left|{m}\right|\le {x}\wedge \left|{n}\right|\le {y}\right)\right)\to \left|{n}\right|\in ℝ$
9 7 8 readdcld ${⊢}\left(\left({x}\in ℝ\wedge {y}\in ℝ\right)\wedge \left({m}\in ℂ\wedge {n}\in ℂ\right)\wedge \left(\left|{m}\right|\le {x}\wedge \left|{n}\right|\le {y}\right)\right)\to \left|{m}\right|+\left|{n}\right|\in ℝ$
10 simp1l ${⊢}\left(\left({x}\in ℝ\wedge {y}\in ℝ\right)\wedge \left({m}\in ℂ\wedge {n}\in ℂ\right)\wedge \left(\left|{m}\right|\le {x}\wedge \left|{n}\right|\le {y}\right)\right)\to {x}\in ℝ$
11 simp1r ${⊢}\left(\left({x}\in ℝ\wedge {y}\in ℝ\right)\wedge \left({m}\in ℂ\wedge {n}\in ℂ\right)\wedge \left(\left|{m}\right|\le {x}\wedge \left|{n}\right|\le {y}\right)\right)\to {y}\in ℝ$
12 10 11 readdcld ${⊢}\left(\left({x}\in ℝ\wedge {y}\in ℝ\right)\wedge \left({m}\in ℂ\wedge {n}\in ℂ\right)\wedge \left(\left|{m}\right|\le {x}\wedge \left|{n}\right|\le {y}\right)\right)\to {x}+{y}\in ℝ$
13 3 4 abstrid ${⊢}\left(\left({x}\in ℝ\wedge {y}\in ℝ\right)\wedge \left({m}\in ℂ\wedge {n}\in ℂ\right)\wedge \left(\left|{m}\right|\le {x}\wedge \left|{n}\right|\le {y}\right)\right)\to \left|{m}+{n}\right|\le \left|{m}\right|+\left|{n}\right|$
14 simp3l ${⊢}\left(\left({x}\in ℝ\wedge {y}\in ℝ\right)\wedge \left({m}\in ℂ\wedge {n}\in ℂ\right)\wedge \left(\left|{m}\right|\le {x}\wedge \left|{n}\right|\le {y}\right)\right)\to \left|{m}\right|\le {x}$
15 simp3r ${⊢}\left(\left({x}\in ℝ\wedge {y}\in ℝ\right)\wedge \left({m}\in ℂ\wedge {n}\in ℂ\right)\wedge \left(\left|{m}\right|\le {x}\wedge \left|{n}\right|\le {y}\right)\right)\to \left|{n}\right|\le {y}$
16 7 8 10 11 14 15 le2addd ${⊢}\left(\left({x}\in ℝ\wedge {y}\in ℝ\right)\wedge \left({m}\in ℂ\wedge {n}\in ℂ\right)\wedge \left(\left|{m}\right|\le {x}\wedge \left|{n}\right|\le {y}\right)\right)\to \left|{m}\right|+\left|{n}\right|\le {x}+{y}$
17 6 9 12 13 16 letrd ${⊢}\left(\left({x}\in ℝ\wedge {y}\in ℝ\right)\wedge \left({m}\in ℂ\wedge {n}\in ℂ\right)\wedge \left(\left|{m}\right|\le {x}\wedge \left|{n}\right|\le {y}\right)\right)\to \left|{m}+{n}\right|\le {x}+{y}$
18 17 3expia ${⊢}\left(\left({x}\in ℝ\wedge {y}\in ℝ\right)\wedge \left({m}\in ℂ\wedge {n}\in ℂ\right)\right)\to \left(\left(\left|{m}\right|\le {x}\wedge \left|{n}\right|\le {y}\right)\to \left|{m}+{n}\right|\le {x}+{y}\right)$
19 1 2 18 o1of2 ${⊢}\left({F}\in 𝑂\left(1\right)\wedge {G}\in 𝑂\left(1\right)\right)\to {F}{+}_{f}{G}\in 𝑂\left(1\right)$