avewright/proofwiki-math huggingface dataset:
Theorem: Tangent of Sum

:$\map \tan {a + b} = \dfrac {\tan a + \tan b} {1 - \tan a \tan b}$

Proof:
First we note:
{{begin-eqn}}
{{eqn | l = \cos \sum_j \theta_j + i \sin \sum_j \theta_j
      | r = \prod_j \paren {\cos \theta_j + i \sin \theta_j}
      | c = Product of Complex Numbers in Polar Form
}}
{{eqn | r = \prod_j \cos \theta_j \prod_j \paren {1 + i \tan \theta_j}
      | c = 
}}
{{eqn | r = \prod_j \cos \theta_j \paren {1 + i \tan \theta_1} \times \paren {1 + i \tan \theta_2} \times \cdots \times \paren {1 + i \tan \theta_n}
      | c = expanding the product
}}
{{eqn | r = \prod_j \cos \theta_j \leftparen {1 + i \paren {\tan \theta_1 + \tan \theta_2 + \cdots + \tan \theta_n} }
      | c = multiplying out
}}
{{eqn | o = 
      | ro= +
      | r = i^2 \paren {\tan \theta_1 \tan \theta_2 + \tan \theta_1 \tan \theta_3 + \cdots + \tan \theta_{n - 1} \tan \theta_n}
}}
{{eqn | o = 
      | ro= +
      | r = \cdots
}}
{{eqn | o = 
      | ro= +
      | r = \rightparen {i^n \tan \theta_1 \tan \theta_2 \ldots \tan \theta_n}
}}
{{eqn | r = \prod_j \cos \theta_j \sum_{k \mathop = 0}^n i^k s_k
      | c = $s_0 = 1$
}}
{{eqn | r = \prod_j \cos \theta_j \paren {1 - s_2 + s_4 - s_6 + \cdots} + \prod_j \cos \theta_j \paren {i s_1 - i s_3 + i s_5 - \cdots}
      | c = 
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = \cos \sum_j \theta_j
      | r = \prod_j \cos \theta_j \paren {1 - s_2 + s_4 - s_6 + \cdots}
      | c = equating real parts
}}
{{eqn | n = 2
      | ll= \leadsto
      | l = \sin \sum_j \theta_j
      | r = \prod_j \cos \theta_j \paren {s_1 - s_3 + s_5 - \cdots }
      | c = equating imaginary parts
}}
{{eqn | ll= \leadsto
      | l = \tan \sum_j \theta_j
      | r = \frac {\paren {s_1 - s_3 + s_5 - \cdots} } {1 - s_2 + s_4 - \cdots}
      | c = $\dfrac {\paren 2} {\paren 1}$
}}
{{end-eqn}}
{{qed}}
Theorem: Tangent of Sum

:$\map \tan {a + b} = \dfrac {\tan a + \tan b} {1 - \tan a \tan b}$

Proof:
{{begin-eqn}}
{{eqn | l = \map \tan {A + B + C}
      | r = \dfrac {\tan A + \map \tan {B + C} } {1 - \tan A \tan {B + C} }
      | c = Tangent of Sum
}}
{{eqn | r = \dfrac {\tan A + \frac {\tan B + \tan C} {1 - \tan B \tan C} } {1 - \tan A \frac {\tan B + \tan C} {1 - \tan B \tan C} }
      | c = Tangent of Sum
}}
{{eqn | r = \dfrac {\tan A \paren {1 - \tan B \tan C} + \tan B + \tan C} {\paren {1 - \tan B \tan C} - \tan A \paren {\tan B + \tan C} }
      | c = multiplying top and bottom by $1 - \tan B \tan C$
}}
{{eqn | r = \dfrac {\tan A + \tan B + \tan C - \tan A \tan B \tan C} {1 - \tan B \tan C - \tan C \tan A - \tan A \tan B}
      | c = simplification
}}
{{end-eqn}}
{{qed}}
Theorem: Tangent of Sum

:$\map \tan {a + b} = \dfrac {\tan a + \tan b} {1 - \tan a \tan b}$

Proof:
This is a special case of Tangent of Sum of Series of Angles, for $n = 3$.
{{qed}}
Theorem: Tangent of Sum

:$\map \tan {a + b} = \dfrac {\tan a + \tan b} {1 - \tan a \tan b}$

Proof:
{{begin-eqn}}
{{eqn | l = \map \tan {a + b}
      | r = \frac {\map \sin {a + b} } {\map \cos {a + b} }
      | c = Tangent is Sine divided by Cosine
}}
{{eqn | r = \frac {\sin a \cos b + \cos a \sin b} {\cos a \cos b - \sin a \sin b}
      | c = Sine of Sum and Cosine of Sum
}}
{{eqn | r = \frac {\frac {\sin a} {\cos a} + \frac {\sin b} {\cos b} } {1 - \frac {\sin a \sin b} {\cos a \cos b} }
      | c = dividing top and bottom by $\cos a \cos b$
}}
{{eqn | r = \frac {\tan a + \tan b} {1 - \tan a \tan b}
      | c = Tangent is Sine divided by Cosine
}}
{{end-eqn}}
{{qed}}
Theorem: Natural Logarithm Function is Differentiable

The (real) natural logarithm function is differentiable.

Proof:
This proof assumes the definition of $\ln$ as:
:$\ln x = \ds \int_1^x \frac 1 t \rd t$
As $\ln$ is defined as a definite integral, the result follows from the {{Corollary|Fundamental Theorem of Calculus/First Part|disp = Fundamental Theorem of Calculus}}.
{{qed}}
Theorem: Natural Logarithm Function is Differentiable

The (real) natural logarithm function is differentiable.

Proof:
This proof assumes the definition of $\ln$ as the inverse of the exponential function.
As the Exponential Function is Differentiable, the result follows from the differentiability of inverse functions.
{{qed}}
Theorem: Countable Basis of Real Number Line

Let $\struct {\R, \tau_d}$ be the real number line with the usual (Euclidean) topology.
Let $\BB$ be the set of subsets of $\R$ defined as:
:$\BB = \set {\openint a b: a, b \in \Q,\ a < b}$
That is, $\BB$ is the set of open intervals of $\R$ whose endpoints are rational numbers.
Then $\BB$ forms a countable basis of $\struct {\R, \tau_d}$

Proof:
Let $U \in \tau_d$.
Let $x \in U$.
Let:
:$\BB' = \set {\openint c d: c, d \in \R,\ c < d}$
By Basis for Euclidean Topology on Real Number Line, $\BB'$ is an analytic basis for the Euclidean topology on $\R$.
Then let $\openint c d \in \BB'$ such that $x \in \openint c d \subseteq U$.
That is, $c < x < d$.
By Between two Real Numbers exists Rational Number, let $a \in \Q$ such that $c < a < x$.
By Between two Real Numbers exists Rational Number, let $b \in \Q$ such that $x < b < d$.
Then $\openint a b \in \BB$ and $x \in \openint a b$.
Let $y \in \openint a b$.
Then $c < a < y < b < d$ implies $y \in \openint c d$.
Thus, $\openint a b \subseteq \openint c d \subseteq U$.
It follows that $\BB$ is a basis of $\struct {\R, \tau_d}$.
{{explain|follows how? What definition are you using?}}
It remains to be confirmed that $\BB$ is countable.
By Rational Numbers are Countably Infinite, $\Q$ is countable.
By Cartesian Product of Countable Sets is Countable, $\Q \times \Q$ is countable.
Define the mapping $f: \Q \times \Q \to \BB$ by:
:<nowiki>$\map f {q, r} := \begin {cases}
\openint q r & : q < r \\
\openint 0 1 & : q \ge r
\end {cases}$</nowiki>
For each $\openint a b \in \BB$, we have $\map f {a, b} = \openint a b$.
Then $f$ is a surjection.
By Image of Countable Set under Mapping is Countable, $\BB$ is countable.
{{qed}}
Theorem: Second-Countable Space is Separable

Let $T = \struct {S, \tau}$ be a second-countable topological space.
Then $T$ is also a separable space.

Proof:
{{Recall|Separable Space|separable space}}
{{:Definition:Separable Space}}
Let $T = \struct {S, \tau}$ be a second-countable space.
{{Recall|Second-Countable Space|second-countable space}}
{{:Definition:Second-Countable Space}}
By definition, there exists a countable basis $\BB$ for $\tau$.
Using the {{Axiom-link|Countable Choice}}, we can obtain a choice function $\phi$ for $\BB \setminus \set \O$.
Define:
:$H = \set {\map \phi B: B \in \BB \setminus \set \O}$
Thus $H \subseteq X$ has been defined by selecting one point from each element of $\BB$.
By Image of Countable Set under Mapping is Countable, it follows that $H$ is countable.
It suffices to show that $H$ is everywhere dense in $T$.
Let $x \in U \in \tau$.
By Equivalence of Definitions of Analytic Basis, there exists a $B \in \BB$ such that $x \in B \subseteq U$.
Then $\map \phi B \in U$, and so $H \cap U$ is non-empty.
Hence, $x$ is an adherent point of $H$.
By Equivalence of Definitions of Adherent Point of Set, it follows that $x \in H^-$, where $H^-$ denotes the closure of $H$.
Therefore, $H^- = S$, and so $H$ is everywhere dense in $T$ by definition.
{{qed}}
{{ACC}}
Theorem: Real Number Line is Second-Countable

Let $\struct {\R, \tau_d}$ be the real number line with the usual (Euclidean) topology.
Then $\struct {\R, \tau_d}$ is a second-countable space.

Proof:
From Countable Basis of Real Number Line we have that $\struct {\R, \tau_d}$ has a countable basis.
The result follows directly from the definition of a second-countable space.
{{qed}}
Theorem: Real Number Line is not Countably Compact

Let $\struct {\R, \tau_d}$ be the real number line with the usual (Euclidean) topology.
Then $\struct {\R, \tau_d}$ is not a countably compact space.

Proof:
Let $\CC$ be the set of subsets of $\R$ defined as:
:$\CC = \set {\openint n {n + 2}: n \in \Z}$
Then $\CC$ is an open cover of $\R$ which is countable.
However, there is no finite subcover for $\R$ of $\CC$.
Hence the result, by definition of countably compact.
{{qed}}
Theorem: Real Number Line is Locally Compact Hausdorff Space

Let $\struct {\R, \tau_d}$ be the real number line with the usual (Euclidean) topology.
Then $\struct {\R, \tau_d}$ is a locally compact Hausdorff space.

Proof:
We have that a Real Number Line satisfies all Separation Axioms.
Specifically, $\struct {\R, \tau_d}$ is a Hausdorff space.
Consider $\CC$ the set of subsets of $\R$ defined as:
:$\CC = \set {\closedint n {n + 1}: n \in \Z}$
where $\closedint n {n + 1}$ is the closed real interval between successive integers.
By the Heine-Borel Theorem, each element of $\CC$ is compact.
Every element of $\R$ is contained in at least one of the elements of $\CC$.
Hence, by definition, $\R$ is locally compact.
{{qed}}
Theorem: Real Number Line is Sigma-Compact

Let $\struct {\R, \tau_d}$ be the real number line with the usual (Euclidean) topology.
Then $\struct {\R, \tau_d}$ is a $\sigma$-compact space.

Proof:
We have that a Real Number Line satisfies all Separation Axioms.
Specifically, $\struct {\R, \tau_d}$ is a Hausdorff space.
Consider $\CC$ the set of subsets of $\R$ defined as:
:$\CC = \set {\closedint n {n + 1}: n \in \Z}$
where $\closedint n {n + 1}$ is the closed real interval between successive integers.
By the Heine-Borel Theorem, each element of $\CC$ is compact.
$\CC$ itself is countable, as there is a (trivial) one-to-one-correspondence between $\CC$ and $\Z$.
Every element of $\R$ is also an element of at least one of the elements of $\CC$.
Thus $\R$ is the union of $\CC$.
Hence, by definition, $\R$ is a $\sigma$-compact space.
{{qed}}
Theorem: Closed Subset of Real Number Line is G-Delta

Let $\struct {\R, \tau_d}$ be the real number line with the usual (Euclidean) topology.
Let $H \subseteq \R$ be a closed subset of $\R$.
Then $H$ is a $G_\delta$ set.

Proof:
We have:
:Real Number Line is Metric Space
:Closed Set in Metric Space is $G_\delta$
Hence the result.
{{qed}}
Theorem: Real Number Line is Paracompact

Let $\struct {\R, \tau_d}$ be the real number line with the usual (Euclidean) topology.
Then $\struct {\R, \tau_d}$ is paracompact.

Proof:
Let $\CC$ be an open cover for $\R$.
Then $\CC$ covers each of the closed real intervals $\closedint n {n + 1}$ for all $n \in \Z$.
By the Heine-Borel Theorem, each of $\closedint n {n + 1}$ is compact.
So, for each of these intervals $\closedint n {n + 1}$, it follows that $\CC$ can be reduced to a sequence $\sequence {G_i^{\paren n} }$ of finite subcovers.
Then each of $G_i^{\paren n} \cap \openint {n - 1} {n + 2}$ forms a refinement of $\CC$ which is locally finite.
Hence, by definition, $\R$ is paracompact.
{{qed}}
Theorem: Real Number Line with Off-Center Distance Function is Quasimetric Space

Let $\struct {\R, \tau_d}$ be the real number line with the usual (Euclidean) topology.
Then $\tau_d$ can be given by a quasimetric defined as:
:<nowiki>$\map d {x, y} = \begin {cases}
y - x & : y \ge x \\
2 \paren {x - y} & : y < x \end {cases}$</nowiki>
Thus $\struct {\R, \tau_d}$ is a quasimetric space.

Proof:
To show that $\map d {x, y}$ is a quasimetric, we need to show that $d: \R \times \R \to \R$ satisfies the following conditions for all $x, y, z \in \R$:
{{begin-itemize}}
{{item|(\text M 1):|$\map d {x, x} {{=}} 0$}}
{{item|(\text M 2):|$\map d {x, y} + \map d {y, z} \ge \map d {x, z}$}}
{{item|(\text M 4):|$x \ne y \implies \map d {x, y} > 0$}}
{{end-itemize}}
Theorem: NAND with Equal Arguments

:$p \uparrow p \dashv \vdash \neg p$
That is, the NAND of a proposition with itself corresponds to the negation operation.

Proof:
{{BeginTableau|p \uparrow p \vdash \neg p}}
{{Premise|1|p \uparrow p}}
{{SequentIntro|2|1|\neg \paren {p \land p}|1|Definition of Logical NAND}}
{{Idempotence|3|1|\neg p|2|Conjunction}}
{{EndTableau|lemma}}
{{BeginTableau|\neg p \vdash p \uparrow p}}
{{Premise|1|\neg p}}
{{Idempotence|2|1|\neg \paren {p \land p}|1|Conjunction}}
{{SequentIntro|3|1|p \uparrow p|2|Definition of Logical NAND}}
{{EndTableau|qed}}
Theorem: NAND with Equal Arguments

:$p \uparrow p \dashv \vdash \neg p$
That is, the NAND of a proposition with itself corresponds to the negation operation.

Proof:
We apply the Method of Truth Tables:
:$\begin{array}{|ccc||cc|} \hline
p & \uparrow & p & \neg & p \\
\hline
\F & \T & \F & \T & \F \\
\T & \F & \T & \F & \T \\
\hline
\end{array}$
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
{{qed}}
Theorem: NAND is Commutative

:$p \uparrow q \dashv \vdash q \uparrow p$

Proof:
{{BeginTableau|p \uparrow q \vdash q \uparrow p}}
{{Premise|1|p \uparrow q}}
{{SequentIntro|2|1|\neg \paren {p \land q}|1|{{Defof|Logical NAND}} }}
{{Commutation|3|1|\neg \paren {q \land p}|2|Conjunction}}
{{SequentIntro|4|1|q \uparrow p|3|{{Defof|Logical NAND}} }}
{{EndTableau|lemma}}
{{BeginTableau|q \uparrow p \vdash p \uparrow q}}
{{Premise|1|q \uparrow p}}
{{SequentIntro|2|1|\neg \paren {q \land p}|1|{{Defof|Logical NAND}} }}
{{Commutation|3|1|\neg \paren {p \land q}|2|Conjunction}}
{{SequentIntro|4|1|p \uparrow q|3|{{Defof|Logical NAND}} }}
{{EndTableau|qed}}
Theorem: NAND is Commutative

:$p \uparrow q \dashv \vdash q \uparrow p$

Proof:
We apply the Method of Truth Tables:
:$\begin{array}{|ccc||ccc|} \hline
p & \uparrow & q & q & \uparrow & p \\
\hline
\F & \T & \F & \F & \T & \F \\
\F & \T & \T & \T & \T & \F \\
\T & \T & \F & \F & \T & \T \\
\T & \F & \T & \T & \F & \T \\
\hline
\end{array}$
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
{{qed}}
Theorem: NAND is not Associative

:$p \uparrow \paren {q \uparrow r} \not \vdash \paren {p \uparrow q} \uparrow r$

Proof:
{{BeginTableau|\neg \paren {\paren {p \uparrow q} \uparrow r \implies p \uparrow \paren {q \uparrow r} } }}
{{Assumption|1|\paren {p \uparrow q} \uparrow r \implies p \uparrow \paren {q \uparrow r} }}
{{Assumption|2|p \land \neg r}}
{{Simplification|3|2|p|2|1}}
{{Simplification|4|2|\neg r|2|2}}
{{Addition|5|2|\paren {\neg q} \lor \paren {\neg r}|4|2}}
{{DeMorgan|6|2|\neg \paren {q \land r}|5|Disjunction of Negations}}
{{SequentIntro|7|2|q \uparrow r|6
  |{{Defof|Logical NAND}} }}
{{Conjunction|8|2|p \land \paren {q \uparrow r}|3|7}}
{{DoubleNegIntro|9|2|\neg \neg \paren {p \land \paren {q \uparrow r} }|8}}
{{SequentIntro|10|2|\neg \paren {p \uparrow \paren {q \uparrow r} }|9
  |{{Defof|Logical NAND}} }}
{{Addition|11|2|\paren {\neg \paren {p \uparrow q} } \lor \paren {\neg r}|4|2}}
{{DeMorgan|12|2|\neg \paren {\paren {p \uparrow q} \land r}|11|Disjunction of Negations}}
{{SequentIntro|13|2|\paren {p \uparrow q} \uparrow r|12
  |{{Defof|Logical NAND}} }}
{{DoubleNegIntro|14|2|\neg \neg \paren {\paren {p \uparrow q} \uparrow r}|13}}
{{Conjunction|15|2|\neg \neg \paren {\paren {p \uparrow q} \uparrow r} \land \neg \paren {p \uparrow \paren {q \uparrow r} }|13|10}}
{{DeMorgan|16|2|\neg \paren {\neg \paren {\paren {p \uparrow q} \uparrow r} \lor \paren {p \uparrow \paren {q \uparrow r} } }|15|Conjunction of Negations}}
{{SequentIntro|17|2
  |\neg \paren {\paren {p \uparrow q} \uparrow r \implies p \uparrow \paren {q \uparrow r} }
  |16
  |Disjunction and Conditional
}}
{{NonContradiction|18|1, 2|1|17}}
{{EndTableau}}
Taking $p = \top$, $r = \bot$, we find $\vdash p \land \neg r$, and conclude our initial assumption was false.
{{qed}}
Theorem: NAND is not Associative

:$p \uparrow \paren {q \uparrow r} \not \vdash \paren {p \uparrow q} \uparrow r$

Proof:
We apply the Method of Truth Tables:
:$\begin{array}{|ccccc||ccccc|} \hline
p & \uparrow & (q & \uparrow & r) & (p & \uparrow & q) & \uparrow & r \\
\hline
\F & \T & \F & \T & \F & \F & \T & \F & \T & \F \\
\F & \T & \F & \T & \T & \F & \T & \F & \F & \T \\
\F & \T & \T & \T & \F & \F & \T & \T & \T & \F \\
\F & \T & \T & \F & \T & \F & \T & \T & \F & \T \\
\T & \F & \F & \T & \F & \T & \T & \F & \T & \F \\
\T & \F & \F & \T & \T & \T & \T & \F & \F & \T \\
\T & \F & \T & \T & \F & \T & \F & \T & \T & \F \\
\T & \T & \T & \F & \T & \T & \F & \T & \T & \T \\
\hline
\end{array}$
As can be seen by inspection, the truth values under the main connectives do not match for all boolean interpretations.
{{qed}}
Theorem: NOR with Equal Arguments

:$p \downarrow p \dashv \vdash \neg p$
That is, the NOR of a proposition with itself corresponds to the negation operator.

Proof:
{{BeginTableau|p \downarrow p \vdash \neg p}}
{{Premise|1|p \downarrow p}}
{{SequentIntro|2|1|\neg \paren {p \lor p}|1|Definition of Logical NOR}}
{{Idempotence|3|1|\neg p|2|Disjunction}}
{{EndTableau|lemma}}
{{BeginTableau|\neg p \vdash p \downarrow p}}
{{Premise|1|\neg p}}
{{Idempotence|2|1|\neg \paren {p \lor p}|1|Disjunction}}
{{SequentIntro|3|1|p \downarrow p|2|Definition of Logical NOR}}
{{EndTableau}}
{{qed}}
Theorem: NOR with Equal Arguments

:$p \downarrow p \dashv \vdash \neg p$
That is, the NOR of a proposition with itself corresponds to the negation operator.

Proof:
Apply the Method of Truth Tables:
:$\begin {array} {|ccc||cc|} \hline
p & \downarrow & p & \neg & p \\
\hline
\F & \T & \F & \T & \F \\
\T & \F & \T & \F & \T \\
\hline
\end{array}$
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
{{qed}}
Theorem: NOR is Commutative

:$p \downarrow q \dashv \vdash q \downarrow p$

Proof:
{{BeginTableau|p \downarrow q \vdash q \downarrow p}}
{{Premise|1|p \downarrow q}}
{{SequentIntro|2|1|\neg \paren {p \lor q}|1|{{Defof|Logical NOR}} }}
{{Commutation|3|1|\neg \paren {q \lor p}|2|Disjunction}}
{{SequentIntro|4|1|q \uparrow p|3|{{Defof|Logical NOR}} }}
{{EndTableau|lemma}}
{{BeginTableau|q \downarrow p \vdash p \uparrow q}}
{{Premise|1|q \downarrow p}}
{{SequentIntro|2|1|\neg \paren {q \lor p}|1|{{Defof|Logical NOR}} }}
{{Commutation|3|1|\neg \paren {p \lor q}|2|Disjunction}}
{{SequentIntro|4|1|p \downarrow q|3|{{Defof|Logical NOR}} }}
{{EndTableau|qed}}
Theorem: NOR is Commutative

:$p \downarrow q \dashv \vdash q \downarrow p$

Proof:
Apply the Method of Truth Tables:
:$\begin{array}{|ccc||ccc|} \hline
p & \downarrow & q & q & \downarrow & p \\
\hline
\F & \T & \F & \F & \T & \F \\
\F & \F & \T & \T & \F & \F \\
\T & \F & \F & \F & \F & \T \\
\T & \F & \T & \T & \F & \T \\
\hline
\end{array}$
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
{{qed}}
Theorem: NOR is not Associative

:$p \downarrow \paren {q \downarrow r} \not \vdash \paren {p \downarrow q} \downarrow r$

Proof:
{{BeginTableau|\neg \paren {p \downarrow \paren {q \downarrow r} \implies \paren {p \downarrow q} \downarrow r} }}
{{Assumption|1|\neg p \land r}}
{{Simplification|2|1|\neg p|1|1}}
{{Simplification|3|1|r|1|2}}
{{Addition|4|1|q \lor r|3|2}}
{{DoubleNegIntro|5|1|\neg \neg \paren {q \lor r}|4}}
{{SequentIntro|6|1|\neg \paren {q \downarrow r}|5|Definition of Logical NOR}}
{{Conjunction|7|1|\neg p \land \neg \paren {q \downarrow r}|2|6}}
{{DeMorgan|8|1|\neg \paren {p \lor \paren {q \downarrow r} }|7|Conjunction of Negations}}
{{SequentIntro|9|1|p \downarrow \paren {q \downarrow r}|8|Definition of Logical NOR}}
{{Addition|10|1|\paren {p \downarrow q} \lor r|3|2}}
{{DoubleNegIntro|11|1|\neg \neg \paren {\paren {p \downarrow q} \lor r}|10}}
{{SequentIntro|12|1|\neg \paren {\paren {p \downarrow q} \downarrow r}|11|Definition of Logical NOR}}
{{DoubleNegIntro|13|1|\neg \neg \paren {p \downarrow \paren {q \downarrow r} }|9}}
{{Conjunction|14|1|\paren {\neg \neg \paren {p \downarrow \paren {q \downarrow r} } } \land \paren {\neg \paren {\paren {p \downarrow q} \downarrow r} }|13|12}}
{{DeMorgan|15|1|\neg \paren {\neg \paren {p \downarrow \paren {q \downarrow r} } \lor \paren {\paren {p \downarrow q} \downarrow r} }|14|Conjunction of Negations}}
{{SequentIntro|16|1
  |\neg \paren {p \downarrow \paren {q \downarrow r} \implies \paren {p \downarrow q} \downarrow r}
  |15
  |Rule of Material Implication
}}
{{EndTableau}}
Taking $p = \bot$ and $r = \top$, we have $\vdash \neg p \land r$, discharging the last assumption.
Hence the result.
{{qed}}
Theorem: NOR is not Associative

:$p \downarrow \paren {q \downarrow r} \not \vdash \paren {p \downarrow q} \downarrow r$

Proof:
Apply the Method of Truth Tables:
:$\begin{array}{|ccccc||ccccc|} \hline
p & \downarrow & (q & \downarrow & r) & (p & \downarrow & q) & \downarrow & r \\
\hline
\F & \F & \F & \T & \F & \F & \T & \F & \F & \F \\
\F & \T & \F & \F & \T & \F & \T & \F & \F & \T \\
\F & \T & \T & \F & \F & \F & \F & \T & \T & \F \\
\F & \T & \T & \F & \T & \F & \F & \T & \F & \T \\
\T & \F & \F & \T & \F & \T & \F & \F & \T & \F \\
\T & \F & \F & \F & \T & \T & \F & \F & \F & \T \\
\T & \F & \T & \F & \F & \T & \F & \T & \T & \F \\
\T & \F & \T & \F & \T & \T & \F & \T & \F & \T \\
\hline
\end{array}$
As can be seen by inspection, the truth values under the main connectives do not match for all boolean interpretations.
{{qed}}
Theorem: Representation of Ternary Expansions

Let $x \in \R$ be a real number.
Let $x$ be represented in base $3$ notation.
While it may be possible for $x$ to have two different such representations, for example:
:$\dfrac 1 3 = 0.100000 \ldots_3 = 0.022222 \ldots_3$
it is not possible for $x$ be written in more than one way without using the digit $1$.

Proof:
It is sufficient to show that two distinct representations represents two distinct numbers.
Let $a$ and $b$ two real numbers representable as the form above.
Their signs are easy to distinguish, so we consider $\size a$ and $\size b$.
There is some $n$ such that:
:$\size a, \size b < 3^n$
In that case, $\dfrac {\size a} {3^n}$ can be represented as:
:$0.a_1 a_2 a_3 \ldots$
and $\dfrac {\size b} {3^n}$ can be represented as:
:$0.b_1 b_2 b_3 \ldots$
where $a_i, b_i$ are either $0$ or $2$.
Let $N$ be the smallest integer such that $a_N \ne b_N$.
{{WLOG}} assume that $a_N = 2$ and $b_N = 0$.
We have:
{{begin-eqn}}
{{eqn | l = \frac {\size a} {3^n}
      | r = \sum_{j \mathop = 1}^\infty \frac {a_j} {3^j}
}}
{{eqn | r = \sum_{j \mathop = 1}^{N - 1} \frac {a_j} {3^j} + \sum_{j \mathop = N}^\infty \frac {a_j} {3^j}
}}
{{eqn | o = \ge
      | r = \sum_{j \mathop = 1}^{N - 1} \frac {a_j} {3^j} + \frac 2 {3^N}
      | c = because $a_N = 2$, $a_j \ge 0$
}}
{{eqn | o = >
      | r = \sum_{j \mathop = 1}^{N - 1} \frac {a_j} {3^j} + \frac 1 {3^N}
}}
{{eqn | r = \sum_{j \mathop = 1}^{N - 1} \frac {b_j} {3^j} + \sum_{j \mathop = N + 1}^\infty \frac 2 {3^j}
      | c = Sum of Infinite Geometric Sequence
}}
{{eqn | o = \ge
      | r = \sum_{j \mathop = 1}^{N - 1} \frac {b_j} {3^j} + \sum_{j \mathop = N}^\infty \frac {b_j} {3^j}
      | c = because $b_N = 0$, $b_j \le 2$
}}
{{eqn | r = \frac {\size b} {3^n}
}}
{{end-eqn}}
and thus $\size a$ and $\size b$ are distinct.
{{qed}}
Theorem: Equivalence of Definitions of Cantor Set

{{TFAE|def = Cantor Set|view = the Cantor Set $\CC$}}:

Proof:
Let $\CC_n$ be defined as in $(1)$.
Let $x \in \closedint 0 1$.
We need to show that:
:$x$ can be written in base $3$ without using the digit $1$ {{iff}}:
::$\forall n \in \Z, n \ge 1: x \in C_n$
First we note that from Sum of Infinite Geometric Sequence:
:$\ds 1 = \sum_{n \mathop = 0}^\infty \frac 2 3 \paren {\frac 1 3}^n$
that is:
:$1 = 0.2222 \ldots_3$
Thus any real number which, expressed in base $3$, ends in $\ldots 10000 \ldots$ can be expressed as one ending in $\ldots 02222 \ldots$ by dividing the above by an appropriate power of $3$.
{{proof wanted|Still some work to do yet, obviously ...<br />New formulation demands new approach}}