avewright/proofwiki-math huggingface dataset:
Theorem: Praeclarum Theorema/Formulation 2

:$\vdash \paren {\paren {p \implies q} \land \paren {r \implies s} } \implies \paren {\paren {p \land r} \implies \paren {q \land s} }$

Proof:
{{BeginTableau|\vdash \paren {\paren {p \implies q} \land \paren {r \implies s} } \implies \paren {\paren {p \land r} \implies \paren {q \land s} } }}
{{Assumption|1|\paren {\paren {p \implies q} \land \paren {r \implies s} } }}
{{SequentIntro|2|1|\paren {p \land r} \implies \paren {q \land s}|1|Praeclarum Theorema: Formulation 1}}
{{Implication|3||\paren {\paren {p \implies q} \land \paren {r \implies s} } \implies \paren {\paren {p \land r} \implies \paren {q \land s} }|1|2}}
{{EndTableau|qed}}
Theorem: Strictly Positive Integer Power Function Strictly Succeeds Each Element

Let $\struct {R, +, \circ, \le}$ be an ordered ring with unity.
Let $\struct {R, \le}$ be a directed set with no upper bound.
Let $n \in \N_{>0}$.
Let $f: R \to R$ be defined by:
:$\forall x \in R: \map f x = \circ^n x$
Then the image of $f$ has elements strictly succeeding each elements of $R$.

Proof:
Let $b \in R$.
By Directed Set has Strict Successors iff Unbounded Above:
:$\exists c \in R: b < c$
:$\exists d \in R: 1 < d$
By the definition of a directed set:
:$\exists e \in R: d \le e, c \le e$
$\struct {R, +, \circ, \le}$ is an ordered ring, so $\le$ is by definition a transitive relation.
Hence by transitivity:
:$b < e$
and:
:$1 < e$
By Strictly Positive Power of Strictly Positive Element Greater than One Succeeds Element:
:$e \le \map f e$
Thus by transitivity:
:$b < \map f e$
{{qed}}
Category:Ring Theory
413wwed1qe7xtz89l3kxirtjmke6ll7
Theorem: Constructive Dilemma/Formulation 3

:$\vdash \paren {\paren {p \lor r} \land \paren {p \implies q} \land \paren {r \implies s} } \implies \paren {q \lor s}$

Proof:
{{BeginTableau  |\vdash \paren {\paren {p \lor r} \land \paren {p \implies q} \land \paren {r \implies s} } \implies \paren {q \lor s} }}
{{Assumption    |1|\paren {\paren {p \lor r} \land \paren {p \implies q} \land \paren {r \implies s} } }}
{{Simplification|2|1|\paren {p \implies q} \land \paren {r \implies s}|1|2|Cutting corners: should use Associativity first}}
{{SequentIntro  |3|1|\paren {p \lor r} \implies \paren {q \lor s}|2|Constructive Dilemma: Formulation 1}}
{{Simplification|4|1|p \lor r|1|1}}
{{ModusPonens   |5|1|q \lor s|3|4}}
{{Implication   |6| |\paren {\paren {p \lor r} \land \paren {p \implies q} \land \paren {r \implies s} } \implies \paren {q \lor s}|1|5}}
{{EndTableau}}
{{qed}}
Theorem: Odd Power Function is Strictly Increasing/Real Numbers

Let $n \in \Z_{> 0}$ be an odd positive integer.
Let $f_n: \R \to \R$ be the real function defined as:
:$\map {f_n} x = x^n$
Then $f_n$ is strictly increasing.

Proof:
From the Power Rule for Derivatives:
:$\map {D_x} {x^n} = n x^{n - 1}$
As $n$ is odd, $n - 1$ is even.
Thus by Even Power is Non-Negative:
:$\map {D_x} {x^n} \ge 0$
for all $x$.
From Derivative of Monotone Function, it follows that $f_n$ is increasing over the whole of $\R$.
The only place where $\map {D_x} {x^n} = 0$ is at $x = 0$.
Everywhere else, $f_n$ is strictly increasing.
By Sign of Odd Power:
:$\map {f_n} x < 0 = \map {f_n} 0$ when $x < 0$ and
:$\map {f_n} 0 = 0 < \map {f_n} x$ when $0 < x$.
Thus $f_n$ is strictly increasing on $\R$.
{{qed}}
Category:Odd Power Function is Strictly Increasing
Category:Strictly Increasing Real Functions
pw9i0yzsyppfzd3shkvs6usaym5mb81
Theorem: Clavius's Law/Formulation 1

:$\neg p \implies p \vdash p$

Proof:
{{BeginTableau|\neg p \implies p \vdash p}}
{{Premise|1|\neg p \implies p}}
{{ExcludedMiddle|2|p \lor \neg p}}
{{Assumption|3|\neg p|Either $p$ is false ...}}
{{ModusPonens|4|1, 3|p|1|3}}
{{Assumption|5|p|... or $p$ is true}}
{{ProofByCases|6|1|p|2|3|4|5|5}}
{{EndTableau|qed}}
{{LEM||3}}
Theorem: Clavius's Law/Formulation 1

:$\neg p \implies p \vdash p$

Proof:
{{BeginTableau|\neg p \implies p \vdash p}}
{{Premise|1|\neg p \implies p}}
{{Assumption|2|p \implies \bot}}
{{SequentIntro|3|2|\neg p|2|Negation as Implication of Bottom}}
{{ModusPonens|4|1,2|p|1|3}}
{{Implication|5|1|(p \implies \bot) \implies p|2|4}}
{{SequentIntro|6|1|p|5|Peirce's Law}}
{{EndTableau|qed}}
{{LEM|Peirce's Law|3}}
Theorem: Clavius's Law/Formulation 2

:$\vdash \paren {\neg p \implies p} \implies  p$

Proof:
{{BeginTableau|\vdash \paren {\neg p \implies p} \implies  p}}
{{Premise|1|\neg p \implies p}}
{{SequentIntro|2|1|p|1|Clavius's Law: Formulation 1}}
{{Implication|3||\paren {\neg p \implies p} \implies  p|1|2}}
{{EndTableau|qed}}
{{LEM|Clavius's Law/Formulation 1|3}}
Theorem: Clavius's Law/Formulation 2

:$\vdash \paren {\neg p \implies p} \implies  p$

Proof:
{{BeginTableau|\vdash \paren {\neg p \implies p} \implies  p}}
{{Premise|1|\neg p \implies p}}
{{ExcludedMiddle|2|p \lor \neg p}}
{{Assumption|3|\neg p|Either $p$ is false ...}}
{{ModusPonens|4|1, 3|p|1|3}}
{{Assumption|5|p|... or $p$ is true}}
{{ProofByCases|6|1|p|2|3|4|5|5}}
{{Implication|7||\paren {\neg p \implies p} \implies  p|1|6}}
{{EndTableau|qed}}
{{LEM||3}}
Theorem: Clavius's Law/Formulation 2

:$\vdash \paren {\neg p \implies p} \implies  p$

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth value under the main connective is true for all boolean interpretations.
:<nowiki>$\begin{array}{|cccc|c|c|} \hline
(\neg & p & \implies & p) & \implies & p \\
\hline
\T & \F & \F & \F & \T & \F \\
\F & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Equivalent Matrices may not be Similar

If two square matrices of order $n > 1$ over a ring with unity $R$ are equivalent, they are not necessarily similar.

Proof:
Proof by Counterexample:
Let $\mathbf A = \mathbf I_n$ be the unit matrix of order $n > 1$.
Let $\mathbf B$ be an arbitrary nonsingular matrix over $R$ of order $n$ that is different from the unit matrix.
Then:
:$\mathbf I_n^{-1} \mathbf A \mathbf B = \mathbf I_n^{-1} \mathbf I_n \mathbf B = \mathbf B$
showing that $\mathbf A$ and $\mathbf B$ are equivalent.
Let $\mathbf P$ be a nonsingular square matrix of order $n$.
Then:
:$\mathbf P^{-1} \mathbf A \mathbf P = \mathbf P^{-1} \mathbf P = \mathbf I_n \ne \mathbf B$
Hence, $\mathbf A$ is not similar to $\mathbf B$.
{{qed}}
Theorem: Odd Power Function is Strictly Increasing/General Result

Let $\struct {R, +, \circ, \le}$ be a totally ordered ring.
Let $n$ be an odd positive integer.
Let $f: R \to R$ be the mapping defined by:
:$\map f x = \map {\circ^n} x$
Then $f$ is strictly increasing on $R$.

Proof:
{{proofread}}
Let $x, y \in R$ such that $0 < x < y$.
By Power Function is Strictly Increasing on Positive Elements:
:$\map f x < \map f y$
Suppose that $x < y < 0$.
By Properties of Ordered Ring:
:$0 < -y < -x$
By Power Function is Strictly Increasing on Positive Elements (applied to $-y$ and $-x$):
:$0 < \map f {-y} < \map f {-x}$
By Power of Ring Negative:
:$\map f {-x} = -\map f x$
:$\map f {-y} = -\map f y$
Thus:
:$0 < -\map f y < -\map f x$
By Properties of Ordered Ring:
:$\map f x < \map f y$
By Sign of Odd Power:
:$\map f x < 0 = \map f 0$ when $x < 0$
:$\map f 0 = 0 < \map f x$ when $0 < x$
Thus we have shown that $f$ is strictly increasing on the positive elements and the negative elements, and across zero.
{{qed}}
Category:Totally Ordered Rings
Category:Odd Power Function is Strictly Increasing
eh5d5yt5qq4k9gyuhnvli3v2uu8bfkm
Theorem: Number of Bijective Restrictions

Let $f: S \to T$ be a surjection.
Let $B$ be the set of all bijective restrictions of $f$.
Then the cardinality of $B$ is:
:$\ds \card {\prod_{i \mathop \in I} \family {S / \RR_f}_i}$
where $S / \RR_f$ denotes the quotient set of the induced equivalence of $f$ indexed by $I$.

Proof:
{{proof wanted}}
Category:Bijections
Category:Restrictions
6kqq43g16lui5yu2a6ryj0y95zgrli4
Theorem: Number of Injective Restrictions

Let $f: S \to T$ be a mapping.
Let $Q$ be the set of all injective restrictions of $f$.
Then the cardinality of $Q$ is:
:$\ds \card {\prod_{i \mathop \in I} \prod_{j \mathop \in J_i} \family {\family {\powerset {S / \RR_f} }_i}_j}$
where:
:$\powerset \cdot$ denotes power set
:$S / \RR_f$ denotes quotient set of the induced equivalence of $f$.

Proof:
{{proof wanted}}
Category:Injections
b3789r3dwtxyt9mvq0dhswfwfa0bkx7
Theorem: Box Topology on Finite Product Space is Product Topology

Let $n \in \N$.
For all $k \in \set {1, \ldots, n}$, let $T_k = \struct {X_k, \tau_k}$ be topological spaces.
Let $\ds X = \prod_{k \mathop = 1}^n X_k$ be the cartesian product of $X_1, \ldots, X_n$.
Then the box topology and the product topology on $X$ are identical.

Proof:
Denote the product topology on $X$ as $\tau$, and the box topology on $X$ as $\tau'$.
Suppose that $U \in \tau'$.
Then there exists an index set $I$ such that:
:$\ds U = \bigcup_{i \mathop \in I} \struct {U_{i, 1} \times U_{i, 2} \times \cdots \times U_{i, n} }$
where $U_{i, k} \in \tau_k$ for all $i \in I, k \in \set {1, \ldots, n}$.
When $\pr_k: X \to X_k$ denotes the $k$th projection on $X$, we have:
:$\pr_k^{-1} \sqbrk {U_{i, k} } = X_1 \times X_2 \times \cdots \times X_{k - 1} \times U_{i, k} \times X_{k + 1} \times \cdots \times X_n$
It follows that:
:$\ds U = \bigcup_{i \mathop \in I} \struct {U_{i, 1} \times U_{i, 2} \times \cdots \times U_{i, n} } = \bigcup_{i \mathop \in I} \bigcap_{k \mathop = 1}^{n_i} \pr_k^{-1} \sqbrk {U_{i, k} }$
By definition of product topology, $U \in \tau$, so $\tau' \subseteq \tau$.
{{qed|lemma}}
Suppose that $U \in \tau$.
Then there exists an index set $I$, so $U$ can be expressed as:
$U = \ds \bigcup_{i \mathop \in I} \bigcap_{l \mathop = 1}^{m_i} \pr_{j_l}^{-1} \sqbrk {U_{i, l} }$
where $m_i \in \N$, $j_1, j_2, \ldots, j_{m_i} \in \set {1, \ldots, n}$, and $U_{i, l} \in \tau_{j_l}$ for all $i \in I, l \in \set {1, \ldots, m_i}$.
Then:
{{begin-eqn}}
{{eqn | l = U
      | r = \bigcup_{i \mathop \in I} \bigcap_{l \mathop = 1}^{m_i} \pr_{j_l}^{-1} \sqbrk {U_{i, l} }
}}
{{eqn | r = \bigcup_{i \mathop \in I} \bigcap_{k \mathop = 1}^n \bigcap_{l: k \mathop = j_l} \pr_k^{-1} \sqbrk {U_{i, l} }
}}
{{eqn | r = \bigcup_{i \mathop \in I} \bigcap_{k \mathop = 1}^n \struct {X_1 \times X_2 \times \cdots \times X_{k - 1} \times \bigcap_{l: k \mathop = j_l} U_{i, l} \times X_{k + 1} \times \cdots \times X_n}
}}
{{end-eqn}}
As $\ds \bigcap_{l: k \mathop = j_l} U_{i, l} \in \tau_k$, it follows that:
:$\ds \struct {X_1 \times X_2 \times \cdots \times X_{k - 1} \times \bigcap_{l: k \mathop = j_l} U_{i, l} \times X_{k + 1} \times \cdots \times X_n} \in \tau'$
By definition of topology, it follows that $U \in \tau'$, so $\tau \subseteq \tau'$.
{{qed}}
Theorem: Strictly Positive Integer Power Function is Unbounded Above/General Case

Let $\struct {R, +, \circ, \le}$ be a totally ordered ring with unity.
Suppose that $R$ has no upper bound.
Let $n \in \N_{>0}$.
Let $f: R \to R$ be defined by:
:$\map f x = \circ^n x$
Then the image of $f$ is unbounded above in $R$.

Proof:
Let $1_R$ be the unity of $R$.
Let $b \in R$.
We will show that $b$ is not an upper bound of the image of $f$.
Since $R$ is totally ordered and unbounded above, there is an element $c \in R$ such that $b < c$ and $1_R < c$.
By Strictly Positive Power of Strictly Positive Element Greater than One Succeeds Element, $c \le \map f c$.
Thus by transitivity of ordering, $b < \map f c$.
{{qed}}
Category:Totally Ordered Rings
Category:Rings with Unity
ourpo7kby1306f7ch5iz4zo25u4c3vb
Theorem: Strictly Positive Integer Power Function is Unbounded Above

Let $\R$ be the real numbers with the usual ordering.
Let $n \in \N_{>0}$.
Let $f: \R \to \R$ be defined by:
:$\map f x = x^n$
Then $f$ is unbounded above.

Proof:
If $n = 1$, then $f$ is the identity function.
By the Axiom of Archimedes, the real numbers are unbounded above.
Thus by definition of the identity function:
$f$ is unbounded above.
{{qed|lemma}}
Let $n \ge 2$.
{{AimForCont}} that $f$ is bounded above by $b \in \R$.
{{WLOG}} suppose that $b > 0$.
Then by the definition of an upper bound:
:$\forall x \in \R: x^n \le b$
Let $x > b$.
Then:
:$\dfrac {x^n - b} {x - b} \le 0$
By the Mean Value Theorem, there exists a point $p$ between $b$ and $x$ such that:
:$\map {f'} p = \dfrac {x^n - b} {x - b}$
By Derivative of Power:
:$\map {f'} p = n p^{n - 1}$
Therefore $n p^{n - 1} \le 0$.
By:
:Power of Strictly Positive Real Number is Positive
and:
:Strictly Positive Real Numbers are Closed under Multiplication it follows that:
:$p > 0 \implies n p^{n - 1} > 0$
But this is impossible because it was previously established that $p \ge b > 0$.
From this contradiction it follows that there can be no such $b$.
Hence the result.
{{qed}}
Theorem: Ring Product preserves Inequalities on Positive Elements

Let $\struct {R, +, \circ, \le}$ be an ordered ring.
Let $x, y, z, w \in R$.
Let $0 < x < y$ and $0 < z < w$.
Then:
:$0 < z \circ x < w \circ y$

Proof:
By Properties of Ordered Ring $(6)$:
:$z \circ x < z \circ y$
:$z \circ y < w \circ y$
Then by transitivity of $\circ$:
:$z \circ x < w \circ y$
Also by Properties of Ordered Ring $(6)$:
:$z \circ 0 < z \circ x$
Hence by Ring Product with Zero:
:$0 < z \circ x$
{{qed}}
Category:Ordered Rings
Category:Inequalities
e0clz004vppggt5grtn0ls0bmjjxvfu
Theorem: Power Function is Strictly Increasing on Positive Elements

Let $\struct {R, +, \circ, \le}$ be an ordered ring.
Let $x, y \in R$.
Let $n \in \N_{>0}$ be a strictly positive integer.
Let $0 < x < y$.
Then:
:$0 < \map {\circ^n} x < \map {\circ^n} y$

Proof:
Proof by induction:
For all $n \in \N_{> 0}$, let $\map P n$ be the proposition:
:$0 < \map {\circ^n} x < \map {\circ^n} y$
Theorem: Biconditional is Associative/Formulation 1

:$p \iff \paren {q \iff r} \dashv \vdash \paren {p \iff q} \iff r$

Proof:
Proof of associativity by natural deduction is just too tedious to be considered.
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connective match for all boolean interpretations.
$\begin{array}{|ccccc||ccccc|} \hline
p & \iff & (q & \iff & r) & (p & \iff & q) & \iff & r \\
\hline
\F & \F & \F & \T & \F & \F & \T & \F & \F & \F \\
\F & \T & \F & \F & \T & \F & \T & \F & \T & \T \\
\F & \T & \T & \F & \F & \F & \F & \T & \T & \F \\
\F & \F & \T & \T & \T & \F & \F & \T & \F & \T \\
\T & \T & \F & \T & \F & \T & \F & \F & \T & \F \\
\T & \F & \F & \F & \T & \T & \F & \F & \F & \T \\
\T & \F & \T & \F & \F & \T & \T & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Biconditional is Associative/Formulation 2

:$\vdash \paren {p \iff \paren {q \iff r} } \iff \paren {\paren {p \iff q} \iff r}$

Proof:
{{BeginTableau|\vdash \paren {p \iff \paren {q \iff r} } \iff \paren {\paren {p \iff q} \iff r} }}
{{Assumption|1|p \iff \paren {q \iff r} }}
{{SequentIntro|2|1|\paren {p \iff q} \iff r|1|Biconditional is Associative: Formulation 1}}
{{Implication|3||\paren {p \iff \paren {q \iff r} } \implies \paren {\paren {p \iff q} \iff r}|1|2}}
{{Assumption|4|\paren {p \iff q} \iff r}}
{{SequentIntro|5|4|p \iff \paren {q \iff r}|4|Biconditional is Associative: Formulation 1}}
{{Implication|6||\paren {\paren {p \iff q} \iff r} \implies \paren {p \iff \paren {q \iff r} }|4|5}}
{{BiconditionalIntro|7||\paren {p \iff \paren {q \iff r} } \iff \paren {\paren {p \iff q} \iff r}|3|6}}
{{EndTableau|qed}}
Theorem: Open Ball is Convex Set

Let $V$ be a normed vector space with norm $\norm {\,\cdot\,}$ over $\R$ or $\C$.
An open ball in the metric induced by $\norm {\,\cdot\,}$ is a convex set.

Proof:
Let $v \in V$ and $\epsilon \in \R_{>0}$.
Denote the open $\epsilon$-ball of $v$ as $\map {B_\epsilon} v$.
Let $x, y \in \map {B_\epsilon} v$.
Then $x + t \paren {y - x}$ lies on line segment joining $x$ and $y$ for all $t \in \closedint 0 1$.
The distance between $x + t \paren {y - x}$ and $v$ is:
{{begin-eqn}}
{{eqn | l = \norm {x + t \paren {y - x} - v}
      | r = \norm {\paren {1 - t} \paren {x - v} + t \paren {y - v} }
}}
{{eqn | o = \le
      | r = \norm {\paren {1 - t} \paren {x - v} } + \norm {t \paren {y - v} }
      | c = {{NormAxiomVector|3}}
}}
{{eqn | r = \paren {1 - t} \norm {x - v} + t \norm {y - v}
      | c = {{NormAxiomVector|2}}
}}
{{eqn | o = <
      | r = \paren {1 - t} \epsilon + t \epsilon
      | c = as $x, y \in \map {B_\epsilon} v$
}}
{{eqn | r = \epsilon
}}
{{end-eqn}}
Hence, $x + t \paren {y - x} \in \map {B_\epsilon} v$.
Thus, by definition, $\map {B_\epsilon} v$ is a convex set.
{{qed}}
Theorem: Pseudometric Space is Metric Space iff T0

Let $M = \struct {S, d}$ be a pseudometric space.
Let $T = \struct {S, \tau}$ be the topological space over $S$ induced by $d$.
Then $M$ is a metric space {{iff}} $T$ is a $T_0$ space.

Proof:
=== Necessary Condition ===
Let $M$ be a metric space.
From Metric Space is Hausdorff, $M$ is a Hausdorff space.
From:
:$T_2$ (Hausdorff) Space is $T_1$ Space
and:
:$T_1$ Space is $T_0$ Space
it follows that $M$ is a $T_0$ space.
{{qed|lemma}}
Theorem: Sequence Converges to Point Relative to Metric iff it Converges Relative to Induced Topology

Let $M = \struct {S, d}$ be a metric space or a pseudometric space.
Let $T = \struct {S, \tau}$ be the topological space induced by $d$.
Let $\sequence {x_n}$ be a infinite sequence in $S$.
Let $l \in S$.
Then $\sequence {x_n}$ converges to $l$ relative to $d$ {{iff}} $\sequence {x_n}$ converges to $l$ relative to $\tau$.

Proof:
=== Necessary Condition ===
Suppose that $\sequence {x_n}$ converges to $l$ relative to $d$.
When $\map {B_\epsilon} l$ denotes the open $\epsilon$-ball of $l$, this means:
:$\forall \epsilon \in \R_{>0}: \exists N \in \R: n > N \implies x_n \in \map {B_\epsilon} l$
Let $U \in \tau$ with $l \in U$.
By definition of induced topology, there exists $\epsilon_0 \in \R_{>0}$ such that:
:$\map {B_{\epsilon_0} } l \subseteq U$
Then there exists $N_0 \in \R$ such that for all $n > N_0$:
:$x_n \in \map {B_{\epsilon_0} } l \subseteq U$
Hence, $\sequence {x_n}$ converges to $l$ in the induced topology $\tau$.
{{qed|lemma}}
Theorem: Isometry Preserves Sequence Convergence

Let $M_1 = \struct {S_1, d_1}$ and $M_2 = \struct {S_2, d_2}$ both be metric spaces or pseudometric spaces.
Let $\phi: S_1 \to S_2$ be an isometry.
Let $\sequence {x_n}$ be an infinite sequence in $S_1$.
Suppose that $\sequence {x_n}$ converges to a point $p \in S_1$.
Then $\sequence {\map \phi {x_n}}$ converges to $\map \phi p$.

Proof:
{{begin-eqn}}
{{eqn | o =
      | r = \lim_{n \mathop \to \infty} \map {d_2} {\map \phi {x_n}, \map \phi p}
}}
{{eqn | r = \lim_{n \mathop \to \infty} \map {d_1} {x_n, p}
      | c = {{Defof|Isometry (Metric Spaces)|index = 1}}
}}
{{eqn | r = 0
      | c = {{Defof|Convergent Sequence|subdef = Metric Space|index = 3}}
}}
{{end-eqn}}
Hence, by definition, $\sequence {\map \phi {x_n}}$ converges to $\map \phi p$.
{{qed}}
Theorem: Isometry Preserves Sequence Convergence

Let $M_1 = \struct {S_1, d_1}$ and $M_2 = \struct {S_2, d_2}$ both be metric spaces or pseudometric spaces.
Let $\phi: S_1 \to S_2$ be an isometry.
Let $\sequence {x_n}$ be an infinite sequence in $S_1$.
Suppose that $\sequence {x_n}$ converges to a point $p \in S_1$.
Then $\sequence {\map \phi {x_n}}$ converges to $\map \phi p$.

Proof:
{{proof wanted|proof from the fact that an isometry is a homeomorphism}}
Theorem: Connected Domain is Connected by Staircase Contours

Let $D \subseteq \C$ be an open set.
Then $D$ is a connected domain {{iff}}:
:for all $z, w \in \C$, there exists a staircase contour in $D$ with start point $z$ and end point $w$.

Proof:
=== Necessary Condition ===
Suppose $D$ is a connected domain.
If $z, w \in D$, there exists a path $\gamma: \closedint 0 1 \to D$ with $\map \gamma 0 = z$ and $\map \gamma 0 = w$.
From the Paving Lemma, it follows that there exist $\epsilon \in \R_{>0}$ and a subdivision $\set {x_0, x_1, \ldots, x_n}$ of $\closedint 0 1$ such that:
:$\ds \bigcup_{k \mathop = 0}^n \map {B_\epsilon} {\map \gamma {x_k} } \subseteq D$
and for all $k \in \set {0, 1, \ldots, n - 1}$:
:$\map \gamma {\closedint {x_k} {x_{k + 1} } } \subseteq \map {B_\epsilon} {\map \gamma {x_k} }$
where $\map {B_\epsilon} {\map \gamma {x_k} }$ is the open $\epsilon$-ball about $\map \gamma {x_k}$.
Let $\map \Re {x_{k + 1} - x_k}$ denote the real part of $x_{k + 1} - x_k$, and $\map \Im {x_{k + 1} - x_k}$ denote the imaginary part of $x_{k + 1} - x_k$.
For all $k \in \set {0, 1, \ldots, n - 1}$, define the smooth paths $\gamma_{2 k + 1}, \gamma_{2 k + 2}: \gamma: \closedint 0 1 \to D$ by:
:$\map {\gamma_{2 k + 1} } t = x_k + t \paren {\map \Re {x_{k + 1} - x_k} }$
:$\map {\gamma_{2 k + 2} } t = x_k + \map \Re {x_{k + 1} - x_k} + i t \paren {\map \Im {x_{k + 1} - x_k} }$
These are the line segments connecting $x_k$, $x_k + \map \Re {x_{k + 1} - x_k}$, and $x_{k + 1}$.
It follows that $x_k + \map \Re {x_{k + 1} - x_k} \in \map {B_\epsilon} {\map \gamma {x_k} }$, as:
{{begin-eqn}}
{{eqn | l = \cmod {\map \Re {x_{k + 1} - x_k} }
      | o = \le 
      | r = \cmod {x_{k + 1} - x_k}
      | c = Modulus Larger than Real Part
}}
{{eqn | o = <
      | r = \epsilon
}}
{{end-eqn}}
Then Open Ball is Convex Set shows that $\map {\gamma_{2 k + 1} } t, \map {\gamma_{2 k + 2} } t \in \map {B_\epsilon} {\map \gamma {x_k} } \subseteq D$ for all $t \in \closedint 0 1$.
It follows that the images of $\gamma_{2k+1}$ and $\gamma_{2k+2}$ are subsets of $D$. 
Define $C_k$ as the directed smooth curve that is parameterized by $\gamma_k$.
Thus $C_{2 k - 1}$ has start point $x_{k - 1}$, and $C_{2 k}$ has end point $x_k$.
Define $C$ as the concatenation of $C_1, \ldots, C_{2n}$.
Then $C$ is a staircase contour in $D$ with start point $z$ and end point $w$.
:File:ConnectedDomainStaircase.png
Illustration of the open balls inside the connected domain $D$.
The path $\gamma$ between $w$ and $z$ is grey, and the constructed staircase contour $C$ is red.
{{qed|lemma}}
Theorem: Dedekind Completeness is Self-Dual

Let $\struct {S, \preceq}$ be an ordered set.
Then $\struct {S, \preceq}$ is Dedekind complete {{iff}} every non-empty subset of $S$ that is bounded below admits an infimum in $S$.
That is, an ordered set is Dedekind complete {{iff}} its dual is Dedekind complete.

Proof:
=== Necessary Condition ===
Let $\struct {S, \preceq}$ be Dedekind complete.
Let $A \subseteq S$ be non-empty and bounded below.
Let $B \subseteq S$ be set of all lower bounds for $A$.
Then every element of $A$ is an upper bound for $B$.
Therefore, $B$ is non-empty and bounded above.
By the definition of Dedekind completeness, $B$ admits a supremum $x \in S$.
By the definition of supremum, it follows that every element of $A$ succeeds $x$.
That is, $x$ is a lower bound for $A$.
If $y \in S$ is a lower bound for $A$, then $y \in B$, and so $y \preceq x$.
Hence, $x$ is the infimum of $A$.
{{qed|lemma}}
Theorem: Biconditional is Transitive/Formulation 1

:$p \iff q, q \iff r \vdash p \iff r$

Proof:
{{BeginTableau|p \iff q, q \iff r \vdash p \iff r}}
{{Premise|1|p \iff q}}
{{Premise|2|q \iff r}}
{{BiconditionalElimination|3|1|p \implies q|1|1}}
{{BiconditionalElimination|4|2|q \implies r|2|1}}
{{SequentIntro|5|1, 2|p \implies r|1, 2|Hypothetical Syllogism: Formulation 1}}
{{BiconditionalElimination|6|1|q \implies p|1|2}}
{{BiconditionalElimination|7|2|r \implies q|2|2}}
{{SequentIntro|8|1, 2|r \implies p|7, 6|Hypothetical Syllogism: Formulation 1}}
{{BiconditionalIntro|9|1, 2|p \iff r|5|8}}
{{EndTableau|qed}}
Theorem: Biconditional is Transitive/Formulation 1

:$p \iff q, q \iff r \vdash p \iff r$

Proof:
We apply the Method of Truth Tables.
As can be seen for all boolean interpretations by inspection, where the truth values under the main connective on the {{LHS}} is $T$, that under the one on the {{RHS}} is also $T$:
:<nowiki>$\begin {array} {|ccccccc||ccc|} \hline
(p & \iff & q) & \land & (q & \iff & r) & p & \iff & r \\
\hline
\F & \T & \F & \T & \F & \T & \F & \F & \T & \F \\
\F & \T & \F & \F & \F & \F & \T & \F & \F & \T \\
\F & \F & \T & \F & \T & \F & \F & \F & \T & \F \\
\F & \F & \T & \F & \T & \T & \T & \F & \F & \T \\
\T & \F & \F & \F & \F & \T & \F & \T & \F & \F \\
\T & \F & \F & \F & \F & \F & \T & \T & \T & \T \\
\T & \T & \T & \F & \T & \F & \F & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end {array}$</nowiki>
Hence the result.
{{qed}}