avewright/proofwiki-math huggingface dataset:
Theorem: Cauchy-Binet Formula

Let $\mathbf A$ be an $m \times n$ matrix.
Let $\mathbf B$ be an $n \times m$ matrix.
Let $1 \le j_1, j_2, \ldots, j_m \le n$.
Let $\mathbf A_{j_1 j_2 \ldots j_m}$ denote the $m \times m$ matrix consisting of columns $j_1, j_2, \ldots, j_m$ of $\mathbf A$.
Let $\mathbf B_{j_1 j_2 \ldots j_m}$ denote the $m \times m$ matrix consisting of rows $j_1, j_2, \ldots, j_m$ of $\mathbf B$.
Then:
:$\ds \map \det {\mathbf A \mathbf B} = \sum_{1 \mathop \le j_1 \mathop < j_2 \mathop < \cdots \mathop < j_m \mathop \le n} \map \det {\mathbf A_{j_1 j_2 \ldots j_m} } \map \det {\mathbf B_{j_1 j_2 \ldots j_m} }$
where $\det$ denotes the determinant.

Proof:
Let $\tuple {k_1, k_2, \ldots, k_m}$ be an ordered $m$-tuple of integers.
Let $\map \epsilon {k_1, k_2, \ldots, k_m}$ denote the sign of $\tuple {k_1, k_2, \ldots, k_m}$.
Let $\tuple {l_1, l_2, \ldots, l_m}$ be the same as $\tuple {k_1, k_2, \ldots, k_m}$ except for $k_i$ and $k_j$ having been transposed.
Then from Transposition is of Odd Parity:
:$\map \epsilon {l_1, l_2, \ldots, l_m} = -\map \epsilon {k_1, k_2, \ldots, k_m}$
Let $\tuple {j_1, j_2, \ldots, j_m}$ be the same as $\tuple {k_1, k_2, \ldots, k_m}$ by arranged into non-decreasing order.
That is:
:$j_1 \le j_2 \le \cdots \le j_m$
Then it follows that:
:$\map \det {\mathbf B_{k_1 \cdots k_m} } = \map \epsilon {k_1, k_2, \ldots, k_m} \map \det {\mathbf B_{j_1 \cdots j_m} }$
Hence:
{{begin-eqn}}
{{eqn | l = \map \det {\mathbf A \mathbf B}
      | r = \sum_{1 \mathop \le l_1, \mathop \ldots \mathop , l_m \mathop \le m} \map \epsilon {l_1, \ldots, l_m} \paren {\sum_{k \mathop = 1}^n a_{1 k} b_{k l_1} } \cdots \paren {\sum_{k \mathop = 1}^n a_{m k} b_{k l_m} }
      | c = {{Defof|Determinant of Matrix}}
}}
{{eqn | r = \sum_{1 \mathop \le k_1, \mathop \ldots \mathop , k_m \mathop \le n} a_{1 k_1} \cdots a_{m k_m} \sum_{1 \mathop \le l_1, \mathop \ldots \mathop , l_m \mathop \le m} \map \epsilon {l_1, \ldots, l_m} b_{k_1 l_1} \cdots b_{k_m l_m} 
      | c = 
}}
{{eqn | r = \sum_{1 \mathop \le k_1, \mathop \ldots \mathop , k_m \mathop \le n} a_{1 k_1} \cdots a_{m k_m} \map \det {\mathbf B_{k_1 \cdots k_m} }
      | c = 
}}
{{eqn | r = \sum_{1 \mathop \le k_1, \mathop \ldots \mathop , k_m \mathop \le n} a_{1 k_1} \map \epsilon {k_1, \ldots, k_m} \cdots a_{m k_m} \map \det {\mathbf B_{j_1 \cdots j_m} }
      | c = 
}}
{{eqn | r = \sum_{1 \mathop \le j_1 \mathop \le j_2 \mathop \le \cdots \mathop \le j_m \mathop \le n} \map \det {\mathbf A_{j_1 \cdots j_m} } \map \det {\mathbf B_{j_1 \cdots j_m} }
      | c = 
}}
{{end-eqn}}
If two $j$s are equal:
:$\map \det {\mathbf A_{j_1 \cdots j_m} } = 0$
{{qed}}
Theorem: Auxiliary Relation is Congruent

Let $\struct {S, \vee, \preceq}$ be a bounded below join semilattice.
Let $\RR$ be relation on $S$ satisfying conditions $(2)$ and $(3)$ of auxiliary relation.
Then:
:$\forall x, y, z, u \in S: \tuple {x, z} \in \RR \land \tuple {y, u} \in \RR \implies \tuple {x \vee y, z \vee u} \in \RR$

Proof:
Let $x, y, z, u \in S$ such that:
:$\tuple {x, z} \in \RR \land \tuple {y, u} \in \RR$
By definition of reflexivity:
:$x \preceq x$ and $y \preceq y$
By Join Succeeds Operands:
:$z \preceq z \vee u$ and $u \preceq z \vee u$
By condition $(2)$ of auxiliary relation:
:$\tuple {x, z \vee u} \in \RR$ and $\tuple {y, z \vee u} \in \RR$
Thus by condition $(3)$ of auxiliary relation:
:$\tuple {x \vee y, z \vee u} \in \RR$
{{qed}}
Theorem: Auxiliary Relation is Transitive

Let $\struct {S, \vee, \preceq}$ be a bounded below join semilattice.
Let $\RR$ be relation on $S$ satisfying conditions $(1)$ and $(2)$ of auxiliary relation.
Then
:$\RR$ is a transitive relation.

Proof:
Let $x, y, z \in S$ such that
:$\tuple {x, y} \in \RR \land \tuple {y, z} \in \RR$
By definition of reflexivity:
:$z \preceq z$ 
By condition $(1)$ of auxiliary relation:
:$x \preceq y$
Thus by condition $(2)$ of auxiliary relation:
:$\tuple {x, z} \in \RR$
Thus by definition
:$\RR$ is a transitive relation.
{{qed}}
Theorem: Cauchy-Binet Formula/Example/m equals 1

Let $\mathbf A = \sqbrk a_{1 n}$ be a row matrix with $n$ columns.
and $\mathbf B = \sqbrk b_{n 1}$ be a column matrix with $n$ rows.
Let $\mathbf A \mathbf B$ be the (conventional) matrix product of $\mathbf A$ and $\mathbf B$.
Then:
:$\ds \map \det {\mathbf A \mathbf B} = \sum_{j \mathop = 1}^n a_j b_j$
where:
:$a_j$ is element $a_{1 j}$ of $\mathbf A$
:$b_j$ is element $b_{j 1}$ of $\mathbf B$.

Proof:
The Cauchy-Binet Formula gives:
:$\ds \map \det {\mathbf A \mathbf B} = \sum_{1 \mathop \le j_1 \mathop < j_2 \mathop < \cdots \mathop < j_m \mathop \le n} \map \det {\mathbf A_{j_1 j_2 \ldots j_m} } \map \det {\mathbf B_{j_1 j_2 \ldots j_m} }$
where:
:$\mathbf A$ is an $m \times n$ matrix
:$\mathbf B$ is an $n \times m$ matrix.
:For $1 \le j_1, j_2, \ldots, j_m \le n$:
::$\mathbf A_{j_1 j_2 \ldots j_m}$ denotes the $m \times m$ matrix consisting of columns $j_1, j_2, \ldots, j_m$ of $\mathbf A$.
::$\mathbf B_{j_1 j_2 \ldots j_m}$ denotes the $m \times m$ matrix consisting of rows $j_1, j_2, \ldots, j_m$ of $\mathbf B$.
When $m = 1$, the relation:
:$1 \le j_1 < j_2 < \cdots < j_m \le n$
degenerates to:
:$1 \le j \le n$
By definition of order $1$ determinant:
:$\det \sqbrk {a_j} = a_j$
:$\det \sqbrk {b_j} = b_j$
Hence the result.
{{qed}}
Theorem: Preceding is Auxiliary Relation

Let $\left({S, \vee, \preceq}\right)$ be a bounded below join semilattice.
Then
:$\preceq$ is an auxiliary relation.

Proof:
:$\forall x, y \in S: x \preceq y \implies x \preceq y$
Then condition $(1)$ of auxiliary relation is satisfied.
By definition of transitivity:
:$\forall x, y, z, u \in S: x \preceq y \preceq z \preceq u \implies x \preceq u$
Then the condition $(2)$ of auxiliary relation is satisfied.
By  definition of supremum:
:$\forall x, y, z \in S: x \preceq z \land y \preceq z \implies x \vee y \preceq z$
Then the condition $(3)$ of auxiliary relation is satisfied.
By definition of smallest element:
:$\forall x \in S: \bot \preceq x$
Then the condition $(4)$ of auxiliary relation is satisfied.
Thus the result by definition auxiliary relation.
{{qed}}
Theorem: Cauchy-Binet Formula/Example/Matrix by Transpose

Let $\mathbf A$ be an $m \times n$ matrix.
Let $\mathbf A^\intercal$ be the transpose $\mathbf A$.
Let $1 \le j_1, j_2, \ldots, j_m \le n$.
Let $\mathbf A_{j_1 j_2 \ldots j_m}$ denote the $m \times m$ matrix consisting of columns $j_1, j_2, \ldots, j_m$ of $\mathbf A$.
Let $\mathbf A^\intercal_{j_1 j_2 \ldots j_m}$ denote the $m \times m$ matrix consisting of rows $j_1, j_2, \ldots, j_m$ of $\mathbf A^\intercal$.
Then:
:$\ds \map \det {\mathbf A \mathbf A^\intercal} = \sum_{1 \mathop \le j_1 \mathop < j_2 \mathop < \cdots \mathop < j_m \le n} \paren {\map \det {\mathbf A_{j_1 j_2 \ldots j_m} } }^2$
where $\det$ denotes the determinant.

Proof:
The Cauchy-Binet Formula gives:
:$\ds \map \det {\mathbf A \mathbf B} = \sum_{1 \mathop \le j_1 \mathop < j_2 \mathop < \cdots \mathop < j_m \le n} \map \det {\mathbf A_{j_1 j_2 \ldots j_m} } \map \det {\mathbf B_{j_1 j_2 \ldots j_m} }$
where:
:$\mathbf A$ is an $m \times n$ matrix
:$\mathbf B$ is an $n \times m$ matrix.
:For $1 \le j_1, j_2, \ldots, j_m \le n$:
::$\mathbf A_{j_1 j_2 \ldots j_m}$ denotes the $m \times m$ matrix consisting of columns $j_1, j_2, \ldots, j_m$ of $\mathbf A$.
::$\mathbf B_{j_1 j_2 \ldots j_m}$ denotes the $m \times m$ matrix consisting of rows $j_1, j_2, \ldots, j_m$ of $\mathbf B$.
From the definition of transpose $\mathbf A^\intercal$ is an $n \times m$ matrix.
Hence the Cauchy-Binet Formula can be applied directly:
:$\ds \map \det {\mathbf A \mathbf A^\intercal} = \sum_{1 \mathop \le j_1 \mathop < j_2 \mathop < \cdots \mathop < j_m \le n} \map \det {\mathbf A_{j_1 j_2 \ldots j_m} } \map \det {\mathbf A^\intercal_{j_1 j_2 \ldots j_m} }$
Note that by construction:
:$\mathbf A_{j_1 j_2 \ldots j_m}$ is a square matrix
Also, by definition of transpose:
:$\mathbf A^\intercal_{j_1 j_2 \ldots j_m} = \paren {\mathbf A_{j_1 j_2 \ldots j_m} }^\intercal$
The result follows from Determinant of Transpose:
:$\map \det {\mathbf A} = \map \det {\mathbf A^\intercal}$
{{qed}}
Theorem: Preceding is Top in Ordered Set of Auxiliary Relations

Let $L = \struct {S, \vee, \preceq}$ be a bounded below join semilattice.
Let $\map {\it Aux} L$ be the set of all auxiliary relations on $S$.
Let $P = \struct {\map {\it Aux} L, \precsim}$ be an ordered set
where $\precsim \mathop = \subseteq \restriction_{\map {\it Aux} L \times \map {\it Aux} L}$
Then
:$\preceq \mathop = \top_P$
where $\top_P$ denotes the greatest element in $P$.

Proof:
By Preceding is Auxiliary Relation:
:$\preceq \mathop \in \map {\it Aux} L$
By definition:
:$\preceq$ is lower bound for $\O$ in $P$
We will prove that:
:$\forall R \in \map {\it Aux} L: R$ is lower bound for $\O \implies R \mathop \precsim \preceq$
Let $R \in \map {\it Aux} L$
By condition $(i)$ of definition of auxiliary relation:
:$R \mathop \subseteq \preceq$
Thus by definition of $\precsim$:
:$R \mathop \precsim \preceq$
{{qed|lemma}}
By definition of infimum:
:$\preceq \mathop = \inf_P \O$
Thus by Infimum of Empty Set is Greatest Element:
:$\preceq \mathop = \top_P$
{{qed}}
Theorem: Bottom Relation is Auxiliary Relation

Let $L = \left({S, \vee, \preceq}\right)$ be a bounded below join semilattice.
Let $B = \left\{ {\left({\bot, x}\right): x \in S}\right\}$
where $\bot$ denotes the smallest element in $L$.
Then
:$B$ is auxiliary relation.

Proof:
By definition of smallest element:
:$\forall x \in S: \bot \preceq x$
Thus by definition of $B$:
:$\forall x, y \in S: \left({x, y}\right) \in B \implies x \preceq y$
We will prove that
:$\forall x, y, z, u \in S: x \preceq y \land \left({y, z}\right) \in B \land z \preceq u \implies \left({x, u}\right) \in B$
Let $x, y, z, u \in S$ such that
:$x \preceq y \land \left({y, z}\right) \in B \land z \preceq u$
By definition of $B$:
:$y = \bot$
By definition of smallest element:
:$\bot \preceq x$
By definition of antisymmetry:
:$x = \bot$
Thus by definition of $B$:
:$\left({x, u}\right) \in B$
{{qed|lemma}}
We will prove that
:$\forall x, y, z \in S: \left({x, z}\right) \in B \land \left({y, z}\right) \in B \implies \left({x \vee y, z}\right) \in B$
Let $x, y, z \in S$ such that
: $\left({x, z}\right) \in B \land \left({y, z}\right) \in B$
By definition of $B$:
:$x = y = \bot$
By Join is Idempotent:
:$x \vee y = \bot$
Thus by definition of $B$:
:$\left({x \vee y, z}\right) \in B$
{{qed|lemma}}
Thus by definition of $B$:
:$\forall x \in S: \left({\bot, x}\right) \in B$
Thus by definition:
:$B$ is auxiliary relation.
{{qed}}
Theorem: Bottom Relation is Bottom in Ordered Set of Auxiliary Relations

Let $L = \struct {S, \vee, \preceq}$ be a bounded below join semilattice.
Let $\map {\it Aux} L$ be the set of all auxiliary relations on $S$.
Let $P = \struct {\map {\it Aux} L, \precsim}$ be an ordered set where:
:$\precsim \mathop = \subseteq \restriction_{ \map {\it Aux} L \times \map {\it Aux} L}$
Let $B = \set {\struct {\bot_L, x}: x \in S}$
where $\bot_L$ denotes smallest element in $L$.
Then
:$B \mathop = \bot_P$

Proof:
By Bottom Relation is Auxiliary Relation:
:$B \in \map {\it Aux} L$
By definition:
:$B$ is an upper bound for $\O$ in $P$
We will prove that:
:$\forall R \in \map {\it Aux} L: R$ is an upper bound for $\O \implies B \mathop \precsim R$
Let $R \in \map {\it Aux} L$.
By condition $(iv)$ of definition of auxiliary relation:
:$B \subseteq R$
Thus by definition of $\precsim$:
:$B \precsim R$
{{qed|lemma}}
By definition of supremum:
:$B = \sup_P \O$
Thus by Supremum of Empty Set is Smallest Element:
:$B = \bot_P$
{{qed}}
Theorem: Inverse of Conditional is Converse of Contrapositive

Let $p \implies q$ be a conditional.
Then the inverse of $p \implies q$ is the converse of its contrapositive.

Proof:
The inverse of $p \implies q$ is:
:$\neg p \implies \neg q$
The contrapositive of $p \implies q$ is:
:$\neg q \implies \neg p$
The converse of $\neg q \implies \neg p$ is:
:$\neg p \implies \neg q$
The two are seen to be equal.
{{qed}}
Category:Conditional
87yc00e6gp5kuh83oqd4glbg0a8ece4
Theorem: Inverse of Conditional is Contrapositive of Converse

Let $p \implies q$ be a conditional.
Then the inverse of $p \implies q$ is the contrapositive of its converse.

Proof:
The inverse of $p \implies q$ is:
:$\neg p \implies \neg q$
The converse of $p \implies q$ is:
:$q \implies p$
The contrapositive of $q \implies p$ is:
:$\neg p \implies \neg q$
The two are seen to be equal.
{{qed}}
Category:Conditional
d44nh6jup1dia42nknek8d9zurgb9wf
Theorem: Converse of Conditional is Contrapositive of Inverse

Let $p \implies q$ be a conditional.
Then the converse of $p \implies q$ is the contrapositive of its inverse.

Proof:
The converse of $p \implies q$ is:
:$q \implies p$
The inverse of $p \implies q$ is:
:$\neg p \implies \neg q$
The contrapositive of $\neg p \implies \neg q$ is:
:$\neg \neg q \implies \neg \neg p$
By Double Negation, the two are seen to be equal.
{{qed}}
Category:Conditional
qxlweqotkrviamlc86s2ga5z7j3idbk
Theorem: Converse of Conditional is Inverse of Contrapositive

Let $p \implies q$ be a conditional.
Then the converse of $p \implies q$ is the inverse of its contrapositive.

Proof:
The converse of $p \implies q$ is:
:$q \implies p$
The contrapositive of $p \implies q$ is:
:$\neg q \implies \neg p$
The inverse of $\neg q \implies \neg p$ is:
:$\neg \neg q \implies \neg \neg p$
By Double Negation, the two are seen to be equal.
{{qed}}
Category:Conditional
4dtdb2u7zqedssj9r5e1eereynfa6au
Theorem: Intersection of Auxiliary Relations is Auxiliary Relation

Let $L = \struct {S, \vee, \preceq}$ be a bounded below join semilattice.
Let $\FF$ be a non-empty set of auxiliary relations on $S$.
Then
:$\ds \bigcap \FF$ is auxiliary relation.

Proof:
By definition of non-empty set:
:$\exists \RR: \RR \in \FF$
We will prove that:
:$\ds \forall x, y \in S: \tuple {x, y} \in \bigcap \FF \implies x \preceq y$
Let $x, y \in S$ such that:
:$\ds \tuple {x, y} \in \bigcap \FF$
By definition of intersection:
:$\tuple {x, y} \in \RR$
Thus by definition of auxiliary relation:
:$x \preceq y$
{{qed|lemma}}
We will prove that:
:$\ds \forall x, y, z, u \in S: x \preceq y \land \tuple {y, z} \in \bigcap \FF \land z \preceq u \implies \tuple {x, u} \in \bigcap \FF$
Let $x, y, z, u \in S$ such that:
:$\ds x \preceq y \land \tuple {y, z} \in \bigcap \FF \land z \preceq u$
By definition of intersection:
:$\forall r \in \FF: \tuple {y, z} \in r$
By definition of auxiliary relation:
:$\forall r \in \FF: \tuple {x, u} \in r$
Thus by definition of intersection:
:$\ds \tuple {x, u} \in \bigcap \FF$
{{qed|lemma}}
We will prove that:
:$\ds \forall x, y, z \in S: \tuple {x, z} \in \bigcap \FF \land \tuple {y, z} \in \bigcap \FF \implies \tuple {x \vee y, z} \in \bigcap \FF$
Let $x, y, z \in S$ such that:
:$\ds \tuple {x, z} \in \bigcap \FF \land \tuple {y, z} \in \bigcap \FF$
By definition of intersection:
:$\forall r \in \FF: \tuple {x, z} \in r \land \tuple {y, z} \in r$
By definition of auxiliary relation:
:$\forall r \in \FF: \tuple {x \vee y, z} \in r$
Thus by definition of intersection:
:$\tuple {x \vee y, z} \in \bigcap \FF$
{{qed|lemma}}
By definition of auxiliary relation:
:$\forall x \in S: \forall r \in \FF: \tuple {\bot, x} \in r$
Thus by definition of intersection:
:$\ds \forall x \in S: \tuple {\bot, x} \in \bigcap \FF$
Thus by definition:
:$\ds \bigcap \FF$ is auxiliary relation.
{{qed}}
Theorem: Ordered Set of Auxiliary Relations is Complete Lattice

Let $L = \struct {S, \vee, \preceq}$ be a bounded below join semilattice.
Let $\map {\operatorname {Aux} } L$ be the set of all auxiliary relations on $S$.
Let $P = \struct {\map {\operatorname {Aux} } L, \precsim}$ be an ordered set
where $\precsim \mathop = \subseteq \restriction_{\map {\operatorname {Aux} } L \times \map {\operatorname {Aux} } L}$
Then
:$P$ is a complete lattice.

Proof:
Let $X \subseteq \map {\operatorname {Aux} } L$
In the case when $X \ne \O$:
By Intersection of Auxiliary Relations is Auxiliary Relation:
:$\bigcap X \in \map {\operatorname {Aux} } L$
By Intersection is Largest Subset, $\bigcap X$ is the infimum of $X$.
In case when $X = \O$:
By proof of Preceding is Top in Ordered Set of Auxiliary Relations:
:$\O$ admits an infimum in $P$
Then:
:$X$ (empty or non-empty) admits an infimum in $P$
By duality of Lattice is Complete iff it Admits All Suprema:
:$P$ is a complete lattice.
{{qed}}
Theorem: Cauchy-Binet Formula/Example/m greater than n

Let $\mathbf A$ be an $m \times n$ matrix.
Let $\mathbf B$ be an $n \times m$ matrix.
Let $m > n$.
Then:
:$\map \det {\mathbf A \mathbf B} = 0$

Proof:
The Cauchy-Binet Formula gives:
:$(1): \quad \ds \map \det {\mathbf A \mathbf B} = \sum_{1 \mathop \le j_1 \mathop < j_2 \mathop < \cdots \mathop < j_m \le n} \map \det {\mathbf A_{j_1 j_2 \ldots j_m} } \map \det {\mathbf B_{j_1 j_2 \ldots j_m} }$
where:
:$\mathbf A$ is an $m \times n$ matrix
:$\mathbf B$ is an $n \times m$ matrix.
:For $1 \le j_1, j_2, \ldots, j_m \le n$:
::$\mathbf A_{j_1 j_2 \ldots j_m}$ denotes the $m \times m$ matrix consisting of columns $j_1, j_2, \ldots, j_m$ of $\mathbf A$.
::$\mathbf B_{j_1 j_2 \ldots j_m}$ denotes the $m \times m$ matrix consisting of rows $j_1, j_2, \ldots, j_m$ of $\mathbf B$.
But here $m > n$.
Therefore the set $\set {j_1, j_2, \ldots, j_m}$ such that:
:$1 \mathop \le j_1 \mathop < j_2 \mathop < \cdots \mathop < j_m \le n$
is the empty set.
Thus the {{RHS}} of $(1)$ is a vacuous summation.
Hence the result.
{{qed}}
Theorem: Krattenthaler's Identity

:$\begin{vmatrix}
\paren {x + q_2} \paren {x + q_3} & \paren {x + p_1} \paren {x + q_3} & \paren {x + p_1} \paren {x + p_2} \\
\paren {y + q_2} \paren {y + q_3} & \paren {y + p_1} \paren {y + q_3} & \paren {y + p_1} \paren {y + p_2} \\
\paren {z + q_2} \paren {z + q_3} & \paren {z + p_1} \paren {z + q_3} & \paren {z + p_1} \paren {z + p_2}
\end{vmatrix} = \paren {x - y} \paren {x - z} \paren {y - z} \paren {p_1 - q_2} \paren {p_1 - q_3} \paren {p_2 - q_3}$
where $\size {\, \cdot \,}$ denotes determinant.

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = \begin{vmatrix}
\paren {x + q_2} \paren {x + q_3} & \paren {x + p_1} \paren {x + q_3} & \paren {x + p_1} \paren {x + p_2} \\
\paren {y + q_2} \paren {y + q_3} & \paren {y + p_1} \paren {y + q_3} & \paren {y + p_1} \paren {y + p_2} \\
\paren {z + q_2} \paren {z + q_3} & \paren {z + p_1} \paren {z + q_3} & \paren {z + p_1} \paren {z + p_2}
\end{vmatrix}
      | c = 
}}
{{eqn | r = \begin{vmatrix}
\paren {x + q_2} \paren {x + q_3} & \paren {p_1 - q_2} \paren {x + q_3} & \paren {p_1 - q_3} \paren {x + p_2} \\
\paren {y + q_2} \paren {y + q_3} & \paren {p_1 - q_2} \paren {y + q_3} & \paren {p_1 - q_3} \paren {y + p_2} \\
\paren {z + q_2} \paren {z + q_3} & \paren {p_1 - q_2} \paren {z + q_3} & \paren {p_1 - q_3} \paren {z + p_2}
\end{vmatrix}
      | c = Multiple of Row Added to Row of Determinant
}}
{{eqn | r = \paren {p_1 - q_2} \paren {p_1 - q_3} \begin{vmatrix}
\paren {x + q_2} \paren {x + q_3} & x + q_3 & x + p_2 \\
\paren {y + q_2} \paren {y + q_3} & y + q_3 & y + p_2 \\
\paren {z + q_2} \paren {z + q_3} & z + q_3 & z + p_2
\end{vmatrix}
      | c = Determinant with Row Multiplied by Constant
}}
{{eqn | r = \paren {p_1 - q_2} \paren {p_1 - q_3} \begin{vmatrix}
x \paren {x + q_3} & x + q_3 & p_2 - q_3 \\
y \paren {y + q_3} & y + q_3 & p_2 - q_3 \\
z \paren {z + q_3} & z + q_3 & p_2 - q_3
\end{vmatrix}
      | c = Multiple of Row Added to Row of Determinant
}}
{{eqn | r = \paren {p_1 - q_2} \paren {p_1 - q_3} \paren {p_2 - q_3} \begin{vmatrix}
x \paren {x + q_3} & x + q_3 & 1\\
y \paren {y + q_3} & y + q_3 & 1\\
z \paren {z + q_3} & z + q_3 & 1
\end{vmatrix}
      | c = Determinant with Row Multiplied by Constant
}}
{{eqn | r = \paren {p_1 - q_2} \paren {p_1 - q_3} \paren {p_2 - q_3} \begin{vmatrix}
x^2 & x & 1\\
y^2 & y & 1\\
z^2 & z & 1
\end{vmatrix}
      | c = Multiple of Row Added to Row of Determinant
}}
{{eqn | r = \paren {p_1 - q_2} \paren {p_1 - q_3} \paren {p_2 - q_3} \paren {x - y} \paren {y - z} \paren {x - z}
      | c = Value of Vandermonde Determinant
}}
{{end-eqn}}
{{qed}}
{{Namedfor|Christian Friedrich Krattenthaler|cat = Krattenthaler}}
Theorem: Floor Function/Examples/Floor of Root 2

:$\floor {\sqrt 2} = 1$

Proof:
The decimal expansion of $\sqrt 2$ is:
:$\sqrt 2 \approx 1.41421 \ 35623 \ 73095 \ 0488 \ldots$
Thus:
:$1 \le \sqrt 2 < 2$
Hence $1$ is the floor of $\sqrt 2$ by definition.
{{qed}}
Theorem: Ceiling Function/Examples/Ceiling of Root 2

:$\ceiling {\sqrt 2} = 2$

Proof:
The decimal expansion of $\sqrt 2$ is:
:$\sqrt 2 \approx 1.41421 \ 35623 \ 73095 \ 0488 \ldots$
Thus:
:$1 < \sqrt 2 \le 2$
Hence $2$ is the ceiling of $\sqrt 2$ by definition.
{{qed}}
Theorem: Floor Function/Examples/Floor of One Half

:$\floor {\dfrac 1 2} = 0$

Proof:
We have that:
:$0 \le \dfrac 1 2$
and:
:$1 = \dfrac 2 2 > \dfrac 1 2$
Hence $0$ is the floor of $\dfrac 1 2$ by definition.
{{qed}}
Theorem: Ceiling Function/Examples/Ceiling of Minus One Half

:$\ceiling {-\dfrac 1 2} = 0$

Proof:
We have:
:$0 \ge -\dfrac 1 2$
and:
:$-1 = -\dfrac 2 2 < -\dfrac 1 2$
Hence $0$ is the ceiling of $-\dfrac 1 2$ by definition.
{{qed}}
Theorem: Floor Function/Examples/Floor of Minus One Half

:$\floor {-\dfrac 1 2} = -1$

Proof:
We have that:
:$-1 = -\dfrac 2 2 \le -\dfrac 1 2$
and:
:$0 > -\dfrac 1 2$
Hence $-1$ is the floor of $-\dfrac 1 2$ by definition.
{{qed}}
Theorem: Infima of two Real Sets

Let $S$ and $T$ be sets of real numbers.
Let $S$ and $T$ admit infima.
Then:
: $\inf S \ge \inf T \iff \forall \epsilon \in \R_{>0}: \forall s \in S: \exists t \in T: s + \epsilon > t$

Proof:
Let:
: $-S = \set {-s: s \in S}$
: $-T = \set {-t: t \in T}$
Observe that:
: $s \in S \iff -s \in -S$
: $t \in T \iff -t \in -T$
We know that $\inf S$ and $\inf T$ exist.
The expression $\inf S \ge \inf T$ exists as $\inf S$ and $\inf T$ exist.
In other words, for fixed sets $S$ and $T$, $\inf S \ge \inf T$ is either true or false.
We find:
{{begin-eqn}}
{{eqn | l = \inf S
      | o = \ge
      | r = \inf T
}}
{{eqn | ll= \leadstoandfrom
      | l = -\sup -S
      | o = \ge
      | r = -\sup -T
      | c = by the lemma
}}
{{eqn | ll= \leadstoandfrom
      | l = \sup -S
      | o = \le
      | r = \sup -T
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall \epsilon \in \R_{>0}: \forall x \in -S: \exists y \in -T
      | l = x
      | o = <
      | r = y + \epsilon
      | c = Suprema of two Real Sets
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall \epsilon \in \R_{>0}: \forall s \in S: \set {x: = -s}: \exists t \in T: \paren {y: = -t}
      | l = x
      | o = <
      | r = y + \epsilon
      | c = as $s \in S \iff -s \in −S$ and $t \in T \iff -t \in −T$
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall \epsilon \in \R_{>0}: \forall s \in S: \exists t \in T
      | l = -s
      | o = <
      | r = -t + \epsilon
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall \epsilon \in \R_{>0}: \forall s \in S: \exists t \in T
      | l = s + \epsilon
      | o = >
      | r = t
}}
{{end-eqn}}
Theorem: Floor Function is Integer

Let $x$ be a real number.
Then the floor function of $x$ is an integer:
:$\floor x \in \Z$

Proof:
This is by definition of the floor function.
{{qed}}
Theorem: Floor of Number plus Integer

:$\forall n \in \Z: \floor x + n = \floor {x + n}$

Proof:
{{begin-eqn}}
{{eqn | l = \floor {x + n}
      | o = \le
      | m = x + n 
      | mo= <
      | r = \floor {x + n} + 1
      | c = {{Defof|Floor Function}}
}}
{{eqn | ll= \leadsto
      | l = \floor {x + n} - n
      | o = \le
      | m = x
      | mo= <
      | r = \floor {x + n} - n + 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \floor x
      | r = \floor {x + n} - n
      | c = {{Defof|Floor Function}}
}}
{{eqn | ll= \leadsto
      | l = \floor {x + n}
      | r = \floor x + n
      | c = adding $n$ to both sides
}}
{{end-eqn}}
{{qed}}
Theorem: Floor is between Number and One Less

:$x - 1 < \floor x \le x$
where $\floor x$ denotes the floor of $x$.

Proof:
By definition of floor function:
:$\floor x \le x < \floor x + 1$
Thus by subtracting $1$:
:$x - 1 < \paren {\floor x + 1} - 1 = \floor x$
So:
:$\floor x \le x$
and:
:$x - 1 < \floor x$
as required.
{{qed}}
Theorem: Equivalence of Definitions of Floor Function

Let $x$ be a real number.
{{TFAE|def = Floor Function}}

Proof:
=== Definition 1 equals Definition 2 ===
Follows from Supremum of Set of Integers equals Greatest Element.
{{qed|lemma}}