avewright/proofwiki-math huggingface dataset:
Theorem: Indirect Proof

Let $P$ be a proposition whose truth value is to be proved (either true or false).
An '''indirect proof''' has one of the following two argument forms:
=== Reductio ad Absurdum ===
A '''reductio ad absurdum''' argument for the truth of $P$ is a valid argument which takes as a premise the negation of $P$, and from it deduces a contradiction:
{{:Reductio ad Absurdum/Proof Rule}}
=== Proof by Contradiction ===
A '''proof by contradiction''' argument for the falsehood of $P$ is a valid argument which takes $P$ as a premise, and from it directly deduces a contradiction:
{{:Proof by Contradiction/Proof Rule}}

Proof:
Let $x$ be an even integer.
Let $y = 2 n + 5$.
Assume $y = x + 5$ is not an odd integer.
Then:
:$y = x + 5 = 2 n$
where $n \in \Z$.
Then:
{{begin-eqn}}
{{eqn | l = x
      | r = 2 n - 5
      | c = 
}}
{{eqn | r = \paren {2 n - 6} + 1
      | c = 
}}
{{eqn | r = 2 \paren {n - 3} + 1
      | c = 
}}
{{eqn | r = 2 r + 1
      | c = where $r = n - 3 \in \Z$
}}
{{end-eqn}}
Hence $x$ is odd.
That is, it is false that $x$ is even.
It follows by the Rule of Transposition that if $x$ is even, then $y$ is odd.
{{qed}}
Theorem: Indirect Proof

Let $P$ be a proposition whose truth value is to be proved (either true or false).
An '''indirect proof''' has one of the following two argument forms:
=== Reductio ad Absurdum ===
A '''reductio ad absurdum''' argument for the truth of $P$ is a valid argument which takes as a premise the negation of $P$, and from it deduces a contradiction:
{{:Reductio ad Absurdum/Proof Rule}}
=== Proof by Contradiction ===
A '''proof by contradiction''' argument for the falsehood of $P$ is a valid argument which takes $P$ as a premise, and from it directly deduces a contradiction:
{{:Proof by Contradiction/Proof Rule}}

Proof:
For proofs, see:
* Reductio ad Absurdum/Sequent Form
* Proof by Contradiction/Sequent Form
Theorem: Continuous Mapping of Separation

Let $T$ and $T'$ be topological spaces.
Let $A \mid B$ be a separation of $T$.
Let $f: T \to T'$ be a mapping such that the restrictions $f \restriction_A$ and $f \restriction_B$ are both continuous.
Then $f$ is continuous on the whole of $T$.

Proof:
Follows directly from Pasting Lemma for Union of Open Sets.
{{Qed}}
Theorem: Fermat's Last Theorem

:$\forall a, b, c, n \in \Z_{>0}: n > 2$, the equation $a^n + b^n = c^n$ has no solutions.

Proof:
The proof of this theorem is beyond the current scope of {{ProofWiki}}, and indeed, is beyond the understanding of many high level mathematicians.
For the curious reader, the proof can be found [https://www.jstor.org/stable/2118559 here], in a paper published by {{AuthorRef|Andrew John Wiles|Andrew Wiles}}, entitled ''Modular elliptic curves and Fermat's Last Theorem'', in volume 141, issue 3, pages 443 through 551 of the ''Annals of Mathematics''.
It is worth noting that Wiles' proof was indirect in that he proved a special case of the Taniyama-Shimura Conjecture, which then along with the already proved Epsilon Conjecture implied that integral solutions of the theorem were impossible.
{{ProofWanted|add a broad overview of Wiles proof}}
Theorem: Subset of Real Numbers is Interval iff Connected

Let the real number line $\R$ be considered as a topological space.
Let $S$ be a subspace of $\R$.
Then $S$ is connected {{iff}} $S$ is an interval of $\R$.
That is, the only subspaces of $\R$ that are connected are intervals.

Proof:
From Rule of Transposition, we may replace the ''only if'' statement by its contrapositive.
Therefore, the following suffices:
Theorem: Continuous Image of Connected Space is Connected

Let $T_1$ and $T_2$ be topological spaces.
Let $S_1 \subseteq T_1$ be connected.
Let $f: T_1 \to T_2$ be a continuous mapping.
Then the image $f \sqbrk {S_1}$ is connected.

Proof:
Let $i: f \sqbrk {T_1} \to T_2$ be the inclusion mapping.
Let $g: T_1 \to f \sqbrk {T_1}$ be the surjective restriction of $f$.
Then $f = i \circ g$.
Hence, by Continuity of Composite with Inclusion: Inclusion on Mapping, it follows that $g$ is continuous.
;Proof by Contradiction
{{Recall|Connected Topological Space|connected topological space}}
{{:Definition:Connected Topological Space/Definition 1}}
{{AimForCont}} that $A, B \subseteq f \sqbrk {S_1}$ such that $A \mid B$.
That is, such that $A$ and $B$ separate $f \sqbrk {S_1}$.
From Preimage of Separation under Continuous Mapping is Separation:
:$g^{-1} \sqbrk A \mid g^{-1} \sqbrk B$ is a separation of $T_1$.
So by definition of connected space, $T_1$ is therefore not connected.
{{qed}}
Theorem: Continuous Image of Connected Space is Connected

Let $T_1$ and $T_2$ be topological spaces.
Let $S_1 \subseteq T_1$ be connected.
Let $f: T_1 \to T_2$ be a continuous mapping.
Then the image $f \sqbrk {S_1}$ is connected.

Proof:
Suppose that $S_2 = f \sqbrk {S_1}$ is not connected in $T_2$.
Then by definition there exist open sets $U_2$ and $V_2$ in $T_2$ such that:
:$S_2 \subseteq U_2 \cup V_2$
:$U_2 \cap V_2 \cap S_2 = \O$
:$U_2 \cap S_2 \ne \O$
:$V_2 \cap S_2 \ne \O$
We have {{hypothesis}} that $f: T_1 \to T_2$ is continuous.
Thus $U_1 = f^{-1} \sqbrk {U_2}$ and $V_1 = f^{-1} \sqbrk {V_2}$ are open in $T_1$.
We have that:
:$U_2 \cap S_2 \ne \O$
Therefore:
:$\exists x \in S_1: \map f x \in U_2$
Then:
:$x \in f^{-1} \sqbrk {U_2} = U_1$
and:
:$x \in S_1$
so:
:$U_1 \cap S_1 \ne \O$
Similarly:
:$V_1 \cap S_1 \ne \O$
Suppose there exists $x \in S_1$ such that $x \in U_1 \cap V_1 \cap S_1$.
Then:
:$\map f x \in U_2 \cap V_2 \cap S_2$
which is a contradiction.
It follows that:
:$U_1 \cap V_1 \cap S_1 = \O$
Thus by definition $S_1$ is not connected in $T_1$.
The result follows by the Rule of Transposition.
{{qed}}
Theorem: Union of Connected Sets with Non-Empty Intersections is Connected

Let $T = \struct {S, \tau}$ be a topological space.
Let $I$ be an indexing set.
Let $\AA = \family {A_\alpha}_{\alpha \mathop \in I}$ be an indexed family of subsets of $S$, all connected in $T$.
Let $\AA$ be such that no two of its elements are disjoint:
:$\forall B, C \in \AA: B \cap C \ne \O$
Then $\ds \bigcup \AA$ is itself connected.

Proof:
Let $A := \ds \bigcup \AA$.
Let $D = \set {0, 1}$, with the discrete topology.
Let $f: A \to D$ be a continuous mapping.
To show that $A$ is connected, we need to show that $f$ is not a surjection.
From Connected Set in Subspace, each $C \in \AA$ is connected in $A$.
From Restriction of Continuous Mapping is Continuous, the restriction $f \restriction_C$ is continuous for all $C \in \AA$.
From Continuous Image of Connected Space is Connected, $f \sqbrk C$ is connected in $D$ for all $C \in \AA$.
From Discrete Space is Totally Disconnected, $f \sqbrk C$ is a singleton for all $C \in \AA$:
:$f \sqbrk C = \set {\map \epsilon C}$
where $\map \epsilon C = 0$ or $1$.
By hypothesis:
:$\forall B, C \in \AA: B \cap C \ne \O$
Hence:
:$\forall B, C \in \AA: \map \epsilon B = \map \epsilon C$
{{Handwaving}}
Thus $f$ is constant on $A$ as required.
{{qed}}
Theorem: Union of Connected Sets with Non-Empty Intersections is Connected

Let $T = \struct {S, \tau}$ be a topological space.
Let $I$ be an indexing set.
Let $\AA = \family {A_\alpha}_{\alpha \mathop \in I}$ be an indexed family of subsets of $S$, all connected in $T$.
Let $\AA$ be such that no two of its elements are disjoint:
:$\forall B, C \in \AA: B \cap C \ne \O$
Then $\ds \bigcup \AA$ is itself connected.

Proof:
Let $C \in \AA$.
From Union of Connected Sets with Non-Empty Intersections is Connected applied to $B$ and $C$, the union $B \cup C$ is connected.
Thus the set $\tilde \AA = \set {B \cup C: C \in \AA}$ satisfies the conditions of the theorem.
Hence the result.
{{qed}}
Theorem: Union of Connected Sets with Non-Empty Intersections is Connected

Let $T = \struct {S, \tau}$ be a topological space.
Let $I$ be an indexing set.
Let $\AA = \family {A_\alpha}_{\alpha \mathop \in I}$ be an indexed family of subsets of $S$, all connected in $T$.
Let $\AA$ be such that no two of its elements are disjoint:
:$\forall B, C \in \AA: B \cap C \ne \O$
Then $\ds \bigcup \AA$ is itself connected.

Proof:
Let $\ds H = B \cup \bigcup \AA$
{{AimForCont}} that $H$ is not connected.
That is, that $H$ is disconnected.
We have that:
:$\forall C \in \AA: B \cap C \ne \O$
Thus:
:$\exists x \in H: x \in B \cap C$
From the definition of disconnected, there exist separated sets $U, V$ whose union is $H$.
So:
:$\forall s \in S: s \in U \lor s \in V$
{{AimForCont}} $s \in V$.
Then $H, V$ serve as separated sets whose union is a cover for $\family {A_\alpha}_{\alpha \mathop \in I}$.
{{explain|How does $s \in V$ imply the above statement?}}
Note that the disconnection is valid as:
:$\exists x \in U \cap \family {A_\alpha}_{\alpha \mathop \in I}$
{{explain|What does the above sentence mean?}}
As $s \in V$, it follows that the $\family {A_\alpha}_{\alpha \mathop \in I}$ are disconnected.
{{explain|How}}
From this contradiction it follows that $s \notin V$.
Hence $s \in U$.
This holds for arbitrary $s \in H$.
Hence:
:$H \subseteq U$
But as $U$ and $V$ are separated, $U \cap H$ is empty, as required per the definition of a disconnected set.
This contradicts our deduction that $H \subseteq U$.
Hence the sets $U, V$ are not separated sets in $H$.
Thus $H$ is connected in $T$.
{{qed}}
Theorem: Product Space of 2 Factors is Connected iff Factors are Connected

Let $T_1$ and $T_2$ be topological spaces.
Then the product space $T_1 \times T_2$ is connected {{iff}} $T_1$ and $T_2$ are connected.

Proof:
==== Necessary Condition ====
Let $T_1 \times T_2$ be connected.
By Projection from Product Topology is Continuous, $T_1$ and $T_2$ are continuous images under the projections $\pr_1$ and $\pr_2$.
Hence by Continuous Image of Connected Space is Connected, $T_1$ and $T_2$ are connected.
{{qed|lemma}}
==== Sufficient Condition ====
Suppose that $T_1$ and $T_2$ are connected.
Define:
:$C_y = T_1 \times \set y$ for each $y \in T_2$
:$B = \set {x_0} \times T_2$ for some fixed $x_0 \in T_1$.
Each $C_y$ is homeomorphic to $T_1$ by Topological Product with Singleton.
By {{Corollary|Continuous Image of Connected Space is Connected|1}}, each $C_y$ is therefore connected.
By the same argument, $B$ is also connected.
Also:
:$C_y \cap B = \set {\tuple {x_0, y} }$ and hence is non-empty
:$\ds T_1 \times T_2 = B \cup \bigcup_{y \mathop \in T_2} C_y$.
So by {{Corollary|Union of Connected Sets with Non-Empty Intersections is Connected}}, it follows that $T_1 \times T_2$ is connected.
Theorem: Set between Connected Set and Closure is Connected

Let $T$ be a topological space.
Let $H$ be a connected set of $T$.
Let $H \subseteq K \subseteq H^-$, where $H^-$ denotes the closure of $H$. 
Then $K$ is connected.

Proof:
Let $D$ be the discrete space $\set {0, 1}$.
Let $f: K \to D$ be an arbitrary continuous mapping.
From Continuity of Composite with Inclusion, the restriction $f \restriction_H$ is continuous.
We have that:
:$H$ is connected
:$f \restriction_H$ is continuous
Thus by definition of connected set:
:$f \sqbrk H = \set 0$ or $f \sqbrk H = \set 1$ 
{{WLOG}}, let $\map f H = \set 0$.
{{AimForCont}} $\exists k \in K: \map f k = 1$.
By definition of discrete space, $\set 1$ is open in $D$.
Hence by definition of continuous mapping:
:$f^{-1} \sqbrk {\set 1}$ is open in $K$.
Let $K$ be given the subspace topology.
Then for some $U$ open in $T$:
:$f^{-1} \sqbrk {\set 1} = K \cap U$
We have that:
:$k \in f^{-1} \sqbrk {\set 1} \subseteq U$
and:
:$k \in H^-$
By definition of topology:
:$\exists x \in H \cap U$
As $x \in H$, we have that:
:$\map f x = 0$
But because $x \in H \cap U \subseteq K \cap U = f^{-1} \sqbrk {\set 1}$:
:$\map f x = 1$
This contradicts the definition of mapping.
Thus by Proof by Contradiction, $f: K \to D$ can not be a surjection.
Thus $K$ is connected.
{{qed}}
Theorem: Set between Connected Set and Closure is Connected

Let $T$ be a topological space.
Let $H$ be a connected set of $T$.
Let $H \subseteq K \subseteq H^-$, where $H^-$ denotes the closure of $H$. 
Then $K$ is connected.

Proof:
Let $T_K = \struct {K, \tau_K}$ be the topological subspace of $T$ whose underlying set is $K$.
Let $\map {\cl_K} H$ denote the closure of $H$ in $K$.
From Closure of Subset in Subspace:
:$\map {\cl_K} H = K \cap H^-$
By hypothesis:
:$K \subseteq H^-$
and so by Intersection with Subset is Subset:
:$\map {\cl_K} H = K$
Let $D$ be the discrete space $\set {0, 1}$.
Let $f: K \to D$ be any continuous mapping.
From Continuity of Composite with Inclusion, the restriction $f \restriction_H$ is continuous.
SWe have that:
:$H$ is connected
:$f \restriction_H$ is continuous
Thus by definition of connected set:
:$f \sqbrk H = \set 0$ or $f \sqbrk H = \set 1$ 
{{WLOG}}, let $f \sqbrk H = \set 0$.
From Continuity Defined by Closure:
:$f \sqbrk {\map {\cl_K} H} \subseteq \map {\cl_K} {f \sqbrk H} = \set 0^-$
where $\set 0^-$ denotes the closure of $\set 0$ in $D$.
As $D$ is the discrete space, it follows from Set in Discrete Topology is Clopen that $\set 0$ is closed in $D$.
Thus by Set is Closed iff Equals Topological Closure:
:$\set 0^- = \set 0$
That is, $f \sqbrk K = \set 0$.
Thus $K$ is connected by definition.
{{qed}}
Theorem: Path-Connected Space is Connected

Let $T$ be a topological space which is path-connected.
Then $T$ is connected.

Proof:
{{AimForCont}} $X \mid Y$ is a separation of $T$.
As $X$ and $Y$ are non-empty, we can find $x \in X$ and $y \in Y$.
As $T$ is path-connected, there exists a path $f : \closedint 0 1 \to T$ with initial point $x$ and final point $y$.
Subset of Real Numbers is Interval iff Connected shows that $\closedint 0 1$ is connected.
Continuous Image of Connected Space is Connected shows that $\Img f$ is connected.
Connected Subspace lies in One Component of Separation shows that either $\Img f \cap X = \O$, or $\Img f \cap Y = \O$.
As we have $x, y \in \Img f$, this is a contradiction.
It follows that there can be no separation of $T$, so $T$ is connected.
{{qed}}
Theorem: Path-Connected Space is Connected

Let $T$ be a topological space which is path-connected.
Then $T$ is connected.

Proof:
Let $D$ be the discrete space $\set {0, 1}$.
Let $T$ be path-connected.
Let $f: T \to D$ be a continuous surjection.
Let $x, y \in T: \map f x = 0, \map f y = 1$.
Let $I \subset \R$ be the closed real interval $\closedint 0 1$.
Let $g: I \to T$ be a path from $x$ to $y$.
Then by Composite of Continuous Mappings is Continuous it follows that $f \circ g: I \to D$ is a continuous surjection.
This contradicts the connectedness of $I$ as proved in Subset of Real Numbers is Interval iff Connected.
{{explain|Why does that follow? Explain what the chain of steps is}}
Hence the result.
{{qed}}
Theorem: Hausdorff Paradox

There exists a disjoint decomposition of the sphere $\mathbb S^2$ into four sets $A, B, C, Q$ such that $A, B, C, B \cup C$ are all congruent and $Q$ is countable.

Proof:
Let $R \subset \map {\mathbb {SO} } 3$ be the group generated by the $\pi$ and $\dfrac {2 \pi} 3$ rotations around different axes.
The elements:
:$\psi = \begin {pmatrix} -\tfrac 1 2 & \tfrac {\sqrt 3} 2 & 0 \\ -\tfrac {\sqrt 3} 2 & -\tfrac 1 2 & 0 \\ 0 & 0 & 1 \\ \end {pmatrix}$
:$\phi = \begin {pmatrix} -\map \cos \vartheta & 0 & \map \sin \vartheta \\ 0 & -1 & 0 \\ \map \sin \vartheta & 0 & \map \cos \vartheta \\ \end {pmatrix}$
form a basis for $R$ for some $\vartheta$.
We have:
:$\psi^3 = \phi^2 = \mathbf I_3$
where $\mathbf I_3$ is the identity mapping in $\mathbb R^3$.
Therefore $\forall r \in R: r \ne \mathbf I_3, \psi, \phi, \psi^2$ there exists some $n \in \N$ and some set of numbers $m_k \in \set {1, 2}, 1 \le k \le n$ such that $r$ can written as one of the following:
:$\text{(a)}: \quad \ds r = \prod_{k \mathop = 1}^n \phi \psi^{m_k}$
:$\text{(b)}: \quad \ds r = \map {\psi^{m_1} } {\prod_{k \mathop = 2}^n \phi \psi^{m_k} }\phi$
:$\text{(c)}: \quad \ds r = \paren {\prod_{k \mathop = 1}^n \phi \psi^{m_k} } \phi$
:$\text{(d)}: \quad \ds r = \map {\psi^{m_1} } {\prod_{k \mathop = 2}^n \phi \psi^{m_k} }$
Now we fix $\vartheta$ such that $\mathbf I_3$ cannot be written in any of the ways $\text{(a)}$, $\text{(b)}$, $\text{(c)}$, $\text{(d)}$. 
The action of $R$ on $\mathbb S^2$ will leave two points unchanged for each element of $R$ (the intersection of the axis of rotation and the sphere, to be exact). 
Since $R$ is finitely generated, it is a countable group.
Therefore the set of points of $\mathbb S^2$ which are unchanged by at least one element of $R$ is also countable. 
We call this set $Q \subset \mathbb S^2$, so that $R$ acts freely on $\mathbb S^2 \setminus Q$.
By Set of Orbits forms Partition, this partitions $\mathbb S^2 \setminus Q$ into orbits.
By the {{Axiom-link|Choice}}, there is a set $X$ containing one element of each orbit. 
For any $r \in R$, let $X_r$ be the right action of $r$ on $X$.
We have:
:$\ds \mathbb S^2 \setminus Q = \bigcup_{r \mathop \in R} X_r$
Define the sets $A, B, C$ to be the smallest sets satisfying 
:$X \subseteq A$
:If $X_r \subset A, B, C$, then $X_{r\phi} \subset B, A, A$, respectively.
:If $X_r \subset A, B, C$, then $X_{r\psi} \subset B, C, A$, respectively.
:If $X_r \subset A, B, C$, then $X_{r\psi^2} \subset C, A, B$, respectively.
These sets are defined due to the uniqueness of the properties $\text{(a)}$ to $\text{(d)}$
Also, $A, B, C, B \cup C$ are congruent since they are rotations of each other, namely:
:$A_\psi = B, B_{\psi^2} = C, A_\phi = B \cup C$
Hence we have constructed the sets $A, B, C, Q$ of the theorem.
{{qed}}
Theorem: Hausdorff Paradox

There exists a disjoint decomposition of the sphere $\mathbb S^2$ into four sets $A, B, C, Q$ such that $A, B, C, B \cup C$ are all congruent and $Q$ is countable.

Proof:
=== Lemma $1$ ===
{{:Hausdorff Paradox/Lemma 1}}{{qed|lemma}}
=== Lemma $2$ ===
{{:Hausdorff Paradox/Lemma 2}}{{qed|lemma}}
Let $Q$ be the set of all fixed points of $\Bbb S^2$ of all rotations $\alpha \in G$.
Each such $\alpha$ has $2$ fixed points.
Hence $Q$ is countable.
The set $\Bbb S^2 \setminus Q$ is a disjoint union of all orbits $P_x$ of $G$:
:$P_x = \set {x \alpha: \alpha \in G}$
By the {{Axiom-link|Choice}}, there exists a set $M$ which contains exactly $1$ element in each $P_x$ where $x \in \Bbb S^2 \setminus Q$.
Let:
{{begin-eqn}}
{{eqn | l = A
      | r = M \circ \mathscr A
}}
{{eqn | l = B
      | r = M \circ \mathscr B
}}
{{eqn | l = C
      | r = M \circ \mathscr C
}}
{{end-eqn}}
It then follows from {{Lemma|Hausdorff Paradox|2}} that:
:$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$
and moreover:
:$S = A \cup B \cup C \cup Q$
{{qed}}
Theorem: Closed Topologist's Sine Curve is not Path-Connected

Let $T$ be the closed topologist's sine curve.
Then $T$ is '''not''' path-connected.

Proof:
{{Recall|Closed Topologist's Sine Curve}}
{{:Definition:Closed Topologist's Sine Curve}}
Let $I = \closedint 0 1 \subseteq \R$ be the closed real interval.
Let $A = \tuple {\dfrac 1 \pi, 0} \in \R^2$.
This proof is based on the fact that a continuous path $f: I \to G \cup J$ beginning at $A$ will never actually arrive at $0 = \tuple {0, 0} \in \R^2$ because $I$ is compact.
Suppose $f: I \to G \cup J$ is continuous and that $\map f 0 = A$.
Let $f_1: I \to \R$ and $f_2: I \to \R$ denote $\pr_1 \circ i \circ f$ and $\pr_2 \circ i \circ f$, where $i$ is the inclusion mapping and $\pr_1, \pr_2$ the first and second projections on the $x$ and $y$ axes.
Thus $f_2$ describes the vertical movement of the graph, and $f_1$ the horizontal movement.
Now $f_2$ is continuous and $I$ compact.
So by the Heine-Cantor Theorem, $f_2$ is uniformly continuous on $I$.
Let $\delta \in \R_{>0}$ be such that $\size {\map {f_2} t - \map {f_2} {t'} } < 2$ for any $t, t' \in I$ such that $\size {t - t'} < \delta$.
Let $0 < t_0 < t_1 < \ldots < t_n = 1$ be such that $t_i - t_{i - 1} < \delta$ for all $i = 1, 2, \ldots, n$.
Now: as $t$ goes from $t_0$ to $t_1$, $\map f t$ (which starts at $A$), can not reach a point $C$ where $y = 1$ without passing through a point $B$ where $y = -1$ on the way.
But then $\map f t = B$ and $\map f {t'} = C$ for some $t, t'$ where $\size {t - t'} < \delta$.
And since $B$ and $C$ are $2$ apart, $\size {\map {f_2} t - \map {f_2} {t'} } = 2$ which contradicts the choice of $\delta$.
Similarly, when going from $t_1$ to $t_2$, $t$ can similarly not get past more than one hump.
So, as $t$ goes from $0$ to $1$, $\map f t$ can not traverse more than $n$ humps.
We formalize this discussion by induction.
We will show that:
:$\forall i \in \set {0, 1, \ldots, n}: \map {f_1} {t_i} > \dfrac 2 {\paren {2 i + 3} \pi}$
Since $\map f {t_0} = \map f 0 = \tuple {\dfrac 1 \pi, 0}$:
:$\map {f_1} {t_0} = \dfrac 1 \pi > \dfrac 2 {3 \pi}$
Suppose:
:$\exists i \in \set {0, 1, \ldots, n}: \map {f_1} {t_i} > \dfrac 2 {\paren {2 i + 3} \pi}$
{{AimForCont}} also that $\map {f_1} {t_{i + 1} } \ge \dfrac 2 {\paren {2 i + 5} \pi}$.
Then since $f_1$ is continuous, by the I.V.P. there exists $t, t' \in \closedint {t_1} {t_{i + 1} }$ such that:
:$\map {f_1} {t_i} = \dfrac 2 {\paren {2 i + 3} \pi}, \map {f_1} {t_{i + 1} } = \dfrac 2 {\paren {2 i + 5} \pi}$
But the only point in $G \cup J$ whose first coordinate is $\dfrac 2 {\paren {2 i + 3} \pi}$ is $\tuple {\dfrac 2 {\paren {2 i + 3} \pi}, \map \sin {\dfrac {\paren {2 i + 3} \pi} 2} }$.
So:
:$\map {f_2} t = \map \sin {\dfrac {\paren {2 i + 3} \pi} 2}$
Similarly:
:$\map {f_2} {t'} = \map \sin {\dfrac {\paren {2 i + 5} \pi} 2}$
Hence $\size {\map {f_2} t - \map {f_2} {t'} } = 2$ while $\size {t - t'} < \delta$.
This contradicts the choice of $\delta$.
This proves the induction.
The result follows from the fact that:
:$\map {f_1} 1 > \dfrac 2 {\paren {2 n + 3} \pi} > 0$, so $\map {f_1} 1 \ne 0$
{{qed}}
Theorem: Sum of Two Sides of Triangle Greater than Third Side

Given a triangle $ABC$, the sum of the lengths of any two sides of the triangle is greater than the length of the third side.
{{:Euclid:Proposition/I/20}}

Proof:
:350 px
Let $ABC$ be a triangle.
By {{EuclidPostulateLink|Second}}, we can produce $BA$ past $A$ in a straight line.
By Construction of Equal Straight Lines from Unequal, there exists a point $D$ such that $DA = CA$.
Therefore, from Isosceles Triangle has Two Equal Angles:
:$\angle ADC = \angle ACD$
Thus by {{EuclidCommonNotionLink|5}}:
:$\angle BCD > \angle BDC$
Thus $\triangle DCB$ is a triangle having $\angle BCD$ greater than $\angle BDC$
Hence from Greater Angle of Triangle Subtended by Greater Side:
:$BD > BC$
But:
:$BD = BA + AD$
and:
:$AD = AC$
Thus:
:$BA + AC > BC$
A similar argument shows that $AC + BC > BA$ and $BA + BC > AC$.
{{qed}}
{{Euclid Note|20|I|This theorem is the original Triangle Inequality, from which algebraic implementations followed.}}
Theorem: Lines Through Endpoints of One Side of Triangle to Point Inside Triangle is Less than Sum of Other Sides

Given a triangle and a point inside it, the sum of the lengths of the line segments from the endpoints of one side of the triangle to the point is less than the sum of the other two sides of the triangle.
{{:Euclid:Proposition/I/21}}

Proof:
:250px
Given a triangle $ABC$ and a point $D$ inside it.
We can construct lines connecting $B$ and $C$ to $D$, and then extend the line $BD$ to a point $E$ on $AC$.
In $\triangle ABE$, $AB + AE>BE$, by Sum of Two Sides of Triangle Greater than Third Side.
Then, $AB + AC = AB + AE + EC > BE + EC$ by Euclid's second common notion.
Similarly, $CE + ED > CD$, so $CE + EB = CE + ED + DB > CD + DB$.
Thus, $AB + AC > BE + EC > CD + DB$.
{{qed}}
{{Euclid Note|21|I}}