avewright/proofwiki-math huggingface dataset:
Theorem: Ceiling Function is Integer

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

Proof:
This is by definition of the ceiling function.
{{qed}}
Theorem: Real Number is Integer iff equals Ceiling

:$x = \ceiling x \iff x \in \Z$

Proof:
Let $x = \ceiling x$.
As $\ceiling x \in \Z$, then so must $x$ be.
Now let $x \in \Z$.
We have:
:$\ceiling x = \inf \set {m \in \Z: m \ge x}$
As $x \in \inf \set {m \in \Z: m \ge x}$, and there can be no lesser $n \in \Z$ such that $n \in \inf \set {m \in \Z: m \ge x}$, it follows that:
:$x = \ceiling x$
{{qed}}
Category:Ceiling Function
3987x4r1nfwbzj69zb29b5k9c9szjdv
Theorem: Ceiling Function is Idempotent

:$\ceiling {\ceiling x} = \ceiling x$

Proof:
Let $y = \ceiling x$.
By Ceiling Function is Integer, $y$ is an integer.
Then from Real Number is Integer iff equals Ceiling:
:$\ceiling y = y$
So:
:$\ceiling {\ceiling x} = \ceiling x$
{{qed}}
Theorem: Way Below Relation is Auxiliary Relation

Lrt $L = \left({S, \vee, \preceq}\right)$ be a bounded below join semilattice.
Then
:$\ll$ is auxiliary relation
where $\ll$ denotes the way below relation.

Proof:
By Way Below implies Preceding:
:$\forall x, y \in S: x \ll y \implies x \preceq y$
By Preceding and Way Below implies Way Below:
:$\forall x, y, z, u \in S: x \preceq y \ll z \preceq u \implies x \ll u$
By Join is Way Below if Operands are Way Below:
:$\forall x, y, z \in S: x \ll z \land y \ll z \implies x \vee y \ll z$
By Bottom is Way Below Any Element:
:$\forall x: \bot \ll x$
where $\bot$ denotes the smallest element in $L$.
Thus by definition:
:$\ll$ is auxiliary relation.
{{qed}}
Theorem: Exponential Sequence is Eventually Strictly Positive

Let $\sequence {E_n}$ be the sequence of real functions $E_n: \R \to \R$ defined as:
:$\map {E_n} x = \paren {1 + \dfrac x n}^n$
Then, for each $x \in \R$ and for sufficiently large $n \in \N$, $\map {E_n} x$ is positive.
That is:
:$\forall x \in \R: \forall n \in \N: n \ge \ceiling {\size x} \implies \map {E_n} x > 0$
where $\ceiling x$ denotes the ceiling of $x$.

Proof:
Fix $x \in \R$.
Then:
{{begin-eqn}}
{{eqn | l = n
      | o = \ge
      | r = \ceiling {\size x}
}}
{{eqn | ll= \leadsto
      | l = n
      | o = >
      | r = -x
      | c = Real Number is between Ceiling Functions and Negative of Absolute Value
}}
{{eqn | ll= \leadsto
      | l = 1
      | o = >
      | r = \frac {-x} n
      | c = dividing both sides by $n$
}}
{{eqn | ll= \leadsto
      | l = 1 + \frac x n
      | o = >
      | r = 0
      | c = adding $\dfrac {-x} n$ to both sides
}}
{{eqn | ll= \leadsto
      | l = \paren {1 + \frac x n}^n
      | o = >
      | r = 0
      | c = Power of Strictly Positive Real Number is Strictly Positive: Positive Integer
}}
{{end-eqn}}
{{qed}}
Category:Exponential Function
8o42vr85nck3e24vs6153xttkzoezxv
Theorem: Number is between Ceiling and One Less

:$\ceiling x - 1 < x \le \ceiling x$

Proof:
By definition of ceiling of $x$:
:$\forall x \in \R: \ceiling x = \map \inf {\set {m \in \Z: m \ge x} }$
By definition of infimum:
:$\ceiling x \ge x$
Also by definition of infimum:
:$\ceiling x - 1 \not \ge x$
as $\ceiling x$ is the smallest integer with that property.
That is:
:$x > \ceiling x - 1$
Hence the result.
{{qed}}
Category:Ceiling Function
l75iq9rcega0z865kapwqgmw7httq2r
Theorem: Ceiling is between Number and One More

:$x \le \ceiling x < x + 1$
where $\ceiling x$ denotes the ceiling of $x$.

Proof:
From Number is between Ceiling and One Less:
:$\ceiling x - 1 < x \le \ceiling x$
Thus by adding $1$:
:$x + 1 > \paren {\ceiling x - 1} + 1 = \ceiling x$
So:
:$x \le \ceiling x$
and:
:$\ceiling x < x + 1$
as required.
{{qed}}
Theorem: Ceiling of Number plus Integer

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

Proof:
{{begin-eqn}}
{{eqn | l = \ceiling {x + n} - 1
      | o = <
      | m = x + n 
      | mo= \le
      | r = \ceiling {x + n}
      | c = Number is between Ceiling and One Less
}}
{{eqn | ll= \leadsto
      | l = \ceiling {x + n} - n - 1
      | o = <
      | m = x
      | mo= \le
      | r = \ceiling {x + n} - n
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \ceiling x
      | r = \ceiling {x + n} - n
      | c = Number is between Ceiling and One Less
}}
{{eqn | ll= \leadsto
      | l = \ceiling {x + n}
      | r = \ceiling x + n
      | c = adding $n$ to both sides
}}
{{end-eqn}}
{{qed}}
Theorem: Relation Segment of Auxiliary Relation is Ideal

Let $L = \struct {S, \vee, \preceq}$ be a bounded below join semilattice.
Let $R$ be auxiliary relation on $S$.
Let $x \in S$.
Then
:$x^R$ is ideal in $L$
where $x^R$ denotes the $R$-segment of $x$.

Proof:
=== Non-empty ===
By definition of auxiliary relation:
:$\tuple {\bot, x} \in R$
where $\bot$ denotes the smallest element in $L$.
By definition of relation segment:
:$\bot \in x^R$
Thus by definition:
:$x^R$ is non-empty.
{{qed|lemma}}
Theorem: Quotient of Modulo Operation with Modulus

Let $x, y \in \R$ be real numbers.
Let $x \bmod y$ denote the modulo operation:
:$x \bmod y := \begin{cases}
x - y \floor {\dfrac x y} & : y \ne 0 \\
x & : y = 0
\end{cases}$
where $\floor {\dfrac x y}$ denotes the floor of $\dfrac x y$.
Let $y \ne 0$.
Then:
:$0 \le \dfrac x y - \floor {\dfrac x y} = \dfrac {x \bmod y} y < 1$

Proof:
From Real Number minus Floor:
:$\dfrac x y - \floor {\dfrac x y} \in \hointr 0 1$
Thus by definition of half-open real interval:
:$0 \le \dfrac x y - \floor {\dfrac x y} < 1$
Then:
{{begin-eqn}}
{{eqn | l = x \bmod y
      | r = x - y \floor {\frac x y}
      | c = {{Defof|Modulo Operation}}
}}
{{eqn | ll= \leadsto
      | l = \frac {x \bmod y} y
      | r = \frac {x - y \floor {\dfrac x y} } y
      | c = 
}}
{{eqn | r = \frac x y - \frac y y \floor {\dfrac x y}
      | c = 
}}
{{eqn | r = \frac x y - \floor {\dfrac x y}
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Range of Modulo Operation for Positive Modulus

Let $x, y \in \R$ be real numbers.
Let $x \bmod y$ denote the modulo operation:
:$x \bmod y := \begin{cases}
x - y \floor {\dfrac x y} & : y \ne 0 \\
x & : y = 0
\end{cases}$
where $\floor {\dfrac x y}$ denotes the floor of $\dfrac x y$.
Let $y > 0$.
Then:
:$0 \le x \bmod y < y$

Proof:
{{begin-eqn}}
{{eqn | l = 0
      | o = \le
      | m = \frac {x \bmod y} y
      | mo= <
      | r = 1
      | c = Quotient of Modulo Operation with Modulus
}}
{{eqn | ll= \leadsto
      | l = 0
      | o = \le
      | m = \frac {x \bmod y} y \times y
      | mo= <
      | r = 1 \times y
      | c = Real Number Ordering is Compatible with Multiplication
}}
{{eqn | ll= \leadsto
      | l = 0
      | o = \le
      | m = x \bmod y
      | mo= <
      | r = y
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Range of Modulo Operation for Negative Modulus

Let $x, y \in \R$ be real numbers.
Let $x \bmod y$ denote the modulo operation:
:$x \bmod y := \begin{cases}
x - y \floor {\dfrac x y} & : y \ne 0 \\
x & : y = 0
\end{cases}$
where $\floor {\dfrac x y}$ denotes the floor of $\dfrac x y$.
Let $y < 0$.
Then:
:$0 \ge x \bmod y > y$

Proof:
{{begin-eqn}}
{{eqn | l = 0
      | o = \le
      | m = \frac {x \bmod y} y
      | mo= <
      | r = 1
      | c = Quotient of Modulo Operation with Modulus
}}
{{eqn | ll= \leadsto
      | l = 0
      | o = \ge
      | m = \frac {x \bmod y} y \times y
      | mo= >
      | r = 1 \times y
      | c = Real Number Ordering is Compatible with Multiplication
}}
{{eqn | ll= \leadsto
      | l = 0
      | o = \ge
      | m = x \bmod y
      | mo= >
      | r = y
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Zero is Integer Multiple of Zero

Zero is an integer multiple of zero.

Proof:
We have that:
:$0 \times 0 = 0$
The result follows by definition of integer multiple.
{{qed}}
Category:Number Theory
cr4qeo16keg2mqnhx82y0t2xypme5gz
Theorem: Number minus Modulo is Integer Multiple

Let $x, y \in \R$ be real numbers.
Let $x \bmod y$ denote the modulo operation:
:$x \bmod y := \begin{cases}
x - y \floor {\dfrac x y} & : y \ne 0 \\
x & : y = 0
\end{cases}$
where $\floor {\dfrac x y}$ denotes the floor of $\dfrac x y$.
Let $y < 0$.
Then:
:$x - \paren {x \bmod y}$
is an integer multiple of $y$.

Proof:
When $y = 0$ we have:
:$x \bmod y := x$
Thus:
:$x - \paren {x \bmod y} = 0$
From Zero is Integer Multiple of Zero it follows that:
:$x - \paren {x \bmod y}$
is an integer multiple of $y$.
Let $y \ne 0$.
Then:
{{begin-eqn}}
{{eqn | l = x \bmod y
      | r = x - y \floor {\dfrac x y}
      | c = {{Defof|Modulo Operation}}
}}
{{eqn | ll= \leadsto
      | l = x - \paren {x \bmod y}
      | r = y \floor {\dfrac x y}
      | c = {{Defof|Modulo Operation}}
}}
{{end-eqn}}
From Floor Function is Integer, $\floor {\dfrac x y}$ is an integer.
Thus:
:$\exists n \in \Z: x - \paren {x \bmod y} = n y$
where in the case $n = \floor {\dfrac x y}$
Hence the result by definition of integer multiple.
{{qed}}
Theorem: Modulo Operation/Examples/5 mod 3

:$5 \bmod 3 = 2$

Proof:
By definition of modulo operation:
:$x \bmod y := x - y \floor {\dfrac x y}$
for $y \ne 0$.
We have:
:$\dfrac 5 3 = 1 + \dfrac 2 3$
and so:
:$\floor {\dfrac 5 3} = 1$
Thus:
:$5 \bmod 3 = 5 - 3 \times \floor {\dfrac 5 3} = 5 - 3 \times 1 = 2$
{{qed}}
Theorem: Modulo Operation/Examples/18 mod 3

:$18 \bmod 3 = 0$

Proof:
By definition of modulo operation:
:$x \bmod y := x - y \floor {\dfrac x y}$
for $y \ne 0$.
We have:
:$\dfrac {18} 3 = 6 + \dfrac 0 3$
and so:
:$\floor {\dfrac {18} 3} = 6$
Thus:
:$18 \bmod 3 = 18 - 3 \times \floor {\dfrac {18} 3} = 18 - 3 \times 6 = 0$
{{qed}}
Theorem: Modulo Operation/Examples/-2 mod 3

:$-2 \bmod 3 = 1$

Proof:
By definition of modulo operation:
:$x \bmod y := x - y \floor {\dfrac x y}$
for $y \ne 0$.
We have:
:$\dfrac {-2} 3 = -1 + \dfrac 1 3$
and so:
:$\floor {\dfrac {-2} 3} = -1$
Thus:
:$-2 \bmod 3 = -2 - 3 \times \floor {\dfrac {-2} 3} = -2 - 3 \times \paren {-1} = 1$
{{qed}}
Theorem: Number is Divisor iff Modulo is Zero

Let $x, y \in \R$ be real numbers.
Let $x \bmod y$ denote the modulo operation:
:$x \bmod y := \begin {cases}
x - y \floor {\dfrac x y} & : y \ne 0 \\
x & : y = 0
\end {cases}$
where $\floor {\dfrac x y}$ denotes the floor of $\dfrac x y$.
Then $x \bmod y = 0$ {{iff}} $x$ is an integer multiple of $y$.

Proof:
=== Sufficient Condition ===
Let $x \bmod y = 0$.
From Number minus Modulo is Integer Multiple:
:$x - \paren {x \bmod y}$
is an integer multiple of $y$.
As $x \bmod y = 0$ it follows that $x - 0 = x$ is an integer multiple of $y$.
{{qed|lemma}}
Theorem: Correctness of Definition of Increasing Mappings Satisfying Inclusion in Lower Closure

Let $R = \struct {S, \preceq}$ be an ordered set.
Let $\map {\it Ids} R$ be the set of all ideals in $R$.
Let $L = \struct {\map {\it Ids} R, \precsim}$ be an ordered set
where $\precsim \mathop = \subseteq \restriction_{\map {\it Ids} R \times \map {\it Ids} R}$
Let:
:$M = \struct {F, \preccurlyeq}$
where:
:$F = \leftset {f: S \to \map {\it Ids} R: f} \,$ is an increasing mapping and $\rightset {\forall x \in S: \map f x \subseteq x^\preceq}$
:$\preccurlyeq$ is ordering on mappings generated by $\precsim$
:$x^\preceq$ denotes the lower closure of $x$.
Then $M$ is an ordered set.

Proof:
=== Reflexivity ===
Let $f \in F$.
By definition of reflexivity:
:$\forall x \in S: \map f x \precsim \map f x$
Thus by definition of ordering on mappings:
:$f \preccurlyeq f$
{{qed|lemma}}
Theorem: Number less than Integer iff Floor less than Integer

:$\floor x < n \iff x < n$

Proof:
=== Necessary Condition ===
Let $x < n$.
By definition of the floor of $x$:
:$\floor x \le x$
Hence:
:$\floor x < n$
{{qed|lemma}}
Theorem: Number not less than Integer iff Floor not less than Integer

:$x \ge n \iff \floor x \ge n$

Proof:
=== Necessary Condition ===
Let $\floor x \ge n$.
By definition of the floor of $x$:
:$x \ge \floor x$
Hence:
:$x \ge n$
{{qed|lemma}}
Theorem: Number not greater than Integer iff Ceiling not greater than Integer

:$\ceiling x \le n \iff x \le n$

Proof:
=== Necessary Condition ===
Let $\ceiling x \le n$.
By Number is between Ceiling and One Less:
:$x \le \ceiling x$
Hence:
:$x \le n$
{{qed|lemma}}
Theorem: Number greater than Integer iff Ceiling greater than Integer

:$\ceiling x > n \iff x > n$

Proof:
=== Necessary Condition ===
Let $x > n$.
By Number is between Ceiling and One Less:
:$\ceiling x \ge x$
Hence:
:$\ceiling x > n$
{{qed|lemma}}
Theorem: Integer equals Floor iff between Number and One Less

:$\floor x = n \iff x - 1 < n \le x$

Proof:
=== Necessary Condition ===
Let $x - 1 < n \le x$.
From $n \le x$, we have by Number not less than Integer iff Floor not less than Integer:
:$n \le \floor x$
From $x - 1 < n$:
:$x < n + 1$
Hence by Number less than Integer iff Floor less than Integer:
:$\floor x < n + 1$
We have that:
:$\forall m, n \in \Z: m \le n \iff m < n + 1$
and so:
:$\floor x \le n$
Thus as:
:$n \le \floor x$
and:
:$\floor x \le n$
it follows that:
:$\floor x = n$
{{qed|lemma}}
Theorem: Integer equals Floor iff Number between Integer and One More

:$\floor x = n \iff n \le x < n + 1$

Proof:
=== Necessary Condition ===
Let $n \le x < n + 1$.
From Number not less than Integer iff Floor not less than Integer:
:$n \le x \implies n \le \floor x$
By definition of the floor of $x$:
:$\floor x \le x$
and so by hypothesis:
:$\floor x < n + 1$
We have that:
:$\forall m, n \in \Z: m \le n \iff m < n + 1$
and so:
:$\floor x \le n$
So we have:
:$n \le \floor x$
and:
:$\floor x \le n$
Thus:
:$n \le x < n + 1 \implies \floor x = n$
{{qed|lemma}}
Theorem: Integer equals Ceiling iff between Number and One More

:$\ceiling x = n \iff x \le n < x + 1$

Proof:
=== Necessary Condition ===
Let $x \le n < x + 1$.
From $x \le n$, we have by Number not greater than Integer iff Ceiling not greater than Integer:
:$\ceiling x \le n$
From $n < x + 1$:
:$n - 1 < x$
Hence by Number greater than Integer iff Ceiling greater than Integer:
:$n - 1 < \ceiling x$
We have that:
:$\forall m, n \in \Z: m < n \iff m \le n - 1$
and so:
:$n \le \ceiling x$
Thus as:
:$\ceiling x \le n$
and:
:$\ceiling x \ge n$
it follows that:
:$\ceiling x = n$
{{qed|lemma}}
Theorem: Integer equals Ceiling iff Number between Integer and One Less

:$\ceiling x = n \iff n - 1 < x \le n$

Proof:
=== Necessary Condition ===
Let $n - 1 < x \le n$.
From Number not greater than Integer iff Ceiling not greater than Integer:
:$x \le n \implies \ceiling x \le n$
From Number is between Ceiling and One Less:
:$x \le \ceiling x$
and so:
:$n - 1 < \ceiling x$
We have that:
:$\forall m, n \in \Z: m - 1 < n \iff m \le n$
and so:
:$n \le \ceiling x$
So we have:
:$\ceiling x \le n$
and:
:$n \le \ceiling x$
Thus:
:$n - 1 < x \le n \implies \ceiling x = n$
{{qed|lemma}}
Theorem: Floor of Root of Floor equals Floor of Root

:$\ds \floor {\sqrt {\floor x} } = \floor {\sqrt x}$

Proof:
The square root is defined on the interval $\hointr 0 \to$.
We have that Square Root is Strictly Increasing.
From Continuity of Root Function, the square root is continuous.
Hence the conditions are fulfilled for for McEliece's Theorem (Integer Functions) to be applied:
:$\forall x \in A: \paren {\map f x \in \Z \implies x \in \Z} \iff \floor {\map f x} = \floor {\map f {\floor x} }$
It remains to be proved that $\sqrt x \in \Z \implies x \in \Z$.
Let $y = \sqrt x$ such that $y \in \Z$.
By definition of the square root:
:$x = y^2$.
From Integer Multiplication is Closed:
:$x \in \Z$
as required.
{{qed}}
Theorem: Ceiling of Root of Ceiling equals Ceiling of Root

:$\ds \ceiling {\sqrt {\ceiling x} } = \ceiling {\sqrt x}$

Proof:
The square root is defined on the interval $\hointr 0 \to$.
We have that Square Root is Strictly Increasing.
From Continuity of Root Function, the square root is continuous.
Hence the conditions are fulfilled for for McEliece's Theorem (Integer Functions) to be applied:
:$\forall x \in A: \paren {\map f x \in \Z \implies x \in \Z} \iff \ceiling {\map f x} = \ceiling {\map f {\ceiling x} }$
It remains to be proved that $\sqrt x \in \Z \implies x \in \Z$.
Let $y = \sqrt x$ such that $y \in \Z$.
By definition of square root:
:$x = y^2$
From Integer Multiplication is Closed:
:$x \in \Z$
as required.
{{qed}}
Theorem: Congruence by Divisor of Modulus/Integer Modulus

Let $r, s \in \Z$ be integers.
Let $a, b \in \Z$ such that $a$ is congruent modulo $r s$ to $b$, that is:
:$a \equiv b \pmod {r s}$
Then:
:$a \equiv b \pmod r$
and:
:$a \equiv b \pmod s$

Proof:
{{begin-eqn}}
{{eqn | l = a
      | o = \equiv
      | r = b
      | rr= \pmod {r s}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a - b
      | r = q r s
      | c = {{Defof|Congruence Modulo Integer}}
}}
{{eqn | ll= \leadsto
      | l = a - b
      | r = \paren {q r} s
      | c = 
}}
{{eqn | lo= \land
      | l = a - b
      | r = \paren {q s} r
      | c = 
}}
{{eqn | l = a
      | o = \equiv
      | r = b
      | rr= \pmod r
      | c = {{Defof|Congruence Modulo Integer}}: $q s$ is an integer
}}
{{eqn | lo= \land
      | l = a
      | o = \equiv
      | r = b
      | rr= \pmod s
      | c = {{Defof|Congruence Modulo Integer}}: $q r$ is an integer
}}
{{end-eqn}}
{{qed}}
Theorem: Modulo Addition is Well-Defined/Real Modulus

Let $z \in \R$ be a real number.
{{Explain|What if z is zero?}}
Let:
:$a \equiv b \pmod z$
and:
:$x \equiv y \pmod z$
where $a, b, x, y \in \R$.
Then:
: $a + x \equiv b + y \pmod z$

Proof:
{{begin-eqn}}
{{eqn | l = a
      | o = \equiv
      | r = b
      | rr= \pmod z
      | c =
}}
{{eqn | l = c
      | o = \equiv
      | r = d
      | rr= \pmod z
      | c =
}}
{{eqn | ll= \leadsto
      | l = a \bmod z
      | r = b \bmod z
      | c = {{Defof|Congruence (Number Theory)|Congruence}}
}}
{{eqn | l = x \bmod z
      | r = y \bmod z
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists k_1 \in \Z
      | l = a - b
      | r = k_1 z
      | c = 
}}
{{eqn | q = \exists k_2 \in \Z
      | l = x - y
      | r = k_2 z
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {a + x} - \paren {b + y}
      | r = \paren {k_1 + k_2} z
      | c = {{Defof|Integer Addition}}
}}
{{eqn | ll= \leadsto
      | l = a + x
      | o = \equiv
      | r = b + y
      | rr= \pmod z
      | c = {{Defof|Congruence (Number Theory)|Congruence}}
}}
{{end-eqn}}
{{qed}}
Theorem: Modulo Multiplication is Well-Defined/Warning

Let $z \in \R$ be a real number.
Let:
:$a \equiv b \pmod z$
and:
:$x \equiv y \pmod z$
where $a, b, x, y \in \R$.
Then it does '''not''' necessarily hold that:
:$a x \equiv b y \pmod z$

Proof:
{{begin-eqn}}
{{eqn | l = a
      | o = \equiv
      | r = b
      | rr= \pmod m
      | c = 
}}
{{eqn | l = x
      | o = \equiv
      | r = y
      | rr= \pmod m
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a \bmod m
      | r = b \bmod m
      | c = {{Defof|Congruence (Number Theory)|Congruence}}
}}
{{eqn | l = x \bmod m
      | r = y \bmod m
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists k_1 \in \Z
      | l = a
      | r = b + k_1 z
      | c = 
}}
{{eqn | q = \exists k_2 \in \Z
      | l = x
      | r = y + k_2 z
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a x
      | r = \paren {b + k_1 z} \paren {y + k_2 z}
      | c = {{Defof|Multiplication}}
}}
{{eqn | r = b y + b k_2 z + y k_1 z + k_1 k_2 z^2
      | c = Integer Multiplication Distributes over Addition
}}
{{eqn | r = b y + \paren {b k_2 + y k_1 + k_1 k_2 z} z
      | c = 
}}
{{end-eqn}}
But it is not necessarily the case that:
:$b k_2 + y k_1 + k_1 k_2 z$
is an integer.
In fact, $b k_2 + y k_1 + k_1 k_2 z$ can only be ''guaranteed'' to be an integer if each of $b, y, z \in \Z$.
Hence $a b$ is not necessarily congruent to $x y$.
{{qed}}
Theorem: Congruence by Product of Moduli/Real Modulus

Let $a, b, z \in \R$.
Let $a \equiv b \pmod z$ denote that $a$ is congruent to $b$ modulo $z$.
Then $\forall y \in \R, y \ne 0$:
:$a \equiv b \pmod z \iff y a \equiv y b \pmod {y z}$

Proof:
Let $y \in \R: y \ne 0$.
Then:
{{begin-eqn}}
{{eqn | l = a
      | o = \equiv
      | r = b
      | rr= \pmod z
      | c =
}}
{{eqn | ll= \leadstoandfrom
      | l = a \bmod z
      | r = b \bmod z
      | c = {{Defof|Congruence (Number Theory)|Congruence}}
}}
{{eqn | ll= \leadstoandfrom
      | l = y \paren {a \bmod z}
      | r = y \paren {b \bmod z}
      | c = Left hand implication valid only when $y \ne 0$
}}
{{eqn | ll= \leadstoandfrom
      | l = \paren {y a} \bmod \paren {y z}
      | r = \paren {y b} \bmod \paren {y z}
      | c = Product Distributes over Modulo Operation
}}
{{eqn | l = y a
      | o = \equiv
      | r = y b
      | rr= \pmod {y z}
      | c = {{Defof|Congruence (Number Theory)|Congruence}}
}}
{{end-eqn}}
Hence the result.
Note the invalidity of the third step when $y = 0$.
{{qed}}
Theorem: Segment of Auxiliary Relation is Subset of Lower Closure

Let $\struct {S, \vee, \preceq}$ be a bounded below join semilattice.
Let $R$ be auxiliary relation on $S$.
Let $x \in S$.
Then
:$x^R \subseteq x^\preceq$
where
:$x^R$ denotes the $R$-segment of $x$,
:$x^\preceq$ denotes the lower closure of $x$.

Proof:
Let $a \in x^R$.
By definition of $R$-segment of $x$:
:$\tuple {a, x} \in R$
By definition of auxiliary relation:
:$a \preceq x$
Thus by definition of lower closure of element:
:$a \in x^\preceq$
{{qed}}
Theorem: Power Function is Completely Multiplicative/Integers

Let $c \in \Z$ be an integer.
Let $f_c: \Z \to \Z$ be the mapping defined as:
:$\forall n \in \Z: \map {f_c} n = n^c$
Then $f_c$ is completely multiplicative.

Proof:
Let $r, s \in \Z$.
Then:
{{begin-eqn}}
{{eqn | l = \map {f_c} {r s}
      | r = \paren {r s}^c
      | c = 
}}
{{eqn | r = r^c s^c
      | c = Product of Powers
}}
{{eqn | r = \map {f_c} r \map {f_c} s
      | c = 
}}
{{end-eqn}}
{{Qed}}
Theorem: Preceding implies Inclusion of Segments of Auxiliary Relation

Let $\left({S, \vee, \preceq}\right)$ be a bounded below join semilattice.
Let $R$ be an auxiliary relation on $S$.
Let $x, y \in S$ such that
:$x \preceq y$
Then
:$x^R \subseteq y^R$
where $x^R$ denotes the $R$-segment of $x$.

Proof:
Let $a \in x^R$.
By definition of $R$-segment of $x$:
:$\left({a, x}\right) \in R$
By definition of reflexivity:
:$a \preceq a$
By definition of auxiliary relation:
:$\left({a, y}\right) \in R$
Thus by definition of $R$-segment of $y$:
:$a \in y^R$
{{qed}}
Theorem: Characteristic Function of Square-Free Integers is Multiplicative

Let $S \subseteq \Z$ be the set of positive integers defined as:
:$S := \set {n \in \Z: \forall k \in \Z_{>1}: k^2 \nmid n}$
That is, let $S$ be the set of all square-free positive integers.
Let $\chi_S: \N \to \Z$ denote the characteristic function of $S$:
:$\forall n \in \Z: \map {\chi_S} n = \sqbrk {n \in S}$
where $\sqbrk {n \in S}$ is Iverson's convention.
Then $\chi_S$ is multiplicative.

Proof:
Let $r, s \in \Z$ such that $r \perp s$.
Theorem: Segment of Auxiliary Relation Mapping is Increasing

Let $R = \left({S, \preceq}\right)$ be an ordered set.
Let ${\it Ids}\left({R}\right)$ be the set of all ideals in $R$.
Let $L = \left({ {\it Ids}\left({R}\right), \precsim}\right)$ be an ordered set
where $\precsim \mathop = \subseteq\restriction_{ {\it Ids}\left({R}\right) \times {\it Ids}\left({R}\right)}$
Let $r$ be an auxiliary relation on $S$.
Let $f: S \to {\it Ids}\left({R}\right)$ be a mapping such that
:$\forall x \in S: f\left({x}\right) = x^r$
where $x^r$ denotes the $r$-segment of $x$.
Then
:$f$ is increasing mapping.

Proof:
$f$ is well-defined because by Relation Segment of Auxiliary Relation is Ideal:
:$\forall x \in S: x^r$ is ideal in $L$
Let $x, y \in S$ such that
:$x \preceq y$
By Preceding implies Inclusion of Segments of Auxiliary Relation:
:$x^r \subseteq y^r$
Thus by definitions of $\precsim$ and $f$:
:$f\left({x}\right) \precsim f\left({y}\right)$
Thus by definition:
:$f$ is increasing mapping.
{{qed}}