Shape of Secant Function

Theorem

The nature of the secant function on the set of real numbers $\R$ is as follows:

$(1): \quad \sec x$ is continuous and strictly increasing on the intervals $\hointr 0 {\dfrac \pi 2}$ and $\hointl {\dfrac \pi 2} \pi$

$(2): \quad \sec x$ is continuous and strictly decreasing on the intervals $\hointr {-\pi} {-\dfrac \pi 2}$ and $\hointl {-\dfrac \pi 2} 0$

$(3): \quad \sec x \to + \infty$ as $x \to -\dfrac \pi 2^+$

$(4): \quad \sec x \to + \infty$ as $x \to \dfrac \pi 2^-$

$(5): \quad \sec x \to - \infty$ as $x \to \dfrac \pi 2^+$

$(6): \quad \sec x \to - \infty$ as $x \to \dfrac {3 \pi} 2^-$

Proof

From Derivative of Secant Function:

$\map {D_x} {\sec x} = \dfrac {\sin x} {\cos^2 x}$

From Sine and Cosine are Periodic on Reals: Corollary:

$\forall x \in \openint {-\pi} \pi \setminus \set {-\dfrac \pi 2, \dfrac \pi 2}: \cos x \ne 0$

Thus, from Square of Non-Zero Element of Ordered Integral Domain is Strictly Positive:

$\forall x \in \openint {-\pi} \pi \setminus \set {-\dfrac \pi 2, \dfrac \pi 2}: \cos^2 x > 0$

Although this article appears correct, it's inelegant. There has to be a better way of doing it.
In particular: Might need to find a less abstract-algebraic version of the above result
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by redesigning it.
To discuss this page in more detail, feel free to use the talk page.
When this work has been completed, you may remove this instance of {{Improve}} from the code.
If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.