By definition of asymptotic positivity, there exists an \(x\_ 0\) such that \(f(x) {\gt} 0\) for all \(x {\gt} x\_ 0\). It follows that \(-f(x) {\gt} 0\), which is what is needed.

By definition of asymptotic negativity, there exists an \(x\_ 0\) such that \(f(x) {\lt} 0\) for all \(x {\gt} x\_ 0\). It follows that \(-f(x) {\lt} 0\), which is what is needed.

Assume with no loss of generality that \(f(x) {\gt} 0\) for all \(x {\gt} x\_ 0\) and that \(f(y) \le g(y)\) for all \(y {\gt} y\_ 0\). Let \(z\_ 0 = \max \{ x\_ 0, y\_ 0 \} \). By transitivity of the inequality relations, we have \(g(z) {\gt} 0\) for all \(z {\gt} z\_ 0\).

Assume with no loss of generality that \(g(x) {\lt} 0\) for all \(x {\gt} x\_ 0\) and that \(f(y) \le g(y)\) for all \(y {\gt} y\_ 0\). Let \(z\_ 0 = \max \{ x\_ 0, y\_ 0 \} \). By transitivity of the inequality relations, we have \(f(z) {\lt} 0\) for all \(z {\gt} z\_ 0\).

By Lemma 17, this statement is equivalent to Lemma 9.

By Theorem 17, this statement is equivalent to Lemma 10.

By reflexivity of \(\le \), we have \(f(x) \le f(x)\) for any given \(x\).

By reflexivity of \(\ge \), we have \(f(x) \ge f(x)\) for any given \(x\).

Since \(f(x) \le g(x)\) for all \(x {\gt} x\_ 0\), we have \(g(x) \ge f(x)\).

Since \(f(x) \ge g(x)\) for all \(x {\gt} x\_ 0\), we have \(g(x) \le f(x)\).

Lemma 15 and Lemma 16 are both directions respectively.

By assumption, \(f(x) \le g(x)\) for all \(x \ge x\_ 0\) and \(g(y) \le h(y)\) for all \(y \ge y\_ 0\). Let \(z\_ 0 = \max \{ x\_ 0, y\_ 0 \} \). By transitivity, we have \(f(z) \le g(z)\) for all \(z \ge z\_ 0\).

By the equivalence given by Lemma 17, we can apply Lemma 18 in reverse, since \(h\) is asymptotically less than \(g\) and \(g\) is asymptotically less than \(f\).

Let \(x\_ 0\) be such that \(f\_ 1(x) \le g\_ 1(x)\) for all \(x {\gt} x\_ 0\) and let \(y\_ 0\) be such that \(f\_ 2(y) \le g\_ 2(y)\) for all \(y {\gt} y\_ 0\). Those exist due to assumptions. Now let \(z\_ 0 = \max \{ x\_ 0, y\_ 0 \} \). By transitivity, \(f\_ 1(z) \le g\_ 1(z)\) and \(f\_ 2(z) \le g\_ 2(z)\) for all \(z {\gt} z\_ 0\). By additivity, we can merge both inequalities by adding both terms on the left side and both terms on the right side. We thus get \(f\_ 1(z) + f\_ 2(z) \le g\_ 1(z) + g\_ 2(z)\), which by definition and and extensionality means that \(f\_ 1 + f\_ 2\) is asymptotically less than \(g\_ 1 + g\_ 2\).

By Theorem 17, \(g\_ 1\) and \(g\_ 2\) are asymptotically less than \(f\_ 1\) and \(f\_ 2\) respectively. It suffices to show that \(g\_ 1 + g\_ 2\) is asymptotically less than \(f\_ 1 + f\_ 2\), which is precisely the result of Lemma 20.

By definition, there exists some \(x\_ 0\) such that \(f\_ 1(x) {\gt} 0\) for all \(x {\gt} x\_ 0\). We also have \(f\_ 2(y) \ge g(y)\) for all \(y {\gt} y\_ 0\) for some \(y\_ 0\). Let \(z\_ 0 = \max \{ x\_ 0, y\_ 0, \} \). We now have, for all \(z {\gt} z\_ 0\) both \(f\_ 1(z) {\gt} 0\) and \(f\_ 2(z) \ge g(z)\). By additivity, we have \(f\_ 1(z) + f\_ 2(z) \ge g(z)\).

By definition, there exists some \(x\_ 0\) such that \(f\_ 1(x) {\lt} 0\) for all \(x {\gt} x\_ 0\). We also have \(f\_ 2(y) \le g(y)\) for all \(y {\gt} y\_ 0\) for some \(y\_ 0\). Let \(z\_ 0 = \max \{ x\_ 0, y\_ 0, \} \). We now have, for all \(z {\gt} z\_ 0\) both \(f\_ 1(z) {\lt} 0\) and \(f\_ 2(z) \le g(z)\). By additivity, we have \(f\_ 1(z) + f\_ 2(z) \le g(z)\).

This is a simple consequence of scalar multiplication by a positive constant.

By applying Theorem 17, the proof boils down to proving that \(c \cdot g\) is asymptotically less than \(c \cdot f\), which is precisely shown by Lemma 24.

This is a simple consequence of the fact that if \(f(x) \le g(x)\), then for a \(c {\lt} 0\) we have \(c \cdot f(x) \ge c \cdot g(x)\).

Similar to above, the proof is a direct application of Theorem 17 and Lemma 26.

Asymptotic properties give constants \(x\_ i, 0 \le i \le 3\), above which each property holds. We take \(x_M = \max _{0 \le i \le 3} x_i\) as the constant of the needed property. For all \(x {\gt} x_M\), all given asymptotic properties hold, so the wanted property holds by properties of the inequality relation.

Analogously to above, the proof comes from taking the maximum of asymptotic constants as the asymptotic lower bound for nonpositivity. This time, however, the inequality flips due to nonpositive terms in \(f\_ 1(n) * f\_ 2(n) \le g\_ 1(n) * g\_ 2(n)\), since \(n\) is larger than all of the asymptotic lower bounds.