avewright/proofwiki-math huggingface dataset:
Theorem: Order is Preserved on Positive Reals by Squaring

:$x < y \iff x^2 < y^2$

Proof:
=== Necessary Condition ===
Assume $x < y$.
Then:
{{begin-eqn}}
{{eqn | l = x < y
      | o = \implies
      | r = x \times x < x \times y
      | c = Real Number Ordering is Compatible with Multiplication
}}
{{eqn | l = x < y
      | o = \implies
      | r = x \times y < y \times y
      | c = Real Number Ordering is Compatible with Multiplication
}}
{{eqn | o = \leadsto
      | r = x^2 < y^2
      | c = Transitive Law
}}
{{end-eqn}}
So:
:$x < y \implies x^2 < y^2$
{{qed|lemma}}
=== Sufficient Condition ===
Assume $x^2 < y^2$.
Then:
{{begin-eqn}}
{{eqn | l = x^2
      | o = <
      | r = y^2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 0
      | o = <
      | r = y^2 - x^2
      | c = Real Number Ordering is Compatible with Addition
}}
{{eqn | ll=\leadsto
      | l = \paren {y - x} \paren {y + x}
      | o = >
      | r = 0
      | c = Difference of Two Squares
}}
{{eqn | ll= \leadsto
      | l = \paren {y - x} \paren {y + x} \paren {y + x}^{-1}
      | o = >
      | r = 0 \times \paren {y + x}^{-1}
      | c = as $x + y > 0$
}}
{{eqn | ll= \leadsto
      | l = y - x
      | o = >
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = <
      | r = y
      | c = 
}}
{{end-eqn}}
So:
:$x^2 < y^2 \implies x < y$
{{qed}}
Theorem: Order is Preserved on Positive Reals by Squaring

:$x < y \iff x^2 < y^2$

Proof:
From Real Numbers form Totally Ordered Field, the real numbers form an ordered field.
The result follows from Order of Squares in Ordered Field.
{{qed}}
Theorem: Order is Preserved on Positive Reals by Squaring

:$x < y \iff x^2 < y^2$

Proof:
From Real Numbers form Totally Ordered Field, the real numbers form a totally ordered field.
By definition, a totally ordered field is a totally ordered ring without proper zero divisors.
The result follows from Order of Squares in Totally Ordered Ring without Proper Zero Divisors.
{{qed}}
Theorem: Order is Preserved on Positive Reals by Squaring

:$x < y \iff x^2 < y^2$

Proof:
=== Necessary Condition ===
Let $x < y$.
Then:
{{begin-eqn}}
{{eqn | l = x < y
      | o = \implies
      | r = x \times x < x \times y
      | c = Real Number Ordering is Compatible with Multiplication
}}
{{eqn | l = x < y
      | o = \implies
      | r = x \times y < y \times y
      | c = Real Number Ordering is Compatible with Multiplication
}}
{{eqn | o = \leadsto
      | r = x^2 < y^2
      | c = Transitive Law
}}
{{end-eqn}}
So:
:$x < y \implies x^2 < y^2$
{{qed|lemma}}
=== Sufficient Condition ===
Let $x^2 < y^2$.
{{AimForCont}} $x \ge y$.
Then:
{{begin-eqn}}
{{eqn | l = x \ge y
      | o = \implies
      | r = x \times x \ge x \times y
      | c = Real Number Ordering is Compatible with Multiplication
}}
{{eqn | l = x \ge y
      | o = \implies
      | r = x \times y \ge y \times y
      | c = Real Number Ordering is Compatible with Multiplication
}}
{{eqn | o = \leadsto
      | r = x^2 \ge y^2
      | c = Transitive Law
}}
{{end-eqn}}
But this contradicts our assertion that $x^2 < y^2$.
Hence by Proof by Contradiction it follows that:
:$x < y$
{{qed}}
Theorem: Real Plus Epsilon

Let $a, b \in \R$, such that:
:$\forall \epsilon \in \R_{>0}: a < b + \epsilon$
where $\R_{>0}$ is the set of strictly positive real numbers.
That is:
:$\epsilon > 0$
Then:
:$a \le b$

Proof:
{{AimForCont}} $a > b$.
Then:
:$a - b > 0$
By hypothesis, we have:
:$\forall \epsilon \in \R_{>0}: a < b + \epsilon$
Let $\epsilon = a - b$.
Then:
:$a < b + \paren {a - b} \implies a < a$
The result follows by Proof by Contradiction.
{{qed}}
Theorem: Difference of Two Squares

Let $\struct {R, +, \circ}$ be a commutative ring whose zero is $0_R$.
Let $x, y \in R$.
Then:
:$x \circ x + \paren {- \paren {y \circ y} } = \paren {x + y} \circ \paren {x + \paren {-y} }$
When $R$ is one of the standard sets of numbers, that is $\Z, \Q, \R$, and so on, then this translates into:
:$x^2 - y^2 = \paren {x + y} \paren {x - y}$

Proof:
Let $n = a^2 - b^2$ for some $a, b \in \Z$.
By Square Modulo 4, both $a$ and $b$ are of the form $4 k$ or $4 k + 1$ for some integer $k$.
There are $4$ cases:
;$a \equiv b \equiv 0 \pmod 4$:
Then:
:$a^2 - b^2 \equiv 0 \pmod 4$
and so $n$ is in the form $4 k$.
;$a \equiv 0 \pmod 4$, $b \equiv 1 \pmod 4$:
Then:
:$a^2 - b^2 \equiv -1 \pmod 4 \equiv 3 \pmod 4$
and so $n$ is in the form $4 k + 3$.
;$a \equiv 1 \pmod 4$, $b \equiv 0 \pmod 4$:
Then:
:$a^2 - b^2 \equiv 1 \pmod 4$
and so $n$ is in the form $4 k + 1$.
;$a \equiv b \equiv 1 \pmod 4$:
Then:
:$a^2 - b^2 \equiv 0 \pmod 4$
and so $n$ is in the form $4 k$.
Thus it is never the case that $a^2 - b^2 = 4 k + 2$.
{{qed}}
Theorem: Difference of Two Squares

Let $\struct {R, +, \circ}$ be a commutative ring whose zero is $0_R$.
Let $x, y \in R$.
Then:
:$x \circ x + \paren {- \paren {y \circ y} } = \paren {x + y} \circ \paren {x + \paren {-y} }$
When $R$ is one of the standard sets of numbers, that is $\Z, \Q, \R$, and so on, then this translates into:
:$x^2 - y^2 = \paren {x + y} \paren {x - y}$

Proof:
Let $n_0 = c^2 - d^2$ for some $c, d \in \Z$.
Then:
:$n_0 = \paren {c + d} \paren {c - d}$
and so:
:$\paren {c + d} - \paren {c - d} = 2 d$
Therefore $n$ must be expressible as a product of two integers whose difference is even.
Now consider the integer $n \in \Z$ that satisfies $n \equiv 2 \pmod 4$.
$n$ is an even number that is not divisible by 4.
This implies that any even number that divides $n$ will produce an odd number.
Consider the ordered pairs of integers $\tuple {a, b}, a < b$ such that $ab = n$.
If  $a$ is odd, then $b = \dfrac n a$ must in turn be even.
Hence the difference will not be even.
If $a$ is even, $b$ must be odd by the implication mentioned earlier.
Hence the difference will once again not be even.
Hence, $n$ cannot be expressed as a product of two integers whose difference is even.
In turn it cannot be expressed as a Difference of Two Squares.
{{qed}}
Theorem: Difference of Two Squares

Let $\struct {R, +, \circ}$ be a commutative ring whose zero is $0_R$.
Let $x, y \in R$.
Then:
:$x \circ x + \paren {- \paren {y \circ y} } = \paren {x + y} \circ \paren {x + \paren {-y} }$
When $R$ is one of the standard sets of numbers, that is $\Z, \Q, \R$, and so on, then this translates into:
:$x^2 - y^2 = \paren {x + y} \paren {x - y}$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {x + y} \circ \paren {x + \paren {-y} }
      | r = x \circ x + y \circ x + x \circ \paren {-y} + y \circ \paren {-y}
      | c = Distributivity of $\circ$ over $+$ in a ring
}}
{{eqn | r = x \circ x + x \circ y + x \circ \paren {-y} + y \circ \paren {-y}
      | c = $R$ is a commutative ring
}}
{{eqn | r = x \circ x + x \circ \paren {y + \paren {-y} } + \paren {-\paren {y \circ y} }
      | c = various ring properties
}}
{{eqn | r = x \circ x + x \circ 0_R + \paren {-\paren {y \circ y} }
      | c = 
}}
{{eqn | r = x \circ x + \paren {-\paren {y \circ y} }
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Difference of Two Squares

Let $\struct {R, +, \circ}$ be a commutative ring whose zero is $0_R$.
Let $x, y \in R$.
Then:
:$x \circ x + \paren {- \paren {y \circ y} } = \paren {x + y} \circ \paren {x + \paren {-y} }$
When $R$ is one of the standard sets of numbers, that is $\Z, \Q, \R$, and so on, then this translates into:
:$x^2 - y^2 = \paren {x + y} \paren {x - y}$

Proof:
This is a special case of Difference of Two Powers:
:$\ds a^n - b^n = \paren {a - b} \paren {a^{n - 1} + a^{n - 2} b + a^{n - 3} b^2 + \cdots + a b^{n - 2} + b^{n - 1} } = \paren {a - b} \sum_{j \mathop = 0}^{n - 1} a^{n - j - 1} b^j$
The result follows by setting $n = 2$.
{{qed}}
Theorem: Difference of Two Squares

Let $\struct {R, +, \circ}$ be a commutative ring whose zero is $0_R$.
Let $x, y \in R$.
Then:
:$x \circ x + \paren {- \paren {y \circ y} } = \paren {x + y} \circ \paren {x + \paren {-y} }$
When $R$ is one of the standard sets of numbers, that is $\Z, \Q, \R$, and so on, then this translates into:
:$x^2 - y^2 = \paren {x + y} \paren {x - y}$

Proof:
{{:Euclid:Proposition/II/5}}
:400px
Let $AB$ be cut into equal segments at $C$ and unequal segments at $D$.
Then the rectangle contained by $AD$ and $DB$ together with the square on $CD$ equals the square on $BC$.
(That is, let $x = AC, y = CD$. Then $\paren {x + y} \paren {x - y} + y^2 = x^2$.)
This is proved as follows.
Construct the square $CBFE$ on $CB$, and join $BE$.
Construct $DG$ parallel to $CE$ through $G$, and let $DG$ cross $BE$ at $H$.
Construct $KM$ parallel to $AB$ through $H$.
Construct $AK$ parallel to $BF$ through $A$.
From Complements of Parallelograms are Equal:
:$\Box CDHL = \Box FGHM$.
Add the square $DBMH$ to each.
Then $\Box CBML = \Box DBFG$.
But as $AC = CB$, from Parallelograms with Equal Base and Same Height have Equal Area we have that:
:$\Box ACLK = \Box CBML$
Add $\Box CDHL$ to each.
Then $\Box ADHK$ is equal in area to the gnomon $CBFGHL$.
But $\Box ADHK$ is the rectangle contained by $AD$ and $DB$, because $DB = DH$.
So the gnomon $CBFGHL$ is equal in area to the rectangle contained by $AD$ and $DB$.
Now $\Box LHGE$ is equal to the square on $CD$.
Add $\Box LHGE$ to each of the gnomon $CBFGHL$ and $\Box ADHK$.
Then the gnomon $CBFGHL$ together with $\Box LHGE$ equals the rectangle contained by $AD$ and $DB$ and the square on $CD$.
But the gnomon $CBFGHL$ together with $\Box LHGE$ is the square $CBFE$.
Hence the result.
{{qed}}
Theorem: Difference of Two Squares

Let $\struct {R, +, \circ}$ be a commutative ring whose zero is $0_R$.
Let $x, y \in R$.
Then:
:$x \circ x + \paren {- \paren {y \circ y} } = \paren {x + y} \circ \paren {x + \paren {-y} }$
When $R$ is one of the standard sets of numbers, that is $\Z, \Q, \R$, and so on, then this translates into:
:$x^2 - y^2 = \paren {x + y} \paren {x - y}$

Proof:
:360px
Let $\Box ABCD$ be a square of side length $x$.
Let $\Box DEFG$ be a square of side length $y$ where $y < x$
Let $EF$ be produced to $H$.
The area of $\Box ABCD$ is seen to be equal to the sum of:
:the area of the rectangle $AEHB$
:the area of the rectangle $FGCH$
:the area of the square $DEFG$
From Area of Square:
:the area of $\Box ABCD$ is equal to $x^2$
:the area of $\Box DEFG$ is equal to $y^2$
From Area of Rectangle:
:the area of $AEHB$ is equal to $x \paren {x - y}$
:the area of $FGCH$ is equal to $y \paren {x - y}$
Hence:
{{begin-eqn}}
{{eqn | l = x^2 - y^2
      | r = x \paren {x - y} + y \paren {x - y}
      | c = 
}}
{{eqn | r = \paren {x + y} \paren {x - y}
      | c = Real Multiplication Distributes over Addition
}}
{{end-eqn}}
{{qed}}
Theorem: Mediant is Between

Let $a, b, c, d \in \R$ be real numbers such that $b > 0, d > 0$.
Let $r = \dfrac a b < \dfrac c d = s$.
Then:
:$r < \dfrac {a + c} {b + d} < s$

Proof:
Let $r, s \in \R$ be such that:
:$r < s$
and:
:$r = \dfrac a b, s = \dfrac c d$
where $a, b, c, d$ are real numbers such that $b > 0, d > 0$.
Because $b, d > 0$, it follows from Real Number Ordering is Compatible with Multiplication that:
:$b d > 0$
Thus:
{{begin-eqn}}
{{eqn | l = \frac a b
      | o = <
      | r = \frac c d
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac a b \paren {b d}
      | o = <
      | r = \frac c d \paren {b d}
      | c = Real Number Ordering is Compatible with Multiplication
}}
{{eqn | ll= \leadsto
      | l = a d
      | o = <
      | r = b c
      | c = 
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = a \paren {b + d}
      | r = a b + a d
      | c = 
}}
{{eqn | o = <
      | r = a b + b c
      | c = Real Number Ordering is Compatible with Addition, as $a d < b c$ from above
}}
{{eqn | r = \paren {a + c} b
      | c = 
}}
{{end-eqn}}
From Reciprocal of Strictly Positive Real Number is Strictly Positive:
:$\paren {a + c}^{-1} > 0$
and:
:$b^{-1} > 0$
It follows from Real Number Ordering is Compatible with Multiplication that:
:$\dfrac a b < \dfrac {a + c} {b + d}$
The other half is proved similarly.
{{Qed}}
Theorem: Mediant is Between

Let $a, b, c, d \in \R$ be real numbers such that $b > 0, d > 0$.
Let $r = \dfrac a b < \dfrac c d = s$.
Then:
:$r < \dfrac {a + c} {b + d} < s$

Proof:
Let $p, q, r, s \in \R$ such that $q > 0, s > 0$.
Then from Mediant is Between:
:$\dfrac p q < \dfrac {p + r} {q + s} < \dfrac r s$
In order to present this in the form required by the Squeeze Theorem for Functions, we weaken the ordering:
:$(1): \quad \dfrac p q \le \dfrac {p + r} {q + s} \le \dfrac r s$
Let $f$, $g$ and $h$ be the constant real functions defined as:
{{begin-eqn}}
{{eqn | q = \forall x \in \R
      | l = \map f x
      | r = \dfrac a b
      | c = 
}}
{{eqn | q = \forall x \in \R
      | l = \map g x
      | r = \dfrac {a + c} {b + d}
      | c = 
}}
{{eqn | q = \forall x \in \R
      | l = \map h x
      | r = \dfrac c d
      | c = 
}}
{{end-eqn}}
From $(1)$:
:$\forall x \in \R: \map f x \le \map g x \le \map h x$
But {{hypothesis}}:
:$\dfrac a b = \dfrac c d$
That is:
:$\forall x \in \R: \map f x = \map h x$
Hence from the Squeeze Theorem for Functions:
:$\forall x \in \R: \map f x = \map g x = \map h x$
That is:
:$\dfrac a b = \dfrac c d \implies \dfrac a b = \dfrac {a + c} {b + d} = \dfrac c d$
{{Qed}}
Theorem: Mediant is Between

Let $a, b, c, d \in \R$ be real numbers such that $b > 0, d > 0$.
Let $r = \dfrac a b < \dfrac c d = s$.
Then:
:$r < \dfrac {a + c} {b + d} < s$

Proof:
{{begin-eqn}}
{{eqn | l = \dfrac {a + c} {b + d}
      | r = \dfrac a b \times \dfrac {b \paren {a + c} } {a \paren {b + d} }
      | c = multiplying by $\dfrac a b \times \dfrac b a$
}}
{{eqn | r = \dfrac a b \times \dfrac {1 + c / a} {1 + d / b}
      | c = dividing top and bottom by $a b$
}}
{{eqn | l = \dfrac {a + c} {b + d}
      | r = \dfrac c d \times \dfrac {d \paren {a + c} } {c \paren {b + d} }
      | c = multiplying by $\dfrac c d \times \dfrac d c$
}}
{{eqn | r = \dfrac c d \times \dfrac {1 + a / c} {1 + b / d}
      | c = dividing top and bottom by $c d$
}}
{{eqn | ll= \leadsto
      | l = \dfrac a b = \dfrac c d
      | r = \dfrac {a + c} {b + d}
      | c = {{explain|How does $\dfrac {a + c} {b + d} {{=}} \dfrac a b \times \dfrac {1 + c / a} {1 + d / b} {{=}} \dfrac c d \times \dfrac {1 + a / c} {1 + b / d}$ imply that $\dfrac a b {{=}} \dfrac c d$?}}
}}
{{end-eqn}}
{{Qed}}
Theorem: Mediant is Between

Let $a, b, c, d \in \R$ be real numbers such that $b > 0, d > 0$.
Let $r = \dfrac a b < \dfrac c d = s$.
Then:
:$r < \dfrac {a + c} {b + d} < s$

Proof:
Let:
:$t := \dfrac a b = \dfrac c d$
Then:
:$a = t c$
and:
:$c = t d$
Hence:
:$\dfrac {a + b}{c + d} = \dfrac {t \paren {c + d} }{c + d} = t$
{{qed}}
Theorem: Mediant is Between

Let $a, b, c, d \in \R$ be real numbers such that $b > 0, d > 0$.
Let $r = \dfrac a b < \dfrac c d = s$.
Then:
:$r < \dfrac {a + c} {b + d} < s$

Proof:
Let $\epsilon \in \R_{>0}$.
Then:
:$\dfrac a b < \dfrac {c + \epsilon} d$
By Mediant is Between:
:$\dfrac a b < \dfrac {a + c + \epsilon} {b + d} < \dfrac {c + \epsilon} d$
By Inequality of Sequences Preserved in Limit, letting $\epsilon \to 0$:
:$\dfrac a b \le \dfrac {a + c} {b + d} \le \dfrac c d$
Since {{hypothesis}}:
:$\dfrac a b = \dfrac c d$
we have:
:$\dfrac a b = \dfrac {a + c} {b + d} = \dfrac c d$
{{qed}}
Theorem: Real Numbers Between Epsilons

Let $a, b \in \R$ such that $\forall \epsilon \in \R_{>0}: a - \epsilon < b < a + \epsilon$.
Then $a = b$.

Proof:
From Real Plus Epsilon:
:$b < a + \epsilon \implies b \le a$
From Real Number Ordering is Compatible with Addition:
:$a - \epsilon < b \implies a < b + \epsilon$
Then from Real Plus Epsilon:
:$a < b + \epsilon \implies a \le b$
The result follows.
{{qed}}
Theorem: Existence of Integer Below Given Real Number

Let $x$ be a real number.
Then there exists an integer less than $x$:
:$\forall x \in \R: \exists n \in \Z: n < x$

Proof:
{{WLOG}}, assume that $x < 0$.
From the Axiom of Archimedes:
:$\exists m \in \N: m > -x$
By Real Numbers form Totally Ordered Field, we have that $\R$ is an ordered field.
Therefore by property $(3)$ of Properties of Ordered Field, $\Z \owns -m < x$.
{{qed}}
Category:Analysis
pyvgsf2jdou7chjgadituqrihwohxo3
Theorem: Axiom of Archimedes

Let $x$ be a real number.
Then there exists a natural number greater than $x$.
:$\forall x \in \R: \exists n \in \N: n > x$
That is, the set of natural numbers is unbounded above.

Proof:
Let $x \in \R$.
Let $S$ be the set of all natural numbers less than or equal to $x$:
:$S = \set {a \in \N: a \le x}$
It is possible that $S = \O$.
Suppose $0 \le x$.
Then by definition, $0 \in S$.
But $S = \O$, so this is a contradiction.
From the Trichotomy Law for Real Numbers it follows that $0 > x$.
Thus we have the element $0 \in \N$ such that $0 > x$.
Now suppose $S \ne \O$.
Then $S$ is bounded above (by $x$, for example).
Thus by the Continuum Property of $\R$, $S$ has a supremum in $\R$.
Let $s = \map \sup S$.
Now consider the number $s - 1$.
Since $s$ is the supremum of $S$, $s - 1$ cannot be an upper bound of $S$ by definition.
So $\exists m \in S: m > s - 1 \implies m + 1 > s$.
But as $m \in \N$, it follows that $m + 1 \in \N$.
Because $m + 1 > s$, it follows that $m + 1 \notin S$ and so $m + 1 > x$.
Theorem: Real Number is between Floor Functions

:$\forall x \in \R: \floor x \le x < \floor {x + 1}$

Proof:
$\floor x$ is defined as:
:$\floor x = \sup \set {m \in \Z: m \le x}$
So $\floor x \le x$ by definition.
From Floor plus One:
:$\floor {x + 1} > \floor x$
Hence by the definition of the supremum:
:$\floor {x + 1} > x$
The result follows.
{{qed}}
Category:Floor Function
akn94fzyqk42jhnqcxjm9xqmvzfon8w
Theorem: Real Number is between Ceiling Functions

:$\forall x \in \R: \ceiling {x - 1} \le x < \ceiling x$

Proof:
$\ceiling x$ is defined as:
:$\ceiling x = \map \inf {\set {m \in \Z: m \ge x} }$
So $\ceiling x \ge x$ by definition.
Now $\ceiling {x - 1} < \ceiling x$, so by the definition of the infimum:
:$\ceiling {x - 1} > x$
The result follows.
{{qed}}
Category:Ceiling Function
p1ftr5soshr01dofp1spqabila6zl24
Theorem: Real Number minus Floor

:$x - \floor x \in \hointr 0 1$

Proof:
{{begin-eqn}}
{{eqn | l = \floor x
      | o = \le
      | m = x
      | mo= <
      | r = \floor x + 1
      | c = {{Defof|Floor Function}}
}}
{{eqn | ll= \leadsto
      | l = \floor x - \floor x
      | o = \le
      | m = x - \floor x
      | mo= <
      | r = \floor x + 1 - \floor x
      | c = subtracting $\floor x$ from all parts
}}
{{eqn | ll= \leadsto
      | l = 0
      | o = \le
      | m = x - \floor x
      | mo= <
      | r = 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x - \floor x
      | o = \in
      | m = \hointr 0 1
      | c = {{Defof|Right Half-Open Real Interval}}
}}
{{end-eqn}}
{{qed}}
Theorem: Ceiling minus Real Number

:$\forall x \in \R: \ceiling x - x \in \hointr 0 1$

Proof:
{{begin-eqn}}
{{eqn | l = \ceiling x - 1
      | o = <
      | r = x \le \ceiling x
      | c = Real Number is between Ceiling Functions
}}
{{eqn | ll= \leadsto
      | l = \ceiling x - 1 - \ceiling x
      | o = <
      | r = x - \ceiling x \le \ceiling x - \ceiling x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = -1
      | o = <
      | r = x - \ceiling x \le 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 1
      | o = >
      | r = \ceiling x - x \ge 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \ceiling x - x
      | o = \in
      | r = \hointr 0 1
      | c = {{Defof|Right Half-Open Real Interval}}
}}
{{end-eqn}}
{{qed}}
Category:Ceiling Function
mmsdldixnpnccboq712p4rmpdp242rf
Theorem: Real Number is Floor plus Difference

:There exists an integer $n \in \Z$ such that for some $t \in \hointr 0 1$:
::$x = n + t$
{{iff}}:
:$n = \floor x$

Proof:
=== Sufficient Condition ===
Let there exist $n \in \Z$ such that $x = n + t$, where $t \in \hointr 0 1$.
We have that $1 - t > 0$.
Thus:
:$0 \le x - n < 1$
Thus:
: $n \le x < n + 1$
That is, $n$ is the floor of $x$.
{{qed|lemma}}
Theorem: Floor plus One

Let $x \in \R$.
Then:
:$\floor {x + 1} = \floor x + 1$
where $\floor x$ is the floor function of $x$.

Proof:
{{begin-eqn}}
{{eqn | l = \floor {x + 1}
      | r = n
      | c =
}}
{{eqn | ll= \leadsto
      | l = n
      | o = \le
      | m = x + 1
      | mo= <
      | r = n + 1
      | c = {{Defof|Floor Function}}
}}
{{eqn | ll= \leadsto
      | l = n - 1
      | o = \le
      | m = x
      | mo= <
      | r = n
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \floor x
      | r = n - 1
      | c = {{Defof|Floor Function}}
}}
{{eqn | ll= \leadsto
      | l = \floor {x + 1}
      | r = \floor x + 1
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Real Number is Integer iff equals Floor

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

Proof:
Let $x = \floor x$.
As $\floor x \in \Z$, then so must $x$ be.
Now let $x \in \Z$.
We have:
:$\floor x = \sup \set {m \in \Z: m \le x}$
As $x \in \sup \set {m \in \Z: m \le x}$, and there can be no greater $n \in \Z$ such that $n \in \sup \set {m \in \Z: m \le x}$, it follows that:
:$x = \floor x$
{{qed}}
Theorem: Sum of Floor and Floor of Negative

Let $x \in \R$. Then:
:$\floor x + \floor {-x} = \begin{cases} 0 & : x \in \Z \\ -1 & : x \notin \Z \end{cases}$
where $\floor x$ denotes the floor of $x$.

Proof:
Let $x \in \Z$.
Then from Real Number is Integer iff equals Floor:
:$x = \floor x$
Now $x \in \Z \implies -x \in \Z$, so:
:$\floor {-x} = -x$
Thus:
:$\floor x + \floor {-x} = x + \paren {-x} = x - x = 0$
Now let $x \notin \Z$.
From Real Number is Floor plus Difference:
:$x = n + t$
where $n = \floor x$ and $t \in \hointr 0 1$.
Thus:
:$-x = -\paren {n + t} = -n - t = -n - 1 + \paren {1 - t}$
As $t \in \hointr 0 1$, we have:
:$1 - t \in \hointr 0 1$
Thus:
:$\floor {-x} = -n - 1$
So:
:$\floor x + \floor {-x} = n + \paren {-n - 1} = n - n - 1 = -1$
{{qed}}
Theorem: Floor defines Equivalence Relation

Let $x \in \R$ be a real number.
Let $\floor x$ denote the floor function of $x$.
Let $\RR$ be the relation defined on $\R$ such that:
:$\forall x, y, \in \R: \tuple {x, y} \in \RR \iff \floor x = \floor y$
Then $\RR$ is an equivalence, and $\forall n \in \Z$, the $\RR$-class of $n$ is the half-open interval $\hointr n {n + 1}$.

Proof:
Checking in turn each of the criteria for equivalence:
Theorem: Ceiling defines Equivalence Relation

Let $\RR$ be the relation defined on $\R$ such that:
:$\forall x, y, \in \R: \tuple {x, y} \in \RR \iff \ceiling x = \ceiling y$
where $\ceiling x$ is the ceiling of $x$.
Then $\RR$ is an equivalence, and $\forall n \in \Z$, the $\RR$-class of $n$ is the half-open interval $\hointl {n - 1} n$.

Proof:
Checking in turn each of the criteria for equivalence:
Theorem: Real Number is Ceiling minus Difference

Let $n$ be a integer.
{{TFAE}}
:$(1): \quad$ There exists $t \in \hointr 0 1$ such that $x = n - t$
:$(2): \quad n = \ceiling x$

Proof:
=== 1 implies 2 ===
Let $x = n - t$, where $t \in \hointr 0 1$.
Because $0 \le t < 1$, we have:
:$0 \leq n - x < 1$
Thus:
:$n - 1 < x \le  n$
That is, $n$ is the ceiling of $x$.
{{qed|lemma}}
Theorem: Cauchy's Inequality

:$\ds \sum {r_i}^2 \sum {s_i}^2 \ge \paren {\sum {r_i s_i} }^2$
where all of $r_i, s_i \in \R$.

Proof:
For any $\lambda \in \R$, we define $f: \R \to \R$ as the function:
:$\ds \map f \lambda = \sum {\paren {r_i + \lambda s_i}^2}$
Now:
:$\map f \lambda \ge 0$
because it is the sum of squares of real numbers.
Hence:
{{begin-eqn}}
{{eqn | q = \forall \lambda \in \R
      | l = \map f \lambda
      | o = \equiv
      | m = \sum {\paren { {r_i}^2 + 2 \lambda r_i s_i + \lambda^2 {s_i}^2} }
      | mo= \ge
      | r = 0
      | c = 
}}
{{eqn | o = \equiv
      | m = \sum { {r_i}^2} + 2 \lambda \sum {r_i s_i} + \lambda^2 \sum { {s_i}^2}
      | mo= \ge
      | r = 0
      | c = 
}}
{{end-eqn}}
This is a quadratic equation in $\lambda$.
From Solution to Quadratic Equation:
:$\ds a \lambda^2 + b \lambda + c = 0: a = \sum { {s_i}^2}, b = 2 \sum {r_i s_i}, c = \sum { {r_i}^2}$
From Discriminant of Quadratic Equation, the discriminant of this equation (that is $b^2 - 4 a c$) is:
:$\ds D := 4 \paren {\sum {r_i s_i} }^2 - 4 \sum { {r_i}^2} \sum { {s_i}^2}$
{{AimForCont}} $D$ is (strictly) positive.
Then $\map f \lambda = 0$ has two distinct real roots, $\lambda_1 < \lambda_2$, say.
From Sign of Quadratic Function Between Roots, it follows that $f$ is (strictly) negative somewhere between $\lambda_1$ and $\lambda_2$.
But we have:
:$\forall \lambda \in \R: \map f \lambda \ge 0$
From this contradiction it follows that:
:$D \le 0$
which is the same thing as saying:
:$\ds \sum { {r_i}^2} \sum { {s_i}^2} \ge \paren {\sum {r_i s_i} }^2$
{{qed}}