avewright/proofwiki-math huggingface dataset:
Theorem: Symmetric Difference with Intersection forms Boolean Ring

Let $S$ be a set.
Let:
:$\symdif$ denote the symmetric difference operation
:$\cap$ denote the set intersection operation
:$\powerset S$ denote the power set of $S$.
Then $\struct {\powerset S, \symdif, \cap}$ is a Boolean ring.

Proof:
From Symmetric Difference with Intersection forms Ring:
:$\struct {\powerset S, \symdif, \cap}$ is a commutative ring with unity.
From Set Intersection is Idempotent, $\cap$ is an idempotent operation on $S$.
Hence the result by definition of Boolean ring.
{{qed}}
Theorem: Parallelism is Reflexive Relation

Let $S$ be the set of straight lines in the plane.
For $l_1, l_2 \in S$, let $l_1 \parallel l_2$ denote that $l_1$ is parallel to $l_2$.
Then $\parallel$ is a reflexive relation on $S$.

Proof:
By definition of parallel lines, the contemporary definition is for a straight line to be declared parallel to itself.
Hence for a straight line $l$:
:$l \parallel l$
Thus $\parallel$ is seen to be reflexive.
Theorem: Parallelism is Symmetric Relation

Let $S$ be the set of straight lines in the plane.
For $l_1, l_2 \in S$, let $l_1 \parallel l_2$ denote that $l_1$ is parallel to $l_2$.
Then $\parallel$ is a symmetric relation on $S$.

Proof:
Let $l_1 \parallel l_2$.
By definition of parallel lines, $l_1$ does not meet $l_2$ when produced indefinitely.
Hence $l_2$ similarly does not meet $l_1$ when produced indefinitely.
That is:
:$l_2 \parallel l_1$
Thus $\parallel$ is seen to be symmetric.
Theorem: Parallelism is Equivalence Relation/Transitivity

Let $S$ be the set of straight lines in the plane.
For $l_1, l_2 \in S$, let $l_1 \parallel l_2$ denote that $l_1$ is parallel to $l_2$.
Then $\parallel$ is a transitive relation on $S$.

Proof:
From Parallelism is Transitive Relation:
:$l_1 \parallel l_2$ and $l_2 \parallel l_3$ implies $l_1 \parallel l_3$.
Thus $\parallel$ is seen to be transitive.
Theorem: 1-Seminorm on Continuous on Closed Interval Real-Valued Functions is Norm

Let $C \closedint a b$ be the space of real-valued functions continuous on $\closedint a b$.
Let $x \in C \closedint a b$ be a continuous real valued function.
Let $\ds \norm x_1 := \int_a^b \size {\map x t} \rd t$ be the 1-seminorm.
Then $\norm {\, \cdot \,}_1$ is a norm on $C \closedint a b$.

Proof:
=== Positive definiteness ===
Let $x \in C \closedint a b$.
Then $\forall t \in \closedint 0 1 : \size {\map x t} \ge 0 $.
Hence:
:$\ds \int_a^b \size {\map x t} \rd t = \norm x_1 \ge 0$.
Suppose $\forall t \in \closedint a b : \map x t = 0$.
Then $\norm x_1 = 0$.
Therefore:
:$\paren {x = 0} \implies \paren {\norm x_1 = 0}$
Let $x \in C \closedint a b : \norm x_1 = 0$.
Suppose:
:$\forall t \in \openint a b : \map x t = 0$.
By assumption of continuity of $x$:
:$\forall t \in \closedint a b : \map x t = 0$.
{{AimForCont}}:
:$\exists t_0 \in \openint a b : \map x {t_0} \ne 0$.
By assumption, $x$ is continuous at $t_0$.
:$\forall \epsilon \in \R_{> 0} : \exists \delta \in \R_{> 0} : \size {t - t_0} < \delta \implies \size {\map x t - \map x {t_0} } < \epsilon$
Furthermore:
:$\exists \delta \in \R_{> 0} : \paren {a < t_0 - \delta} \land \paren {t_0 + \delta < b}$
Let $\ds \epsilon = \frac {\size {\map x {t_0} } } 2$.
We have that:
{{begin-eqn}}
{{eqn | l = \size {\map x t}
      | r = \size {\map x t + \map x {t_0} - \map x {t_0} }
}}
{{eqn | o = \ge
      | r = \size {\map x {t_0} } - \size {\map x t - \map x {t_0} }
      | c = Reverse triangle inequality
}}
{{eqn | o = >
      | r = \size {\map x {t_0} } - \frac {\size {\map x {t_0} } } 2
}}
{{eqn | r = \frac {\size {\map x {t_0} } } 2 
}}
{{eqn | o = >
      | r = 0
      | c = $\map x {t_0} \ne 0$
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = 0
      | r = \norm x_1
}}
{{eqn | r = \int_a^b \size {\map x t} \rd t
}}
{{eqn | o = \ge
      | r = \int_{t_0 - \delta}^{t_0 + \delta} \size {\map x t} \rd t
      | c = $t_0 + \delta < b$, $a < t_0 - \delta$
}}
{{eqn | o = \ge
      | r = \int_{t_0 - \delta}^{t_0 + \delta} \frac {\size {\map x {t_0} } } 2 \rd t
}}
{{eqn | r = 2 \delta \frac {\size {\map x {t_0} } } 2
}}
{{eqn | r = \delta \size {\map x {t_0} }
}}
{{eqn | o = >
      | r = 0
}}
{{end-eqn}}
Hence, we reached a contradiction.
Therefore:
:$\paren {\norm x_1 = 0} \implies \paren {x = 0}$
Theorem: Approximation/Examples/22 over 7

$\dfrac {22} 7$ is a convenient approximation to $\pi$:
:$\dfrac {22} 7 = 3 \cdotp \dot 14285 \dot 7$

Proof:
{{begin-eqn}}
{{eqn | l = \dfrac {22} 7
      | r = 3 \cdotp \dot 14285 \dot 7
      | c = 
}}
{{eqn | l = \pi
      | o = \approx
      | r = 3 \cdotp 14159265
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {22} 7 - \pi
      | o = \approx
      | r = 0 \cdotp 0012645
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\frac {22} 7 - \pi} \pi
      | o = \approx
      | r = 0 \cdotp 0004025
      | c = 
}}
{{eqn | o = \approx
      | r = 0 \cdotp 04025 \%
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Perpendicularity is Symmetric Relation

Let $S$ be the set of straight lines in the plane.
For $l_1, l_2 \in S$, let $l_1 \perp l_2$ denote that $l_1$ is perpendicular to $l_2$.
Then $\perp$ is a symmetric relation on $S$.

Proof:
Let $l_1 \perp l_2$.
By definition of perpendicular lines, $l_1$ meets $l_2$ at a right angle.
Hence $l_2$ similarly meets $l_1$ at a right angle.
That is:
:$l_2 \perp l_1$
Thus $\parallel$ is seen to be symmetric.
Theorem: Perpendicularity is Antireflexive Relation

Let $S$ be the set of straight lines in the plane.
For $l_1, l_2 \in S$, let $l_1 \perp l_2$ denote that $l_1$ is perpendicular to $l_2$.
Then $\perp$ is an antireflexive relation on $S$.

Proof:
By definition of perpendicular lines, for $l_1$ to be perpendicular to itself would mean it would have to meet itself in a right angle.
This it does not do.
So $l_1 \not \perp l_1$.
Thus $\perp$ is seen to be antireflexive.
Theorem: Larger Set has Larger Set Difference

:$\card {V \setminus U} < \card {U \setminus V}$

Proof:
We have:
{{begin-eqn}}
{{eqn | l = \card {U \setminus V}
      | r = \card U - \card {U \cap V}
      | c = Cardinality of Set Difference
}}
{{eqn | o = > 
      | r = \card V - \card {U \cap V}
      | c = As $\card V < \card U$
}}
{{eqn | r = \card {V \setminus U}
      | c = Cardinality of Set Difference
}}
{{end-eqn}}
{{qed}}
Category:Set Difference
Category:Cardinality
qlpgh0skgeqocl5yjv5pudpj21853gl
Theorem: Perpendicularity is Antitransitive Relation

Let $S$ be the set of straight lines in the plane.
For $l_1, l_2 \in S$, let $l_1 \perp l_2$ denote that $l_1$ is perpendicular to $l_2$.
Then $\perp$ is an antitransitive relation on $S$.

Proof:
Let $l_1 \perp l_2$ and $l_2 \perp l_3$.
Then $l_1$ and $l_3$ are parallel, and not perpendicular.
Thus $\perp$ is seen to be antitransitive.
Theorem: Equivalence of Formulations of Axiom of Choice/Formulation 2 implies Formulation 1

The following formulation of the Axiom of Choice:

Proof:
Suppose that Formulation 2 holds.
That is, the Cartesian product of a non-empty family of non-empty sets is non-empty.
Let $\CC$ be a non-empty set of non-empty sets.
$\CC$ may be converted into an indexed set by using $\CC$ itself as the indexing set and using the identity mapping on $\CC$ to do the indexing.
Then the Cartesian product of all the sets in $\CC$ has at least one element.
An element of such a Cartesian product is a mapping, that is a family whose domain is the indexing set which in this context is $\CC$.
The value of this mapping at each index is an element of the set which bears that index.
So we have a mapping $f$ whose domain is $\CC$ such that:
:$A \in \CC \implies \map f A \in A$
Now let $\CC$ be the set of all non-empty subsets of some set $X$.
Then the assertion means that there exists a mapping $f$ whose domain is $\powerset X \setminus \set \O$ such that:
:$A \in \powerset X \setminus \set \O \implies \map f A \in A$
That is, Formulation 1 holds.
Theorem: Equivalence of Formulations of Axiom of Choice/Formulation 1 implies Formulation 3

The following formulation of the Axiom of Choice:

Proof:
Let $\SS$ be the set:
:$\SS = \set {s: \O \notin s \land \forall t, u \in s: t = u \lor t \cap u = \O}$
Let $c$ be a choice function on $\SS$ and consider the image set $c \sqbrk \SS$:
:$c \sqbrk \SS = \set {\map c s: \O \notin s \land \forall t, u \in s: t = u \lor t \cap u = \O}$
By the definition of choice function:
:$\map c s \in s$
By construction of $\SS$, for any $s \in \SS$:
:$s \cap c \sqbrk \SS = \set {\map c s}$
Theorem: Equivalence of Formulations of Axiom of Choice/Formulation 3 implies Formulation 1

The following formulation of the Axiom of Choice:

Proof:
Let $\BB$ be a non-empty indexed family of non-empty sets indexed by $\II$.
Consider sets of the following form:
:$\CC = \set {\tuple {B_i, x}: i \in \II, B_i \in \BB, x \in B_i}$
That is, it is the set of ordered pairs of which the first coordinate is a set $B_i \in \BB$ and the second coordinate is an element of $B_i$.
This is, by construction, a subset of the cartesian product:
:$\CC \subseteq \ds \BB \times \bigcup_{i \mathop \in \II} B_i$
By hypothesis all sets $B$ are non-empty.
Thus there exists at least one $\tuple {B_i, x}$ element in $\CC$ for each $B_i \in \CC$.
By Equality of Ordered Pairs, if $B_j \ne B_k$ in $\BB$, then $\tuple {B_i, x} \ne \tuple {B_j, x}$ for all such pairs in $\CC$.
So any two sets $\set {\tuple {B_j, x}: x \in B_j}$ and $\set {\tuple {B_k, x} :x \in B_k}$ are disjoint, by the inequality of their first coordinates.
Then $\CC$ is an indexed family of disjoint non-empty sets in $\BB \times \bigcup_{i \mathop \in \II} B_i$.
Hence $\CC$ satisfies the hypotheses of the third formulation of the Axiom of Choice.
Let $c$ be a set satisfying:
:$\forall r \in \CC: c \cap r = \set t$
All elements of $c$ are ordered pairs:
:the first coordinate of which is a set in $B_i \in \BB$
and:
:the second coordinate of which is an element $x \in B_i$.
Viewed as a relation, each set in $\BB$ bears $c$ to an element in that set.
Every set in $\BB$ bears $c$ to exactly one element inside that set.
So $c$ is in fact a mapping and satisfies the criteria of a choice function as expounded in formulation $(1)$.
Theorem: C^k Norm is Norm

Let $I = \closedint a b$ be a closed real interval.
Let $\struct {\map {C^k} I, +, \, \cdot \,}_\R$ be the vector space of real-valued functions, k-times differentiable on $I$.
Let $x \in \map {C^k} I$ be a real-valued function of differentiability class $k$.
Let $\norm {\, \cdot \,}_{\map {C^k} I}$ be the $C^k$ norm on $I$.
Then $\norm {\, \cdot \,}_{\map {C^k} I}$ is a norm on $\struct {\map {C^k} I, +, \, \cdot \,}_\R$.

Proof:
=== Positive definiteness ===
Let $x \in \map {C^k} I$.
Then:
{{begin-eqn}}
{{eqn | l = \norm x_{\map {C^k} I}
      | r = \sum_{i \mathop = 0}^k \norm {x^{\paren i} }_\infty
}}
{{eqn | o = \ge
      | r = \sum_{i \mathop = 0}^k 0
      | c = Supremum Norm is Norm, {{NormAxiomVector|1}}
}}
{{eqn | r = 0
}}
{{end-eqn}}
Suppose $\norm x_{\map {C^k} I} = 0$.
We have that the sum of non-negatives is zero if every element is zero.
Hence:
:$\forall i \in \N : 0 \le i \le k : \norm {x^{\paren i} }_\infty = 0$
That is:
:$\norm x_\infty = 0$
By Supremum Norm is Norm and {{NormAxiomVector|1}}:
:$\forall t \in I : \map x t = 0$
Theorem: Existence of Minimal Polynomial for Square Matrix over Field

Let $K$ be a field.
Let $n$ be a natural number.
Let $K^{n \times n}$ be the set of $n \times n$ matrices over $K$. 
Let $A \in K^{n \times n}$.
Then the minimal polynomial of $A$ exists and has degree at most $n^2$.

Proof:
By Matrices over Field form Vector Space:
:$K^{n \times n}$ forms a vector space under usual matrix addition and scalar multiplication.
By Dimension of Vector Space of Matrices:
:$K^{n \times n}$ has dimension $n^2$. 
Consider the collection of vectors: 
:$I, A, A^2, \ldots, A^{n^2}$
Since this is a collection of $n^2 + 1$ vectors, and $K^{n \times n}$ has dimension $n^2$, we have by Size of Linearly Independent Subset is at Most Size of Finite Generator:
:$I, A, A^2, \ldots, A^{n^2}$ are linearly dependent.
That is, there exists $\alpha_0, \alpha_1, \ldots, \alpha_{n^2} \in K$ not all zero such that: 
:$\ds \sum_{i \mathop = 0}^{n^2} \alpha_i A^i = 0$
That is, the polynomial: 
:$\ds \sum_{i \mathop = 0}^{n^2} \alpha_i X^i \in K \sqbrk X$
has $\map P A = 0$, and degree at most $n^2$. 
Let: 
:$S = \set {P \in K \sqbrk X \setminus \set 0 \mid \map P A = 0}$ 
$S$ is certainly non-empty since we have found such an element in the computation above. 
Now consider the set: 
:$D = \set {\deg P \mid P \in S}$
Since $D$ is a subset of the natural numbers, it contains a least element $N$ by the Well-Ordering Principle.
Since the polynomial we constructed has degree at most $n^2$, we have $N \le n^2$.
Let $Q \in S$ be of degree $N$.
Let $a_N$ be the coefficient of the $X^N$ term in $Q$. 
Then $\mu = \dfrac 1 {a_N} Q$ is a monic polynomial of minimum degree with $\map \mu A = 0$. 
So $\mu$ is a minimal polynomial for $A$. 
{{qed}}
Category:Linear Algebra
Category:Minimal Polynomials
qq47wak54iefnhx6y5n80jyg8r36sv5
Theorem: Homeomorphic Topologies on Same Set may not be Identical

Let $S$ be a set.
Let $\tau_1$ and $\tau_2$ both be topologies on $S$ such that the topological spaces $\struct {S, \tau_1}$ and $\struct {S, \tau_2}$ are homeomorphic.
Then it is not necessarily the case that $\struct {S, \tau_1} = \struct {S, \tau_2}$.

Proof:
Let $p, q \in S$ such that $p \ne q$.
Let $\tau_p$ and $\tau_q$ be the particular point topologies on $S$ by $p$ and $q$ respectively.
From Homeomorphic Non-Comparable Particular Point Topologies, $\struct {S, \tau_p}$ and $\struct {S, \tau_q}$ are homeomorphic.
But $\struct {S, \tau_p} \ne \struct {S, \tau_q}$, as $\set p \in \tau_p$ but $\set p \notin \tau_q$, and similarly $\set q \in \tau_q$ but $\set q \notin \tau_p$.
{{Qed}}
Theorem: Topologies on Set with More than One Element may not be Homeomorphic

Let $S$ be a set which contains at least $2$ elements.
Let $\tau_1$ and $\tau_2$ be topologies on $S$.
Then it is not necessarily the case that $\struct {S, \tau_1}$ and $\struct {S, \tau_2}$ are homeomorphic.

Proof:
Let $\tau_1$ be the indiscrete topology on $S$.
Let $\tau_2$ be the discrete topology on $S$.
Then $\struct {S, \tau_1}$ has $2$ elements: $S$ and $\O$.
Let $a, b \in S$ such that $a \ne b$.
Then $\set a \in \tau_2$ and $\set b \in \tau 2$, as well as $S$ and $\O$.
So there cannot be a bijection between $\struct {S, \tau_1}$ and $\struct {S, \tau_2}$.
{{qed}}
Theorem: Clopen Sets in Indiscrete Topology

The only subsets of $S$ which are both closed and open in $T$ are $S$ and $\O$.

Proof:
By definition of indiscrete topological space, the only open sets in $\struct {S, \tau}$ are $S$ and $\O$.
From Open and Closed Sets in Topological Space, both $S$ and $\O$ are both closed and open in $\struct {S, \tau}$ are $S$ and $\O$. 
Hence the result.
{{qed}}
Theorem: Equivalence of Definitions of Connected Topological Space/No Separation iff No Clopen Sets

{{TFAE|def = Connected Topological Space}}
Let $T = \struct {S, \tau}$ be a topological space.

Proof:
=== Definition by No Clopen Sets implies Definition by Separation ===
Let $T$ be connected by having no clopen sets.
{{AimForCont}} $T$ admits a separation, $A \mid B$ say.
Then both $A$ and $B$ are clopen sets of $T$, neither of which is either $S$ or $\O$.
From this contradiction it follows that $T$ can admit no separation
{{qed|lemma}}
=== Definition by Separation implies Definition by No Clopen Sets ===
Let $T$ be connected by admitting no separation.
Suppose $\exists H \subseteq S$ which is clopen.
Then $\relcomp S H$ is also clopen.
Hence $H \mid \relcomp S H$ is a separation of $T$.
From this contradiction it follows that $T$ can have no non-empty proper subsets which are clopen.
Theorem: Dependent Subset of Independent Set Union Singleton Contains Singleton

Let $M = \struct {S, \mathscr I}$ be a matroid.
Let $X$ be an independent subset of $M$.
Let $x \in S$.
Let $C$ be a dependent subset of $M$ such that:
:$C \subseteq X \cup \set x$.
Then:
:$x \in C$

Proof:
From the contrapositive statement of Superset of Dependent Set is Dependent:
:$C \nsubseteq X$
From the contrapositive statement of Set Difference with Superset is Empty Set:
:$C \setminus X \ne \O$
From Set Difference over Subset:
:$C \setminus X \subseteq \paren {X \cup \set x} \setminus X = \set x$
From Power Set of Singleton:
:$C \setminus X = \set x$
From Set Difference is Subset:
:$\set x \subseteq C$
From Singleton of Element is Subset:
:$x \in C$
{{qed}}
Category:Matroid Dependent Subsets
Category:Matroid Independent Subsets
f7aqf9pstmv5k0cfxpw20h7fne539tm
Theorem: Matroid Unique Circuit Property/Corollary

Let $B$ be a base of $M$.
Let $x \in S \setminus B$.
Then there exists a unique circuit $C$ such that:
:$x \in C \subseteq B \cup \set x$
That is, $C$ is the fundamental circuit of $x$ in $B$.

Proof:
From Union of Matroid Base with Element of Complement is Dependent:
:$B \cup \set x$ is dependent.
From Matroid Unique Circuit Property there exists a unique circuit $C$ such that:
:$x \in C \subseteq B \cup \set x$
{{qed}}
Theorem: Matroid Base Substitution From Fundamental Circuit

Let $M = \struct {S, \mathscr I}$ be a matroid.
Let $B$ be a base of $M$.
Let $y \in S \setminus B$.
Let $\map C {y,B}$ denote the fundamental circuit of $y$ in $B$.
Let $x \in B$.
Then:
:$\paren{B \setminus \set x} \cup \set y$ is a base of $M$ {{iff}} $x \in \map C {y,B}$
That is, $y$ can be substituted for $x$ in $B$ to form another base of $M$ {{iff}} $x \in \map C {y,B}$.

Proof:
=== Necessary Condition ===
Let $\paren{B \setminus \set x} \cup \set y$ be a base of $M$.
By definition of the fundamental circuit:
:$\map C {y,B} \subseteq B \cup \set y$
and
:$\map C {y,B}$ is dependent
{{AimForCont}} $x \notin \map C {y,B}$.
Then:
:$\map C {y,B} \subseteq \paren{B \setminus \set x} \cup \set y$
By matroid axiom $( \text I 2)$:
:$\map C {y,B}$ is independent
This contradicts the fact that:
:$\map C {y,B}$ is dependent
It follows that:
:$x \in \map C {y,B}$ 
{{qed|lemma}}
Theorem: Socrates is Mortal/Variant

:$(1): \quad$ ''If {{AuthorRef|Socrates}} is a man then {{AuthorRef|Socrates}} is mortal.''
:$(2): \quad$ ''{{AuthorRef|Socrates}} is a man.''
:$(3): \quad$ ''Therefore {{AuthorRef|Socrates}} is mortal.''

Proof:
Let $P$ denote the simple statement ''{{AuthorRef|Socrates}} is a man.''.
Let $Q$ denote the simple statement ''{{AuthorRef|Socrates}} is mortal.''.
The argument can then be expressed as:
{{begin-eqn}}
{{eqn | n = 1
      | l = P
      | o = \implies
      | r = Q
      | c = 
}}
{{eqn | n = 2
      | l = P
      | o = 
      | c = 
}}
{{eqn | n = 3
      | ll= \therefore
      | l = Q
      | o = 
      | c = Modus Ponendo Ponens
}}
{{end-eqn}}
That is: 
:''{{AuthorRef|Socrates}} is mortal.''
{{qed}}
Theorem: Self-Distributive Law for Conditional/Formulation 2/Forward Implication

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

Proof:
{{BeginTableau|\paren {p \implies \paren {q \implies r} } \implies \paren {\paren {p \implies q} \implies \paren {p \implies r} } }}
{{Assumption  |1|p \implies \paren {q \implies r} }}
{{SequentIntro|2|1|\paren {p \implies q} \implies \paren {p \implies r}|1|Self-Distributive Law for Conditional: Formulation 1}}
{{Implication |3||\paren {p \implies \paren {q \implies r} } \implies \paren {\paren {p \implies q} \implies \paren {p \implies r} }|1|2}}
{{EndTableau}}
{{Qed}}
Theorem: Self-Distributive Law for Conditional/Formulation 2/Forward Implication

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

Proof:
{{BeginTableau|\paren {p \implies \paren {q \implies r} } \implies \paren {\paren {p \implies q} \implies \paren {p \implies r} } }}
{{Assumption  |1|p \implies \paren {q \implies r} }}
{{Assumption  |2|p \implies q}}
{{Assumption  |3|p}}
{{ModusPonens |4|1,3|q \implies r|1|3}}
{{ModusPonens |5|2,3|q|2|3}}
{{ModusPonens |6|1,2,3|r|4|5}}
{{Implication |7|1,2|p \implies r|3|6}}
{{Implication |8|1|\paren {p \implies q} \implies \paren {p \implies r}|2|7}}
{{Implication |9||\paren {p \implies \paren {q \implies r} } \implies \paren {\paren {p \implies q} \implies \paren {p \implies r} }|1|8}}
{{EndTableau}}
{{Qed}}
Theorem: Self-Distributive Law for Conditional/Formulation 2/Forward Implication

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

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth value under the main connective is true for all boolean interpretations.
:<nowiki>$\begin{array}{|ccccc|c|ccccccc|}
\hline
(p & \implies & (q & \implies & r)) & \implies & ((p & \implies & q) & \implies & (p & \implies & r)) \\
\hline
\F & \T & \F & \T & \F & \T & \F & \T & \F & \T & \F & \T & \F \\
\F & \T & \F & \T & \T & \T & \F & \T & \F & \T & \F & \T & \T \\
\F & \T & \T & \F & \F & \T & \F & \T & \T & \T & \F & \T & \F \\
\F & \T & \T & \T & \T & \T & \F & \T & \T & \T & \F & \T & \T \\
\T & \T & \F & \T & \F & \T & \T & \F & \F & \T & \T & \F & \F \\
\T & \T & \F & \T & \T & \T & \T & \F & \F & \T & \T & \T & \T \\
\T & \F & \T & \F & \F & \T & \T & \T & \T & \F & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
Theorem: Self-Distributive Law for Conditional/Formulation 2/Reverse Implication

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

Proof:
{{BeginTableau |\vdash \paren {\paren {p \implies q} \implies \paren {p \implies r} } \implies \paren {p \implies \paren {q \implies r} } }}
{{Assumption   |1|\paren {p \implies q} \implies \paren {p \implies r} }}
{{SequentIntro |2|1|p \implies \paren {q \implies r}|1|Self-Distributive Law for Conditional: Formulation 1}}
{{Implication  |3||\paren {\paren {p \implies q} \implies \paren {p \implies r} } \implies \paren {p \implies \paren {q \implies r} }|1|2}}
{{EndTableau}}
{{Qed}}
Theorem: Self-Distributive Law for Conditional/Formulation 2/Reverse Implication

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

Proof:
{{BeginTableau |\vdash \paren {\paren {p \implies q} \implies \paren {p \implies r} } \implies \paren {p \implies \paren {q \implies r} } }}
{{Assumption|1|\paren {p \implies q} \implies \paren {p \implies r} }}
{{Assumption|2|p}}
{{Assumption|3|q}}
{{SequentIntro|4|3|p \implies q|3|True Statement is implied by Every Statement}}
{{ModusPonens|5|1, 3|p \implies r|1|4}}
{{ModusPonens|6|1, 2, 3|r|5|2}}
{{Implication|7|1, 2|q \implies r|3|6}}
{{Implication|8|1|p \implies \paren {q \implies r}|2|7}}
{{Implication|9||\paren {\paren {p \implies q} \implies \paren {p \implies r} } \implies \paren {p \implies \paren {q \implies r} }|1|8}}
{{EndTableau|qed}}
Theorem: Odd Integers under Addition do not form Group

Let $S$ be the set of odd integers:
:$S = \set {x \in \Z: \exists n \in \Z: x = 2 n + 1}$
Let $\struct {S, +}$ denote the algebraic structure formed by $S$ under the operation of addition.
Then $\struct {S, +}$ is not a group.

Proof:
It is to be demonstrated that $\struct {S, +}$ does not satisfy the group axioms.
Let $a$ and $b$ be odd integers.
Then  $a = 2 n + 1$ and $b = 2 m + 1$ for some $m, n \in \Z$.
Then:
{{begin-eqn}}
{{eqn | l = a + b
      | r = 2 n + 1 + 2 m + 1
      | c = 
}}
{{eqn | r = 2 \paren {n + m + 1}
      | c = 
}}
{{end-eqn}}
and it is seen that $a + b$ is even.
That is:
:$a + b \notin S$
Thus $\struct {S, +}$ does not fulfil {{Group-axiom|0}}.
Hence the result.
{{qed}}