avewright/proofwiki-math huggingface dataset:
Theorem: Conjunction with Negative is Equivalent to Negation of Conditional/Formulation 2

:$\vdash \paren {p \land \neg q} \iff \paren {\neg \paren {p \implies q} }$

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connective is true for all boolean interpretations.
:<nowiki>$\begin{array}{|cccc|c|cccc|} \hline
p & \land & \neg & q & \iff & \neg & (p & \implies & q) \\
\hline
\F & \F & \T & \F & \T & \F & \F & \T & \F \\
\F & \F & \F & \T & \T & \F & \F & \T & \T \\
\T & \T & \T & \F & \T & \T & \T & \F & \F \\
\T & \F & \F & \T & \T & \F & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Conjunction with Negative is Equivalent to Negation of Conditional/Formulation 2

:$\vdash \paren {p \land \neg q} \iff \paren {\neg \paren {p \implies q} }$

Proof:
{{BeginTableau|\vdash \paren {\neg \paren {p \implies q} } \implies \paren {p \land \neg q} }}
{{Assumption|1|\neg \paren {p \implies q} }}
{{Assumption|2|\neg \paren {p \land \neg q} }}
{{SequentIntro|3|2|p \implies q|2|Conditional is Equivalent to Negation of Conjunction with Negative}}
{{NonContradiction|4|1, 2|3|1}}
{{Reductio|5|1|p \land \neg q|2|4}}
{{Implication|6||\paren {\neg \paren {p \implies q} } \implies \paren {p \land \neg q}|1|5}}
{{EndTableau|qed}}
{{LEM|Reductio ad Absurdum|3}}
Theorem: Conjunction with Negative is Equivalent to Negation of Conditional/Formulation 2

:$\vdash \paren {p \land \neg q} \iff \paren {\neg \paren {p \implies q} }$

Proof:
{{BeginTableau|\vdash \paren {\neg \paren {p \implies q} } \implies \paren {p \land \neg q} }}
{{Assumption|1|\neg \paren {p \implies q} }}
{{SequentIntro|2|1|p \land \neg q|1|Conjunction with Negative is Equivalent to Negation of Conditional: Formulation 1: Reverse Implication}}
{{Implication|3||\paren {\neg \paren {p \implies q} } \implies \paren {p \land \neg q}|1|2}}
{{EndTableau|qed}}
{{LEM|Conjunction with Negative is Equivalent to Negation of Conditional/Formulation 1/Reverse Implication|3}}
Theorem: Reflexive Circular Relation is Equivalence

Let $\RR \subseteq S \times S$ be a reflexive and circular relation in $S$.
Then $\RR$ is an equivalence relation.

Proof:
To prove a relation is an equivalence, we need to prove it is reflexive, symmetric and transitive.
So, checking in turn each of the criteria for equivalence:
Theorem: Inverse of Algebraic Structure Isomorphism is Isomorphism/General Result

Let $\phi: \struct {S, \circ_1, \circ_2, \ldots, \circ_n}$ and $\struct {T, *_1, *_2, \ldots, *_n}$ be algebraic structures.
Let $\phi: \struct {S, \circ_1, \circ_2, \ldots, \circ_n} \to \struct {T, *_1, *_2, \ldots, *_n}$ be a mapping.
Then:
:$\phi: \struct {S, \circ_1, \circ_2, \ldots, \circ_n} \to \struct {T, *_1, *_2, \ldots, *_n}$ is an isomorphism
{{iff}}:
:$\phi^{-1}: \struct {T, *_1, *_2, \ldots, *_n} \to \struct {S, \circ_1, \circ_2, \ldots, \circ_n}$ is also an isomorphism.

Proof:
As $\paren {\phi^{-1} }^{-1} = \phi$, it suffices to show the sufficient condition.
Suppose that $\phi$ is an isomorphism.
We shall show that $\phi^{-1}$ is also an isomorphism.
We have {{afortiori}} that $\phi$ is a bijection.
Hence from Inverse of Bijection is Bijection we have that $\phi^{-1}$ is also a bijection.
Then for all $x, y \in T$ and $i \in \set {1, 2, \ldots, n}$:
{{begin-eqn}}
{{eqn | l = x \ast_i y
      | r = \map \phi {\map {\phi^{-1} } x} \ast_i \map \phi {\map {\phi^{-1} } y}
      | c = {{Defof|Inverse Mapping|index = 2}}
}}
{{eqn | r = \map \phi {\map {\phi^{-1} } x \circ_i \map {\phi^{-1} } y}
      | c = as $\phi$ is a homomorphism
}}
{{eqn | ll= \leadsto
      | l = \map {\phi^{-1} } {x \ast_i y}
      | r = \map {\phi^{-1} } {\map \phi {\map {\phi^{-1} } x \circ_i \map {\phi^{-1} } y} }
      | c = applying $\phi^{-1}$ to both sides
}}
{{eqn | r = \map {\phi^{-1} } x \circ_i \map {\phi^{-1} } y
      | c = {{Defof|Inverse Mapping|index = 2}}
}}
{{end-eqn}}
Therefore $\phi^{-1}$ is a homomorphism.
{{qed}}
Category:Inverse of Algebraic Structure Isomorphism is Isomorphism
7yqi9869wvllfbqst9b4bunztgity1h
Theorem: Fundamental Theorem of Calculus for Complex Riemann Integrals

Let $\closedint a b$ be a closed real interval.
Let $F, f: \closedint a b \to \C$ be complex functions.
Suppose that $F$ is a primitive of $f$.
Then the complex Riemann integral of $f$ satisfies:
:$\ds \int_a^b \map f t \rd t = \map F b - \map F a$

Proof:
{{proofread|Missing proof that the conditions for Cauchy-Riemann Equations are satisfied}}
Let $u, v: \closedint a b \times \set 0 \to \R$ be defined as in the Cauchy-Riemann Equations:
:$\map u {t, y} = \map \Re {\map F z}$
:$\map v {t, y} = \map \Im {\map F z}$
where:
:$\map \Re {\map F z}$ denotes the real part of $\map F z$
:$\map \Im {\map F z}$ denotes the imaginary part of $\map F z$.
Then:
{{begin-eqn}}
{{eqn | l = \int_a^b \map f t \rd t
      | r = \int_a^b \map {F'} {t} \rd t
      | c = {{Defof|Complex Primitive}}
}}
{{eqn | r = \int_a^b \map {F'} {t + 0 i} \rd t
      | c = 
}}
{{eqn | r = \int_a^b \paren {\map {\dfrac {\partial u} {\partial t} } {t, 0} + i \map {\dfrac {\partial v} {\partial t} } {t, 0} } \rd t
      | c = Cauchy-Riemann Equations
}}
{{eqn | r = \int_a^b \map {\dfrac {\partial u} {\partial t} } {t, 0} \rd t + i \int_a^b \map {\dfrac {\partial v} {\partial t} } {t, 0} \rd t
      | c = {{Defof|Complex Riemann Integral}}
}}
{{eqn | r = \map u {b, 0} - \map u {a, 0} + i \paren {\map v {b, 0} - \map v {a, 0} }
      | c = Fundamental Theorem of Calculus 
}}
{{eqn | r = \map F b - \map F a
}}
{{end-eqn}}
{{qed}}
Theorem: Fundamental Theorem of Calculus for Contour Integrals

Let $F, f: D \to \C$ be complex functions, where $D$ is a connected domain.
Let $C$ be a contour that is a concatenation of the directed smooth curves $C_1, \ldots, C_n$.
Let $C_k$ be parameterized by the smooth path $\gamma_k: \closedint {a_k} {b_k} \to D$ for all $k \in \set {1, \ldots, n}$.
Suppose that $F$ is an antiderivative of $f$.
If $C$ has start point $z$ and end point $w$, then:
:$\ds \int_C \map f z \rd z = \map F w - \map F z$
If $C$ is a closed contour, then:
:$\ds \oint_C \map f z \rd z = 0$

Proof:
{{begin-eqn}}
{{eqn | l = \int_C \map f z
      | r = \sum_{k \mathop = 1}^n \int_{a_k}^{b_k} \map f {\map {\gamma_k} t} \map {\gamma_k'} t \rd t
      | c = {{Defof|Complex Contour Integral}}
}}
{{eqn | r = \sum_{k \mathop = 1}^n \int_{a_k}^{b_k} \paren {\dfrac \rd {\rd t} \map F {\map {\gamma_k} t} } \rd t
      | c = Derivative of Complex Composite Function
}}
{{eqn | r = \sum_{k \mathop = 1}^n \paren {\map F {\map {\gamma_k} {b_k} } - \map F {\map {\gamma_k} {a_k} } }
      | c = Fundamental Theorem of Calculus for Complex Riemann Integrals
}}
{{eqn | r = \map F {\map {\gamma_n} {b_n} } - \map F {\map {\gamma_1} {a_1} }
      | c = the sum is telescoping
}}
{{eqn | r = \map F w - \map F z
      | c = {{Defof|Endpoints of Contour (Complex Plane)}}
}}
{{end-eqn}}
If $C$ is a closed contour, then $z = w$.
It follows that:
:$\map F w - \map F z = 0$
{{qed}}
Theorem: Power Series is Taylor Series

Let $\ds \map f z = \sum_{n \mathop = 0}^\infty a_n \paren {z - \xi}^n$ be a complex power series about $\xi \in \C$.
Let $R$ be the radius of convergence of $f$.
Then, $f$ is of differentiability class $C^\infty$.
For all $n \in \N$:
:$a_n = \dfrac {\map {f^{\paren n} } \xi} {n!}$
Hence, $f$ is equal to its Taylor series expansion about $\xi$:
:$\ds \forall z \in \C, \size {z - \xi} < R: \quad \map f z = \sum_{n \mathop = 0}^\infty \dfrac {\paren {z - \xi}^n} {n!} \map {f^{\paren n} } \xi$

Proof:
First, we prove by induction over $k \in \N_{\ge 1}$ that:
:$\ds \map {f^{\paren k} } z = \sum_{n \mathop = k}^\infty a_n \paren {z - \xi}^{n - k} n^{\underline k}$
where $n^{\underline k}$ denotes the falling factorial.
Theorem: Image of Complex Exponential Function

The image of the complex exponential function is $\C \setminus \set 0$.

Proof:
Let $z \in \C \setminus \set 0$.
Let $r = \cmod z$ denote the modulus of $z$.
Let $\theta = \map \arg z$ denote the argument of $z$.
Then $r > 0$.
Let $\ln$ denote the real natural logarithm.
Let $e$ denote the real exponential function.
Then:
{{begin-eqn}}
{{eqn | l = \map \exp {\ln r + i \theta}
      | r = e^{\ln r} \paren {\cos \theta + i \sin \theta}
      | c = {{Defof|Exponential Function/Complex|subdef = Real Functions|Complex Exponential Function}}
}}
{{eqn | r = r \paren {\cos \theta + i \sin \theta}
      | c = Exponential of Natural Logarithm
}}
{{eqn | r = z
      | c = {{Defof|Polar Form of Complex Number}}
}}
{{end-eqn}}
Hence, $z \in \Img \exp$.
Suppose instead that $z = 0$.
Let $z_0 = r_0 \paren {\cos \theta_0 + i \sin \theta_0} \in \C$.
From Exponential Tends to Zero and Infinity, it follows that $e^{r_0} \ne 0$.
As $\cmod {\cos \theta_0 + i \sin \theta_0} = 1$, it follows that:
:$\cos \theta_0 + i \sin \theta_0 \ne 0$
Then this equation has no solutions:
:$0 = \exp z_0 = e^{r_0} \paren {\cos \theta_0 + i \sin \theta_0}$
Hence:
:$\Img \exp = \C \setminus \set 0$
{{qed}}
Theorem: Reciprocal of Complex Exponential

:$\dfrac 1 {\map \exp z} = \map \exp {-z}$

Proof:
{{begin-eqn}}
{{eqn | l = \map \exp {-z}
      | r = \dfrac {\map \exp {-z} } {\map \exp 0}
      | c = as $\map \exp 0 = 1$ by Exponential of Zero
}}
{{eqn | r = \dfrac {\map \exp {-z} } {\map \exp {z - z} }
}}
{{eqn | r = \dfrac {\map \exp {-z} } {\map \exp z \, \map \exp {-z} }
      | c = Exponential of Sum: Complex Numbers
}}
{{eqn | r = \dfrac 1 {\map \exp z}
}}
{{end-eqn}}
{{qed}}
Theorem: Power Function Preserves Ordering in Ordered Semigroup

Let $\struct {S, \circ, \preceq}$ be an ordered semigroup.
Let $x, y \in S$ such that $x \preceq y$.
Let $n \in \N_{>0}$ be a strictly positive integer.
Then:
:$x^n \preceq y^n$
where $x^n$ is the $n$th power of $x$.

Proof:
By definition of ordered semigroup:
:$\preceq$ is compatible with $\circ$.
By definition of ordering:
:$\preceq$ is transitive.
Thus by Transitive Relation Compatible with Semigroup Operation Relates Powers of Related Elements:
:$x^n \preceq y^n$
{{qed}}
Theorem: Power Function Preserves Ordering in Ordered Semigroup

Let $\struct {S, \circ, \preceq}$ be an ordered semigroup.
Let $x, y \in S$ such that $x \preceq y$.
Let $n \in \N_{>0}$ be a strictly positive integer.
Then:
:$x^n \preceq y^n$
where $x^n$ is the $n$th power of $x$.

Proof:
The proof proceeds by induction.
For all $n \in \Z_{>0}$, let $\map P n$ be the proposition:
:$x \preceq y \implies x^n \preceq y^n$
$\map P 1$ is the case:
:$x \preceq y \implies x \preceq y$
which is trivially true.
Thus $\map P 1$ is seen to hold.
=== Basis for the Induction ===
We have:
{{begin-eqn}}
{{eqn | l = x
      | o = \preceq
      | r = y
}}
{{eqn | ll= \implies
      | l = x \circ x
      | o = \preceq
      | r = x \circ y
      | c = Ordered Semigroup Axiom $\text {OS} 2$: Compatibility of $\preceq$ with $\circ$
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = x
      | o = \preceq
      | r = y
}}
{{eqn | ll= \implies
      | l = x \circ y
      | o = \preceq
      | r = y \circ y
      | c = Ordered Semigroup Axiom $\text {OS} 2$: Compatibility of $\preceq$ with $\circ$
}}
{{end-eqn}}
Hence as $\preceq$ is an ordering and hence transitive:
:$x \preceq y \implies x \circ x \preceq y \circ y$
That is:
:$x \preceq y \implies x^2 \preceq y^2$
Thus $\map P 2$ is seen to hold.
This is the basis for the induction.
=== Induction Hypothesis ===
Now it needs to be shown that if $\map P k$ is true, where $k \ge 1$, then it logically follows that $\map P {k + 1}$ is true.
So this is the induction hypothesis:
:$x \preceq y \implies x^k \preceq y^k$
from which it is to be shown that:
:$x \preceq y \implies x^{k + 1} \preceq y^{k + 1}$
=== Induction Step ===
This is the induction step:
{{begin-eqn}}
{{eqn | l = x
      | o = \preceq
      | r = y
}}
{{eqn | ll= \implies
      | l = x \circ x^k
      | o = \preceq
      | r = x \circ y^k
      | c = Ordered Semigroup Axiom $\text {OS} 2$: Compatibility of $\preceq$ with $\circ$ and Induction Hypothesis
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = x
      | o = \preceq
      | r = y
}}
{{eqn | ll= \implies
      | l = x \circ y^k
      | o = \preceq
      | r = y \circ y^k
      | c = Ordered Semigroup Axiom $\text {OS} 2$: Compatibility of $\preceq$ with $\circ$
}}
{{end-eqn}}
Hence as $\preceq$ is an ordering and hence transitive:
:$x \preceq y \implies x \circ x^k \preceq y \circ y^k$
That is:
:$x \preceq y \implies x^{k + 1} \preceq y^{k + 1}$
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\forall n \in \Z_{\ge 0}: x \preceq y \implies x^n \preceq y^n$
{{qed}}
Theorem: Power Function Preserves Ordering in Ordered Group

Let $n \in \N_{>0}$ be a strictly positive integer.
Let $\prec$ be the reflexive reduction of $\preccurlyeq$.
Then the following hold:
{{begin-eqn}}
{{eqn | q = \forall x, y \in S
      | l = x \preccurlyeq y
      | o = \implies
      | r = x^n \preccurlyeq y^n
}}
{{eqn | q = \forall x, y \in S
      | l = x \prec y
      | o = \implies
      | r = x^n \prec y^n
}}
{{end-eqn}}
where $x^n$ denotes the $n$th power of $x$.

Proof:
By Power Function Preserves Ordering in Ordered Group:
{{begin-eqn}}
{{eqn | q = \forall x \in S
      | l = x \preccurlyeq e
      | o = \implies
      | r = x^n \preccurlyeq e^n
}}
{{eqn | l = e \preccurlyeq x
      | o = \implies
      | r = e^n \preccurlyeq x^n
}}
{{eqn | l = x \prec e
      | o = \implies
      | r = x^n \prec e^n
}}
{{eqn | l = e \prec x
      | o = \implies
      | r = e^n \prec x^n
}}
{{end-eqn}}
By Identity Element is Idempotent, $e$ is idempotent with respect to $\circ$.
Therefore by the definition of an idempotent element, $e^n = e$.
Thus the theorem holds.
{{qed}}
Theorem: Power Function Preserves Ordering in Ordered Group

Let $n \in \N_{>0}$ be a strictly positive integer.
Let $\prec$ be the reflexive reduction of $\preccurlyeq$.
Then the following hold:
{{begin-eqn}}
{{eqn | q = \forall x, y \in S
      | l = x \preccurlyeq y
      | o = \implies
      | r = x^n \preccurlyeq y^n
}}
{{eqn | q = \forall x, y \in S
      | l = x \prec y
      | o = \implies
      | r = x^n \prec y^n
}}
{{end-eqn}}
where $x^n$ denotes the $n$th power of $x$.

Proof:
By the definition of an ordered group, $\preccurlyeq$ is a transitive relation compatible with $\circ$.
By Transitive Relation Compatible with Semigroup Operation Relates Powers of Related Elements:
:$x \preccurlyeq e \implies x^n \preccurlyeq e^n$
:$e \preccurlyeq x \implies e^n \preccurlyeq x^n$
By Identity Element is Idempotent, $e$ is idempotent with respect to $\circ$.
Thus we obtain the first two results:
:$x \preccurlyeq e \implies x^n \preccurlyeq e$
:$e \preccurlyeq x \implies e \preccurlyeq x^n$
By Reflexive Reduction of Relation Compatible with Group Operation is Compatible, $\prec$ is compatible with $\circ$.
By Reflexive Reduction of Transitive Antisymmetric Relation is Strict Ordering, $\prec$ is transitive.
Thus by the same method as above, we obtain the remaining results:
:$x \prec e \implies x^n \prec e$
:$e \prec x \implies e \prec x^n$
{{qed}}
Theorem: Power Function Preserves Ordering in Ordered Group

Let $n \in \N_{>0}$ be a strictly positive integer.
Let $\prec$ be the reflexive reduction of $\preccurlyeq$.
Then the following hold:
{{begin-eqn}}
{{eqn | q = \forall x, y \in S
      | l = x \preccurlyeq y
      | o = \implies
      | r = x^n \preccurlyeq y^n
}}
{{eqn | q = \forall x, y \in S
      | l = x \prec y
      | o = \implies
      | r = x^n \prec y^n
}}
{{end-eqn}}
where $x^n$ denotes the $n$th power of $x$.

Proof:
By definition of ordered group:
:$\preccurlyeq$ is compatible with $\circ$.
By definition of ordering:
:$\preccurlyeq$ is transitive.
From Reflexive Reduction of Relation Compatible with Group Operation is Compatible:
:$\prec$ is also compatible with $\circ$.
From Reflexive Reduction of Transitive Antisymmetric Relation is Strict Ordering:
:$\prec$ is also transitive.
By definition of ordered group:
:$\struct {S, \circ}$ is a  ordered group, and therefore {{afortiori}} a semigroup.
The result follows from Transitive Relation Compatible with Semigroup Operation Relates Powers of Related Elements.
{{qed}}
Theorem: Power Function Preserves Ordering in Ordered Group

Let $n \in \N_{>0}$ be a strictly positive integer.
Let $\prec$ be the reflexive reduction of $\preccurlyeq$.
Then the following hold:
{{begin-eqn}}
{{eqn | q = \forall x, y \in S
      | l = x \preccurlyeq y
      | o = \implies
      | r = x^n \preccurlyeq y^n
}}
{{eqn | q = \forall x, y \in S
      | l = x \prec y
      | o = \implies
      | r = x^n \prec y^n
}}
{{end-eqn}}
where $x^n$ denotes the $n$th power of $x$.

Proof:
An ordered group is an ordered structure which is also a group.
Hence an ordered group is {{afortiori}} an ordered semigroup.
From Power Function Preserves Ordering in Ordered Semigroup:
:$\forall x, y \in S: x \preccurlyeq y \implies x^n \preccurlyeq y^n$
From the Cancellation Laws, every element of a group is cancellable.
Hence from Power Function with Cancellable Element Preserves Strict Ordering in Ordered Semigroup:
:$\forall x, y \in S: x \prec y \implies x^n \prec y^n$
{{qed}}
Theorem: Period of Complex Exponential Function

:$\map \exp {z + 2 k \pi i} = \map \exp z$

Proof:
{{begin-eqn}}
{{eqn | l = \map \exp {z + 2 k \pi i}
      | r = \map \exp z \, \map \exp {2 k \pi i}
      | c = Exponential of Sum: Complex Numbers
}}
{{eqn | r = \map \exp z \times 1
      | c = Euler's Formula Example: $e^{2 k i \pi}$
}}
{{eqn | r = \map \exp z
}}
{{end-eqn}}
{{qed}}
Theorem: Period of Complex Exponential Function

:$\map \exp {z + 2 k \pi i} = \map \exp z$

Proof:
{{begin-eqn}}
{{eqn | l = e^{i \paren {\theta + 2 k \pi} }
      | r = \map \cos {\theta + 2 k \pi} + i \, \map \sin {\theta + 2 k \pi}
      | c = Euler's Formula
}}
{{eqn | r = \cos \theta + i \sin \theta
      | c = Sine and Cosine are Periodic on Reals
}}
{{eqn | r = e^{i \theta}
      | c = Euler's Formula
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Complex Polynomial

Let $a_n \in \C$ for $n \in \set {0, 1, \ldots, N}$, where $N \in \N$.
Let $f: \C \to \C$ be a complex polynomial defined by $\ds \map f z = \sum_{n \mathop = 0}^N a_n z^n$.
Then $f$ is complex differentiable and its derivative is:
:$\ds \map {f'} z = \sum_{n \mathop = 1}^N n a_n z^{n - 1}$

Proof:
For all $n > N$, put $a_n = 0$.
Then:
:$\ds \map f z = \sum_{n \mathop = 0}^\infty a_n z^n$
The result now follows from Derivative of Complex Power Series.
{{qed}}
Category:Complex Differential Calculus
42ks1h3kb95t4difyockiyrqs87ify7
Theorem: Cantor's Intersection Theorem

Let $M = \struct {A, d}$ be a complete metric space.
Let $\sequence {S_n}$ be a nested sequence of closed balls in $M$ defined by:
:$S_n = \map {B^-_{\rho_n} } {x_n}$
where $\rho_n \to 0$ as $n \to \infty$ and:
:$S_1 \supseteq S_2 \supseteq \cdots \supseteq S_n \supseteq \cdots$
Then there exists a unique $x \in A$ such that:
:$\ds \bigcap_{n \mathop = 1}^\infty S_n = \set x$

Proof:
Let $S_n = \map {B^-_{\rho_n} } {x_n}$ be the closed ball of radius $\rho_n$ about the point $x_n$.
That is, let $S_n = \set {x \in A: \map d {x_n, x} \le \rho_n}$.
Then the sequence $\sequence {x_n}$ forms a Cauchy sequence:
:$\map d {x_n, x_{n + p} } < \rho_n$
for any $p \ge 0$ since $S_{n + p} \subseteq S_n$.
However, $\rho_n \to 0$ as $n \to \infty$ and therefore $\map d {x_n, x_{n + p} } \to 0$ as $n \to \infty$ for any $p \ge 0$.
Since the space $M$ is complete, there exists $x \in X$ such that $x_n \to x$ as $n \to \infty$.
Then since the subsequence $\sequence {x_k}_{k \mathop = n}^\infty$ is contained entirely in $S_n$ and converges to $x$, $x$ is a member of the closure of $S_n$ by Closure of Subset of Metric Space by Convergent Sequence.
Since $S_n$ is closed, by Closed Set Equals its Closure, we have:
:$\forall n \in \N: x \in S_n$
Hence:
:$\ds x \in \bigcap_{n \mathop = 1}^\infty S_n$
Suppose now that $y \ne x$.
Then it follows that $\map d {x, y} > 0$, and hence that for some $n$:
:$\map d {x, y} > 2 \rho_n$
Since $x, x_n \in S_n$, it then follows that:
:$\map d {x, x_n} \le \rho_n$
Now:
{{begin-eqn}}
{{eqn | l = 2 \rho_n
      | o = <
      | r = \map d {x, y}
}}
{{eqn | o = \le
      | r = \map d {x, x_n} + \map d {x_n, y}
      | c = {{Metric-space-axiom|2}}
}}
{{eqn | o = \le
      | r = \rho_n + \map d {x_n, y}
}}
{{end-eqn}}
From the above, it follows that:
:$\map d {x_n, y} > \rho_n$
so that $y \notin S_n$, and consequently:
:$\ds y \notin \bigcap_{i \mathop = 1}^\infty S_n$
Hence:
:$\ds \bigcap_{n \mathop = 1}^\infty S_n = \set x$
{{qed}}
Theorem: Principle of Dilemma/Formulation 1

:$\paren {p \implies q} \land \paren {\neg p \implies q} \dashv \vdash q$

Proof:
{{BeginTableau|\paren {p \implies q} \land \paren {\neg p \implies q} \vdash q}}
{{Premise|1|\paren {p \implies q} \land \paren {\neg p \implies q} }}
{{Simplification|2|1|p \implies q|1|1}}
{{Simplification|3|1|\neg p \implies q|1|2}}
{{SequentIntro|4|1|p \lor \neg p \implies q \lor q|2, 3|Constructive Dilemma}}
{{ExcludedMiddle|5|p \lor \neg p}}
{{ModusPonens|6|1|q \lor q|4|5}}
{{Idempotence|7|1|q|6|Disjunction}}
{{EndTableau|qed}}
{{LEM||3}}
Theorem: Principle of Dilemma/Formulation 1

:$\paren {p \implies q} \land \paren {\neg p \implies q} \dashv \vdash q$

Proof:
{{BeginTableau|\paren {p \implies q} \land \paren {\neg p \implies q} \vdash q}}
{{Premise|1|\paren {p \implies q} \land \paren {\neg p \implies q} }}
{{Simplification|2|1|p \implies q|1|1}}
{{Simplification|3|1|\neg p \implies q|1|2}}
{{ExcludedMiddle|4|p \lor \neg p}}
{{Assumption|5|p}}
{{ModusPonens|6|1, 5|q|2|5}}
{{Assumption|7|\neg p}}
{{ModusPonens|8|1, 7|q|3|7}}
{{ProofByCases|9|1|q|4|5|6|7|8}}
{{EndTableau|qed}}
{{LEM||3}}
Theorem: Principle of Dilemma/Formulation 1

:$\paren {p \implies q} \land \paren {\neg p \implies q} \dashv \vdash q$

Proof:
From the Constructive Dilemma we have:
:$p \implies q, r \implies s \vdash p \lor r \implies q \lor s$
from which, changing the names of letters strategically:
:$p \implies q, \neg p \implies q \vdash p \lor \neg p \implies q \lor q$
From Law of Excluded Middle, we have:
:$\vdash p \lor \neg p$
From the Rule of Idempotence we have:
:$q \lor q \vdash q$
and the result follows by Hypothetical Syllogism.
{{qed}}
{{LEM||3}}
Theorem: Principle of Dilemma/Formulation 1

:$\paren {p \implies q} \land \paren {\neg p \implies q} \dashv \vdash q$

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
:<nowiki>$\begin{array}{|cccccccc||c|} \hline
(p & \implies & q) & \land & (\neg & p & \implies & q) & q \\
\hline
\F & \T & \F & \F & \T & \F & \F & \F & \F \\
\F & \T & \T & \T & \T & \F & \T & \T & \T \\
\T & \F & \F & \F & \F & \T & \T & \F & \F \\
\T & \T & \T & \T & \F & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Principle of Dilemma/Formulation 1/Forward Implication

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

Proof:
{{BeginTableau|\paren {p \implies q} \land \paren {\neg p \implies q} \vdash q}}
{{Premise|1|\paren {p \implies q} \land \paren {\neg p \implies q} }}
{{Simplification|2|1|p \implies q|1|1}}
{{Simplification|3|1|\neg p \implies q|1|2}}
{{SequentIntro|4|1|p \lor \neg p \implies q \lor q|2, 3|Constructive Dilemma}}
{{ExcludedMiddle|5|p \lor \neg p}}
{{ModusPonens|6|1|q \lor q|4|5}}
{{Idempotence|7|1|q|6|Disjunction}}
{{EndTableau|qed}}
{{LEM||3}}
Theorem: Principle of Dilemma/Formulation 1/Forward Implication

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

Proof:
{{BeginTableau|\paren {p \implies q} \land \paren {\neg p \implies q} \vdash q}}
{{Premise|1|\paren {p \implies q} \land \paren {\neg p \implies q} }}
{{Simplification|2|1|p \implies q|1|1}}
{{Simplification|3|1|\neg p \implies q|1|2}}
{{ExcludedMiddle|4|p \lor \neg p}}
{{Assumption|5|p}}
{{ModusPonens|6|1, 5|q|2|5}}
{{Assumption|7|\neg p}}
{{ModusPonens|8|1, 7|q|3|7}}
{{ProofByCases|9|1|q|4|5|6|7|8}}
{{EndTableau|qed}}
{{LEM||3}}