avewright/proofwiki-math huggingface dataset:
Theorem: Banach-Tarski Paradox

Let $\mathbb D^3 \subset \R^3$ be a unit ball in real Euclidean space of $3$ dimensions.
Then $\mathbb D^3$ is equidecomposable to the union of two such unit balls.

Proof:
=== Lemmata ===
{{:Banach-Tarski Paradox/Lemmata}}
Let $U$ denote the closed ball in real Euclidean space of $3$ dimensions defined as:
:$U = \set {\mathbf x \in \R^3 : \size {\mathbf x - \mathbf c} \le r}$
where:
:$r$ is the radius of $U$
:$\mathbf x$ is the position vector of a point $\tuple {x_1, x_2, x_3} \in \R^3$
:$\mathbf c$ is the position vector of the center $\tuple {c_1, c_2, c_3}$ of $U$
:$\size {\mathbf x - \mathbf c}$ denotes the Euclidean distance:
::$\size {\mathbf x - \mathbf c} = \sqrt { {x_1 - c_1}^2 + {x_2 - c_2}^2 + {x_3 - c_3}^2}$
Let $\Bbb S^2$ denote the sphere which is the boundary of $U$:
:$\Bbb S^2 = \set {\mathbf x \in \R^3 : \size {\mathbf x - \mathbf c} = r}$
Let:
:$(1): \quad \Bbb S^2 = A \cup B \cup C \cup Q$
be the partition of $\Bbb S^2$ from Hausdorff Paradox.
Recall:
:$A$, $B$ and $C$ are disjoint
:$A$, $B$ and $C$ are congruent to each other
:$B \cup C$ is congruent to each of $A$, $B$ and $C$
Hence {{hypothesis}}:
:$A \approx B \approx C \approx B \cup C$
For a given subset $T \subseteq \Bbb S^2$, let $\overline T \subseteq U$ be defined as the set of all $\mathbb x \in U$ apart from $\mathbf c$ whose projection onto $\Bbb S^2$ from $\mathbf c$ is $T$.
Hence using Vector Equation of Straight Line in Space:
:$\overline T = \set {\mathbf y \in U: \mathbf y = \paren {1 - s} \mathbf c + s \mathbf x: \mathbf x \in T, s \in \hointl 0 1}$
That is, for all points $\mathbf x$ in $T$, all the points in $U$ along the radius of $U$ to $\mathbf x$ but not including the center of $U$.
We have that:
:$U = \overline A \cup \overline B \cup \overline C \cup \overline Q \cup \set {\mathbb c}$
Because we have:
:$A \approx B \approx C \approx B \cup C$
it follows that:
:$(2): \quad \overline A \approx \overline B \approx \overline C \approx \overline B \cup \overline C$
Let:
{{begin-eqn}}
{{eqn | l = X
      | r = \overline A \cup \overline Q \cup \set {\mathbb c}
      | c = 
}}
{{eqn | l = Y
      | r = U \setminus X
      | c = where $\setminus$ denotes set difference
}}
{{end-eqn}}
From $(2)$ and {{Lemma|Banach-Tarski Paradox|3}}:
:$\overline A \approx \overline A \cup \overline B \cup \overline C$
and so:
:$(3): \quad X \approx U$
Let $\alpha$ be a rotation of $U$ such that $\alpha$ is not in the original $G$ that was used to construct $(1)$ with the property that:
:$Q \cap \alpha Q = \O$
Hence using:
:$\overline C \approx \overline A \cup \overline B \cup \overline C$
there exists $S \subseteq C$ such that:
:$\overline S \approx \overline Q$
Let $p$ be an arbitrary point in $\overline C \setminus \overline S$.
We have that:
:$(4): \quad \overline A \cup \overline Q \cup \set {\mathbb c} \approx \overline B \cup \overline S \cup \set p$
Because:
:$\overline B \cup \overline S \cup \set p \subseteq Y \subseteq U$
we can use $(3)$ and $(4)$ along with {{Lemma|Banach-Tarski Paradox|3}} to get:
:$Y \approx U$
Hence the result.
{{qed}}
Theorem: Equidecomposability is Equivalence Relation

The property of being equidecomposable is an equivalence relation on the power set $\powerset {\R^n}$.

Proof:
=== Relexivity ===
A set is necessarily equidecomposable with itself; the same decomposition and set of isometries suffice for $A$ as for $A$.
Theorem: Equidecomposability Unaffected by Union

{{explain|I guess the sets should be disjoint, in the sense that $S_i \cap S_j$ is empty for $i \ne j$. Similar for $T$.}}
Let $\set {S_1, \ldots, S_m}, \set {T_1, \ldots, T_m}$ be sets of sets in $\R^n$ such that:
:for each $k \in \set {1, \dots, m}, S_k$ and $T_k$ are equidecomposable. 
Then the set $\ds S = \bigcup_{i \mathop = 1}^m S_i$ is equidecomposable with $\ds T = \bigcup_{i \mathop = 1}^m T_i$.

Proof:
We have for each $k \in \set{1, \dots, m}$ a decomposition $\set {A_{k, 1}, \cdots, A_{k, l_k} }$ and set of isometries $\phi_{i, j}: \R^n \to \R^n$ such that:
:$\ds S_k = \bigcup_{a \mathop = 1}^{l_k} \map {\phi_{k, a} } {A_{k, a} }$
and similarly for $T_k$ and some isometries $\theta_{i, j}: \R^n \to \R^n$:
:$\ds T_k = \bigcup_{a \mathop = 1}^{l_k} \map {\theta_{k, a} } {A_{k, a} }$
Thus:
:$\ds S = \bigcup_{k \mathop = 1}^m \bigcup_{i \mathop = 1}^{l_k} \map {\phi_{k, i} } {A_{k, i} }$
and:
:$\ds T = \bigcup_{k \mathop = 1}^m \bigcup_{i \mathop = 1}^{l_k} \map {\theta_{k, i} } {A_{k, i} }$
This yields equivalent decompositions of $S$ and $T$.
{{qed}}
Category:Equidecomposable Sets
Category:Topology
r00csg127qu4zz9gh8ff1blbg4npeoc
Theorem: Subsets of Equidecomposable Subsets are Equidecomposable

Let $A, B \subseteq \R^n$ be equidecomposable.
Let $S \subseteq A$.
Then there exists $T \subseteq B$ such that $S$ and $T$ are equidecomposable.

Proof:
Let $X_1, \dots, X_m$ be a decomposition of $A, B$ together with isometries $\mu_1, \ldots, \mu_m, \nu_1, \ldots, \nu_m: \R^n \to \R^n$ such that:
:$\ds A = \bigcup_{i \mathop = 1}^m \map {\mu_i} {X_i}$ 
and 
:$\ds B = \bigcup_{i \mathop = 1}^m \map {\nu_i} {X_i}$
Define:
:$Y_i = \mu_i^{-1} \paren {S \cap \map {\mu_i} {X_i} }$
Then:
{{begin-eqn}}
{{eqn | l = \bigcup_{i \mathop = 1}^m \map {\mu_i} {Y_i}
      | r = \bigcup_{i \mathop = 1}^m \map {\mu_i} { \mu_i^{-1} \paren {S \cap \map {\mu_i} {X_i} } }
      | c = {{hypothesis}}
}}
{{eqn | r = \bigcup_{i \mathop = 1}^m \paren {S \cap \map {\mu_i} {X_i} }
      | c = {{Corollary|Image of Preimage under Mapping}}
}}
{{eqn | r = S \cap \bigcup_{i \mathop = 1}^m \map {\mu_i} {X_i}
      | c = Intersection Distributes over Union of Family
}}
{{eqn | r = S \cap A
      | c = {{hypothesis}}
}}
{{eqn | r = S
      | c = Intersection with Subset is Subset
}}
{{end-eqn}}
and so $\sequence {Y_i}_{i \mathop = 1}^m$ forms a decomposition of $S$.
But for each $i$:
:$\paren {S \cap \map {\mu_i} {X_i} } \subseteq \map {\mu_i} {X_i}$
and so:
{{begin-eqn}}
{{eqn | l = Y_i
      | r = \map {\mu_i^{-1} } {S \cap \map {\mu_i} {X_i} }
      | c = {{hypothesis}}
}}
{{eqn | o = \subseteq
      | r = \map {\mu_i^{-1} } {\map {\mu_i} {X_i} }
      | c = Preimage of Subset is Subset of Preimage
}}
{{eqn | r = X_i
      | c = {{Defof|Isometry (Metric Spaces)}} and {{Defof|Bijection}}
}}
{{end-eqn}}
Hence:
:$\map {\nu_i} {Y_i} \subseteq \map {\nu_i} {X_i}$
and so:
{{begin-eqn}}
{{eqn | l = \bigcup_{i \mathop = 1}^m \map {\nu_i} {Y_i}
      | o = \subseteq
      | r = \bigcup_{i \mathop = 1}^m \map {\nu_i} {X_i}
      | c = Set Union Preserves Subsets
}}
{{eqn | r = B
      | c = {{hypothesis}}
}}
{{end-eqn}}
Define:
:$\ds \bigcup_{i \mathop = 1}^m \map {\nu_i} {Y_i} = T$
Hence the result.
{{qed}}
Category:Equidecomposable Sets
Category:Topology
sphe3vm2htfgoqgxu35v7x92iclbm1k
Theorem: Shape of Cosine Function

The cosine function is:
:$(1): \quad$ strictly decreasing on the interval $\closedint 0 \pi$
:$(2): \quad$ strictly increasing on the interval $\closedint \pi {2 \pi}$
:$(3): \quad$ concave on the interval $\closedint {-\dfrac \pi 2} {\dfrac \pi 2}$
:$(4): \quad$ convex on the interval $\closedint {\dfrac \pi 2} {\dfrac {3 \pi} 2}$

Proof:
{{improve|Extract those results into separate pages and reference them. Referencing the "discussion" is unsound because the proof can be changed and that "discussion" removed.}}
From the discussion of Real Cosine Function is Periodic, we know that:
:$\cos x \ge 0$ on the closed interval $\closedint {-\dfrac \pi 2} {\dfrac \pi 2}$
and:
:$\cos x > 0$ on the open interval $\openint {-\dfrac \pi 2} {\dfrac \pi 2}$
From the same discussion, we have that:
:$\map \sin {x + \dfrac \pi 2} = \cos x$
So immediately we have that $\sin x \ge 0$ on the closed interval $\closedint 0 \pi$, $\sin x > 0$ on the open interval $\openint 0 \pi$.
But $\map {\dfrac \d {\d x} } {\cos x} = -\sin x$ from Derivative of Cosine Function.
Thus from Derivative of Monotone Function, $\cos x$ is strictly decreasing on $\closedint 0 \pi$.
From Derivative of Sine Function it follows that:
:$\map {\dfrac {\d^2} {\d x^2} } {\cos x} = -\cos x$
On $\closedint {-\dfrac \pi 2} {\dfrac \pi 2}$ where $\cos x \ge 0$, therefore, $\map {\dfrac {\d^2} {\d x^2} } {\cos x} \le 0$.
From Second Derivative of Concave Real Function is Non-Positive it follows that $\cos x$ is concave on $\closedint {-\dfrac \pi 2} {\dfrac \pi 2}$.
The rest of the result follows similarly.
{{qed}}
Theorem: Tangent Function is Periodic on Reals

The real tangent function is periodic with period $\pi$.
This can be written:
:$\tan x = \map \tan {x \bmod \pi}$
where $x \bmod \pi$ denotes the modulo operation.

Proof:
{{begin-eqn}}
{{eqn | l = \map \tan {x + \pi}
      | r = \frac {\map \sin {x + \pi} } {\map \cos {x + \pi} }
      | c = {{Defof|Real Tangent Function}}
}}
{{eqn | r = \frac {-\sin x} {-\cos x}
      | c = Sine and Cosine are Periodic on Reals
}}
{{eqn | r = \tan x
      | c = 
}}
{{end-eqn}}
From Derivative of Tangent Function, we have that:
:$\map {D_x} {\tan x} = \dfrac 1 {\cos^2 x}$
provided $\cos x \ne 0$.
From Shape of Cosine Function, we have that $\cos > 0$ on the interval $\openint {-\dfrac \pi 2} {\dfrac \pi 2}$.
From Derivative of Monotone Function, $\tan x$ is strictly increasing on that interval, and hence can not have a period of ''less'' than $\pi$.
Hence the result.
{{qed}}
Theorem: Derivative of Tangent Function

:$\map {\dfrac \d {\d x} } {\tan x} = \sec^2 x = \dfrac 1 {\cos^2 x}$
when $\cos x \ne 0$.

Proof:
From the definition of the tangent function:
:$\tan x = \dfrac {\sin x} {\cos x}$
From Derivative of Sine Function:
:$\map {\dfrac \d {\d x} } {\sin x} = \cos x$
From Derivative of Cosine Function:
:$\map {\dfrac \d {\d x} } {\cos x} = -\sin x$
Then:
{{begin-eqn}}
{{eqn | l = \map {\dfrac \d {\d x} } {\tan x}
      | r = \frac {\cos x \cos x - \sin x \paren {-\sin x} } {\cos^2 x}
      | c = Quotient Rule for Derivatives
}}
{{eqn | r = \frac {\cos^2 x + \sin^2 x} {\cos^2 x}
      | c = 
}}
{{eqn | r = \frac 1 {\cos^2 x}
      | c = Sum of Squares of Sine and Cosine
}}
{{end-eqn}}
This is valid only when $\cos x \ne 0$.
The result follows from the Secant is Reciprocal of Cosine.
{{qed}}
Theorem: Derivative of Tangent Function

:$\map {\dfrac \d {\d x} } {\tan x} = \sec^2 x = \dfrac 1 {\cos^2 x}$
when $\cos x \ne 0$.

Proof:
{{begin-eqn}}
{{eqn | l = \map {\frac \d {\d x} } {\tan x}
      | r = \lim_{h \mathop \to 0} \frac {\map \tan {x + h} - \tan x} h
      | c = {{Defof|Derivative of Real Function at Point}}
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {\frac {\tan x + \tan h} {1 - \tan x \tan h} - \tan x} h
      | c = Tangent of Sum
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {\frac {\tan x + \tan h - \tan x + \tan^2 x \tan h} {1 - \tan x \tan h} } h
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {\tan h + \tan^2 x \tan h} {h \paren {1 - \tan x \tan h} } 
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {1 + \tan^2 x} {1 - \tan x \tan h} \cdot \lim_{h \mathop \to 0} \frac {\tan h} h
      | c = Product Rule for Limits of Real Functions
}}
{{eqn | r = \frac {1 + \tan^2 x} {1 - \tan x \tan 0} \cdot 1
      | c = Limit of $\dfrac {\tan x} x$ at Zero
}}
{{eqn | r = 1 + \tan^2 x
      | c = Tangent of Zero
}}
{{eqn | r = \sec^2 x
      | c = Difference of Squares of Secant and Tangent
}}
{{eqn | r = \frac 1 {\cos^2 x}
      | c = Secant is Reciprocal of Cosine ($\cos x \ne 0$)
}}
{{end-eqn}}
{{qed}}
Theorem: Stirling's Formula

The factorial function can be approximated by the formula:
:$n! \sim \sqrt {2 \pi n} \paren {\dfrac n e}^n$
where $\sim$ denotes asymptotically equal.

Proof:
Consider the sequence $\sequence {d_n}$ defined as:
:$d_n = \map \ln {n!} - \paren {n + \dfrac 1 2} \ln n + n$
From Lemma 2 it is seen that $\sequence {d_n}$ is a decreasing sequence.
From Lemma 3 it is seen that the sequence:
:$\sequence {d_n - \dfrac 1 {12 n} }$
is increasing.
In particular:
:$\forall n \in \N_{>0}: d_n - \dfrac 1 {12 n} \ge d_1 - \dfrac 1 {12}$
and so $\sequence {d_n}$ is bounded below.
From the Monotone Convergence Theorem (Real Analysis), it follows that $\sequence {d_n}$ is convergent.
Let $d_n \to d$ as $n \to \infty$.
From Exponential Function is Continuous, we have:
:$\exp d_n \to \exp d$ as $n \to \infty$
Let $C = \exp d$.
Then:
:$\dfrac {n!} {n^n \sqrt n e^{-n} } \to C$ as $n \to \infty$
It remains to be shown that $C = \sqrt {2 \pi}$.
Let $I_n$ be defined as:
:$\ds I_n = \int_0^{\frac \pi 2} \sin^n x \rd x$
Then from Lemma 4:
:$\ds \lim_{n \mathop \to \infty} \frac {I_{2 n} } {I_{2 n + 1} } = 1$
So:
{{begin-eqn}}
{{eqn | l = \lim_{n \mathop \to \infty} \dfrac {n!} {n^n \sqrt n e^{-n} }
      | r = \sqrt {2 \pi}
      | c = Lemma 5
}}
{{eqn | ll= \leadsto
      | l = \lim_{n \mathop \to \infty} \dfrac {n!} {\sqrt {2 \pi n} \paren {\frac n e}^n}
      | r = 1
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Stirling's Formula

The factorial function can be approximated by the formula:
:$n! \sim \sqrt {2 \pi n} \paren {\dfrac n e}^n$
where $\sim$ denotes asymptotically equal.

Proof:
From Poisson Distribution Approximated by Normal Distribution, we have:
Let $X$ be a discrete random variable which has the Poisson distribution $\Poisson \lambda$.
Then for large $\lambda$:
:$\Poisson \lambda \approx \Gaussian \lambda \lambda$
where $\Gaussian \lambda \lambda$ denotes the normal distribution.
Since the Poisson Distribution with parameter $\lambda$ converges to the Normal Distribution with mean $\lambda$ and variance $\lambda$, their density functions will be asymptotically equal.
:$\dfrac 1 {k!} \lambda^k e^{-\lambda} \approx \dfrac 1 {\sqrt {2 \pi \lambda} } \map \exp {-\dfrac {\paren {k - \lambda}^2} {2 \lambda} }$
Evaluating this expression at the mean simplifies to the expression:
:$\dfrac 1 {\lambda!} \lambda^\lambda e^{-\lambda} \approx \dfrac 1 {\sqrt {2 \pi \lambda} }$
Rearranging, we obtain:
:$\lambda! \approx \sqrt {2 \pi \lambda} \lambda^\lambda e^{-\lambda}$
{{qed}}
Theorem: Stirling's Formula

The factorial function can be approximated by the formula:
:$n! \sim \sqrt {2 \pi n} \paren {\dfrac n e}^n$
where $\sim$ denotes asymptotically equal.

Proof:
Let:
:$\ds \map f n := \dfrac {n!} {\sqrt {2 \pi n} n^n e^{-n} } - \paren {1 + \frac 1 {12 n} }$
We need to show:
:$\ds \map f n = \map \OO {\dfrac 1 {n^2} }$
Recall Limit of Error in Stirling's Formula:
:$e^{1 / \paren {12 n + 1} } \le \dfrac {n!} {\sqrt {2 \pi n} n^n e^{-n} } \le e^{1 / 12 n}$
Furthermore, observe:
{{begin-eqn}}
{{eqn | l = e^{1 / {12 n + 1} }
      | o = \ge
      | r = 1 + \frac 1 {12 n + 1}
      | c = Exponential Function Inequality
}}
{{eqn | r = 1 + \frac 1 {12 n} - \frac 1 {12 n \paren {12 n + 1} }
}}
{{eqn | o = \ge
      | r = \paren {1 + \frac 1 {12 n} } - \frac 1 {n^2}
}}
{{end-eqn}}
On the other hand:
{{begin-eqn}}
{{eqn | l = e^{1 / {12 n} }
      | r = 1 + \frac 1 {12 n} + \frac {e^\xi}{2!} \paren {\frac 1 {12 n} }^2
      | c = for a $\xi \in \closedint 0 {\frac 1 {12n} }$ by Taylor's Theorem
}}
{{eqn | o = \le
      | r = 1 + \frac 1 {12 n} + \frac {e^1} {2!} \paren {\frac 1 {12 n} }^2
      | c = Exponential is Strictly Increasing
}}
{{eqn | o = \le
      | r = \paren {1 + \frac 1 {12 n} } + \frac 1 {n^2}
      | c = $e=2.71\ldots$
}}
{{end-eqn}}
Altogether we have:
:$-\dfrac 1 {n^2} \le e^{1 / \paren {12 n + 1} } - \paren {1 + \dfrac 1 {12 n} } \le \map f n \le e^{1 / \paren {12 n} } - \paren {1 + \dfrac 1 {12 n} } \le \dfrac 1 {n^2}$
Therefore:
:$ \size {\map f n} \le \dfrac 1 {n^2}$
{{qed}}
Theorem: Shape of Sine Function

The sine function is:
:$(1): \quad$ strictly increasing on the interval $\closedint {-\dfrac \pi 2} {\dfrac \pi 2}$
:$(2): \quad$ strictly decreasing on the interval $\closedint {\dfrac \pi 2} {\dfrac {3 \pi} 2}$
:$(3): \quad$ concave on the interval $\closedint 0 \pi$
:$(4): \quad$ convex on the interval $\closedint \pi {2 \pi}$

Proof:
From the discussion of Real Sine Function is Periodic, we have that:
:$\sin \paren {x + \dfrac \pi 2} = \cos x$
The result then follows directly from the Shape of Cosine Function.
Theorem: Derivative of Secant Function

:$\map {\dfrac \d {\d x} } {\sec x} = \sec x \tan x$
where $\cos x \ne 0$.

Proof:
{{begin-eqn}}
{{eqn | l = \map {\dfrac \d {\d x} } {\sec x}
      | r = \map {\dfrac \d {\d x} } {\dfrac 1 {\cos x} }
      | c = {{Defof|Real Secant Function}}
}}
{{eqn | r = \dfrac {\cos x \map {\frac \d {\d x} } 1 - 1 \map {\frac \d {\d x} } {\cos x} } {\cos^2 x}
      | c = Quotient Rule for Derivatives
}}
{{eqn | r = \dfrac {0 - \paren {-\sin x} } {\cos^2 x}
      | c = Derivative of Cosine Function, Derivative of Constant
}}
{{eqn | r = \sec x \tan x
      | c = {{Defof|Real Secant Function}}, {{Defof|Real Tangent Function}}
}}
{{end-eqn}}
This is valid only when $\cos x \ne 0$.
{{qed}}
Theorem: Derivative of Cosecant Function

:$\map {\dfrac \d {\d x} } {\csc x} = -\csc x \cot x$
where $\sin x \ne 0$.

Proof:
* {{BookReference|A Note Book in Pure Mathematics|1953|L. Harwood Clarke|prev = Derivative of Tangent Function/Proof 1|next = Derivative of Secant Function/Proof 2}}: $\text {II}$. Calculus: Differentiation: Quotient
Category:Derivative of Cosecant Function
f16wucwytsunbruw1jlda17nropk15w
Theorem: Shape of Tangent Function

The nature of the tangent function on the set of real numbers $\R$ is as follows:
:$\tan x$ is continuous and strictly increasing on the interval $\openint {-\dfrac \pi 2} {\dfrac \pi 2}$
:$\tan x \to +\infty$ as $x \to \dfrac \pi 2 ^-$
:$\tan x \to -\infty$ as $x \to -\dfrac \pi 2 ^+$
:$\tan x$ is not defined on $\forall n \in \Z: x = \paren {n + \dfrac 1 2} \pi$, at which points it is discontinuous
:$\forall n \in \Z: \map \tan {n \pi} = 0$.

Proof:
$\tan x$ is continuous and strictly increasing on $\openint {-\dfrac \pi 2} {\dfrac \pi 2}$:
Continuity follows from the Quotient Rule for Continuous Real Functions:
:$(1): \quad$ Both $\sin x$ and $\cos x$ are continuous on $\openint {-\dfrac \pi 2} {\dfrac \pi 2}$ from Real Sine Function is Continuous and Cosine Function is Continuous
:$(2): \quad$ $\cos x > 0$ on this interval.
The fact of $\tan x$ being strictly increasing on this interval has been demonstrated in the discussion on Tangent Function is Periodic on Reals.
$\tan x \to + \infty$ as $x \to \dfrac \pi 2^-$:
From Sine and Cosine are Periodic on Reals, we have that both $\sin x > 0$ and $\cos x > 0$ on $\openint 0 {\dfrac \pi 2}$.
We have that:
:$(1): \quad \cos x \to 0$ as $x \to \dfrac \pi 2^-$
:$(2): \quad \sin x \to 1$ as $x \to \dfrac \pi 2^-$
From the Infinite Limit Theorem it follows that:
:$\tan x = \dfrac {\sin x} {\cos x} \to + \infty$ as $x \to \dfrac \pi 2 ^-$
$\tan x \to - \infty$ as $x \to -\dfrac \pi 2 ^+$:
From Sine and Cosine are Periodic on Reals, we have that $\sin x < 0$ and $\cos x > 0$ on $\openint {-\dfrac \pi 2} 0$.
We have that:
:$(1): \quad \cos x \to 0$ as $x \to -\dfrac \pi 2 ^+$
:$(2): \quad \sin x \to -1$ as $x \to -\dfrac \pi 2 ^+$
Thus it follows that $\tan x = \dfrac {\sin x} {\cos x} \to -\infty$ as $x \to -\dfrac \pi 2 ^+$.
$\tan x$ is not defined and discontinuous at $x = \paren {n + \dfrac 1 2} \pi$:
From the discussion of Sine and Cosine are Periodic on Reals, it was established that:
:$\forall n \in \Z: x = \paren {n + \dfrac 1 2} \pi \implies \cos x = 0$
As division by zero is not defined, it follows that at these points $\tan x$ is not defined either.
Now, from the above, we have:
:$(1): \quad \tan x \to + \infty$ as $x \to \dfrac \pi 2^-$
:$(2): \quad \tan x \to - \infty$ as $x \to -\dfrac \pi 2^+$
As $\map \tan {x + \pi} = \tan x$ from Tangent Function is Periodic on Reals, it follows that:
:$\tan x \to - \infty$ as $x \to \dfrac \pi 2 ^+$
Hence the left hand limit and right hand limit at $x = \dfrac \pi 2$ are not the same.
From Tangent Function is Periodic on Reals, it follows that the same applies $\forall n \in \Z: x = \paren {n + \dfrac 1 2} \pi$.
The fact of its discontinuity at these points follows from the definition of discontinuity.
$\map \tan {n \pi} = 0$:
Follows directly from Sine and Cosine are Periodic on Reals::
:$\forall n \in \Z: \map \sin {n \pi} = 0$
{{qed}}
Theorem: Derivative of Arcsine Function

:$\dfrac {\map \d {\arcsin x} } {\d x} = \dfrac 1 {\sqrt {1 - x^2} }$

Proof:
Let $y = \arcsin x$ where $-1 < x < 1$.
Then:
{{begin-eqn}}
{{eqn | l = x
      | r = \sin y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\d x} {\d y}
      | r = \cos y
      | c = Derivative of Sine Function
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \cos^2 y + \sin^2 y
      | r = 1
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | ll= \leadsto
      | l = \cos y
      | r = \pm \sqrt {1 - \sin^2 y}
      | c = 
}}
{{end-eqn}}
Now $\cos y \ge 0$ on the image of $\arcsin x$, that is:
:$y \in \closedint {-\dfrac \pi 2} {\dfrac \pi 2}$
Thus it follows that we need to take the positive root of $\sqrt {1 - \sin^2 y}$.
So:
{{begin-eqn}}
{{eqn | l = \frac {\d y} {\d x}
      | r = \frac 1 {\sqrt {1 - \sin^2 y} }
      | c = 
}}
{{eqn | r = \frac 1 {\sqrt {1 - x^2} }
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Arccosine Function

:$\map {D_x} {\arccos x} = \dfrac {-1} {\sqrt {1 - x^2} }$

Proof:
Let $y = \arccos x$ where $-1 < x < 1$.
Then:
:$x = \cos y$
Then from Derivative of Cosine Function:
:$\dfrac {\d x} {\d y} = -\sin y$
Hence from Derivative of Inverse Function:
:$\dfrac {\d y} {\d x} = \dfrac {-1} {\sin y}$
From Sum of Squares of Sine and Cosine, we have:
:$\cos^2 y + \sin^2 y = 1 \implies \sin y = \pm \sqrt {1 - \cos^2 y}$
Now $\sin y \ge 0$ on the range of $\arccos x$, that is, for $y \in \closedint 0 \pi$.
Thus it follows that we need to take the positive root of $\sqrt {1 - \cos^2 y}$.
So:
:$\dfrac {\d y} {\d x} = \dfrac {-1} {\sqrt {1 - \cos^2 y} }$
and hence the result.
{{qed}}
Theorem: Sum of Arcsine and Arccosine

Let $x \in \R$ be a real number such that $-1 \le x \le 1$.
Then:
:$\arcsin x + \arccos x = \dfrac \pi 2$
where $\arcsin$ and $\arccos$ denote arcsine and arccosine respectively.

Proof:
Let $y \in \R$ such that:
:$\exists x \in \closedint {-1} 1: x = \map \cos {y + \dfrac \pi 2}$
Then:
{{begin-eqn}}
{{eqn | l = x
      | r = \map \cos {y + \frac \pi 2}
      | c = 
}}
{{eqn | r = -\sin y
      | c = Cosine of Angle plus Right Angle
}}
{{eqn | r = \map \sin {-y}
      | c = Sine Function is Odd
}}
{{end-eqn}}
Suppose $-\dfrac \pi 2 \le y \le \dfrac \pi 2$.
Then we can write:
:$-y = \arcsin x$
But then:
:$\map \cos {y + \dfrac \pi 2} = x$
Now since $-\dfrac \pi 2 \le y \le \dfrac \pi 2$ it follows that:
:$0 \le y + \dfrac \pi 2 \le \pi$
Hence:
:$y + \dfrac \pi 2 = \arccos x$
That is:
:$\dfrac \pi 2 = \arccos x + \arcsin x$
{{qed}}
Theorem: Sum of Arcsine and Arccosine

Let $x \in \R$ be a real number such that $-1 \le x \le 1$.
Then:
:$\arcsin x + \arccos x = \dfrac \pi 2$
where $\arcsin$ and $\arccos$ denote arcsine and arccosine respectively.

Proof:
:400px
Consider the diagram above.
{{begin-eqn}}
{{eqn | l = \alpha
      | r = \arcsin A
      | c = 
}}
{{eqn | l = \beta
      | r = \arccos A
      | c = 
}}
{{eqn | l = \alpha + \beta
      | r = \frac \pi 2
      | c = Sum of Angles of Triangle equals Two Right Angles
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Arctangent Function

:$\dfrac {\map \d {\arctan x} } {\d x} = \dfrac 1 {1 + x^2}$

Proof:
{{begin-eqn}}
{{eqn | l = y
      | r = \arctan x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = \tan y
      | c = {{Defof|Real Arctangent}}
}}
{{eqn | ll= \leadsto
      | l = \frac {\d x} {\d y}
      | r = \sec^2 y
      | c = Derivative of Tangent Function
}}
{{eqn | r = 1 + \tan^2 y
      | c = Difference of Squares of Secant and Tangent
}}
{{eqn | r = 1 + x^2
      | c = Definition of $x$
}}
{{eqn | ll= \leadsto
      | l = \frac {\d y} {\d x}
      | r = \frac 1 {1 + x^2}
      | c = Derivative of Inverse Function
}}
{{end-eqn}}
{{qed}}