avewright/proofwiki-math huggingface dataset:
Theorem: De Morgan's Laws (Set Theory)/Proof by Induction/Difference with Intersection/Proof

Let $\mathbb T = \set {T_i: i \mathop \in I}$, where each $T_i$ is a set and $I$ is some finite indexing set.
Then:
:$\ds S \setminus \bigcap_{i \mathop \in I} T_i = \bigcup_{i \mathop \in I} \paren {S \setminus T_i}$

Proof:
Let the cardinality $\card I$ of the indexing set $I$ be $n$.
Then by the definition of cardinality, it follows that $I \cong \N^*_n$ and we can express the proposition:
:$\ds S \setminus \bigcap_{i \mathop \in I} T_i = \bigcup_{i \mathop \in I} \paren {S \setminus T_i}$
as:
:$\ds S \setminus \bigcap_{i \mathop = 1}^n T_i = \bigcup_{i \mathop = 1}^n \paren {S \setminus T_i}$
The proof of this is more amenable to proof by Principle of Mathematical Induction.
For all $n \in \N_{>0}$, let $\map P n$ be the proposition:
:$\ds S \setminus \bigcap_{i \mathop = 1}^n T_i = \bigcup_{i \mathop = 1}^n \paren {S \setminus T_i}$
$\map P 1$ is true, as this just says $S \setminus T_1 = S \setminus T_1$.
=== Base Case ===
$\map P 2$ is the case:
:$S \setminus \paren {T_1 \cap T_2} = \paren {S \setminus T_1} \cup \paren {S \setminus T_2}$
which has been proved. 
This is our basis for the induction.
=== Induction Hypothesis ===
Now we need to show that, if $\map P k$ is true, where $k \ge 2$, then it logically follows that $\map P {k + 1}$ is true.
So this is our induction hypothesis:
:$\ds S \setminus \bigcap_{i \mathop = 1}^k T_i = \bigcup_{i \mathop = 1}^k \paren {S \setminus T_i}$
=== Induction Step ===
Now we need to show:
:$\ds S \setminus \bigcap_{i \mathop = 1}^{k + 1} T_i = \bigcup_{i \mathop = 1}^{k + 1} \paren {S \setminus T_i}$
This is our induction step:
{{begin-eqn}}
{{eqn | l = S \setminus \bigcap_{i \mathop = 1}^{k + 1} T_i
      | r = S \setminus \paren {\bigcap_{i \mathop = 1}^k T_i \cap T_{k + 1} }
      | c = Intersection is Associative
}}
{{eqn | r = \paren {S \setminus \bigcap_{i \mathop = 1}^k T_i} \cup \paren {S \setminus T_{k + 1} }
      | c = Base case
}}
{{eqn | r = \paren {\bigcup_{i \mathop = 1}^k \paren {S \setminus T_i} } \cup \paren {S \setminus T_{k + 1} }
      | c = Induction hypothesis
}}
{{eqn | r = \bigcup_{i \mathop = 1}^{k + 1} \paren {S \setminus T_i}
      | c = Union is Associative
}}
{{end-eqn}}
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\ds S \setminus \bigcap_{i \mathop = 1}^n T_i = \bigcup_{i \mathop = 1}^n \paren {S \setminus T_i}$
that is:
:$\ds S \setminus \bigcap_{i \mathop \in I} T_i = \bigcup_{i \mathop \in I} \paren {S \setminus T_i}$
{{qed}}
Theorem: De Morgan's Laws (Set Theory)/Proof by Induction/Difference with Intersection

:$\ds S \setminus \bigcap_{i \mathop \in I} T_i = \bigcup_{i \mathop \in I} \paren {S \setminus T_i}$

Proof:
Let the cardinality $\card I$ of the indexing set $I$ be $n$.
Then by the definition of cardinality, it follows that $I \cong \N^*_n$ and we can express the proposition:
:$\ds S \setminus \bigcap_{i \mathop \in I} T_i = \bigcup_{i \mathop \in I} \paren {S \setminus T_i}$
as:
:$\ds S \setminus \bigcap_{i \mathop = 1}^n T_i = \bigcup_{i \mathop = 1}^n \paren {S \setminus T_i}$
The proof of this is more amenable to proof by Principle of Mathematical Induction.
For all $n \in \N_{>0}$, let $\map P n$ be the proposition:
:$\ds S \setminus \bigcap_{i \mathop = 1}^n T_i = \bigcup_{i \mathop = 1}^n \paren {S \setminus T_i}$
$\map P 1$ is true, as this just says $S \setminus T_1 = S \setminus T_1$.
=== Base Case ===
$\map P 2$ is the case:
:$S \setminus \paren {T_1 \cap T_2} = \paren {S \setminus T_1} \cup \paren {S \setminus T_2}$
which has been proved. 
This is our basis for the induction.
=== Induction Hypothesis ===
Now we need to show that, if $\map P k$ is true, where $k \ge 2$, then it logically follows that $\map P {k + 1}$ is true.
So this is our induction hypothesis:
:$\ds S \setminus \bigcap_{i \mathop = 1}^k T_i = \bigcup_{i \mathop = 1}^k \paren {S \setminus T_i}$
=== Induction Step ===
Now we need to show:
:$\ds S \setminus \bigcap_{i \mathop = 1}^{k + 1} T_i = \bigcup_{i \mathop = 1}^{k + 1} \paren {S \setminus T_i}$
This is our induction step:
{{begin-eqn}}
{{eqn | l = S \setminus \bigcap_{i \mathop = 1}^{k + 1} T_i
      | r = S \setminus \paren {\bigcap_{i \mathop = 1}^k T_i \cap T_{k + 1} }
      | c = Intersection is Associative
}}
{{eqn | r = \paren {S \setminus \bigcap_{i \mathop = 1}^k T_i} \cup \paren {S \setminus T_{k + 1} }
      | c = Base case
}}
{{eqn | r = \paren {\bigcup_{i \mathop = 1}^k \paren {S \setminus T_i} } \cup \paren {S \setminus T_{k + 1} }
      | c = Induction hypothesis
}}
{{eqn | r = \bigcup_{i \mathop = 1}^{k + 1} \paren {S \setminus T_i}
      | c = Union is Associative
}}
{{end-eqn}}
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\ds S \setminus \bigcap_{i \mathop = 1}^n T_i = \bigcup_{i \mathop = 1}^n \paren {S \setminus T_i}$
that is:
:$\ds S \setminus \bigcap_{i \mathop \in I} T_i = \bigcup_{i \mathop \in I} \paren {S \setminus T_i}$
{{qed}}
Theorem: De Morgan's Laws (Set Theory)/Proof by Induction/Difference with Union/Proof

Let $\mathbb T = \set {T_i: i \mathop \in I}$, where each $T_i$ is a set and $I$ is some finite indexing set.
Then:
:$\ds S \setminus \bigcup_{i \mathop \in I} T_i = \bigcap_{i \mathop \in I} \paren {S \setminus T_i}$

Proof:
Let the cardinality $\size I$ of the indexing set $I$ be $n$.
Then by the definition of cardinality, it follows that $I \cong \N^*_n$ and we can express the proposition:
:$\ds S \setminus \bigcup_{i \mathop \in I} T_i = \bigcap_{i \mathop \in I} \paren {S \setminus T_i}$
as:
:$\ds S \setminus \bigcup_{i \mathop = 1}^n T_i = \bigcap_{i \mathop = 1}^n \paren {S \setminus T_i}$
The proof of this is more amenable to proof by Principle of Mathematical Induction.
For all $n \in \N_{>0}$, let $\map P n$ be the proposition:
:$\ds S \setminus \bigcup_{i \mathop = 1}^n T_i = \bigcap_{i \mathop = 1}^n \paren {S \setminus T_i}$.
$\map P 1$ is true, as this just says $S \setminus T_1 = S \setminus T_1$.
=== Base Case ===
$\map P 2$ is the case:
:$S \setminus \paren {T_1 \cup T_2} = \paren {S \setminus T_1} \cap \paren {S \setminus T_2}$
which has been proved.
This is our basis for the induction.
=== Induction Hypothesis ===
Now we need to show that, if $\map P k$ is true, where $k \ge 2$, then it logically follows that $\map P {k + 1}$ is true.
So this is our induction hypothesis:
:$\ds S \setminus \bigcup_{i \mathop = 1}^k T_i = \bigcap_{i \mathop = 1}^k \paren {S \setminus T_i}$
=== Induction Step ===
Now we need to show:
:$\ds S \setminus \bigcup_{i \mathop = 1}^{k + 1} T_i = \bigcap_{i \mathop = 1}^{k + 1} \paren {S \setminus T_i}$
This is our induction step:
{{begin-eqn}}
{{eqn | l = S \setminus \bigcup_{i \mathop = 1}^{k + 1} T_i
      | r = S \setminus \paren {\bigcup_{i \mathop = 1}^k T_i \cup T_{k + 1} }
      | c = Union is Associative
}}
{{eqn | r = \paren {S \setminus \bigcup_{i \mathop = 1}^k T_i} \cap \paren {S \setminus T_{k + 1} }
      | c = Base case
}}
{{eqn | r = \paren {\bigcap_{i \mathop = 1}^k \paren {S \setminus T_i} } \cap \paren {S \setminus T_{k + 1} }
      | c = Induction hypothesis
}}
{{eqn | r = \bigcap_{i \mathop = 1}^{k + 1} \paren {S \setminus T_i}
      | c = Intersection is Associative
}}
{{end-eqn}}
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\ds S \setminus \bigcup_{i \mathop = 1}^n T_i = \bigcap_{i \mathop = 1}^n \paren {S \setminus T_i}$
that is:
:$\ds S \setminus \bigcup_{i \mathop \in I} T_i = \bigcap_{i \mathop \in I} \paren {S \setminus T_i}$
{{qed}}
Theorem: De Morgan's Laws (Set Theory)/Proof by Induction/Difference with Union

:$\ds S \setminus \bigcup_{i \mathop \in I} T_i = \bigcap_{i \mathop \in I} \paren {S \setminus T_i}$

Proof:
Let the cardinality $\size I$ of the indexing set $I$ be $n$.
Then by the definition of cardinality, it follows that $I \cong \N^*_n$ and we can express the proposition:
:$\ds S \setminus \bigcup_{i \mathop \in I} T_i = \bigcap_{i \mathop \in I} \paren {S \setminus T_i}$
as:
:$\ds S \setminus \bigcup_{i \mathop = 1}^n T_i = \bigcap_{i \mathop = 1}^n \paren {S \setminus T_i}$
The proof of this is more amenable to proof by Principle of Mathematical Induction.
For all $n \in \N_{>0}$, let $\map P n$ be the proposition:
:$\ds S \setminus \bigcup_{i \mathop = 1}^n T_i = \bigcap_{i \mathop = 1}^n \paren {S \setminus T_i}$.
$\map P 1$ is true, as this just says $S \setminus T_1 = S \setminus T_1$.
=== Base Case ===
$\map P 2$ is the case:
:$S \setminus \paren {T_1 \cup T_2} = \paren {S \setminus T_1} \cap \paren {S \setminus T_2}$
which has been proved.
This is our basis for the induction.
=== Induction Hypothesis ===
Now we need to show that, if $\map P k$ is true, where $k \ge 2$, then it logically follows that $\map P {k + 1}$ is true.
So this is our induction hypothesis:
:$\ds S \setminus \bigcup_{i \mathop = 1}^k T_i = \bigcap_{i \mathop = 1}^k \paren {S \setminus T_i}$
=== Induction Step ===
Now we need to show:
:$\ds S \setminus \bigcup_{i \mathop = 1}^{k + 1} T_i = \bigcap_{i \mathop = 1}^{k + 1} \paren {S \setminus T_i}$
This is our induction step:
{{begin-eqn}}
{{eqn | l = S \setminus \bigcup_{i \mathop = 1}^{k + 1} T_i
      | r = S \setminus \paren {\bigcup_{i \mathop = 1}^k T_i \cup T_{k + 1} }
      | c = Union is Associative
}}
{{eqn | r = \paren {S \setminus \bigcup_{i \mathop = 1}^k T_i} \cap \paren {S \setminus T_{k + 1} }
      | c = Base case
}}
{{eqn | r = \paren {\bigcap_{i \mathop = 1}^k \paren {S \setminus T_i} } \cap \paren {S \setminus T_{k + 1} }
      | c = Induction hypothesis
}}
{{eqn | r = \bigcap_{i \mathop = 1}^{k + 1} \paren {S \setminus T_i}
      | c = Intersection is Associative
}}
{{end-eqn}}
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\ds S \setminus \bigcup_{i \mathop = 1}^n T_i = \bigcap_{i \mathop = 1}^n \paren {S \setminus T_i}$
that is:
:$\ds S \setminus \bigcup_{i \mathop \in I} T_i = \bigcap_{i \mathop \in I} \paren {S \setminus T_i}$
{{qed}}
Theorem: De Morgan's Laws (Set Theory)/Set Difference/General Case/Difference with Intersection

:$\ds S \setminus \bigcap \mathbb T = \bigcup_{T' \mathop \in \mathbb T} \paren {S \setminus T'}$
where:
:$\ds \bigcap \mathbb T := \set {x: \forall T' \in \mathbb T: x \in T'}$
that is, the intersection of $\mathbb T$

Proof:
Suppose:
:$\ds x \in S \setminus \bigcap \mathbb T$
Note that by Set Difference is Subset we have that $x \in S$ (we need this later).
Then:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = S \setminus \bigcap \mathbb T
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \notin
      | r = \bigcap \mathbb T
      | c = {{Defof|Set Difference}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \neg \leftparen {\forall T' \in \mathbb T}
      | l = x
      | o = \in
      | r = \rightparen {T'}
      | c = {{Defof|Intersection of Set of Sets}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists T' \in \mathbb T
      | l = x
      | o = \notin
      | r = T'
      | c = Denial of Universality
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists T' \in \mathbb T
      | l = x
      | o = \in
      | r = S \setminus T'
      | c = {{Defof|Set Difference}}: note $x \in S$ from above
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = \bigcup_{T' \mathop \in \mathbb T} \paren {S \setminus T'}
      | c = {{Defof|Union of Set of Sets}}
}}
{{end-eqn}}
Therefore:
:$\ds S \setminus \bigcap \mathbb T = \bigcup_{T' \mathop \in \mathbb T} \paren {S \setminus T'}$
{{qed}}
Theorem: De Morgan's Laws (Set Theory)/Set Difference/General Case/Difference with Union

:$\ds S \setminus \bigcup \mathbb T = \bigcap_{T' \mathop \in \mathbb T} \paren {S \setminus T'}$
where:
:$\ds \bigcup \mathbb T := \set {x: \exists T' \in \mathbb T: x \in T'}$
that is, the union of $\mathbb T$.

Proof:
Suppose:
:$\ds x \in S \setminus \bigcup \mathbb T$
Note that by Set Difference is Subset we have that $x \in S$ (we need this later).
Then:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = S \setminus \bigcup \mathbb T
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \notin
      | r = \bigcup \mathbb T
      | c = {{Defof|Set Difference}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \nexists T' \in \mathbb T
      | l = x
      | o = \in
      | r = T'
      | c = {{Defof|Union of Set of Sets}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall T' \in \mathbb T
      | l = x
      | o = \notin
      | r = T'
      | c = Denial of Existence
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall T' \in \mathbb T
      | l = x
      | o = \in
      | r = S \setminus T'
      | c = {{Defof|Set Difference}}: note $x \in S$ from above
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = \bigcap_{T' \mathop \in \mathbb T} \paren {S \setminus T'}
      | c = {{Defof|Intersection of Set of Sets}}
}}
{{end-eqn}}
Therefore:
:$\ds S \setminus \bigcup \mathbb T = \bigcap_{T' \mathop \in \mathbb T} \paren {S \setminus T'}$
{{qed}}
Theorem: De Morgan's Laws (Set Theory)/Set Difference/Difference with Intersection

:$S \setminus \paren {T_1 \cap T_2} = \paren {S \setminus T_1} \cup \paren {S \setminus T_2}$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = x \in S \setminus \paren {T_1 \cap T_2}
}}
{{eqn | o = \leadstoandfrom
      | r = \paren {x \in S} \land \paren {x \notin \paren {T_1 \cap T_2} }
      | c = {{Defof|Set Difference}}
}}
{{eqn | o = \leadstoandfrom
      | r = \paren {x \in S} \land \paren {\neg \paren {x \in T_1 \land x \in T_2} }
      | c = {{Defof|Set Intersection}}
}}
{{eqn | o = \leadstoandfrom
      | r = \paren {x \in S} \land \paren {x \notin T_1 \lor x \notin T_2}
      | c = De Morgan's Laws: Disjunction of Negations
}}
{{eqn | o = \leadstoandfrom
      | r = \paren {x \in S \land x \notin T_1}) \lor \paren {x \in S \land x \notin T_2}
      | c = Rule of Distribution
}}
{{eqn | o = \leadstoandfrom
      | r = x \in \paren {S \setminus T_1} \cup \paren {S \setminus T_2}
      | c = {{Defof|Set Union}} and {{Defof|Set Difference}}
}}
{{end-eqn}}
By definition of set equality:
: $S \setminus \paren {T_1 \cap T_2} = \paren {S \setminus T_1} \cup \paren {S \setminus T_2}$
{{qed}}
{{Namedfor|Augustus De Morgan}}
Theorem: De Morgan's Laws (Set Theory)/Set Difference/Difference with Union

:$S \setminus \paren {T_1 \cup T_2} = \paren {S \setminus T_1} \cap \paren {S \setminus T_2}$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = x \in S \setminus \paren {T_1 \cup T_2}
}}
{{eqn | o = \leadstoandfrom
      | r = \paren {x \in S} \land \paren {x \notin \paren {T_1 \cup T_2} }
      | c = {{Defof|Set Difference}}
}}
{{eqn | o = \leadstoandfrom
      | r = \paren {x \in S} \land \paren {\neg \paren {x \in T_1 \lor x \in T_2} }
      | c = {{Defof|Set Union}}
}}
{{eqn | o = \leadstoandfrom
      | r = \paren {x \in S} \land \paren {x \notin T_1 \land x \notin T_2}
      | c = De Morgan's Laws: Conjunction of Negations
}}
{{eqn | o = \leadstoandfrom
      | r = \paren {x \in S \land x \notin T_1} \land \paren {x \in S \land x \notin T_2}
      | c = Rules of Idempotence, Commutation and Association
}}
{{eqn | o = \leadstoandfrom
      | r = x \in \paren {S \setminus T_1} \cap \paren {S \setminus T_2}
      | c = {{Defof|Set Intersection}} and {{Defof|Set Difference}}
}}
{{end-eqn}}
By definition of set equality:
:$S \setminus \paren {T_1 \cup T_2} = \paren {S \setminus T_1} \cap \paren {S \setminus T_2}$
{{qed}}
{{Namedfor|Augustus De Morgan}}
Theorem: Isomorphism between Ring of Integers Modulo 2 and Parity Ring

The ring of integers modulo $2$ and the parity ring are isomorphic.

Proof:
To simplify the notation, let the elements of $\Z_2$ be identified as $0$ for $\eqclass 0 2$ and $1$ for $\eqclass 1 2$.
Let $f$ be the mapping from the parity ring $R := \struct {\set {\text{even}, \text{odd} }, +, \times}$ and the ring of integers modulo $2$ $\struct {\Z_2, +_2, \times_2}$:
:$f: \struct {\set {\text{even}, \text{odd} }, +, \times} \to \struct {\Z_2, +_2, \times_2}$:
::$\forall x \in R: \map f x = \begin{cases}
0 & : x = \text{even} \\
1 & : x = \text{odd}  \end{cases}$
The bijective nature of $f$ is apparent:
:$f^{-1}: \struct {\Z_2, +_2, \times_2} \to \struct {\set {\text{even}, \text{odd} }, +, \times}$:
::$\forall x \in \Z_2: \map {f^{-1} } x = \begin{cases}
\text{even} & : x = 0 \\
\text{odd}  & : x = 1 \end{cases}$
Thus the following equations can be checked:
{{begin-eqn}}
{{eqn | ll= 0 +_2 0 =
      | l = \map f {\text{even} } +_2 \map f {\text{even} }
      | r = \map f {\text{even} + \text{even} }
      | rr= = 0
}}
{{eqn | ll= 0 +_2 1 =
      | l = \map f {\text{even} } +_2 \map f {\text{odd} }
      | r = \map f {\text{even} + \text{odd} }
      | rr= = 1
}}
{{eqn | ll= 1 +_2 0 =
      | l = \map f {\text{odd} } +_2 \map f {\text{even} }
      | r = \map f {\text{odd} + \text{even} }
      | rr= = 1
}}
{{eqn | ll= 1 +_2 1 =
      | l = \map f {\text{odd} } +_2 \map f {\text{odd} }
      | r = \map f {\text{odd} + \text{odd} }
      | rr= = 0
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | ll= 0 \times_2 0 =
      | l = \map f {\text{even} } \times_2 \map f {\text{even} }
      | r = \map f {\text{even} \times \text{even} }
      | rr= = 0
}}
{{eqn | ll= 0 \times_2 1 =
      | l = \map f {\text{even} } \times_2 \map f {\text{odd} }
      | r = \map f {\text{even} \times \text{odd} }
      | rr= = 0
}}
{{eqn | ll= 1 \times_2 0 =
      | l = \map f {\text{odd} } \times_2 \map f {\text{even} }
      | r = \map f {\text{odd} \times \text{even} }
      | rr= = 0
}}
{{eqn | ll= 1 \times_2 1 =
      | l = \map f {\text{odd} } \times_2 \map f {\text{odd} }
      | r = \map f {\text{odd} \times \text{odd} }
      | rr= = 1
}}
{{end-eqn}}
{{qed}}
These results can be determined from their Cayley tables:
Theorem: Parity Addition is Associative

Let $R := \struct {\set {\text{even}, \text{odd} }, +, \times}$ be the parity ring.
The operation $+$ is associative:
:$\forall a, b, c \in R: \paren {a + b} + c = a + \paren {b + c}$

Proof:
From Isomorphism between Ring of Integers Modulo 2 and Parity Ring:
:$\struct {\set {\text {even}, \text {odd} }, +, \times}$ is isomorphic with $\struct {\Z_2, +_2, \times_2}$
the ring of integers modulo $2$.
The result follows from:
:Modulo Addition is Associative
and:
:Isomorphism Preserves Associativity.
{{qed}}
Theorem: Parity Addition is Associative

Let $R := \struct {\set {\text{even}, \text{odd} }, +, \times}$ be the parity ring.
The operation $+$ is associative:
:$\forall a, b, c \in R: \paren {a + b} + c = a + \paren {b + c}$

Proof:
Let $a, b, c \in R$.
That is, $a, b, c$ are all either $\text{even}$ or $\text{odd}$.
By definition of odd:
:$\text{odd} = 2 m + 1$
for some $m \in \Z$.
By definition of even:
:$\text{even} = 2 n + 0$
for some $n \in \Z$.
Thus we can define the mapping $f: R \to \Z$ as:
:$\forall x \in R: \map f x := \begin{cases}
0 & : x \text { is even} \\
1 & : x \text { is odd} \end{cases}$
Thus an element of $R$ can be expressed as an arbitrary integer of the form:
:$x = 2 k + \map f x$
where:
:$k \in \Z$ is an integer
:$\map f x$ is either $0$ or $1$ according to whether $x$ is even or odd.
Let $+_2$ be used to denote the operation of $+$ in $R$, that is, the addition of two parities.
Then:
{{begin-eqn}}
{{eqn | l = \paren {a +_2 b} +_2 c
      | r = \paren {2 r + \map f a + 2 s + \map f b} + 2 t + \map f c
      | c = where $r, s, t \in \Z$
}}
{{eqn | r = 2 r + \map f a + \paren {2 s + \map f b + 2 t + \map f c}
      | c = Integer Addition is Associative
}}
{{eqn | r = a +_2 \paren {b +_2 c}
      | c = {{Defof|Odd Integer}} and {{Defof|Even Integer}}
}}
{{end-eqn}}
The result follows by the identification of $+_2$ to be used to denote the operation of $+$ in $R$:
:$\paren {a + b} + c = a + \paren {b + c}$
{{qed}}
Theorem: Parity Addition is Commutative

Let $R := \struct {\set {\text{even}, \text{odd} }, +, \times}$ be the parity ring.
The operation $+$ is commutative:
:$\forall a, b \in R: a + b = b + a$

Proof:
From Isomorphism between Ring of Integers Modulo 2 and Parity Ring:
:$\struct {\set {\text{even}, \text{odd} }, +, \times}$ is isomorphic with $\struct {\Z_2, +_2, \times_2}$
the ring of integers modulo $2$.
The result follows from:
:Modulo Addition is Commutative
and:
:Isomorphism Preserves Commutativity.
{{qed}}
Theorem: Parity Addition is Commutative

Let $R := \struct {\set {\text{even}, \text{odd} }, +, \times}$ be the parity ring.
The operation $+$ is commutative:
:$\forall a, b \in R: a + b = b + a$

Proof:
Let $a, b \in R$.
That is, $a$ and $b$ are both either $\text{even}$ or $\text{odd}$.
By definition of odd:
:$\text{odd} = 2 m + 1$
for some $m \in \Z$.
By definition of even:
:$\text{even} = 2 n + 0$
for some $n \in \Z$.
Thus we can define the mapping $f: R \to \Z$ as:
:$\forall x \in R: \map f x := \begin{cases}
0 & : x \text { is even} \\
1 & : x \text { is odd} \end{cases}$
Thus an element of $R$ can be expressed as an arbitrary integer of the form:
:$x = 2 k + \map f x$
where:
:$k \in \Z$ is an integer
:$\map f x$ is either $0$ or $1$ according to whether $x$ is even or odd.
Let $+_2$ be used to denote the operation of $+$ in $R$, that is, the addition of two parities.
Then:
{{begin-eqn}}
{{eqn | l = a +_2 b
      | r = 2 r + \map f a + 2 s + \map f b
      | c = where $r, s \in \Z$
}}
{{eqn | r = 2 s + \map f b + 2 r + \map f a
      | c = Integer Addition is Commutative
}}
{{eqn | r = b +_2 a
      | c = {{Defof|Odd Integer}} and {{Defof|Even Integer}}
}}
{{end-eqn}}
The result follows by the identification of $+_2$ to be used to denote the operation of $+$ in $R$:
:$a + b = b + a$
{{qed}}
Theorem: Parity Multiplication is Associative

Let $R := \struct {\set {\text{even}, \text{odd} }, +, \times}$ be the parity ring.
The operation $\times$ is associative:
:$\forall a, b, c \in R: \paren {a \times b} \times c = a \times \paren {b \times c}$

Proof:
From Isomorphism between Ring of Integers Modulo 2 and Parity Ring:
:$\struct {\set {\text{even}, \text{odd} }, +, \times}$ is isomorphic with $\struct {\Z_2, +_2, \times_2}$
the ring of integers modulo $2$.
The result follows from:
:Modulo Multiplication is Associative
and:
:Isomorphism Preserves Associativity.
{{qed}}
Theorem: Parity Multiplication is Associative

Let $R := \struct {\set {\text{even}, \text{odd} }, +, \times}$ be the parity ring.
The operation $\times$ is associative:
:$\forall a, b, c \in R: \paren {a \times b} \times c = a \times \paren {b \times c}$

Proof:
Let $a, b, c \in R$.
That is, $a, b, c$ are all either $\text{even}$ or $\text{odd}$.
By definition of odd:
:$\text{odd} = 2 m + 1$
for some $m \in \Z$.
By definition of even:
:$\text{even} = 2 n + 0$
for some $n \in \Z$.
Thus we can define the mapping $f: R \to \Z$ as:
:$\forall x \in R: \map f x := \begin{cases}
0 & : x \text { is even} \\
1 & : x \text { is odd} \end{cases}$
Thus an element of $R$ can be expressed as an arbitrary integer of the form:
:$x = 2 k + \map f x$
where:
:$k \in \Z$ is an integer
:$\map f x$ is either $0$ or $1$ according to whether $x$ is even or odd.
Then:
{{begin-eqn}}
{{eqn | l = \paren {a \times b} \times c
      | r = \paren {\paren {2 r + \map f a} \paren {2 s + \map f b} } \paren {2 t + \map f c}
      | c = where $r, s, t \in \Z$
}}
{{eqn | r = \paren {2 r + \map f a} \paren {\paren {2 s + \map f b} \paren {2 t + \map f c} }
      | c = Integer Multiplication is Associative
}}
{{eqn | r = a \times \paren {b \times c}
      | c = {{Defof|Odd Integer}} and {{Defof|Even Integer}}
}}
{{end-eqn}}
{{qed}}
Theorem: Parity Multiplication is Commutative

Let $R := \struct {\set {\text{even}, \text{odd} }, +, \times}$ be the parity ring.
The operation $\times$ is commutative:
:$\forall a, b \in R: a \times b = b \times a$

Proof:
From Isomorphism between Ring of Integers Modulo 2 and Parity Ring:
:$\struct {\set {\text{even}, \text{odd} }, +, \times}$ is isomorphic with $\struct {\Z_2, +_2, \times_2}$
the ring of integers modulo $2$.
The result follows from:
:Modulo Multiplication is Commutative
and:
:Isomorphism Preserves Associativity.
{{qed}}