avewright/proofwiki-math huggingface dataset:
Theorem: Conditions for Floor of Log base b of x to equal Floor of Log base b of Floor of x

Let $b \in \R$ be a real number.
:$\forall x \in \R_{\ge 1}: \floor {\log_b x} = \floor {\log_b \floor x} \iff b \in \Z_{> 1}$
where $\floor x$ denotes the floor of $x$.

Proof:
=== Necessary Condition ===
Let:
:$\forall x \in \R_{\ge 1}: \floor {\log_b x} = \floor {\log_b \floor x}$
Let $x = b$.
Then:
:$\floor {\log_b b} = \floor {\log_b \floor b}$
{{begin-eqn}}
{{eqn | l = \floor {\log_b b}
      | r = \floor {\log_b \floor b}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \floor 1
      | r = \floor {\log_b \floor b}
      | c = Logarithm of Base
}}
{{eqn | ll= \leadsto
      | l = 1
      | r = \floor {\log_b \floor b}
      | c = Real Number is Integer iff equals Floor
}}
{{end-eqn}}
{{AimForCont}} $b \notin \Z$.
{{begin-eqn}}
{{eqn | l = \floor b
      | o = <
      | r = b
      | c = Floor of Non-Integer
}}
{{eqn | ll= \leadsto
      | l = \log_b \floor b
      | o = <
      | r = 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \floor {\log_b \floor b}
      | o = <
      | r = \floor {\log_b b}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \floor {\log_b \floor b}
      | o = \ne
      | r = \floor {\log_b b}
      | c = which contradicts $\floor {\log_b b} = \floor {\log_b \floor b}$
}}
{{end-eqn}}
Thus by Proof by Contradiction:
:$b \in \Z$
But for $\log_b$ to be defined, $b > 0$ and $b \ne 1$.
Hence:
:$b \in \Z_{> 1}$
{{qed|lemma}}
=== Sufficient Condition ===
Let $b \in \Z_{> 1}$.
Let $\floor {\log_b x} = n$.
Then:
{{begin-eqn}}
{{eqn | l = n
      | m = \floor {\log_b x}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = n
      | o = \le
      | m = \log_b x
      | mo= <
      | r = n + 1
      | c = Integer equals Floor iff Number between Integer and One More
}}
{{eqn | ll= \leadstoandfrom
      | l = b^n
      | o = \le
      | m = x
      | mo= <
      | r = b^{n + 1}
      | c = Power Function is Strictly Increasing over Positive Reals
}}
{{eqn | ll= \leadstoandfrom
      | l = b^n
      | o = \le
      | m = \floor x
      | mo= <
      | r = b^{n + 1}
      | c = Number not less than Integer iff Floor not less than Integer
}}
{{eqn | ll= \leadstoandfrom
      | l = n
      | o = \le
      | m = \log_b \floor x
      | mo= <
      | r = n + 1
      | c = Power Function is Strictly Increasing over Positive Reals
}}
{{eqn | ll= \leadstoandfrom
      | l = n
      | m = \floor {\log_b \floor x}
      | c = Integer equals Floor iff Number between Integer and One More
}}
{{eqn | ll= \leadstoandfrom
      | l = \floor {\log_b x}
      | m = \floor {\log_b \floor x}
      | c = Definition of $n$
}}
{{end-eqn}}
{{qed}}
Theorem: Conditions for Floor of Log base b of x to equal Floor of Log base b of Floor of x

Let $b \in \R$ be a real number.
:$\forall x \in \R_{\ge 1}: \floor {\log_b x} = \floor {\log_b \floor x} \iff b \in \Z_{> 1}$
where $\floor x$ denotes the floor of $x$.

Proof:
We have that:
:Logarithm is Strictly Increasing
and:
:Real Natural Logarithm Function is Continuous
Suppose that $\log_b x \in \Z$: let $\log_b x = n$, say.
Then:
:$x = b^n$
It follows that:
:$x \in \Z \iff b \in \Z$
Thus by McEliece's Theorem (Integer Functions):
:$\forall x \in \R_{\ge 1}: \floor {\log_b x} = \floor {\log_b \floor x} \iff b \in \Z_{>1}$
{{qed}}
Theorem: Floor of x+m over n

Let $m, n \in \Z$ such that $n > 0$.
Let $x \in \R$.
Then:
:$\floor {\dfrac {x + m} n} = \floor {\dfrac {\floor x + m} n}$
where $\floor x$ denotes the floor of $x$.

Proof:
Let:
:$y = x - \floor x$
:$M = \floor x + m$
We now have:
:$(1): \quad 0 \le y < 1$
and thus:
:$\floor y = 0$
By Division Theorem, we can write:
:$(2): \quad M = k n + r$
with $k \in \Z$ and $0 \le r \le n - 1$.
By $(1)$ and $(2)$:
:$(3): \quad 0 \le y + r < 1 + n - 1 = n$
We have:
{{begin-eqn}}
{{eqn | l = \floor {\frac {y + M} n}
      | r = \floor {\frac {y + k n + r} n}
      | c = from $(2)$
}}
{{eqn | r = \floor {k + \frac {y + r} n}
      | c = 
}}
{{eqn | r = k + \floor {\frac {y + r} n}
      | c = Floor of Number plus Integer
}}
{{eqn | r = k
      | c = from $(3)$
}}
{{eqn | r = \floor {\frac M n}
      | c = 
}}
{{end-eqn}}
Substituting $y$ and $M$, we obtain:
{{begin-eqn}}
{{eqn | l = \floor {\frac {x + m} n}
      | r = \floor {\frac {x - \floor x + \floor x + m} n}
      | c = 
}}
{{eqn | r = \floor {\frac {y + M} n}
      | c = 
}}
{{eqn | r = \floor {\frac M n}
      | c = 
}}
{{eqn | r = \floor {\frac {\floor x + m} n}
      | c = 
}}
{{end-eqn}}
and the result follows.
{{qed}}
Theorem: Floor of x+m over n

Let $m, n \in \Z$ such that $n > 0$.
Let $x \in \R$.
Then:
:$\floor {\dfrac {x + m} n} = \floor {\dfrac {\floor x + m} n}$
where $\floor x$ denotes the floor of $x$.

Proof:
Let $f: \R \to \R$ be the real function defined as:
:$\forall x \in \R: \map f x = \dfrac {x + m} n$
It is clear that $f$ is both strictly increasing and continuous on the whole of $\R$.
Let $\dfrac {x + m} n \in \Z$.
Then:
{{begin-eqn}}
{{eqn | q = \exists s \in \Z
      | l = \dfrac {x + m} n
      | r = s
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x + m
      | r = n s
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = n s - m
      | c = 
}}
{{eqn | o = \in
      | r = \Z
      | c = 
}}
{{end-eqn}}
Thus:
:$\forall x \in \R: \map f x \in \Z \implies x \in \Z$
So the conditions are fulfilled for McEliece's Theorem (Integer Functions) to be applied:
:$\floor {\map f x} = \floor {\map f {\floor x} } \iff \paren {\map f x \in \Z \implies x \in \Z}$
Hence the result.
{{qed}}
Theorem: McEliece's Theorem (Integer Functions)

Let $f: \R \to \R$ be a continuous, strictly increasing real function defined on an interval $A$.
Let:
:$\forall x \in A: \floor x \in A \text { and } \ceiling x \in A$
where:
:$\floor x$ denotes the floor of $x$
:$\ceiling x$ denotes the ceiling of $x$
Then:
:$\forall x \in A: \paren {\map f x \in \Z \implies x \in \Z} \iff \floor {\map f x} = \floor {\map f {\floor x} }$
:$\forall x \in A: \paren {\map f x \in \Z \implies x \in \Z} \iff \ceiling {\map f x} = \ceiling {\map f {\ceiling x} }$

Proof:
Let $x \in A$.
Hence {{hypothesis}} we have that both $\floor x \in A$ and $\ceiling x \in A$.
Theorem: Ceiling of Non-Integer

Let $x \in \R$ be a real number.
Let $x \notin \Z$.
Then:
:$\ceiling x > x$
where $\ceiling x$ denotes the ceiling  of $x$.

Proof:
From Ceiling is between Number and One More:
:$\ceiling x \ge x$
From Real Number is Integer iff equals Ceiling:
:$x = \ceiling x \iff x \in \Z$
But we have $x \notin \Z$.
So:
:$\ceiling x \ne x$
and so:
:$\ceiling x > x$
{{qed}}
Theorem: Ceiling of x+m over n

Let $m, n \in \Z$ such that $n > 0$.
Let $x \in \R$.
Then:
:$\ceiling {\dfrac {x + m} n} = \ceiling {\dfrac {\ceiling x + m} n}$
where $\ceiling x$ denotes the ceiling of $x$.

Proof:
{{begin-eqn}}
{{eqn | l = \ceiling {\dfrac {x + m} n}
      | r = -\floor {-\dfrac {x + m} n}
      | c = Floor of Negative equals Negative of Ceiling
}}
{{eqn | r = -\floor {\dfrac {-x - m} n}
      | c = 
}}
{{eqn | r = -\floor {\dfrac {\floor {-x} - m} n}
      | c = Floor of $\dfrac {x + m} n$
}}
{{eqn | r = -\floor {\dfrac {-\ceiling x - m} n}
      | c = Floor of Negative equals Negative of Ceiling
}}
{{eqn | r = -\floor {-\dfrac {\ceiling x + m} n}
      | c = 
}}
{{eqn | r = \ceiling {\dfrac {\ceiling x + m} n}
      | c = Floor of Negative equals Negative of Ceiling
}}
{{end-eqn}}
{{qed}}
Theorem: Ceiling of x+m over n

Let $m, n \in \Z$ such that $n > 0$.
Let $x \in \R$.
Then:
:$\ceiling {\dfrac {x + m} n} = \ceiling {\dfrac {\ceiling x + m} n}$
where $\ceiling x$ denotes the ceiling of $x$.

Proof:
Let $f: \R \to \R$ be the real function defined as:
:$\forall x \in \R: \map f x = \dfrac {x + m} n$
It is clear that $f$ is both strictly increasing and continuous on the whole of $\R$.
Let $\dfrac {x + m} n \in \Z$.
Then:
{{begin-eqn}}
{{eqn | q = \exists s \in \Z
      | l = \dfrac {x + m} n
      | r = s
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x + m
      | r = n s
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = n s - m
      | c = 
}}
{{eqn | o = \in
      | r = \Z
      | c = 
}}
{{end-eqn}}
Thus:
:$\forall x \in \R: \map f x \in \Z \implies x \in \Z$
So the conditions are fulfilled for McEliece's Theorem (Integer Functions) to be applied:
:$\ceiling {\map f x} = \ceiling {\map f {\ceiling x} } \iff \paren {\map f x \in \Z \implies x \in \Z}$
Hence the result.
{{qed}}
Theorem: Summation over k of Floor of x plus k over y

Let $x, y \in \R$ such that $y > 0$.
Then:
:$\ds \sum_{0 \mathop \le k \mathop < y} \floor {x + \dfrac k y} = \floor {x y + \floor {x + 1} \paren {\ceiling y - y} }$

Proof:
When $x$ increases by $1$, both sides increase by $\ceiling y$.
So we can assume $0 \le x < 1$.
When $x = 0$, both sides are equal to $0$.
When $x$ increases past $1 - \dfrac k y$ for $0 \le k < y$, both sides increase by $1$.
Hence the result.
{{qed}}
Theorem: Summation over k of Ceiling of mk+x over n

Let $m, n \in \Z$ such that $n > 0$.
Let $x \in \R$.
Then:
:$\ds \sum_{0 \mathop \le k \mathop < n} \ceiling {\dfrac {m k + x} n} = \dfrac {\paren {m + 1} \paren {n - 1} } 2 - \dfrac {d - 1} 2 + d \ceiling {\dfrac x d}$
where:
:$\ceiling x$ denotes the ceiling of $x$
:$d$ is the greatest common divisor of $m$ and $n$.

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{0 \mathop \le k \mathop < n} \ceiling {\dfrac {m k + x} n}
      | r = \sum_{0 \mathop \le k \mathop < n} \paren {-\floor {-\dfrac {m k + x} n} }
      | c = Floor of Negative equals Negative of Ceiling
}}
{{eqn | r = -\sum_{0 \mathop \le k \mathop < n} \floor {\dfrac {-m k - x} n}
      | c = 
}}
{{eqn | r = -\paren {\dfrac {\paren {\paren {-m} - 1} \paren {n - 1} } 2 + \dfrac {d - 1} 2 + d \floor {\dfrac {\paren {-x} } d} }
      | c = Summation over $k$ of $\floor {\dfrac {m k + x} n}$
}}
{{eqn | r = \dfrac {\paren {m + 1} \paren {n - 1} } 2 - \dfrac {d - 1} 2 - d \floor {-\dfrac x d}
      | c = 
}}
{{eqn | r = \dfrac {\paren {m + 1} \paren {n - 1} } 2 - \dfrac {d - 1} 2 + d \ceiling {\dfrac x d}
      | c = Floor of Negative equals Negative of Ceiling
}}
{{end-eqn}}
{{qed}}
Theorem: Semantic Consequence preserved in Supersignature

Let $\LL, \LL'$ be signatures for the language of predicate logic.
Let $\LL'$ be a supersignature of $\LL$.
Let $\mathbf A$ be an $\LL$-sentence.
Let $\Sigma$ be a set of $\LL$-sentences.
Then the following are equivalent:
:$\AA \models_{\mathrm{PL} } \mathbf A$ for all $\LL$-structures $\AA$ for which $\AA \models_{\mathrm{PL} } \Sigma$
:$\AA' \models_{\mathrm{PL} } \mathbf A$ for all $\LL'$-structures $\AA'$ for which $\AA' \models_{\mathrm{PL} } \Sigma$
where $\models_{\mathrm{PL} }$ denotes the models relation.
That is to say, the notion of semantic consequence is preserved in passing to a supersignature.

Proof:
{{finish|
* every $\AA$ arises as the reduct of some $\AA'$;
* every $\AA'$ has the same valuations as its reduct.
}}
Theorem: Satisfiability preserved in Supersignature

Let $\LL, \LL'$ be signatures for the language of predicate logic.
Let $\LL'$ be a supersignature of $\LL$.
Let $\Sigma$ be a set of $\LL$-sentences.
Then the following are equivalent:
:$\AA \models_{\mathrm{PL} } \Sigma$ for some $\LL$-structure $\AA$
:$\AA' \models_{\mathrm{PL} } \Sigma$ for some $\LL'$-structure $\AA'$
where $\models_{\mathrm{PL} }$ is the models relation.
That is to say, the notion of satisfiability is preserved in passing to a supersignature.

Proof:
{{finish|* every $\AA$ arises as the reduct of some $\AA'$;
* every $\AA'$ has the same valuations as its reduct.
}}
Theorem: Floor Function is Replicative

The floor function is a replicative function in the sense that:
:$\ds \forall n \in \Z_{> 0}: \sum_{k \mathop = 0}^{n - 1} \floor {x + \frac k n} = \floor {n x}$

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 0}^{n - 1} \floor {x + \dfrac k n}
      | r = \floor {x n + \floor {x + 1} \paren {\ceiling n - n} }
      | c =  Summation over $k$ of $\floor {x + \dfrac k y}$, setting $y = n$
}}
{{eqn | r = \floor {x n + \floor {x + 1} \paren {n - n} }
      | c = Real Number is Integer iff equals Ceiling
}}
{{eqn | r = \floor {n x + \floor {x + 1} \times 0}
      | c = 
}}
{{eqn | r = \floor {n x}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Subtract Half is Replicative Function

Let $f: \R \to \R$ be the real function defined as:
:$\forall x \in \R: \map f x = x - \dfrac 1 2$
Then $f$ is a replicative function.

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 0}^{n - 1} \map f {x + \frac k n}
      | r = \sum_{k \mathop = 0}^{n - 1} \paren {x - \frac 1 2 + \frac k n}
      | c = 
}}
{{eqn | r = n x - \frac n 2 + \frac 1 n \sum_{k \mathop = 0}^{n - 1} k
      | c = 
}}
{{eqn | r = n x - \frac n 2 + \frac 1 n \frac {n \paren {n - 1} } 2
      | c = Closed Form for Triangular Numbers
}}
{{eqn | r = n x - \frac n 2 + \frac n 2 - \frac 1 2
      | c = 
}}
{{eqn | r = n x - \frac 1 2
      | c = 
}}
{{eqn | r = \map f {n x}
      | c = 
}}
{{end-eqn}}
Hence the result by definition of replicative function.
{{qed}}
Theorem: Membership of Set of Integers is Replicative Function

Let $f: \R \to \R$ be the real function defined as:
:$\forall x \in \R: \map f x = \sqbrk {x \in \Z}$
where $\sqbrk {\cdots}$ is Iverson's convention.
Then $f$ is a replicative function.

Proof:
First note that the interval between $x$ and $x + \dfrac {n - 1} n$ is less than $1$.
Thus there can be no more than one $k$ such that $0 \le k < n$ such that:
:$x + \dfrac k n \in \Z$
Hence:
:$\ds \sum_{k \mathop = 0}^{n - 1} \sqbrk {x + \frac k n \in \Z} \le 1$
First let:
:$\ds \sum_{k \mathop = 0}^{n - 1} \sqbrk {x + \frac k n \in \Z} = 1$
Then:
{{begin-eqn}}
{{eqn | l = x + \frac k n
      | o = \in 
      | r = \Z
      | c = 
}}
{{eqn | ll= \leadsto
      | l = n \paren {x + \frac k n}
      | o = \in 
      | r = \Z
      | c = 
}}
{{eqn | ll= \leadsto
      | l = n x + k
      | o = \in 
      | r = \Z
      | c = 
}}
{{eqn | ll= \leadsto
      | l = n x
      | o = \in 
      | r = \Z
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sqbrk {n x \in \Z}
      | r = 1
      | c = 
}}
{{end-eqn}}
{{qed|lemma}}
Let:
:$\ds \sum_{k \mathop = 0}^{n - 1} \sqbrk {x + \frac k n \in \Z} = 0$
{{AimForCont}} $\sqbrk {n x \in \Z} = 1$.
Then:
{{begin-eqn}}
{{eqn | l = n x
      | o = \in
      | r = \Z
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \forall k \in \Z
      | l = n x + k
      | o = \in
      | r = \Z
      | c = 
}}
{{end-eqn}}
But at least one $n x + k$ such that $0 \le k < n$ is a multiple of $n$.
Hence:
:$\exists k \in \Z: 0 \le k < n: \sqbrk {x + \dfrac k n \in \Z} = 1$
So:
:$\ds \sum_{k \mathop = 0}^{n - 1} \sqbrk {x + \frac k n \in \Z} = 1$
which contradicts the supposition that $\sqbrk {n x \in \Z} = 1$.
Hence the result by definition of replicative function.
{{qed}}
Theorem: Membership of Set of Strictly Positive Integers is Replicative Function

Let $f: \R \to \R$ be the real function defined as:
:$\forall x \in \R: \map f x = \sqbrk {x \in \Z_{> 0} }$
where $\sqbrk \cdots$ is Iverson's convention.
Then $f$ is a replicative function.

Proof:
Let $x \in \R$ such that $x > 0$.
Then for all $k \in \Z$ such that $0 \le k < n$:
:$x + \dfrac k n \in \Z_{> 0}$
and so from Membership of Set of Integers is Replicative Function:
:$\ds \sum_{k \mathop = 0}^{n - 1} \sqbrk {x + \frac k n \in \Z_{> 0} } = \sqbrk {n x \in \Z_{> 0} }$
Let $x \le 0$.
Then for all $k \in \Z$ such that $0 \le k < n$:
:$x + \dfrac k n < 1$
and so:
:$\ds \sum_{k \mathop = 0}^{n - 1} \sqbrk {x + \frac k n \in \Z_{> 0} } = 0 = \sqbrk {n x \in \Z_{> 0} }$
{{qed}}
Theorem: Membership of Equivalence Class of m mod pi is Replicative Function

Let $f: \R \to \R$ be the real function defined as:
:$\forall x \in \R: \map f x = \sqbrk {\exists r \in \Q, \exists m \in \Z: x = r \pi + m}$
where $\sqbrk {\cdots}$ is Iverson's convention.
Then $f$ is a replicative function.

Proof:
Let $\map f x = 1$.
Then:
:$\exists r \in \Q, \exists m \in \Z: x = r \pi + m$
and:
{{begin-eqn}}
{{eqn | l = x
      | r = r \pi + m
      | c = 
}}
{{eqn | ll= \leadsto
      | l = n x
      | r = \paren {r n} \pi + m n
      | c = 
}}
{{end-eqn}}
But $r n \in \Q$ and $m n \in \Z$.
So:
:$\map f x = 1 \implies \map f {n x} = 1$
Let $n \in \Z_{>0}$.
Let $k \in \Z: 0 \le k < n$.
Then:
{{begin-eqn}}
{{eqn | l = x + \frac k n
      | r = r \pi + m + \frac k n 
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x + \frac k n
      | r = \paren {r + \frac {k \pi} n} \pi + m
      | c = 
}}
{{end-eqn}}
Thus, when $0 \le k < n$ it follows that the coefficient of $\pi$ cannot be rational.
Thus:
:$\map f x = 1 \implies \map f {x + \dfrac k n} = 0$
and so:
:$\ds \sum_{k \mathop = 0}^{n - 1} \map f {x + \frac k n} = \map f {n x}$
{{qed|lemma}}
Now let $\map f {n x} = 1$.
Then:
:$r_n \pi + m_n = n x$
for some rational $r_n$ and integer $m_n$.
Thus exactly one of $m_n + k$ where $0 \le n < k$ is a multiple of $n$.
Therefore there exists exactly one $k \in \Z$ such that $0 \le n < k$ such that:
:$\map f {x + \dfrac k n} = 1$
Therefore:
:$\ds \sum_{k \mathop = 0}^{n - 1} \map f {x + \frac k n} = 1 = \map f {n x}$
Hence the result by definition of replicative function.
{{qed}}
Theorem: Logarithm of Absolute Value of 2 times Sine of pi x is Replicative Function

Let $f: \R \to \R$ be the real function defined as:
:$\forall x \in \R: \map f x = \log \, \size {2 \sin \pi x}$
Then $f$ is a replicative function.

Proof:
We have that:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 0}^{n - 1} \map f {x + \frac k n}
      | r = \sum_{k \mathop = 0}^{n - 1} \log \, \size {2 \sin \pi \paren {x + \frac k n} }
      | c = 
}}
{{eqn | r = \log \prod_{k \mathop = 0}^{n - 1} \size {2 \sin \pi \paren {x + \frac k n} }
      | c = Sum of Logarithms
}}
{{end-eqn}}
Thus to demonstrate that $f$ is replicative, it is sufficient to demonstrate that:
:$\ds \prod_{k \mathop = 0}^{n - 1} \paren {2 \sin \pi \paren {x + \frac k n} } = 2 \sin \pi n x$
By Product Formula for Sine:
{{begin-eqn}}
{{eqn | l = 2 \sin \pi n x
      | r = 2^n \prod_{k \mathop = 0}^{n - 1} \paren {\map \sin {\pi x + \frac {k \pi} n} }
}}
{{eqn | r = \prod_{k \mathop = 0}^{n - 1} \paren {2 \sin \pi \paren {x + \frac k n} }
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Supremum of Ideals is Upper Adjoint implies Lattice is Continuous

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a bounded below up-complete lattice.
Let $\map {\mathit {Ids} } L$ be the set of all ideals in $L$.
Let $P = \struct {\map {\mathit {Ids} } L, \precsim}$ be an ordered set where $\mathord \precsim = \subseteq \restriction_{\map {\mathit {Ids} } L \times \map {\mathit {Ids} } L}$
Let $f: \map {\mathit {Ids} } L \to S$ be a mapping such that
:$\forall I \in \map {\mathit {Ids} } L: f \sqbrk I = \sup I$
Let $f$ be an upper adjoint of a Galois connection.
Then $L$ is continuous.

Proof:
We will prove that
:$\forall x \in S: \exists I \in \map {\mathit {Ids} } L: x \preceq \sup I \land \forall J \in \map {\mathit {Ids} } L: x \preceq \sup J \implies I \subseteq J$ 
Let $x \in S$.
Define $I := \map \inf {f^{-1} \sqbrk {x^\succeq} }$.
By definition of $P$:
:$I \in \map {\mathit {Ids} } L$
We will prove that
:$\forall J \in \map {\mathit {Ids} } L: x \preceq \sup J \implies I \subseteq J$
Let $J \in \map {\mathit {Ids} } L$ such that
:$x \preceq \sup J$
By definition of $f$:
:$x \preceq f \sqbrk J$
By definition of upper closure of element:
:$f \sqbrk J \in x^\succeq$
By definition of image of set:
:$J \in f^{-1} \sqbrk {x^\succeq}$
By definition of infimum:
:$I \precsim J$
Hence by definition of $\precsim$:
:$I \subseteq J$
{{qed|lemma}}
By definition of upper adjoint of a Galois connection:
:there exists a mapping $d: S \to \map {\mathit {Ids} } L$: $\struct {f, d}$ is a Galois connection.
By Galois Connection is Expressed by Minimum
:$\map d x = \map \min {f^{-1} \sqbrk {x^\succeq} }$
By definition of smallest element:
:$I \in f^{-1} \sqbrk {x^\succeq}$
By definition of image of set:
:$f \sqbrk I \in x^\succeq$
By definition of upper closure of element:
:$x \preceq f \sqbrk I$
Thus by definition of $f$:
:$x \preceq \sup I$
Hence
:$\exists I \in \map {\mathit {Ids} } L: x \preceq \sup I \land \forall J \in \map {\mathit {Ids} } L: x \preceq \sup J \implies I \subseteq J$ 
{{qed|lemma}}
Hence by Continuous iff For Every Element There Exists Ideal Element Precedes Supremum:
:$L$ is continuous.
{{qed}}
Theorem: Sum of Replicative Functions is Replicative

Let $f: \R \to \R$ and $g: \R \to \R$ be real functions.
Let $f$ and $g$ both be replicative functions.
Then the pointwise sum of $f$ and $g$ is also a replicative function.

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 0}^{n - 1} \map {\paren {f + g} } {x + \frac k n}
      | r = \sum_{k \mathop = 0}^{n - 1} \paren {\map f {x + \frac k n} + \map g {x + \frac k n} }
      | c = {{Defof|Pointwise Sum}}
}}
{{eqn | r = \sum_{k \mathop = 0}^{n - 1} \map f {x + \frac k n} + \sum_{k \mathop = 0}^{n - 1} \map g {x + \frac k n}
      | c = 
}}
{{eqn | r = \map f {n x} + \map g {n x}
      | c = {{Defof|Replicative Function}}
}}
{{eqn | r = \map {\paren {f + g} } {n x}
      | c = {{Defof|Pointwise Sum}}
}}
{{end-eqn}}
Hence the result by definition of replicative function.
{{qed}}
Theorem: Constant Multiple of Replicative Function is Replicative

Let $f: \R \to \R$ be a real function.
Let $f$ be a replicative function.
Let $c \in \R$ be a constant.
Let $g: \R \to \R$ be the real function defined as:
:$\map g x = c \map f x$
Then $g$ is also a replicative function.

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 0}^{n - 1} \map g {x + \frac k n}
      | r = \sum_{k \mathop = 0}^{n - 1} c \map f {x + \frac k n}
      | c = 
}}
{{eqn | r = c \sum_{k \mathop = 0}^{n - 1} \map f {x + \frac k n}
      | c = 
}}
{{eqn | r = c \map f {n x}
      | c = {{Defof|Replicative Function}}
}}
{{eqn | r = \map g {n x}
      | c = 
}}
{{end-eqn}}
Hence the result by definition of replicative function.
{{qed}}
Theorem: Closed Form for Sequence 1, 2, 2, 3, 3, 3, 4, 4, 4, 4, ...

Let $a_1, a_2, a_3, \ldots$ be the integer sequence:
:$\sequence {a_n} = 1, 2, 2, 3, 3, 3, 4, 4, 4, 4, \ldots$
Then:
:$a_n = \ceiling {\dfrac {\sqrt {1 + 8 n} - 1} 2}$

Proof:
From Closed Form for Triangular Numbers, for $n = 1, 3, 6, 10, \ldots$:
:$n = \dfrac {a_n \paren {a_n + 1} } 2$
Thus by the Quadratic Formula:
$a_n = \dfrac {-1 \pm \sqrt {1 + 8 n} } 2$
In this context it is the positive root that is required.
The result follows by definition of ceiling function.
{{qed}}
Theorem: Sum of Sequence as Summation of Difference of Adjacent Terms

Let $n \in \Z_{> 0}$ be a strictly positive integer.
Then:
:$\ds \sum_{k \mathop = 1}^n a_k = n a_n - \sum_{k \mathop = 1}^{n - 1} k \paren {a_{k + 1} - a_k}$

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 1}^n a_k
      | r = \sum_{k \mathop = 1}^n \left({k - \left({k - 1}\right)}\right) a_k
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 1}^n k a_k - \sum_{k \mathop = 1}^n \left({k - 1}\right) a_k
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 1}^n k a_k - \sum_{k \mathop = 0}^{n - 1} k a_{k + 1}
      | c = Translation of Index Variable of Summation
}}
{{eqn | r = n a_n + \sum_{k \mathop = 1}^{n - 1} k a_k - \sum_{k \mathop = 1}^{n - 1} k a_{k + 1} + 0 \times a_0
      | c = extracting the end terms
}}
{{eqn | r = n a_n + \sum_{k \mathop = 1}^{n - 1} k \left({a_k - a_{k + 1} }\right)
      | c = 
}}
{{eqn | r = n a_n - \sum_{k \mathop = 1}^{n - 1} k \left({a_{k + 1} - a_k}\right)
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Sequence as Summation of Difference of Adjacent Terms

Let $n \in \Z_{> 0}$ be a strictly positive integer.
Then:
:$\ds \sum_{k \mathop = 1}^n a_k = n a_n - \sum_{k \mathop = 1}^{n - 1} k \paren {a_{k + 1} - a_k}$

Proof:
From Abel's Lemma: Formulation 2, after renaming and reassigning variables:
:$\ds \sum_{k \mathop = 1}^n a_k b_k = \sum_{k \mathop = 1}^{n - 1} \map {A_k} {a_k - a_{k + 1} } + A_n a_n$
where:
:$\sequence a$ and $\sequence b$ are sequences in $\R$
:$\ds A_n = \sum_{k \mathop = 1}^n {b_k}$ be the partial sum of $\sequence b$ from $1$ to $n$.
Let $\sequence b$ be defined as:
:$\forall k: b_k = 1$
Thus:
:$\ds A_n = \sum_{k \mathop = 1}^n 1 = n$
and so:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 1}^n a_k
      | r = \sum_{k \mathop = 1}^{n - 1} k \paren {a_k - a_{k + 1} } + n a_n
      | c = 
}}
{{eqn | r = n a_n - \sum_{k \mathop = 1}^{n - 1} k \paren {a_{k + 1} - a_k}
      | c = 
}}
{{end-eqn}}
{{qed}}