avewright/proofwiki-math huggingface dataset:
Theorem: Second Principle of Mathematical Induction

Let $\map P n$ be a propositional function depending on $n \in \Z$.
Let $n_0 \in \Z$ be given.
Suppose that:
:$(1): \quad \map P {n_0}$ is true
:$(2): \quad \forall k \in \Z: k \ge n_0: \map P {n_0} \land \map P {n_0 + 1} \land \ldots \land \map P {k - 1} \land \map P k \implies \map P {k + 1}$
Then:
:$\map P n$ is true for all $n \ge n_0$.
This process is called '''proof by (mathematical) induction'''.

Proof:
For each $n \ge n_0$, let $\map {P'} n$ be defined as:
:$\map {P'} n := \map P {n_0} \land \dots \land \map P n$
It suffices to show that $\map {P'} n$ is true for all $n \ge n_0$.
It is immediate from the assumption $\map P {n_0}$ that $\map {P'} {n_0}$ is true.
Now suppose that $\map {P'} n$ holds.
By $(2)$, this implies that $\map P {n + 1}$ holds as well.
Consequently, $\map {P'} n \land \map P {n + 1} = \map {P'} {n + 1}$ holds.
Thus by the Principle of Mathematical Induction:
:$\map {P'} n$ holds for all $n \ge n_0$
as desired.
{{Qed}}
Theorem: Second Principle of Mathematical Induction

Let $\map P n$ be a propositional function depending on $n \in \Z$.
Let $n_0 \in \Z$ be given.
Suppose that:
:$(1): \quad \map P {n_0}$ is true
:$(2): \quad \forall k \in \Z: k \ge n_0: \map P {n_0} \land \map P {n_0 + 1} \land \ldots \land \map P {k - 1} \land \map P k \implies \map P {k + 1}$
Then:
:$\map P n$ is true for all $n \ge n_0$.
This process is called '''proof by (mathematical) induction'''.

Proof:
For each $n \in \N_{>0}$, let $\map {P'} n$ be defined as:
:$\map {P'} n := \map P 1 \land \dots \land \map P n$
It suffices to show that $\map {P'} n$ is true for all $n \in \N_{>0}$.
It is immediate from the assumption $\map P 1$ that $\map {P'} 1$ is true.
Now suppose that $\map {P'} n$ holds.
By $(2)$, this implies that $\map P {n + 1}$ holds as well.
Consequently, $\map {P'} n \land \map P {n + 1} = \map {P'} {n + 1}$ holds.
Thus by the Principle of Mathematical Induction:
:$\map {P'} n$ holds for all $n \in \N_{>0}$
as desired.
{{Qed}}
Theorem: Second Principle of Mathematical Induction

Let $\map P n$ be a propositional function depending on $n \in \Z$.
Let $n_0 \in \Z$ be given.
Suppose that:
:$(1): \quad \map P {n_0}$ is true
:$(2): \quad \forall k \in \Z: k \ge n_0: \map P {n_0} \land \map P {n_0 + 1} \land \ldots \land \map P {k - 1} \land \map P k \implies \map P {k + 1}$
Then:
:$\map P n$ is true for all $n \ge n_0$.
This process is called '''proof by (mathematical) induction'''.

Proof:
Let $S \subseteq \N_{>0}$ containing those $n \in \N_{>0}$ for which $\map P n$ does not hold.
{{AimForCont}} $S \ne \O$.
Then by the Well-Ordering Principle $S$ contains a minimal element $s$.
We have that $s \ne 1$ because $\map P 1$ is true from $(1)$.
Thus there must exist some $k \in \N_{>0}$ such that $s = k + 1$.
As $k + 1$ is the minimal element of $S$ it follows that all $n$ such that $n < k + 1 = s$ are not in $S$
But this means that $\map P n$ is true for all $n < s$
But by $(2)$ it follows that $\map P s$ is true.
That is, $s \notin S$.
This contradicts our assertion that $s \in S$.
Hence our assumption that $S \ne \O$ is false.
It follows by Proof by Contradiction that $S = \O$.
So $\map P n$ holds for all $n \in \N_{>0}$.
{{Qed}}
Theorem: Second Principle of Finite Induction

Let $S \subseteq \Z$ be a subset of the integers.
Let $n_0 \in \Z$ be given.
Suppose that:
:$(1): \quad n_0 \in S$
:$(2): \quad \forall n \ge n_0: \paren {\forall k: n_0 \le k \le n \implies k \in S} \implies n + 1 \in S$
Then:
:$\forall n \ge n_0: n \in S$

Proof:
Define $T$ as:
:$T = \set {n \in \Z : \forall k: n_0 \le k \le n: k \in S}$
Since $n \le n$, it follows that $T \subseteq S$.
Therefore, it will suffice to show that:
:$\forall n \ge n_0: n \in T$
Firstly, we have that $n_0 \in T$ {{iff}} the following condition holds:
:$\forall k: n_0 \le k \le n_0 \implies k \in S$
Since $n_0 \in S$, it thus follows that $n_0 \in T$.
Now suppose that $n \in T$; that is:
:$\forall k: n_0 \le k \le n \implies k \in S$
By $(2)$, this implies:
:$n + 1 \in S$
Thus, we have:
:$\forall k: n_0 \le k \le n + 1 \implies k \in S$
{{MissingLinks|Closed Interval of Naturally Ordered Semigroup with Successor equals Union with Successor for $\Z$}}
Therefore, $n + 1 \in T$.
Hence, by the Principle of Finite Induction:
:$\forall n \ge n_0: n \in T$
as desired.
{{Qed}}
Theorem: Sign of Cosine

Let $x$ be a real number.
Then:
{{begin-eqn}}
{{eqn | l = \cos x
      | o = >
      | r = 0
      | c = if there exists an integer $n$ such that $\paren {2 n - \dfrac 1 2} \pi < x < \paren {2 n + \dfrac 1 2} \pi$
}}
{{eqn | l = \cos x
      | o = <
      | r = 0
      | c = if there exists an integer $n$ such that $\paren {2 n + \dfrac 1 2} \pi < x < \paren {2 n + \dfrac 3 2} \pi$
}}
{{end-eqn}}
where $\cos$ is the real cosine function.

Proof:
Proof by induction:
Theorem: Sign of Tangent

Let $x$ be a real number.
Then:
{{begin-eqn}}
{{eqn | l = \tan x
      | o = >
      | r = 0
      | c = if there exists an integer $n$ such that $n \pi < x < \paren {n + \dfrac 1 2} \pi$
}}
{{eqn | l = \tan x
      | o = <
      | r = 0
      | c = if there exists an integer $n$ such that $\paren {n + \dfrac 1 2} \pi < x < \paren {n + 1} \pi$
}}
{{end-eqn}}
where $\tan$ denotes the tangent function.

Proof:
From Tangent is Sine divided by Cosine:
:$\tan x = \dfrac {\sin x} {\cos x}$
Since $n$ is an integer, $n$ is either odd or even.
Theorem: Reciprocal of Strictly Negative Real Number is Strictly Negative

:$\forall x \in \R: x < 0 \implies \dfrac 1 x < 0$

Proof:
Let $x < 0$.
{{AimForCont}} $\dfrac 1 x > 0$.
Then:
{{begin-eqn}}
{{eqn | l = x
      | o = <
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x \times \dfrac 1 x
      | o = <
      | r = 0 \times 0
      | c = Real Number Ordering is Compatible with Multiplication: Negative Factor
}}
{{eqn | ll= \leadsto
      | l = 1
      | o = <
      | r = 0
      | c = {{Real-number-axiom|A4}}
}}
{{end-eqn}}
But from Real Zero is Less than Real One:
:$1 > 0$
Therefore by Proof by Contradiction:
:$\dfrac 1 x < 0$
{{qed}}
Theorem: Sign of Cosecant

Let $x$ be a real number.
Then:
{{begin-eqn}}
{{eqn | l = \csc x
      | o = >
      | r = 0
      | c = if there exists an integer $n$ such that $2 n \pi < x < \paren {2 n + 1} \pi$
}}
{{eqn | l = \csc x
      | o = <
      | r = 0
      | c = if there exists an integer $n$ such that $\paren {2 n + 1} \pi < x < \paren {2 n + 2} \pi$
}}
{{end-eqn}}
where $\csc$ is the real cosecant function.

Proof:
For the first part:
{{begin-eqn}}
{{eqn | l = \sin x
      | o = >
      | r = 0
      | c = if there exists an integer $n$ such that $2 n \pi < x < \paren {2 n + 1} \pi$
      | cc= Sign of Sine
}}
{{eqn | ll= \leadsto
      | l = \frac 1 {\sin x}
      | o = >
      | r = 0
      | c = if there exists an integer $n$ such that $2 n \pi < x < \paren {2 n + 1} \pi$
      | cc= Reciprocal of Strictly Positive Real Number is Strictly Positive
}}
{{eqn | ll= \leadsto
      | l = \csc x
      | o = >
      | r = 0
      | c = if there exists an integer $n$ such that $2 n \pi < x < \paren {2 n + 1} \pi$
      | cc= Cosecant is Reciprocal of Sine
}}
{{end-eqn}}
For the second part:
{{begin-eqn}}
{{eqn | l = \sin x
      | o = <
      | r = 0
      | c = if there exists an integer $n$ such that $\paren {2 n + 1} \pi < x < \paren {2 n + 2} \pi$
      | cc= Sign of Sine
}}
{{eqn | ll= \leadsto
      | l = \frac 1 {\sin x}
      | o = <
      | r = 0
      | c = if there exists an integer $n$ such that $\paren {2 n + 1} \pi < x < \paren {2 n + 2} \pi$
      | cc= Reciprocal of Strictly Negative Real Number is Strictly Negative
}}
{{eqn | ll= \leadsto
      | l = \csc x
      | o = <
      | r = 0
      | c = if there exists an integer $n$ such that $\paren {2 n + 1} \pi < x < \paren {2 n + 2} \pi$
      | cc= Cosecant is Reciprocal of Sine
}}
{{end-eqn}}
{{qed}}
Theorem: Sign of Secant

Let $x$ be a real number.
{{begin-eqn}}
{{eqn | l = \sec x
      | o = >
      | r = 0
      | c = if there exists an integer $n$ such that $\paren {2 n - \dfrac 1 2} \pi < x < \paren {2 n + \dfrac 1 2} \pi$
}}
{{eqn | l = \sec x
      | o = <
      | r = 0
      | c = if there exists an integer $n$ such that $\paren {2 n + \dfrac 1 2} \pi < x < \paren {2 n + \dfrac 3 2} \pi$
}}
{{end-eqn}}
where $\sec$ is the real secant function.

Proof:
For the first part:
{{begin-eqn}}
{{eqn | l = \cos x
      | o = >
      | r = 0
      | c = if there exists an integer $n$ such that $\paren {2 n - \dfrac 1 2} \pi < x < \paren {2 n + \dfrac 1 2} \pi$
      | cc= Sign of Cosine
}}
{{eqn | ll= \leadsto
      | l = \frac 1 {\cos x}
      | o = >
      | r = 0
      | c = if there exists an integer $n$ such that $\paren {2 n - \dfrac 1 2} \pi < x < \paren {2 n + \dfrac 1 2} \pi$
      | cc= Reciprocal of Strictly Positive Real Number is Strictly Positive
}}
{{eqn | ll= \leadsto
      | l = \sec x
      | o = >
      | r = 0
      | c = if there exists an integer $n$ such that $\paren {2 n - \dfrac 1 2} \pi < x < \paren {2 n + \dfrac 1 2} \pi$
      | cc= Secant is Reciprocal of Cosine
}}
{{end-eqn}}
For the second part:
{{begin-eqn}}
{{eqn | l = \cos x
      | o = <
      | r = 0
      | c = if there exists an integer $n$ such that $\paren {2 n + \dfrac 1 2} \pi < x < \paren {2 n + \dfrac 3 2} \pi$
      | cc= Sign of Cosine
}}
{{eqn | ll= \leadsto
      | l = \frac 1 {\cos x}
      | o = <
      | r = 0
      | c = if there exists an integer $n$ such that $\paren {2 n + \dfrac 1 2} \pi < x < \paren {2 n + \dfrac 3 2} \pi$
      | cc= Reciprocal of Strictly Negative Real Number is Strictly Negative
}}
{{eqn | ll= \leadsto
      | l = \sec x
      | o = <
      | r = 0
      | c = if there exists an integer $n$ such that $\paren {2 n + \dfrac 1 2} \pi < x < \paren {2 n + \dfrac 3 2} \pi$
      | cc= Secant is Reciprocal of Cosine
}}
{{end-eqn}}
{{qed}}
Theorem: Sign of Cotangent

Let $x$ be a real number.
Then:
{{begin-eqn}}
{{eqn | l = \cot x
      | o = >
      | r = 0
      | c = if there exists an integer $n$ such that $n \pi < x < \paren {n + \dfrac 1 2} \pi$
}}
{{eqn | l = \cot x
      | o = <
      | r = 0
      | c = if there exists an integer $n$ such that $\paren {n + \dfrac 1 2} \pi < x < \paren {n + 1} \pi$
}}
{{end-eqn}}
where $\cot$ is the real cotangent function.

Proof:
For the first part:
{{begin-eqn}}
{{eqn | l = \tan x
      | o = >
      | r = 0
      | c = if there exists an integer $n$ such that $n \pi < x < \paren {n + \dfrac 1 2} \pi$
      | cc= Sign of Tangent
}}
{{eqn | ll= \leadsto
      | l = \frac 1 \tan x
      | o = >
      | r = 0
      | c = if there exists an integer $n$ such that $n \pi < x < \paren {n + \dfrac 1 2} \pi$
      | cc= Reciprocal of Strictly Positive Real Number is Strictly Positive
}}
{{eqn | ll= \leadsto
      | l = \cot x
      | o = >
      | r = 0
      | c = if there exists an integer $n$ such that $n \pi < x < \paren {n + \dfrac 1 2} \pi$
      | cc= Cotangent is Reciprocal of Tangent
}}
{{end-eqn}}
For the second part:
{{begin-eqn}}
{{eqn | l = \tan x
      | o = <
      | r = 0
      | c = if there exists an integer $n$ such that $\paren {n + \dfrac 1 2} \pi < x < \paren {n + 1} \pi$
      | cc= Sign of Tangent
}}
{{eqn | ll= \leadsto
      | l = \frac 1 {\tan x}
      | o = <
      | r = 0
      | c = if there exists an integer $n$ such that $\paren {n + \dfrac 1 2} \pi < x < \paren {n + 1} \pi$
      | cc= Reciprocal of Strictly Negative Real Number is Strictly Negative
}}
{{eqn | ll= \leadsto
      | l = \cot x
      | o = <
      | r = 0
      | c = if there exists an integer $n$ such that $\paren {n + \dfrac 1 2} \pi < x < \paren {n + 1} \pi$
      | cc= Cotangent is Reciprocal of Tangent
}}
{{end-eqn}}
{{qed}}
Theorem: Cosine in terms of Tangent

{{begin-eqn}}
{{eqn | l = \cos x
      | r = +\frac 1 {\sqrt {1 + \tan^2 x} }
      | c = if there exists an integer $n$ such that $\paren {2 n - \dfrac 1 2} \pi < x < \paren {2 n + \dfrac 1 2} \pi$
}}
{{eqn | l = \cos x
      | r = -\frac 1 {\sqrt {1 + \tan^2 x} }
      | c = if there exists an integer $n$ such that $\paren {2 n + \dfrac 1 2} \pi < x < \paren {2 n + \dfrac 3 2} \pi$
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = \sec^2 x - \tan^2 x
      | r = 1
      | c = Difference of Squares of Secant and Tangent
}}
{{eqn | ll= \leadsto
      | l = \sec^2 x
      | r = 1 + \tan ^2 x
}}
{{eqn | ll= \leadsto
      | l = \frac 1 {\cos^2 x}
      | r = 1 + \tan^2 x
      | c = Secant is Reciprocal of Cosine
}}
{{eqn | ll= \leadsto
      | l = \cos^2 x
      | r = \frac 1 {1 + \tan^2 x}
}}
{{eqn | ll= \leadsto
      | l = \cos x
      | r = \pm \frac 1 {\sqrt {1 + \tan^2 x} }
}}
{{end-eqn}}
Then from Sign of Cosine:
{{begin-eqn}}
{{eqn | l = \cos x
      | o = >
      | r = 0
      | c = if there exists an integer $n$ such that $\paren {2 n - \dfrac 1 2} \pi < x < \paren {2 n + \dfrac 1 2} \pi$
}}
{{eqn | l = \cos x
      | o = <
      | r = 0
      | c = if there exists an integer $n$ such that $\paren {2 n + \dfrac 1 2} \pi < x < \paren {2 n + \dfrac 3 2} \pi$
}}
{{end-eqn}}
When $\cos x = 0$, $\tan x$ is undefined.
{{qed}}
Theorem: Tangent in terms of Secant

{{begin-eqn}}
{{eqn | l = \tan x
      | r = +\sqrt {\sec^2 x - 1}
      | c = if there exists an integer $n$ such that $n \pi < x < \paren {n + \dfrac 1 2} \pi$
}}
{{eqn | l = \tan x
      | r = -\sqrt {\sec^2 x - 1}
      | c = if there exists an integer $n$ such that $\paren {n + \dfrac 1 2} \pi < x < \paren {n + 1} \pi$
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = \sec^2 x - \tan^2 x
      | r = 1
      | c = Difference of Squares of Secant and Tangent
}}
{{eqn | ll= \leadsto
      | l = \tan^2 x
      | r = \sec^2 x - 1
}}
{{eqn | ll= \leadsto
      | l = \tan x
      | r = \pm \sqrt {\sec^2 x - 1}
}}
{{end-eqn}}
Also, from Sign of Tangent:
:If there exists integer $n$ such that $n \pi < x < \paren {n + \dfrac 1 2} \pi$, $\tan x > 0$.
:If there exists integer $n$ such that $\paren {n + \dfrac 1 2} \pi < x < \paren {n + 1} \pi$, $\tan x < 0$.
When $\cos x = 0$, $\tan x$ and $\sec x$ is undefined.
{{qed}}
Theorem: Union of Left-Total Relations is Left-Total

Let $S_1, S_2, T_1, T_2$ be sets or classes.
Let $\RR_1 \subseteq S_1 \times T_1$ and $\RR_2 \subseteq S_2 \times T_2$ be left-total relations.
Then $\RR_1 \cup \RR_2$ is left-total.

Proof:
Let both $\RR_1$ and $\RR_2$ be left-total.
Let $\RR = \RR_1 \cup \RR_2$.
Let $s \in S_1 \cup S_2$.
By the definition of union:
:$s \in S_1 \lor s \in S_2$
Thus $s \in S_i$ for $i \in \set {1, 2}$.
By definition of left-total relation, there is a $t \in T_i$ such that $\tuple {s, t} \in \RR_i$.
We have that $\RR$ is a superset of $\RR_i$.
Hence from Union is Smallest Superset:
:$\tuple {s, t} \in \RR_i \subseteq \RR \implies \tuple {s, t} \in \RR$
{{qed}}
Theorem: Union of Inverse of Relations is Inverse of their Union

For $i \in \set {1, 2}$, let $\RR_i \subseteq S_i \times T_i$ be relations on $S_i \times T_i$.
Let ${\RR_i}^{-1} \subseteq T_i \times S_i$ be the inverse of $\RR_i$.
Then:
:${\RR_1}^{-1} \cup {\RR_2}^{-1} = \paren {\RR_1 \cup \RR_2}^{-1}$

Proof:
Let $\tuple {t, s} \in {\RR_1}^{-1} \cup {\RR_2}^{-1}$.
By definition of union:
:$\tuple {t, s} \in {\RR_1}^{-1} \lor \tuple {t, s} \in {\RR_2}^{-1}$.
For $i \in \set {1, 2}$, let $\tuple {t, s} \in {\RR_i}^{-1}$.
By definition of inverse:
:$\tuple {s, t} \in \RR_i$
That is:
:$\tuple {s, t} \in \RR_1 \lor \tuple {s, t} \in \RR_2$
By definition of union:
:$\tuple {s, t} \in \RR_1 \lor \tuple {s, t} \in \RR_2 \iff \tuple {s, t} \in \RR_1 \cup \RR_2$
By the definition of inverse:
:$\tuple {t, s} \in \paren {\RR_1 \cup \RR_2}^{-1}$
{{qed}}
Category:Inverse Relations
Category:Set Union
89ptkoyyc6bz2swaa66r1nh4dz93pqr
Theorem: Open Set minus Closed Set is Open

Let $T = \struct {S, \tau}$ be a topological space.
For $A \subseteq S$ denote by $\relcomp S A$ the relative complement of $A$ in $S$.
Let $U \in \tau$ and $\relcomp S V \in \tau$.
Then:
:$U \setminus V \in \tau$
and:
:$\relcomp S {V \setminus U} \in \tau$

Proof:
From Set Difference as Intersection with Relative Complement:
:$U \setminus V = U \cap \relcomp S V$
Since $\tau$ is a topology:
:$U, \relcomp S V \in \tau \implies U \cap \relcomp S V \in \tau \implies U \setminus V \in \tau$
The other statement follows {{mutatis}}.
{{qed}}
Theorem: Union of Right-Total Relations is Right-Total

Let $S_1, S_2, T_1, T_2$ be sets or classes.
Let $\RR_1 \subseteq S_1 \times T_1$ and $\RR_2 \subseteq S_2 \times T_2$ be right-total relations.
Then $\RR_1 \cup \RR_2$ is right-total.

Proof:
Define the predicates $L$ and $R$ by:
:$\map L X \iff \text {$X$ is left-total}$
:$\map R X \iff \text {$X$ is right-total}$
{{begin-eqn}}
{{eqn | l = \map R {\RR_1} \land \map R {\RR_2}
      | o = \leadsto
      | r = \map L {\RR_1^{-1} } \land \map L {\RR_2^{-1} }
      | c = Inverse of Right-Total Relation is Left-Total
}}
{{eqn | o = \leadsto
      | r = \map L {\RR_1^{-1} \cup \RR_2^{-1} }
      | c = Union of Left-Total Relations is Left-Total
}}
{{eqn | o = \leadsto
      | r = \map L {\paren {\RR_1 \cup \RR_2}^{-1} }
      | c = Union of Inverse of Relations is Inverse of their Union
}}
{{eqn | o = \leadsto
      | r = \map R {\RR_1 \cup \RR_2}
      | c = Inverse of Right-Total Relation is Left-Total
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of x over a x + b squared by p x + q/Corollary

:$\ds \int \frac {x \rd x} {\paren {a x + b}^2 \paren {p x + q} } = \frac 1 {b p - a q} \paren {\frac q {b p - a q} \ln \size {\frac {a x + b} {p x + q} } + \frac x {a x + b} } + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {x \rd x} {\paren {a x + b}^2 \paren {p x + q} }
      | r = \frac 1 {b p - a q} \paren {\frac q {b p - a q} \ln \size {\frac {a x + b} {p x + q} } - \frac b {a \paren {a x + b} } } + C
      | c = Primitive of $\dfrac x {\paren {a x + b}^2 \paren {p x + q} }$
}}
{{eqn | r = \frac 1 {b p - a q} \paren {\frac q {b p - a q} \ln \size {\frac {a x + b} {p x + q} } - \frac {a x + b} {a \paren {a x + b} } + \frac {a x} {a \paren {a x + b} } } + C
      | c = 
}}
{{eqn | r = \frac 1 {b p - a q} \paren {\frac q {b p - a q} \ln \size {\frac {a x + b} {p x + q} } - \frac 1 a + \frac x {a x + b} } + C
      | c = 
}}
{{eqn | r = \frac 1 {b p - a q} \paren {\frac q {b p - a q} \ln \size {\frac {a x + b} {p x + q} } + \frac x {a x + b} } + \paren {C - \frac 1 {a \paren {b p - a q} } }
      | c = 
}}
{{eqn | r = \frac 1 {b p - a q} \paren {\frac q {b p - a q} \ln \size {\frac {a x + b} {p x + q} } + \frac x {a x + b} } + C
      | c = subsuming constant
}}
{{end-eqn}}
{{qed}}
Category:Primitive of x over a x + b squared by p x + q
Category:Primitives involving a x + b and p x + q
ck0rs0lrayxqq0sz0eh3ko6le7i75ot
Theorem: Arctangent of Imaginary Number

Let $x$ belong to the open real interval $\openint {-1} 1$.
Then:
:$\map {\tan^{-1} } {i x} = \dfrac i 2 \map \ln {\dfrac {1 + x} {1 - x} }$
where $\tan$ is the complex tangent function, $\ln$ is the real natural logarithm, and $i$ is the imaginary unit.

Proof:
Let $y = \map {\tan^{-1} } {i x}$.
Let $x = \tanh \theta$, then $\theta = \tanh^{-1} x$.
{{begin-eqn}}
{{eqn | l = \tan y
      | r = i x
      | c = 
}}
{{eqn | l = \tan y
      | r = i \tanh \theta
      | c = 
}}
{{eqn | l = \tan y
      | r = \map \tan {i \theta}
      | c = Hyperbolic Tangent in terms of Tangent
}}
{{eqn | ll= \leadsto
      | l = y
      | r = i \theta
      | c = 
}}
{{eqn | l = y
      | r = i \tanh^{-1} x
      | c = 
}}
{{eqn | l = y
      | r = \frac i 2 \map \ln {\frac {1 + x} {1 - x} }
      | c = {{Defof|Real Hyperbolic Arctangent}}
}}
{{end-eqn}}
{{qed}}
Category:Complex Numbers
Category:Tangent Function
ltvuizouywxeukypjt6rxq3tg1fc6c2
Theorem: Equivalence of Definitions of Real Area Hyperbolic Tangent

Let $S$ denote the open real interval:
:$S := \openint {-1} 1$
{{TFAE|def = Real Area Hyperbolic Tangent}}

Proof:
=== Definition 1 implies Definition 2 ===
Let $x = \tanh y$.
Then:
{{begin-eqn}}
{{eqn | l = x
      | r = \frac {e^{2 y} - 1} {e^{2 y} + 1}
      | c = {{Defof|Hyperbolic Tangent|index = 3}}
}}
{{eqn | ll= \leadsto
      | l = x e^{2 y} + x
      | r = e^{2 y} - 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = e^{2 y} - x e^{2 y}
      | r = 1 + x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = e^{2 y}
      | r = \frac {1 + x} {1 - x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 2 y
      | r = \map \ln {\frac {1 + x} {1 - x} }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y
      | r = \frac 1 2 \map \ln {\frac {1 + x} {1 - x} }
      | c = 
}}
{{end-eqn}}
{{qed|lemma}}
Theorem: Square Root is Strictly Increasing

The positive square root function is strictly increasing, that is:
:$\forall x, y \in \R_{>0}: x < y \implies \sqrt x < \sqrt y$

Proof:
Let $x$ and $y$ be positive real numbers such that $x < y$.
{{AimForCont}} $\sqrt x \ge \sqrt y$.
{{begin-eqn}}
{{eqn | n = 1
      | l = \sqrt x
      | o = \ge
      | r = \sqrt y
      | c = 
}}
{{eqn | n = 2
      | l = \sqrt x
      | o = \ge
      | r = \sqrt y
      | c = 
}}
{{eqn | l = x
      | o = \ge
      | r = y
      | c = {{Real-number-axiom|O2}}: $(1) \times (2)$
}}
{{end-eqn}}
Thus a contradiction is created.
Therefore:
:$\forall x, y \in \R_{>0}: x < y \implies \sqrt x < \sqrt y$
{{qed}}
Category:Real Numbers
Category:Square Roots
Category:Examples of Strictly Increasing Real Functions
63m6h1a8z0eanfhu7exn5f8yc49p4d1
Theorem: Minimum of Real Hyperbolic Cosine Function

Let $x$ be a real number.
Then:
:$\cosh x \ge 1$
where $\cosh$ denotes the hyperbolic cosine function.

Proof:
{{begin-eqn}}
{{eqn | l = \cosh^2 x - \sinh^2 x
      | r = 1
      | c = Difference of Squares of Hyperbolic Cosine and Sine
}}
{{eqn | ll= \leadsto
      | l = \cosh^2 x
      | r = 1 + \sinh^2 x
      | c = 
}}
{{eqn | o = \ge
      | r = 1
      | c = Square of Real Number is Non-Negative
}}
{{end-eqn}}
Furthermore, $\cosh x = 1$ when $x = 0$, satisfying the equality case.
{{qed}}
Category:Hyperbolic Cosine Function
1c4szrr57lywuqxqhmd77xy3o014eh0
Theorem: Exponential of Real Number is Strictly Positive

Let $x$ be a real number.
Let $\exp$ denote the (real) exponential function.
Then:
:$\forall x \in \R : \exp x > 0$

Proof:
This proof assumes the series definition of $\exp$.
That is, let:
:$\ds \exp x = \sum_{n \mathop = 0}^\infty \dfrac {x^n} {n!}$
First, suppose $0 < x$.
Then:
{{begin-eqn}}
{{eqn | l = 0
      | o = <
      | r = x^n
      | c = Power Function is Strictly Increasing over Positive Reals: Natural Exponent
}}
{{eqn | ll= \leadsto
      | l = 0
      | o = <
      | r = \frac {x^n} {n!}
      | c = Real Number Ordering is Compatible with Multiplication
}}
{{eqn | ll= \leadsto
      | l = 0
      | o = <
      | r = \sum_{n \mathop = 0}^\infty \frac {x^n} {n!}
      | c = Ordering of Series of Ordered Sequences
}}
{{eqn | ll= \leadsto
      | l = 0
      | o = <
      | r = \exp x
      | c = Definition of $\exp$
}}
{{end-eqn}}
So $\exp$ is strictly positive on $\R_{>0}$.
From Exponential of Zero, $\exp 0 = 1$.
Finally, suppose that $x < 0$.
Then:
{{begin-eqn}}
{{eqn | l = 0
      | o = <
      | r = -x
      | c = Order of Real Numbers is Dual of Order of their Negatives
}}
{{eqn | ll= \leadsto
      | l = 0
      | o = <
      | r = \map \exp {-x}
      | c = from above
}}
{{eqn | ll= \leadsto
      | l = 0
      | o = <
      | r = \frac 1 {\exp x}
      | c = Reciprocal of Real Exponential
}}
{{eqn | ll= \leadsto
      | l = 0
      | o = <
      | r = \exp x
      | c = Ordering of Reciprocals
}}
{{end-eqn}}
So $\exp$ is strictly positive on $\R_{<0}$.
Hence the result.
{{qed}}