nyuuzyou/wikis huggingface dataset:
Non-Divisbility of Binomial Coefficients of n by Prime

== Theorem ==
Let $n \in \Z_{\ge 0}$ be a positive integer.
Let $p$ be a prime number.
Then:
:$\dbinom n k$ is not divisible by $p$ for any $k \in \Z_{\ge 0}$ where $0 \le k \le n$
:
:$n = a p^m - 1$ where $1 \le a < p$
for some $m \in \Z_{\ge 0}$.
== Proof ==
The statement:
:$\dbinom n k$ is not divisible by $p$
is equivalent to:
:$\dbinom n k \not \equiv 0 \pmod p$
The corollary to Lucas' Theorem gives:
:$\ds \dbinom n k \equiv \prod_{j \mathop = 0}^r \dbinom {a_j} {b_j} \pmod p$
where:
:$n, k \in \Z_{\ge 0}$ and $p$ is prime
:the representations of $n$ and $k$ to the base $p$ are given by:
::$n = a_r p^r + \cdots + a_1 p + a_0$
::$k = b_r p^r + \cdots + b_1 p + b_0$
Consider the form of $n = a p^m - 1$ when represented to the base $p$:
That is, all of the digits of $n$ are $p - 1$ except perhaps the first one.
For $k$ such that $0 \le k \le n$, the digits of $k$ will all range over $0$ to $p - 1$.
=== Necessary Condition ===
Let $n = a p^m - 1$.
Then all the binomial coefficients $\dbinom {a_j} {b_j}$ (except perhaps the first) are of the form $\dbinom {p - 1} k$ for $0 \le k < p$.
By Binomial Coefficient of Prime Minus One Modulo Prime:
:$\dbinom {p - 1} k \equiv \paren {-1}^k \pmod p$
and so:
:$\dbinom {a_j} {b_j} \equiv \paren {-1}^k \pmod p$ for $0 \le j < r$
For the first digit, we have $0 \le b_r \le a_r < p$.
We have $\dbinom {a_r} {b_r} > 0$.
Since $a_r!$ is not divisible by $p$, neither does $\dbinom {a_r} {b_r}$.
Thus:
:$\dbinom {a_r} {b_r} \not \equiv 0 \pmod p$
Hence:
:$\ds \prod_{j \mathop = 0}^r \dbinom {a_j} {b_j} \equiv \pm \dbinom {a_r} {b_r} \not \equiv 0 \pmod p$
which means $\dbinom n k$ is not divisible by $p$ for any $k \in \Z_{\ge 0}$ where $0 \le k \le n$.
=== Sufficient Condition ===
We show the contrapositive.
Suppose $n \ne a p^m - 1$.
Then one of the digits $a_j$ (that is not the first one) will be less than $p - 1$.
But the digits of all possible $k$ will range over $0$ to $p - 1$.
Therefore there must be at least one $\dbinom {a_j} {b_j}$ such that $b_j > a_j$.
Such a condition leads to $\dbinom {a_j} {b_j} = 0$.
That is:
:$\ds \prod_{j \mathop = 0}^r \dbinom {a_j} {b_j} \equiv 0 \pmod p$
which means $\dbinom n k$ is divisible by $p$ for some $k \le n$.
== Sources ==
* : $\S 1.2.6$: Binomial Coefficients: Exercise $12$
Category:Pascal's Triangle
Non-Empty Bounded Above Subset of Banach Space with Archimedean Property has Supremum

== Theorem ==
Let $\BB$ be a Banach space.
Let $\BB$ have the Archimedean property.
Let $S \subseteq \BB$ be a subset of $\BB$ which is bounded above.
Then $S$ admits a supremum.
== Proof ==
== Sources ==
* : $1$: Review of some real analysis: $\S 1.2$: Real Sequences: Theorem $1.2.10$
Category:Banach Spaces
Non-Empty Bounded Subset of Minimally Inductive Class under Progressing Mapping has Greatest Element

== Theorem ==
Let $M$ be a class which is minimally inductive under a progressing mapping $g$.
Then every non-empty bounded subset of $M$ has a greatest element.
== Proof 1 ==
== Proof 2 ==
Category:Bounded Classes
Category:Progressing Mappings
Category:Minimally Inductive Classes
Category:Non-Empty Bounded Subset of Minimally Inductive Class under Progressing Mapping has Greatest Element
Non-Empty Bounded Subset of Minimally Inductive Class under Progressing Mapping has Greatest Element/Proof 1

== Theorem ==
== Proof ==
Let the hypothesis be assumed.
The proof proceeds by general induction.
For all $x \in M$, let $\map P x$ be the proposition:
:Every non-empty subset of $M$ which is bounded by $x$ has a greatest element.
=== Basis for the Induction ===
Let $x = \O$.
The only non-empty subset of $M$ which is bounded by $\O$ is $\set \O$.
Then it is seen that $\set \O$ has a greatest element, that is $\O$.
Thus $\map P \O$ is seen to hold.
This is the basis for the induction.
=== Induction Hypothesis ===
Now it needs to be shown that if $\map P x$ is true, where $x \in M$, then it logically follows that $\map P {\map g x}$ is true.
So this is the induction hypothesis:
:Every non-empty subset of $M$ which is bounded by $x$ has a greatest element.
from which it is to be shown that:
:Every non-empty subset of $M$ which is bounded by $\map g x$ has a greatest element.
=== Induction Step ===
This is the induction step:
Let the induction hypothesis be assumed.
Let $B$ be a non-empty subset of $M$ which is bounded by $\map g x$.
Thus, by definition, every element of $B$ is a subset of $\map g x$.
It is to be shown that $B$ has a greatest element $m$.
That is, that $m \in B$ and every element of $B$ is a subset of $m$
Let $\map g x \in B$.
By definition of subset bounded by $\map g x$, every element of $B$ is a subset of $\map g x$.
That is, $\map g x$ is itself the greatest element of $B$.
Suppose that $\map g x \notin B$.
Then every element of $B$ is a proper subset of $\map g x$.
Let $y \in B$ be arbitrary.
Because $y$ is a proper subset of $\map g x$, there exists $z \in \map g x$ such that $z \notin y$.
Thus $\map g x$ is not a subset of $y$.
From Minimally Inductive Class under Progressing Mapping induces Nest:
:$\forall x, y \in M: \map g x \subseteq y \lor y \subseteq x$
Because it is not the case that $\map g x \subseteq y$, it must be that:
:$y \subseteq x$
Thus, as $y$ is arbitrary, it follows that every element of $B$ is a proper subset of $x$.
Thus $B$ is bounded by $x$.
It follows by the induction hypothesis that $B$ has a greatest element.
So $\map P x \implies \map P {\map g x}$ and the result follows by the Principle of General Induction.
Therefore:
:For all $x \in M$, every non-empty subset of $M$ which is bounded by $x$ has a greatest element.
That is:
:Every non-empty bounded subset of $M$ has a greatest element.
== Sources ==
* : Chapter $3$: The Natural Numbers: $\S 4$ A double induction principle and its applications: Theorem $4.12$
Category:Non-Empty Bounded Subset of Minimally Inductive Class under Progressing Mapping has Greatest Element
Non-Empty Bounded Subset of Minimally Inductive Class under Progressing Mapping has Greatest Element/Proof 2

== Theorem ==
== Proof ==
A minimally inductive class under $g$ is the same thing as a minimally closed class under $g$ with respect to $\O$.
The result then follows by a direct application of Bounded Subset of Minimally Closed Class under Progressing Mapping has Greatest Element.
== Sources ==
* : Chapter $3$: The Natural Numbers: $\S 4$ A double induction principle and its applications: Exercise $4.1$
Category:Non-Empty Bounded Subset of Minimally Inductive Class under Progressing Mapping has Greatest Element
Non-Empty Bounded Subset of Natural Numbers has Greatest Element

== Theorem ==
Let $\omega$ be the set of natural numbers defined as the von Neumann construction.
Then every non-empty bounded subset of $\omega$ has a greatest element.
== Proof ==
From Von Neumann Construction of Natural Numbers is Minimally Inductive, $\omega$ is minimally inductive class under the successor mapping.
From Successor Mapping on Natural Numbers is Progressing, this successor mapping is a progressing mapping.
The result is a direct application of Non-Empty Bounded Subset of Minimally Inductive Class under Progressing Mapping has Greatest Element.
== Sources ==
* : Chapter $3$: The Natural Numbers: $\S 5$ Applications to natural numbers: Theorem $5.4$
Category:Ordering on Natural Numbers
Non-Empty Class has Element of Least Rank

== Theorem ==
Let $C$ be a class.
Let $C \ne \O$.
Then $C$ has an element of least rank.
That is:
:$\exists x \in C: \forall y \in C: \map {\operatorname {rank} } x \le \map {\operatorname {rank} } y$
where $\map {\operatorname {rank} } x$ is the rank of $x$.
== Proof ==
By Set has Rank, each element of $C$ has a rank.
Let $R$ be the class of ranks of elements of $C$.
$R$ is non-empty because $C$ is non-empty.
Since any non-empty class of ordinals has a least element, $R$ has a least element, $q$.
By the definition of $R$:
:$\exists x \in C: \map {\operatorname {rank} } x = q$
Then $x$ is an element of $C$ of least rank.
Category:Von Neumann Hierarchy
Non-Empty Compact Closure is Directed

== Theorem ==
Let $L = \left({S, \vee, \preceq}\right)$ be a join semilattice.
Let $x \in S$ such that
:$x^{\mathrm{compact} }$ is a non-empty set,
where $x^{\mathrm{compact} }$ denotes the compact closure of $x$.
Then :$x^{\mathrm{compact} }$ is directed.
== Proof ==
Thus by assumption:
:$x^{\mathrm{compact} }$ is a non-empty set.
Let $y, z \in x^{\mathrm{compact} }$.
By definition of compact closure:
:$y \preceq x$, $z \preceq x$, and $y$ and $z$ are compact.
By definition of compact element:
:$y \ll y$ and $z \ll z$
where $\ll$ denotes the way below relation.
By Way Below is Congruent for Join:
:$y \vee z \ll y \vee z$
By definition:
:$y \vee z$ is a compact element
By definition of supremum:
:$y \vee z \preceq x$
Thus by definition of compact closure:
:$y \vee z \in x^{\mathrm{compact} }$
Thus by Join Succeeds Operands:
:$y \preceq y \vee z$ and $z \preceq y \vee z$
== Sources ==
* 
Category:Way Below Relation
Category:Order Theory
Non-Empty Finite Set of Natural Numbers has Greatest Element

== Theorem ==
Let $A$ be a non-empty finite set of natural numbers.
Then $A$ has a greatest element.
== Proof ==
The proof proceeds by induction.
By definition, if $A$ is a non-empty finite set, then $A$ has $m$ elements for some $m \in \N$ such that $m > 0$.
So, for all $n \in \N_{>0}$, let $\map P n$ be the proposition:
:If $A$ has $n$ elements, then $A$ has a greatest element.
=== Basis for the Induction ===
Let $A$ have one element which we will call $x$
Trivially:
:$\forall y \in A: y \le x$
and so $A$ has a greatest element $x$, by definition.
Thus $\map P 1$ 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:
:If $A$ has $k$ elements, then $A$ has a greatest element
from which it is to be shown that:
:If $A$ has $k + 1$ elements, then $A$ has a greatest element.
=== Induction Step ===
This is the induction step:
Let $A$ have $k + 1$ elements:
:$A = \set {a_1, a_2, \ldots, a_k, a_{k + 1} }$
Then:
:$A = \set {a_1, a_2, \ldots, a_k} \cup \set {a_{k + 1} }$
By the induction hypothesis, $\set {a_1, a_2, \ldots, a_k}$ has a greatest element, which we will call $m$.
By definition of greatest element, $m$ is one of the elements of $\set {a_1, a_2, \ldots, a_k}$.
As $A$ is a set, all elements of $A$ are distinct.
Hence:
:$\forall a \in \set {a_1, a_2, \ldots, a_k}: a \ne a_{k + 1}$
It follows that $m \ne a_{k + 1}$.
Suppose $a_{k + 1}$ is such that $a_{k + 1} > m$.
By definition of greatest element:
:$\forall y \in \set {a_1, a_2, \ldots, a_k}: y \le m$
and so:
:$\forall y \in \set {a_1, a_2, \ldots, a_k}: y < a_{k + 1}$
It follows that:
:$\forall y \in A: y \le a_{k + 1}$
and so $A$ has a greatest element, that is: $a_{k + 1}$.
Suppose $a_{k + 1}$ is such that $a_{k + 1} < m$.
Then it follows immediately that:
:$\forall y \in A: y \le m$
and so $A$ has a greatest element, that is: $m$.
In both cases $A$ has been shown to have a greatest element.
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore, for all $n \in \N_{>0}$:
:If $A$ has $n$ elements, then $A$ has a greatest element.
== Sources ==
* : Chapter $3$: The Natural Numbers: $\S 6$ Finite Sets: Exercise $6.1 \ (3)$
Category:Ordering on Natural Numbers
Category:Finite Sets
Non-Empty Set of Natural Numbers with no Greatest Element is Denumerable

== Theorem ==
Let $A$ be a non-empty set of natural numbers.
Let $A$ have no greatest element.
Then $A$ is a countably infinite set.
== Proof ==
 $A$ is finite.
From Subset of Naturals is Finite iff Bounded, it follows that $A$ is bounded.
Hence $A$ has a greatest element.
This contradicts the fact that $A$ has no greatest element.
Hence by Proof by Contradiction it follows that $A$ is not finite.
From Subset of Natural Numbers is either Finite or Denumerable, $A$ is a countably infinite set.
== Sources ==
* : Chapter $3$: The Natural Numbers: $\S 8$ Definition by finite recursion: Exercise $8.1$
Category:Natural Numbers
Category:Countably Infinite
Non-Empty Set of Type M has Maximal Element

== Theorem ==
Let $S$ be a non-empty set of sets which is of type $M$.
Then $S$ has a maximal element under the subset relation.
== Proof ==
Let $S$ be a non-empty set type $M$ set.
Let $x \in S$ be arbitrary.
Then by definition $x$ is a subset of a maximal element of $S$ under the subset relation.
Hence there has to actually be such a maximal element of $S$ for $x$ to be a subset of.
== Sources ==
* : Chapter $4$: Superinduction, Well Ordering and Choice: Part $\text {II}$ -- Maximal principles: $\S 5$ Maximal principles
Category:Type M Sets
Non-Empty Subset of Initial Segment of Natural Numbers has Greatest Element

== Theorem ==
Let $n \in \N_{>0}$ be a non-zero natural number.
Let $\N^*_n$ denote the Initial segment $\set {1, 2, \ldots, n}$ of the non-zero natural numbers.
Then every non-empty subset of $\N^*_n$ has a greatest element.
== Proof ==
The proof will proceed by the Principle of Mathematical Induction on $\N_{>0}$.
Let $S$ be the set defined as:
:$S := \leftset {n \in \N:}$ Every non-empty subset of $\N^*_n$ has a greatest element$\rightset{}$
=== Basis for the Induction ===
We have that:
: $\N^*_1 = \set 1$
The only non-empty subset of $\set 1$ is $\set 1$ itself.
This has a greatest element $1$.
So $1 \in S$.
This is our basis for the induction.
=== Induction Hypothesis ===
It is to be shown that, if $k \in S$ where $k \ge 1$, then it follows that $k + 1 \in S$.
This is the induction hypothesis:
:Every non-empty subset of $\N^*_k$ has a greatest element.
It is to be demonstrated that it follows that:
:Every non-empty subset of $\N^*_{k + 1}$ has a greatest element.
=== Induction Step ===
This is our induction step:
Let $T \subseteq \N^*_{k + 1}$.
Either $k + 1 \in T$ or $k + 1 \notin T$.
If $k + 1 \notin T$ then $T \subseteq \N^*_k$.
In that case, then from the induction hypothesis:
: $T$ has a greatest element.
If $k + 1 \in T$ then:
:$\forall x \in T: x \le k + 1$
and so $k + 1$ is the greatest element of $T$.
So in both cases $T$ has a greatest element and so $k + 1 \in S$.
So $k \in S \implies k + 1 \in S$ and the result follows by the Principle of Mathematical Induction:
:$\forall n \in \N$: every non-empty subset of $\N^*_n$ has a greatest element.
== Sources ==
* : $1$: Set Theory and Logic: $\S 4$: The Integers and the Real Numbers: Exercise $4 \ \text{(a)}$
Category:Natural Numbers
Non-Empty Way Below Closure is Directed in Join Semilattice

== Theorem ==
Let $L = \struct {S, \vee, \preceq}$ be a join semilattice.
Let $x \in S$ such that:
:$x^\ll \ne \O$
where $x^\ll$ denotes the way below closure of $x$.
Then $x^\ll$ is directed.
== Proof ==
By assumption:
:$x^\ll$ is a non-empty set.
Let $y, z \in x^\ll$.
By definition of way below closure:
:$y \ll x$ and $z \ll x$
By Join is Way Below if Operands are Way Below:
:$y \vee z \ll x$
By definition of way below closure:
:$y \vee z \in x^\ll$
By Join Succeeds Operands:
:$y \preceq y \vee z$ and $z \preceq y \vee z$
Thus by definition:
:$x^\ll$ is directed.
== Sources ==
* 
* 
Category:Join and Meet Semilattices
Category:Way Below Relation
Non-Equivalence

== Theorem ==
=== Non-Equivalence as Disjunction of Conjunctions ===
=== Non-Equivalence as Disjunction of Negated Conditionals ===
=== Non-Equivalence as Conjunction of Disjunction with Negation of Conjunction ===
=== Non-Equivalence as Conjunction of Disjunction with Disjunction of Negations ===
Category:Logical Negation
Category:Biconditional
Non-Equivalence as Conjunction of Disjunction with Disjunction of Negations

== Theorem ==
:$\neg \paren {p \iff q} \dashv \vdash \paren {p \lor q} \land \paren {\neg p \lor \neg q}$
== Proof 1 ==
== Proof by Truth Table ==
Category:Non-Equivalence as Conjunction of Disjunction with Disjunction of Negations
Category:Conjunction
Category:Disjunction
Category:Logical Negation
Category:Biconditional
Non-Equivalence as Conjunction of Disjunction with Disjunction of Negations/Proof by Truth Table

== Theorem ==
== 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}{|cccc||ccccccccc|} \hline
\neg & (p & \iff & q) & (p & \lor & q) & \land & (\neg & p & \lor & \neg & q) \\
\hline
\F & \F & \T & \F & \F & \F & \F & \F & \T & \F & \T & \T & \F \\
\T & \F & \F & \T & \F & \T & \T & \T & \T & \F & \T & \F & \T \\
\T & \T & \F & \F & \T & \T & \F & \T & \F & \T & \T & \T & \F \\
\F & \T & \T & \T & \T & \T & \T & \F & \F & \T & \F & \F & \T \\
\hline
\end{array}$
Category:Non-Equivalence as Conjunction of Disjunction with Disjunction of Negations
Category:Truth Table Proofs
Non-Equivalence as Conjunction of Disjunction with Negation of Conjunction

== Theorem ==
:$\neg \paren {p \iff q} \dashv \vdash \paren {p \lor q} \land \neg \paren {p \land q}$
That is, negation of the biconditional means the same thing as either-or but not both, that is, exclusive or.
== Proof 1 ==
== Proof by Truth Table ==
Category:Non-Equivalence as Conjunction of Disjunction with Negation of Conjunction
Category:Conjunction
Category:Disjunction
Category:Logical Negation
Category:Biconditional
Non-Equivalence as Conjunction of Disjunction with Negation of Conjunction/Proof by Truth Table

== Theorem ==
== 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}{|cccc||cccccccc|} \hline
\neg & (p & \iff & q) & (p & \lor & q) & \land & \neg & (p & \land & q) \\
\hline
\F & \F & \T & \F & \F & \F & \F & \F & \T & \F & \F & \F \\
\T & \F & \F & \T & \F & \T & \T & \T & \T & \F & \F & \T \\
\T & \T & \F & \F & \T & \T & \F & \T & \T & \T & \F & \F \\
\F & \T & \T & \T & \T & \T & \T & \F & \F & \T & \T & \T \\
\hline
\end{array}$
Category:Non-Equivalence as Conjunction of Disjunction with Negation of Conjunction
Category:Truth Table Proofs
Non-Equivalence as Disjunction of Conjunctions/Formulation 1

== Theorem ==
: $\neg \left ({p \iff q}\right) \dashv \vdash \left({\neg p \land q}\right) \lor \left({p \land \neg q}\right)$
This can be expressed as two separate theorems:
=== Forward Implication ===
=== Reverse Implication ===
== Proof 1 ==
== Proof 2 ==
Category:Non-Equivalence as Disjunction of Conjunctions
Non-Equivalence as Disjunction of Conjunctions/Formulation 1/Proof 1

== Theorem ==
: $\neg \left ({p \iff q}\right) \dashv \vdash \left({\neg p \land q}\right) \lor \left({p \land \neg q}\right)$
== Proof ==
=== Forward Implication: Proof ===
=== Reverse Implication: Proof ===
Category:Non-Equivalence as Disjunction of Conjunctions
Non-Equivalence as Disjunction of Conjunctions/Formulation 1/Proof 2

== Theorem ==
: $\neg \left ({p \iff q}\right) \dashv \vdash \left({\neg p \land q}\right) \lor \left({p \land \neg q}\right)$
== 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}{|cccc||ccccccccc|} \hline
\neg & (p & \iff & q) & (\neg & p & \land & q) & \lor & (p & \land & \neg & q) \\
\hline
F & F & T & F & T & F & F & F & F & F & F & T & F \\
T & F & F & T & T & F & T & T & T & F & F & F & T \\
T & T & F & F & F & T & F & F & T & T & T & T & F \\
F & T & T & T & F & T & F & T & F & T & F & F & T \\
\hline
\end{array}$
Category:Non-Equivalence as Disjunction of Conjunctions
Category:Truth Table Proofs
Non-Equivalence as Disjunction of Conjunctions/Formulation 2

== Theorem ==
:$\vdash \paren {\neg \paren {p \iff q} } \iff \paren {\paren {\neg p \land q} \lor \paren {p \land \neg q} }$
== Proof ==
== Sources ==
* : $\text{II}$: 'AND', 'OR', 'IF AND ONLY IF': $\S 5$: Theorem $\text{T87}$
Category:Non-Equivalence as Disjunction of Conjunctions
Non-Equivalence as Disjunction of Negated Conditionals

== Theorem ==
:$\neg \paren {p \iff q} \dashv \vdash \neg \paren {p \implies q} \lor \neg \paren {q \implies p}$
== Proof 1 ==
== Proof by Truth Table ==
== Sources ==
* : $\S 2.3.3$
Category:Non-Equivalence as Disjunction of Negated Conditionals
Category:Biconditional
Category:Disjunction
Category:Logical Negation
Category:Conditional
Non-Equivalence as Disjunction of Negated Conditionals/Proof by Truth Table

== Theorem ==
== 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}{|cccc||ccccccccc|} \hline
\neg & (p & \iff & q) & \neg & (p & \implies & q) & \lor & \neg & (q & \implies & p) \\
\hline
\F & \F & \T & \F & \F & \F & \T & \F & \F & \F & \F & \T & \F \\
\T & \F & \F & \T & \F & \F & \T & \T & \T & \T & \T & \F & \F \\
\T & \T & \F & \F & \T & \T & \F & \F & \T & \F & \F & \T & \T \\
\F & \T & \T & \T & \F & \T & \T & \T & \F & \F & \T & \T & \T \\
\hline
\end{array}$
Category:Non-Equivalence as Disjunction of Negated Conditionals
Category:Truth Table Proofs
Non-Equivalence as Equivalence with Negation/Formulation 1

== Theorem ==
:$\neg \paren {p \iff q} \dashv \vdash \paren {p \iff \neg q}$
This can be expressed as two separate theorems:
=== Forward Implication ===
=== Reverse Implication ===
== Proof 1 ==
== Proof by Truth Table ==
Category:Non-Equivalence as Equivalence with Negation
Non-Equivalence as Equivalence with Negation/Formulation 1/Proof by Truth Table

== Theorem ==
== 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}{|cccc||cccc|} \hline
\neg & (p & \iff & q) & (p & \iff & \neg & q) \\
\hline
\F & \F & \T & \F & \T & \F & \T & \F \\
\T & \F & \F & \T & \T & \T & \F & \T \\
\T & \T & \F & \F & \F & \T & \T & \F \\
\F & \T & \T & \T & \F & \F & \F & \T \\
\hline
\end{array}$
Category:Non-Equivalence as Equivalence with Negation
Category:Truth Table Proofs
Non-Equivalence as Equivalence with Negation/Formulation 2

== Theorem ==
:$\vdash \neg \paren {p \iff q} \iff \paren {p \iff \neg q}$
== Proof ==
== Sources ==
* : $\text{II}$: 'AND', 'OR', 'IF AND ONLY IF': $\S 5$: Theorem $\text{T90}$
Category:Non-Equivalence as Equivalence with Negation
Non-Field Integral Domain has Infinite Number of Ideals

== Theorem ==
Let $\struct {D, +, \circ}$ be an integral domain which is not a field.
Then $\struct {D, +, \circ}$ has an infinite number of distinct ideals.
== Proof ==
Let $a \in D$ be a proper element of $D$.
Because $\struct {D, +, \circ}$ is not a field, such an element is known to exist.
From Principal Ideal in Integral Domain generated by Power Plus One is Subset of Principal Ideal generated by Power:
:$\forall n \in \Z_{\ge 0}: \ideal {a^{n + 1} } \subsetneq \ideal {a_n}$
where $\ideal x$ denotes the principal ideal of $D$ generated by $x$.
Hence the set:
:$S = \set {\ideal {1_D}, \ideal a, \ideal {a^2}, \ideal {a^3}, \dotsc}$
is infinite.
== Sources ==
* : Chapter $9$: Rings: Exercise $7 \ \text {(i)}$
Category:Integral Domains
Category:Ideals of Rings