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 f G 𝑂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 f G 𝑂1