avewright/proofwiki-math huggingface dataset:
Theorem: Rule of Idempotence/Conjunction/Formulation 1

:$p \dashv \vdash p \land p$

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connectives match for each boolean interpretations.
$\begin{array} {|c||ccc|} \hline
p & p & \land & p \\
\hline
\T & \T & \T & \T \\
\F & \F & \F & \F \\
\hline
\end{array}$
{{qed}}
Theorem: Rule of Idempotence/Conjunction/Formulation 2

:$\vdash p \iff \paren {p \land p}$

Proof:
{{BeginTableau|\vdash p \iff \paren {p \land p} }}
{{Assumption|1|p}}
{{Conjunction|2|1|p \land p|1|1}}
{{Implication|3||p \implies \paren {p \land p}|1|2}}
{{Assumption|4|p \land p}}
{{Simplification|5|4|p|4|1}}
{{Implication|6||\paren {p \land p} \implies p|4|5}}
{{BiconditionalIntro|7||p \iff \paren {p \land p}|3|6}}
{{EndTableau|qed}}
Theorem: Ordering Cycle implies Equality

Let $\struct {S, \preceq}$ be an ordered set.
Let $x_1$, $x_2$, and $x_3$ be elements of $S$.
Suppose that
{{begin-eqn}}
{{eqn | l = x_1
      | o = \preceq
      | r = x_2
}}
{{eqn | l = x_2
      | o = \preceq
      | r = x_3
}}
{{eqn | l = x_3
      | o = \preceq
      | r = x_1
}}
{{end-eqn}}
Then $x_1 = x_2 = x_3$.

Proof:
Because $\preceq$ is an ordering, it is transitive and antisymmetric.
By transitivity, $x_1 \preceq x_3$.
Because $x_1 \preceq x_3$ and $x_3 \preceq x_1$, antisymmetry allows us to conclude that $x_1 = x_3$.
Because $x_1 = x_3$ and $x_1 \preceq x_2$, we must have $x_3 \preceq x_2$.
Because $x_3 \preceq x_2$ and $x_2 \preceq x_3$, antisymmetry allows us to conclude that $x_2 = x_3$.
Thus $x_1 = x_2 = x_3$.
{{qed}}
Category:Order Theory
jnqoq4qotaxv6j6szamy3emo8iswegt
Theorem: Euclidean Topology is Product Topology

Let $T_1 = \struct {\R, \tau_1}$ be the topological space such that $\tau_1$ is the Euclidean topology on $\R$.
Let $T_n = \struct {\R^n, \tau_n}$ be the topological space such that $\tau_n$ is the product topology on the cartesian product $\ds \R_n = \prod_{i \mathop = 1}^n \R$.
Then the Euclidean topology on $\R^n$ and the product topology on $\R^n$ are the same.

Proof:
Denote the Euclidean topology on $\R^n$ as $\tau$, and denote the product topology on $\R^n$ as $\tau'$.
Let $U \in \tau$, and let $x = \tuple{x_1, \ldots, x_n} \in U$.
Then there exists $\epsilon \in \R_{>0}$ such that the open ball $\map {B_\epsilon} x \subseteq U$.
We show that:
:$\ds B' = \prod_{i \mathop = 1}^n \openint {x_i - \dfrac \epsilon n} {x_i + \dfrac \epsilon n} \subseteq \map {B_\epsilon} x$
For if $y = \tuple {y_1, \ldots, y_n} \in B'$, then:
{{begin-eqn}}
{{eqn | l = \map d {x, y}
      | r = \paren {\sum_{i \mathop = 1}^n \size {x_i - y_i}^2}^{1/2}
      | c = where $d$ denotes the Euclidean metric
}}
{{eqn | o = \le
      | r = \sum_{i \mathop = 1}^n \size{x_i - y_i}
      | c = by Minkowski's Inequality for Sums
}}
{{eqn | o = <
      | r = \sum_{i \mathop = 1}^n \dfrac \epsilon n
}}
{{eqn | r = \epsilon
}}
{{end-eqn}}
From Natural Basis of Product Topology of Finite Product, $B' \in \tau'$.
As $B' \subseteq \map {B_\epsilon} x \subseteq U$, Neighborhood Condition for Coarser Topology shows that $\tau' \subseteq \tau$.
{{qed|lemma}}
Let $U' \in \tau'$.
Let $x = \tuple {x_1, \ldots, x_n} \in U'$.
From Natural Basis of Product Topology of Finite Product, sets of the type $\ds \prod_{i \mathop = 1}^n U'_i$ with $U'_i \in \tau_1$ form an analytic basis for $\tau'$.
From Equivalence of Definitions of Analytic Basis, it follows that we can select $U'_1, \ldots, U'_n \in \tau_1$ such that $\ds x \in \prod_{i \mathop = 1}^n U'_i \subseteq U'$.
By definition of open set, it follows that for all $i \in \set {1, \ldots, n}$, we can find $\epsilon_i \in \R_{>0}$ such that $\openint {x_i - \epsilon_i} {x_i + \epsilon_i} \subseteq U'_i$.
Put $\epsilon = \min \set {\epsilon_i : i = 1, \ldots, n}$.
We show that the open ball $\map {B_\epsilon} x \subseteq U'$.
For if $y = \tuple {y_1, \ldots, y_n} \in \map {B_\epsilon} x$, then $y_i \in \openint {x_i - \epsilon_i} {x_i + \epsilon_i }$, as:
:$\size {x_i - y_i} < \epsilon \le \epsilon_i$
It follows that:
:$\ds \map {B_\epsilon} x \subseteq \prod_{i \mathop = 1}^n \openint {x_i - \epsilon_i} {x_i + \epsilon_i} \subseteq \prod_{i \mathop = 1}^n U'_i \subseteq U'$
Then Neighborhood Condition for Coarser Topology shows that $\tau \subseteq \tau'$.
{{qed|lemma}}
It follows that $\tau = \tau'$.
{{qed}}
Theorem: Euclidean Topology is Product Topology

Let $T_1 = \struct {\R, \tau_1}$ be the topological space such that $\tau_1$ is the Euclidean topology on $\R$.
Let $T_n = \struct {\R^n, \tau_n}$ be the topological space such that $\tau_n$ is the product topology on the cartesian product $\ds \R_n = \prod_{i \mathop = 1}^n \R$.
Then the Euclidean topology on $\R^n$ and the product topology on $\R^n$ are the same.

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 2}$, let $\map P n$ be the proposition:
:the Euclidean topology on $\R^n$ and the product topology on $\R^n$ are the same.
=== Basis for the Induction ===
$\map P 2$ is the case:
:the Euclidean topology on $\R^n$ and the product topology on $\R^n$ are the same.
This is demonstrated in Euclidean Topology on Cartesian Plane is Product Topology.
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:
:the Euclidean topology on $\R^k$ and the product topology on $\R^k$ are the same.
from which it is to be shown that:
:the Euclidean topology on $\R^{k + 1}$ and the product topology on $\R^{k + 1}$ are the same.
=== Induction Step ===
This is the induction step:
We have that:
:$\R^{k + 1} = \R^k \times \R$
By the induction hypothesis:
:the Euclidean topology on $\R^k$ and the product topology on $\R^k$ are the same.
By the basis for the induction:
:the Euclidean topology on $\R^k \times \R$ and the product topology on $\R^k \times \R$ are the same.
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}:$
::the Euclidean topology on $\R^n$ and the product topology on $\R^n$ are the same.
{{qed}}
Theorem: Modus Ponendo Tollens/Variant/Formulation 1/Proof

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

Proof:
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
$\begin{array}{|cccc||cccc|} \hline
\neg & (p & \land & q) & p & \implies & \neg & q \\
\hline
T & F & F & F & F & T & T & F \\
T & F & F & T & F & T & F & T \\
T & T & F & F & T & T & T & F \\
F & T & T & T & T & F & F & T \\
\hline
\end{array}$
{{qed}}
Theorem: Modus Ponendo Tollens/Variant/Formulation 1/Forward Implication

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

Proof:
{{BeginTableau|\neg \paren {p \land q} \vdash p \implies \neg q}}
{{Premise|1|\neg \paren {p \land q} }}
{{Assumption|2|p}}
{{Assumption|3|q}}
{{Conjunction|4|2, 3|p \land q|2|3}}
{{NonContradiction|5|1, 2, 5|4|1}}
{{Contradiction|6|1, 2|\neg q|3|5}}
{{Implication|7|1|p \implies \neg q|2|6}}
{{EndTableau|qed}}
Category:Modus Ponendo Tollens
jpjvh2hi3g9yzhon2kclhojexlzq1na
Theorem: Modus Ponendo Tollens/Variant/Formulation 1/Reverse Implication

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

Proof:
{{BeginTableau|p \implies \neg q \vdash \neg \paren {p \land q} }}
{{Premise|1|p \implies \neg q}}
{{Assumption|2|p \land q|Assume the opposite of what is to be proved ...}}
{{Simplification|3|2|p|2|1}}
{{Simplification|4|2|q|2|2}}
{{ModusPonens|5|1, 2|\neg q|1|3}}
{{NonContradiction|6|1, 2|4|5|... and demonstrate a contradiction}}
{{Contradiction|7|1|\neg \paren {p \land q}|2|6}}
{{EndTableau|qed}}
Category:Modus Ponendo Tollens
5z8tpfk79jnx16ntyyx18hj42odr2ag
Theorem: Modus Ponendo Tollens/Variant/Formulation 1

: $\neg \left({p \land q}\right) \dashv \vdash p \implies \neg q$

Proof:
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
$\begin{array}{|cccc||cccc|} \hline
\neg & (p & \land & q) & p & \implies & \neg & q \\
\hline
T & F & F & F & F & T & T & F \\
T & F & F & T & F & T & F & T \\
T & T & F & F & T & T & T & F \\
F & T & T & T & T & F & F & T \\
\hline
\end{array}$
{{qed}}
Theorem: Modus Ponendo Tollens/Variant/Formulation 2

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

Proof:
{{BeginTableau|\vdash \paren {\neg \paren {p \land q} } \iff \paren {p \implies \neg q} }}
{{Assumption|1|\neg \paren {p \land q} }}
{{SequentIntro|2|1|p \implies \neg q|1|Modus Ponendo Tollens: Formulation 1: Forward Implication}}
{{Implication|3||\paren {\neg \paren {p \land q} } \implies \paren {p \implies \neg q}|1|2}}
{{Assumption|4|p \implies \neg q}}
{{SequentIntro|5|4|\neg \paren {p \land q}|4|Modus Ponendo Tollens: Formulation 1: Reverse Implication}}
{{Implication|6||\paren {p \implies \neg q} \implies \paren {\neg \paren {p \land q} }|4|5}}
{{BiconditionalIntro|7||\paren {\neg \paren {p \land q} } \iff \paren {p \implies \neg q}|3|6}}
{{EndTableau|qed}}
Theorem: Conditional is Equivalent to Negation of Conjunction with Negative/Formulation 1/Reverse Implication

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

Proof:
{{BeginTableau|\neg \paren {p \land \neg q} \vdash p \implies q}}
{{Premise|1|\neg \paren {p \land \neg q} }}
{{DeMorgan|2|1|\neg p \lor \neg \neg q|1|Disjunction of Negations}}
{{SequentIntro|3|1|p \implies \neg \neg q|2|Rule of Material Implication}}
{{Assumption|4|p}}
{{ModusPonens|5|1, 4|\neg \neg q|3|4}}
{{DoubleNegElimination|6|1, 4|q|5}}
{{Implication|7|1|p \implies q|4|6}}
{{EndTableau|qed}}
{{LEM|Double Negation Elimination|3}}
Theorem: Conditional is Equivalent to Negation of Conjunction with Negative/Formulation 1

:$p \implies q \dashv \vdash \neg \paren {p \land \neg 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.
$\begin{array}{|ccc||ccccc|} \hline
p & \implies & q & \neg & (p & \land & \neg & q) \\
\hline
\F & \T & \F & \T & \F & \F & \T & \F \\
\F & \T & \T & \T & \F & \F & \F & \T \\
\T & \F & \F & \F & \T & \T & \T & \F \\
\T & \T & \T & \T & \T & \F & \F & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Zero Derivative implies Constant Complex Function

Let $D \subseteq \C$ be a connected domain of $\C$.
Let $f: D \to \C$ be a complex-differentiable function.
For all $z \in D$, let $\map {f'} z = 0$.
Then $f$ is constant on $D$.

Proof:
Let $u, v: \set {\tuple {x, y} \in \R^2: x + i y = z \in D} \to \R$ be the two real-valued functions defined in the Cauchy-Riemann Equations:
:$\map u {x, y} = \map \Re {\map f z}$
:$\map v {x, y} = \map \Im {\map f z}$
By the Cauchy-Riemann Equations:
:$f' = \dfrac {\partial f} {\partial x} = \dfrac {\partial u} {\partial x} + i \dfrac {\partial v} {\partial x}$
:$f' = -i \dfrac {\partial f} {\partial y} = \dfrac {\partial v} {\partial y} - i \dfrac {\partial u} {\partial y}$
As $f' = 0$ by assumption, this implies:
:$0 = \dfrac {\partial u} {\partial x} = \dfrac {\partial u} {\partial y} = \dfrac {\partial v} {\partial x} = \dfrac {\partial v} {\partial y}$
Then Zero Derivative implies Constant Function shows that $\map u {x + t, y} = \map u {x, y}$ for all $t \in \R$.
Similar results apply for the other three partial derivatives.
Let $z, w \in D$.
From Connected Domain is Connected by Staircase Contours, it follows that there exists a staircase contour $C$ in $D$ with endpoints $z$ and $w$.
The contour $C$ is a concatenation of directed smooth curves that can be parameterized as line segments on one of these two forms:
:$(1): \quad \map \gamma t = z_0 + t r$
:$(2): \quad \map \gamma t = z_0 + i t r$
for some $z_0 \in D$ and $r \in \R$ for all $t \in \closedint 0 1$.
If $z_1 \in D$ lies on the same line segment as $z_0$, it follows that for parameterizations of type $(1)$:
{{begin-eqn}}
{{eqn | l = \map f {z_1}
      | r = \map u {z_0 + t r} + \map v {z_0 + t r}
      | c = for some $t \in \closedint 0 1$
}}
{{eqn | r = \map u {z_0} + \map v {z_0}
      | c = Zero Derivative implies Constant Function
}}
{{eqn | r = \map f {z_0}
}}
{{end-eqn}}
Similarly, for parameterizations of type $(2)$:
{{begin-eqn}}
{{eqn | l = \map f {z_1}
      | r = \map u {z_0 + i t r} + \map v {z_0 + i t r}
      | c = for some $t \in \closedint 0 1$
}}
{{eqn | r = \map f {z_0}
      | c = Zero Derivative implies Constant Function
}}
{{end-eqn}}
As the image of $C$ is connected by these line segments, it follows that for all $z_0$ and $z_1$ in the image of $C$:
:$\map f {z_0} = \map f {z_1}$
In particular:
:$\map f z = \map f w$
so $f$ is constant on $D$.
{{qed}}
Theorem: Relation between P-Product Metric and Chebyshev Distance on Real Vector Space

For $n \in \N$, let $\R^n$ be a Euclidean space.
Let $p \in \R_{\ge 1}$.
Let $d_p$ be the $p$-product metric on $\R^n$. 
Let $d_\infty$ be the Chebyshev distance on $\R^n$.
Then
:$\forall x, y \in \R^n: \map {d_\infty} {x, y} \le \map {d_p} {x, y} \le n^{1/p} \map {d_\infty} {x, y}$

Proof:
By definition of the Chebyshev distance on $\R^n$, we have:
:$\ds \map {d_\infty} {x, y} = \max_{i \mathop = 1}^n \size {x_i - y_i}$
where $x = \tuple {x_1, x_2, \ldots, x_n}$ and $y = \tuple {y_1, y_2, \ldots, y_n}$.
Let $j$ be chosen so that:
:$\ds \size {x_j - y_j} = \max_{i \mathop = 1}^n \size {x_i - y_i}$
Then:
{{begin-eqn}}
{{eqn | l = \map {d_\infty} {x, y}
      | r = \paren {\size {x_j - y_j}^p}^{1/p}
}}
{{eqn | o = \le
      | r = \paren {\sum_{i \mathop = 1}^n \size {x_i - y_i}^p}^{1/p}
      | c = Power of Maximum is not Greater than Sum of Powers
}}
{{eqn | r = \map {d_p} {x, y}
}}
{{eqn | o = \le
      | r = \paren {n \size {x_j - y_j}^p}^{1/p}
      | c = Sum of $r$ Powers is not Greater than $r$ times Power of Maximum
}}
{{eqn | r = n^{1/p} \size {d_\infty} {x, y}
}}
{{end-eqn}}
Theorem: De Morgan's Laws (Logic)/Disjunction of Negations/Formulation 1/Forward Implication

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

Proof:
{{BeginTableau|\neg p \lor \neg q \vdash \neg \paren {p \land q} }}
{{Premise|1|\neg p \lor \neg q}}
{{Assumption|2|p \land q}}
{{Simplification|3|2|p|2|1}}
{{Simplification|4|2|q|2|2}}
{{Assumption|5|\neg p}}
{{NonContradiction|6|2, 5|3|5}}
{{Assumption|7|\neg q}}
{{NonContradiction|8|2, 7|4|7}}
{{ProofByCases|9|1, 2|\bot|1|5|6|7|8}}
{{Contradiction|10|1|\neg \paren {p \land q}|2|9}}
{{EndTableau}}
{{qed}}
Theorem: De Morgan's Laws (Logic)/Disjunction of Negations/Formulation 1/Reverse Implication

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

Proof:
{{BeginTableau|\neg \paren {p \land q} \vdash \neg p \lor \neg q}}
{{Premise|1|\neg \paren {p \land q} }}
{{Assumption|2|\neg \paren {\neg p \lor \neg q} }}
{{Assumption|3|\neg p}}
{{Addition|4|3|\neg p \lor \neg q|3|1}}
{{NonContradiction|5|2, 3|4|2}}
{{Reductio|6|2|p|3|5}}
{{Assumption|7|\neg q}}
{{Addition|8|7|\neg p \lor \neg q|7|2}}
{{NonContradiction|9|2, 7|8|2}}
{{Reductio|10|2|q|7|9}}
{{Conjunction|11|2|p \land q|6|10}}
{{NonContradiction|12|1, 2|11|1}}
{{Reductio|13|1|\neg p \lor \neg q|2|12}}
{{EndTableau|qed}}
{{LEM|Reductio ad Absurdum|3}}
Theorem: De Morgan's Laws (Logic)/Disjunction of Negations/Formulation 1

:$\neg p \lor \neg q \dashv \vdash \neg \paren {p \land 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}{|ccccc||cccc|} \hline
\neg & p & \lor & \neg & q & \neg & (p & \land & q) \\
\hline
\T & \F & \T & \T & \F & \T & \F & \F & \F \\
\T & \F & \T & \F & \T & \T & \F & \F & \T \\
\F & \T & \T & \T & \F & \T & \T & \F & \F \\
\F & \T & \F & \F & \T & \F & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: De Morgan's Laws (Logic)/Disjunction of Negations/Formulation 1

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

Proof:
{{BeginTableau|\neg \paren {p \land q} \vdash \neg p \lor \neg q}}
{{Premise|1|\neg \paren {p \land q} }}
{{Assumption|2|\neg \paren {\neg p \lor \neg q} }}
{{Assumption|3|\neg p}}
{{Addition|4|3|\neg p \lor \neg q|3|1}}
{{NonContradiction|5|2, 3|4|2}}
{{Reductio|6|2|p|3|5}}
{{Assumption|7|\neg q}}
{{Addition|8|7|\neg p \lor \neg q|7|2}}
{{NonContradiction|9|2, 7|8|2}}
{{Reductio|10|2|q|7|9}}
{{Conjunction|11|2|p \land q|6|10}}
{{NonContradiction|12|1, 2|11|1}}
{{Reductio|13|1|\neg p \lor \neg q|2|12}}
{{EndTableau|qed}}
{{LEM|Reductio ad Absurdum|3}}
Theorem: De Morgan's Laws (Logic)/Disjunction of Negations/Formulation 2

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

Proof:
{{BeginTableau|\vdash \paren {\neg p \lor \neg q} \iff \paren {\neg \paren {p \land q} } }}
{{Assumption|1|\neg p \lor \neg q}}
{{SequentIntro|2|1|\neg \paren {p \land q}|1|De Morgan's Laws (Logic): Disjunction of Negations: Formulation 1}}
{{Implication|3||\paren {\neg p \lor \neg q} \implies \paren {\neg \paren {p \land q} }|1|2}}
{{Assumption|4|\neg \paren {p \land q} }}
{{SequentIntro|5|4|\neg p \lor \neg q|4|De Morgan's Laws (Logic): Disjunction of Negations: Formulation 1}}
{{Implication|6||\paren {\neg \paren {p \land q} } \implies \paren {\neg p \lor \neg q}|4|5}}
{{BiconditionalIntro|7||\paren {\neg p \lor \neg q} \iff \paren {\neg \paren {p \land q} }|3|6}}
{{EndTableau}}
{{qed}}
Theorem: De Morgan's Laws (Logic)/Disjunction of Negations/Formulation 2

:$\vdash \paren {\neg p \lor \neg q} \iff \paren {\neg \paren {p \land 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}{|ccccc|c|cccc|} \hline
\neg & p & \lor & \neg & q & \iff & \neg & (p & \land & q) \\
\hline
\T & \F & \T & \T & \F & \T & \T & \F & \F & \F \\
\T & \F & \T & \F & \T & \T & \T & \F & \F & \T \\
\F & \T & \T & \T & \F & \T & \T & \T & \F & \F \\
\F & \T & \F & \F & \T & \T & \F & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: De Morgan's Laws (Logic)/Conjunction of Negations/Formulation 1/Forward Implication

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

Proof:
{{BeginTableau|\neg p \land \neg q \vdash \neg \paren {p \lor q} }}
{{Premise|1|\neg p \land \neg q}}
{{Simplification|2|1|\neg p|1|1}}
{{Simplification|3|1|\neg q|1|2}}
{{Assumption|4|p \lor q}}
{{Assumption|5|p}}
{{NonContradiction|6|1, 5|5|2}}
{{Assumption|7|q}}
{{NonContradiction|8|1, 7|7|3}}
{{ProofByCases|9|1, 4|\bot|4|5|6|7|8}}
{{Contradiction|10|1|\neg \paren {p \lor q}|4|9}}
{{EndTableau|qed}}
Theorem: De Morgan's Laws (Logic)/Conjunction of Negations/Formulation 1/Reverse Implication

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

Proof:
{{BeginTableau|\neg \paren {p \lor q} \vdash \neg p \land \neg q}}
{{Premise|1|\neg \paren {p \lor q} }}
{{Assumption|5|p}}
{{Addition|3|2|p \lor q|2|1}}
{{NonContradiction|4|1, 3|3|1}}
{{Contradiction|5|1|\neg p|2|4}}
{{Assumption|6|q}}
{{Addition|7|6|p \lor q|6|2}}
{{NonContradiction|8|1, 7|7|1}}
{{Contradiction|9|1|\neg q|6|8}}
{{Conjunction|10|1|\neg p \land \neg q|5|9}}
{{EndTableau|qed}}
Category:De Morgan's Laws (Logic)
7hif3lo8kwg7txhdhfm6bvpm7fym2tn
Theorem: De Morgan's Laws (Logic)/Conjunction of Negations/Formulation 1

:$\neg p \land \neg q \dashv \vdash \neg \paren {p \lor 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}{|ccccc||cccc|} \hline
\neg & p & \land & \neg & q & \neg & (p & \lor & q) \\
\hline
\T & \F & \T & \T & \F & \T & \F & \F & \F \\
\T & \F & \F & \F & \T & \F & \F & \T & \T \\
\F & \T & \F & \T & \F & \F & \T & \T & \F \\
\F & \T & \F & \F & \T & \F & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: De Morgan's Laws (Logic)/Conjunction of Negations/Formulation 2

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

Proof:
{{BeginTableau|\vdash \paren {\neg p \land \neg q} \iff \paren {\neg \paren {p \lor q} } }}
{{Assumption|1|\neg p \land \neg q}}
{{SequentIntro|2|1|\neg \paren {p \lor q}|1|De Morgan's Laws (Logic): Disjunction of Negations: Formulation 1}}
{{Implication|3||\paren {\neg p \land \neg q} \implies \paren {\neg \paren {p \lor q} }|1|2}}
{{Assumption|4|\neg \paren {p \lor q} }}
{{SequentIntro|5|4|\neg p \land \neg q|4|De Morgan's Laws (Logic): Disjunction of Negations: Formulation 1}}
{{Implication|6||\paren {\neg \paren {p \lor q} } \implies \paren {\neg p \land \neg q}|4|5}}
{{BiconditionalIntro|7||\paren {\neg p \land \neg q} \iff \paren {\neg \paren {p \lor q} }|3|6}}
{{EndTableau|qed}}
Theorem: De Morgan's Laws (Logic)/Conjunction of Negations/Formulation 2

:$\vdash \paren {\neg p \land \neg q} \iff \paren {\neg \paren {p \lor 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}{|ccccc|c|cccc|} \hline
\neg & p & \land & \neg & q & \iff & \neg & (p & \lor & q) \\
\hline
\T & \F & \T & \T & \F & \T & \T & \F & \F & \F \\
\T & \F & \F & \F & \T & \T & \F & \F & \T & \T \\
\F & \T & \F & \T & \F & \T & \F & \T & \T & \F \\
\F & \T & \F & \F & \T & \T & \F & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: De Morgan's Laws (Logic)/Conjunction/Formulation 1/Forward Implication

: $p \land q \vdash \neg \left({\neg p \lor \neg q}\right)$

Proof:
{{BeginTableau|p \land q \vdash \neg \left({\neg p \lor \neg q}\right)}}
{{Premise|1|p \land q}}
{{Simplification|2|1|p|1|1}}
{{Simplification|3|1|q|1|2}}
{{Assumption|4|\neg p \lor \neg q}}
{{Assumption|5|\neg p}}
{{NonContradiction|6|1, 5|2|5}}
{{Assumption|7|\neg q}}
{{NonContradiction|8|1, 7|3|7}}
{{ProofByCases|9|1, 4|\bot|4|5|6|7|8}}
{{Contradiction|10|1|\neg \left({\neg p \lor \neg q}\right)|4|9}}
{{EndTableau}}
{{qed}}
Theorem: De Morgan's Laws (Logic)/Conjunction/Formulation 1/Reverse Implication

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

Proof:
{{BeginTableau|\neg \paren {\neg p \lor \neg q} \vdash p \land q}}
{{Premise|1|\neg \paren {\neg p \lor \neg q} }}
{{Assumption|2|\neg \paren {p \land q} }}
{{DeMorgan|3|2|\neg p \lor \neg q|2|Disjunction of Negations}}
{{NonContradiction|4|1, 2|3|1}}
{{Reductio|5|1|p \land q|2|4}}
{{EndTableau|qed}}
{{LEM|Reductio ad Absurdum}}
Theorem: De Morgan's Laws (Logic)/Conjunction/Formulation 1

:$p \land q \dashv \vdash \neg \paren {\neg p \lor \neg 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.
$\begin{array}{|ccc||cccccc|} \hline
p & \land & q & \neg & (\neg & p & \lor & \neg & q)  \\
\hline
\F & \F & \F & \F & \T & \F & \T & \T & \F \\
\F & \F & \T & \F & \T & \F & \T & \F & \T \\
\T & \F & \F & \F & \F & \T & \T & \T & \F \\
\T & \T & \T & \T & \F & \T & \F & \F & \T \\
\hline
\end{array}$
{{qed}}
Theorem: De Morgan's Laws (Logic)/Conjunction/Formulation 2

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

Proof:
{{BeginTableau|\vdash \paren {p \land q} \iff \paren {\neg \paren {\neg p \lor \neg q} } }}
{{Assumption|1|p \land q}}
{{SequentIntro|2|1|\neg \paren {\neg p \lor \neg q}|1|De Morgan's Laws (Logic): Conjunction: Formulation 1}}
{{Implication|3||\paren {p \land q} \implies \paren {\neg \paren {\neg p \lor \neg q} }|1|2}}
{{Assumption|4|\neg \paren {\neg p \lor \neg q} }}
{{SequentIntro|5|4|p \land q|4|De Morgan's Laws (Logic): Conjunction: Formulation 1}}
{{Implication|6||\paren {\neg \paren {\neg p \lor \neg q} } \implies \paren {p \land q}|4|5}}
{{BiconditionalIntro|7||\paren {p \land q} \iff \paren {\neg \paren {\neg p \lor \neg q} }|3|6}}
{{EndTableau}}
{{qed}}