avewright/proofwiki-math huggingface dataset:
Theorem: Power Function on Base between Zero and One is Strictly Decreasing/Integer

Let $a \in \R$ be a real number such that $0 < a < 1$.
Let $f: \Z \to \R$ be the real-valued function defined as:
:$\map f k = a^k$
where $a^k$ denotes $a$ to the power of $k$.
Then $f$ is strictly decreasing.

Proof:
Let $0 < a < 1$.
By Power Function on Base between Zero and One is Strictly Decreasing: Positive Integer, the theorem is already proven for positive integers.
It remains to be proven over the negative integers.
Let $i, j$ be integers such that $i < j < 0$.
From Order of Real Numbers is Dual of Order of their Negatives:
:$0 < -j < -i$
So:
{{begin-eqn}}
{{eqn | l = a^{-j}
      | o = > 
      | r = a^{-i}
      | c = Power Function on Base between Zero and One is Strictly Decreasing: Positive Integer
}}
{{eqn | ll= \leadsto
      | l = \frac 1 {a^j}
      | o = >
      | r = \frac 1 {a^i}
      | c = Real Number to Negative Power: Positive Integer
}}
{{eqn | ll= \leadsto
      | l = a^i
      | o = >
      | r = a^j
      | c = Ordering of Reciprocals
}}
{{end-eqn}}
Hence the result.
{{qed}}
Category:Power Function on Base between Zero and One is Strictly Decreasing
rtbdssg7n11m3w8hg6poyxc849q5hfi
Theorem: Meet-Continuous iff Meet Preserves Directed Suprema

Let $\mathscr S = \struct {S, \vee, \wedge, \preceq}$ be an up-complete lattice.
Let $\struct {S \times S, \precsim}$ be the simple order product of $\mathscr S$ and $\mathscr S$.
Let $f: S \times S \to S$ be a mapping such that
:$\forall x, y \in S: \map f {x, y} = x \wedge y$
Then:
:$\mathscr S$ is meet-continuous
{{iff}}:
:$f$ preserves directed suprema

Proof:
=== Sufficient Condition ===
Assume that:
:$\mathscr S$ is meet-continuous.
We will prove that:
:for every element $x$ of $S$, a directed subset $D$ of $S$ if $x \preceq \sup D$, then $x = \sup \set {x \wedge d: d \in D}$
Let $x \in S$, $D$ be a directed subset of $S$ such that:
:$x \preceq \sup D$
Thus
{{begin-eqn}}
{{eqn | l = x
      | r = x \wedge \sup D
      | c = Preceding iff Meet equals Less Operand
}}
{{eqn | r = \sup \set {x \wedge d: d \in D}
      | c = {{Defof|Meet-Continuous Lattice}}
}}
{{end-eqn}}
{{qed|lemma}}
By definition of reflexivity:
:for every an element $x$ of $S$, a directed subset $D$ of $S$ if $x \preceq \sup D$, then $x \preceq \sup \set {x \wedge d: d \in D}$
By Meet is Directed Suprema Preserving:
:$f$ preserves directed suprema.
{{qed|lemma}}
Theorem: Power Function on Base Greater than One is Strictly Increasing/Integer

Let $a \in \R$ be a real number such that $a > 1$.
Let $f: \Z \to \R$ be the real-valued function defined as:
:$\map f k = a^k$
where $a^k$ denotes $a$ to the power of $k$.
Then $f$ is strictly decreasing.

Proof:
Let $a > 1$.
By Power Function on Base Greater than One is Strictly Increasing: Positive Integer, the theorem is already proven for positive integers.
It remains to be proven over the strictly negative integers.
Let $i, j$ be integers such that $i < j < 0$.
From Order of Real Numbers is Dual of Order of their Negatives:
:$0 < -j < -i$
So:
{{begin-eqn}}
{{eqn | l = a^{-j}
      | o = < 
      | r = a^{-i}
      | c = Power Function on Base Greater than One is Strictly Increasing: Positive Integer
}}
{{eqn | ll= \leadsto
      | l = \frac 1 {a^j}
      | o = < 
      | r = \frac 1 {a^i}
      | c = Real Number to Negative Power: Positive Integer
}}
{{eqn | ll= \leadsto
      | l = a^i
      | o = < 
      | r = a^j
      | c = Ordering of Reciprocals
}}
{{end-eqn}}
{{qed}}
Category:Power Function on Base Greater than One is Strictly Increasing
sjlmfdufptgv70wy09w64dxget1hs7b
Theorem: Real Star-Algebra is Commutative

Let $A = \struct {A_F, \oplus}$ be a real $*$-algebra whose conjugation is denoted as $*$.
Then:
:$\forall a, b \in A, a \oplus b = b \oplus a$
That is, real $*$-algebra is commutative.

Proof:
{{begin-eqn}}
{{eqn | l = a \oplus b
      | r = \paren {a \oplus b}^*
      | c = {{Defof|Real Star-Algebra|Real $*$-Algebra}}
}}
{{eqn | r = b^* \oplus a^*
      | c = {{Defof|Conjugation on Algebra}}
}}
{{eqn | r = b \oplus a
      | c = {{Defof|Real Star-Algebra|Real $*$-Algebra}}
}}
{{end-eqn}}
{{qed}}
Category:Real Star-Algebras
Category:Commutative Algebras
mqlscx9yw475bf97wqqpcbg4xpuvv13
Theorem: Meet-Continuous implies Shift Mapping Preserves Directed Suprema

Let $\mathscr S = \struct {S, \vee, \wedge, \preceq}$ be a meet-continuous lattice.
Let $x \in S$.
Let $f: S \to S$ be a mapping such that:
:$\forall y \in S: \map f y = x \wedge y$
Then:
:$f$ preserves directed suprema.

Proof:
Let $D$ be a directed subset of $S$ such that
:$D$ admits a supremum.
By Singleton is Directed and Filtered Subset:
:$\set x$ is directed.
By Up-Complete Product/Lemma 1:
:$\set x \times D$ is directed in the simple order product $\struct {S \times S, \precsim}$ of $\mathscr S$ and $\mathscr S$.
Define a mapping $g: S \times S \to S$:
:$\forall s, t \in S: \map g {s, t} = s \wedge t$
By Meet-Continuous iff Meet Preserves Directed Suprema:
:$g$ preserves directed suprema.
By definition of meet-continuous:
:$\mathscr S$ is up-complete.
By Up-Complete Product:
:$\struct {S \times S, \precsim}$ is up-complete.
By definition of up-complete:
:$\set x \times D$ admits a supremum.
Thus
{{begin-eqn}}
{{eqn | l = \map \sup {\map {f^\to} D}
      | r = \sup \sety {\map f d: d \in D}
      | c = {{Defof|Image of Subset under Mapping}}
}}
{{eqn | r = \sup \set {x \wedge d: d \in D}
      | c = Definition of $f$
}}
{{eqn | r = \sup \set {\map g {y, d}: y \in \set x, d \in D}
      | c = Definition of $g$
}}
{{eqn | r = \map \sup {\map {g^\to} {\set x \times D} }
      | c = {{Defof|Image of Subset under Mapping}}
}}
{{eqn | r = \map g {\map \sup {\set x \times D} }
      | c = {{Defof|Mapping Preserves Supremum of Subset}}
}}
{{eqn | r = \map g {\sup \set x, \sup D}
      | c = Supremum of Simple Order Product
}}
{{eqn | r = \map g {x, \sup D}
      | c = Supremum of Singleton
}}
{{eqn | r = x \wedge \sup D
      | c = Definition of $g$
}}
{{eqn | r = \map f {\sup D}
      | c = Definition of $f$
}}
{{end-eqn}}
{{qed}}
Theorem: Power of Strictly Positive Real Number is Strictly Positive/Positive Integer

Let $x \in \R_{>0}$ be a (strictly) positive real number.
Let $n \in \Z_{\ge 0}$ be a positive integer.
Then:
:$x^n > 0$
where $x^n$ denotes the $n$th power of $x$.

Proof:
Proof by Mathematical Induction:
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\forall x \in \R_{>0}: x^n > 0$
$\map P 0$ is true, as this just says:
{{begin-eqn}}
{{eqn | l = x^0
      | r = 1
      | c = {{Defof|Integer Power}}
}}
{{eqn | o = >
      | r = 0
}}
{{end-eqn}}
Theorem: Power of Positive Real Number is Positive/Integer

Let $x \in \R_{>0}$ be a (strictly) positive real number.
Let $n \in \Z$ be an integer.
Then:
:$x^n > 0$
where $x^n$ denotes the $n$th power of $x$.

Proof:
By Power of Positive Real Number is Positive: Natural Number, the theorem is already proven for non-negative integers.
Suppose $n \in \Z_{< 0}$.
When $n < 0$, by Real Number Ordering is Compatible with Multiplication: Negative Factor:
:$-n > 0$
Then, by Power of Positive Real Number is Positive: Natural Number:
:$x^{-n} > 0$
Therefore, by Reciprocal of Strictly Positive Real Number is Strictly Positive:
:$x^n = \dfrac 1 {x^{-n} } > 0$
{{qed}}
Category:Power of Positive Real Number is Positive
q6y71g607yse61jxsqnx1yreip7soz1
Theorem: Power of Positive Real Number is Positive/Rational Number

Let $x \in \R_{>0}$ be a (strictly) positive real number.
Let $q \in \Q$ be a rational number.
Then:
:$x^q > 0$
where $x^q$ denotes the $x$ to the power of $q$.

Proof:
Let $q = \dfrac r s$, where $r \in \Z$, $s \in \Z \setminus \set 0$.
Then:
{{begin-eqn}}
{{eqn | l = x > 0
      | o = \leadsto
      | r = x^r > 0
      | c = Power of Positive Real Number is Positive: Integer
}}
{{eqn | o = \leadsto
      | r = \sqrt [s] {\paren {x^r} } > 0
      | c = Existence of Positive Root of Positive Real Number
}}
{{eqn | o = \leadsto
      | r = x^{r / s}
      | c = {{Defof|Rational Power|Rational Power}}
}}
{{end-eqn}}
Hence the result.
{{qed}}
Category:Power of Positive Real Number is Positive
82zj1qzhj73vryu2ve2f4ricm3ohqr4
Theorem: Power Function is Monotone/Rational Number

Let $a \in \R_{>0}$.
Let $f: \Q \to \R$ be the real-valued function defined as:
:$\map f r = a^r$
where $a^r$ denotes $a$ to the power of $r$.
Then $f$ is monotone.
Further, $f$ is strictly monotone unless $a = 1$.

Proof:
=== Case 1: $a > 1$ ===
Let $a > 1$.
Then by Power Function on Base Greater than One is Strictly Increasing:
:$f$ is strictly increasing.
By Strictly Increasing Mapping is Increasing:
:$f$ is increasing.
Theorem: Power Function tends to One as Power tends to Zero/Rational Number

Let $a \in \R_{> 0}$.
Let $f: \Q \to \R$ be the real-valued function defined as:
:$\map f q = a^q$
where $a^q$ denotes $a$ to the power of $q$.
Then:
:$\ds \lim_{x \mathop \to 0} \map f x = 1$

Proof:
=== Case 1: $a > 1$ ===
If $a > 1$, then:
:$\ds \lim_{x \mathop \to 0} \map f x = 1$
from Power Function on Base greater than One tends to One as Power tends to Zero/Rational Number.
Theorem: Power Function on Base greater than One tends to One as Power tends to Zero/Rational Number/Lemma

Let $a \in \R$ be a real number such that $a > 1$.
Let $r \in \Q_{> 0}$ be a strictly positive rational number such that $r < 1$.
Then:
:$1 < a^r < 1 + a r$

Proof:
Define a real function $g_r: \R_{> 0} \to \R$ as:
:$\map {g_r} a = 1 + a r - a^r$
Then differentiating {{WRT|Differentiation}} $a$ gives:
:$D_a \map {g_r} a = r \paren {1 - a^{r - 1} }$
We show now that the derivative of $g_r$ is positive for all $a > 1$:
{{begin-eqn}}
{{eqn | l = r
      | o = <
      | r = 1
}}
{{eqn | ll= \leadsto
      | l = r - 1
      | o = <
      | r = 0
      | c = Subtract $1$ from both sides
}}
{{eqn | ll= \leadsto
      | l = a^{r - 1}
      | o = <
      | r = a^0
      | c = Power Function on Base Greater than One is Strictly Increasing: Rational Number
}}
{{eqn | ll= \leadsto
      | l = a^{r - 1}
      | o = <
      | r = 1
      | c = {{Defof|Integer Power}}
}}
{{eqn | ll= \leadsto
      | l = -1 
      | o = <
      | r = -a^{r - 1}
      | c = Order of Real Numbers is Dual of Order of their Negatives
}}
{{eqn | ll= \leadsto
      | l = 0 
      | o = <
      | r = 1 - a^{r - 1}
      | c = adding $1$ to both sides
}}
{{eqn | ll= \leadsto
      | l = 0 
      | o = <
      | r = r \left({1 - a^{r - 1} }\right)
      | c = multiplying both sides by $r > 0$
}}
{{eqn | ll= \leadsto
      | l = 0 
      | o = <
      | r = D_a \map {g_r} a
      | c = from the formula found for $D_a \map {g_r} a$ above
}}
{{end-eqn}}
So $D_a \map {g_r} a$ is positive for all $a > 1$.
Whence, by Derivative of Monotone Function, $g_r$ is increasing for all $a > 1$.
Now:
:$\map {g_r} 1 = r > 0$
So $\map {g_r} a$ is positive for all $a > 1$.
That is:
:$0 < 1 + a r - a^r$
Adding $a^r$ to both sides of the above yields:
:$a^r < 1 + a r$
Finally:
{{begin-eqn}}
{{eqn | l = 0
      | o = <
      | r = r
}}
{{eqn | ll= \leadsto
      | l = a^0
      | o = <
      | r = a^r
      | c = Power Function on Base Greater than One is Strictly Increasing: Rational Number
}}
{{eqn | ll= \leadsto
      | l = 1
      | o = <
      | r = a^r
      | c = {{Defof|Integer Power}}
}}
{{end-eqn}}
So, for $0 < r < 1$:
:$1 < a^r < 1 + a r$
{{qed}}
Category:Powers
ee733l081xaewexuydgpzitbjpw99in
Theorem: Power Function on Base greater than One tends to One as Power tends to Zero/Rational Number

Let $a \in \R_{> 0}$ be a strictly positive real number such that $a > 1$.
Let $f: \Q \to \R$ be the real-valued function defined as:
:$\map f r = a^r$
where $a^r$ denotes $a$ to the power of $r$.
Then:
:$\ds \lim_{r \mathop \to 0} \map f r = 1$

Proof:
We start by treating the right-sided limit.
Let $0 < r < 1$.
Theorem: Power Function on Base between Zero and One Tends to One as Power Tends to Zero/Rational Number

Let $a \in \R_{> 0}$ be a strictly positive real number such that $0 < a < 1$.
Let $f: \Q \to \R$ be the real-valued function defined as:
:$\map f r = a^r$
where $a^r$ denotes $a$ to the power of $r$.
Then:
:$\ds \lim_{r \mathop \to 0} \map f r = 1$

Proof:
From Ordering of Reciprocals:
:$0 < a < 1 \implies 1 < \dfrac 1 a$
So:
{{begin-eqn}}
{{eqn | l = \lim_{r \mathop \to 0} \paren {\frac 1 a}^r
      | r = 1
      | c = Power Function on Base greater than One tends to One as Power tends to Zero: Rational Number
}}
{{eqn | ll= \leadsto
      | l = \lim_{r \mathop \to 0} \frac 1 {a^r}
      | r = 1
      | c = Power of Quotient: Rational Numbers
}}
{{eqn | ll= \leadsto
      | l = \frac 1 {\ds \lim_{r \mathop \to 0} a^r}
      | r = 1
      | c = Quotient Rule for Limits of Real Functions
}}
{{eqn | ll= \leadsto
      | l = \lim_{r \mathop \to 0} a^r 
      | r = 1
      | c = taking reciprocal of each side
}}
{{end-eqn}}
{{qed}}
Category:Powers
fv1iupyrsarv7biirg38lcru8b8rx3k
Theorem: Euler's Number to Rational Power permits Unique Continuous Extension

Let $e$ be Euler's number.
Let $f: \Q \to \R$ be the real-valued function defined as:
:$f \left({q}\right) = e^q$
where $e^q$ denotes  $e$ to the power of $q$.
Then there exists a unique continuous extension of $f$ to $\R$.

Proof:
Since $e > 0$, we may apply Power Function to Rational Power permits Unique Continuous Extension.
Hence the result.
{{qed}}
Category:Exponential Function
j3aj4ucitdfj9juy3c0f2ti85dhfkmm
Theorem: Open Unit Interval is Proper Subset of Closed Unit Interval

The open unit interval:
:$I_o = \openint 0 1$
is a proper subset of the closed unit interval:
:$I_c = \closedint 0 1$

Proof:
Let $x \in I_o$.
Then by definition:
:$0 < x < 1$
and so:
:$0 \le x \le 1$
and so:
:$x \in I_c$.
Thus:
:$I_o \subseteq I_c$
Consider:
:$0 \in I_c$
by definition of closed interval.
But it is not the case that $0 < 0$.
So $0 \notin I_o$ and so $I_c \nsubseteq I_o$.
Hence the result by definition of proper subset.
{{qed}}
Theorem: Vector Cross Product satisfies Jacobi Identity

Let $\mathbf a, \mathbf b, \mathbf c$ be vectors in $3$ dimensional Euclidean space.
Let $\times$ denotes the cross product.
Then:
:$\mathbf a \times \paren {\mathbf b \times \mathbf c} + \mathbf b \times \paren {\mathbf c \times \mathbf a} + \mathbf c \times \paren {\mathbf a \times \mathbf b} = \mathbf 0$
That is, the cross product operation satisfies the Jacobi identity.

Proof:
{{begin-eqn}}
{{eqn | l = \mathbf a \times \paren {\mathbf b \times \mathbf c} + \mathbf b \times \paren {\mathbf c \times \mathbf a} + \mathbf c \times \paren {\mathbf a \times \mathbf b}
      | r = \paren {\mathbf {a \cdot c} } \mathbf b - \paren {\mathbf {a \cdot b} } \mathbf c
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = \paren {\mathbf {b \cdot a} } \mathbf c - \paren {\mathbf {b \cdot c} } \mathbf a
      | c = 
}}
{{eqn | o =
      | ro= +
      | r = \paren {\mathbf {c \cdot b} } \mathbf a - \paren {\mathbf {c \cdot a} } \mathbf b
      | c = Lagrange's Formula
}}
{{eqn | r = \mathbf 0
      | c = Dot Product Operator is Commutative
}}
{{end-eqn}}
{{qed}}
Category:Vector Cross Product
Category:Jacobi Identity
Category:Algebra
tkqigial39c0o4i5xgvg4qsvs9pcc55
Theorem: Meet-Continuous and Distributive implies Shift Mapping Preserves Finite Suprema

Let $\struct {S, \vee, \wedge, \preceq}$ be a meet-continuous distributive complete lattice.
Let $x \in S$.
Let $f: S \to S$ be a mapping such that
:$\forall y \in S: \map f y = x \wedge y$
Then
:$f$ preserves finite suprema

Proof:
Let $X$ be finite subset of $S$ such that:
:$X$ admits a supremum
By definition of complete lattice:
:$f \sqbrk X$ admits a supremum
We will prove the result by induction on the cardinality of $X$.
Theorem: Set Union is not Cancellable

Set union is not a cancellable operation.
That is, for a given $A, B, C \subseteq S$ for some $S$, it is not always the case that:
:$A \cup B = A \cup C \implies B = C$

Proof:
Proof by Counterexample:
Let $S = \set {a, b}$.
Let:
:$A = \set {a, b}$
:$B = \set a$
:$C = \set b$
Then:
{{begin-eqn}}
{{eqn | l = A \cup B
      | r = \set {a, b}
      | c = 
}}
{{eqn | r = A \cup C
      | c = 
}}
{{end-eqn}}
but:
{{begin-eqn}}
{{eqn | l = B
      | r = \set a
      | c = 
}}
{{eqn | o = \ne
      | r = \set b
      | c = 
}}
{{eqn | r = C
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Set Intersection is not Cancellable

Set intersection is not a cancellable operation.
That is, for a given $A, B, C \subseteq S$ for some $S$, it is not always the case that:
:$A \cap B = A \cap C \implies B = C$

Proof:
Proof by Counterexample:
Let $S = \set {a, b, c}$.
Let:
:$A = \set a$
:$B = \set {a, b}$
:$C = \set {a, c}$
Then:
{{begin-eqn}}
{{eqn | l = A \cap B
      | r = \set a
      | c = 
}}
{{eqn | r = A \cap C
      | c = 
}}
{{end-eqn}}
but:
{{begin-eqn}}
{{eqn | l = B
      | r = \set {a, b}
      | c = 
}}
{{eqn | o = \ne
      | r = \set {a, c}
      | c = 
}}
{{eqn | r = C
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Intersection of Real Intervals is Real Interval

Let $I_1$ and $I_2$ be real intervals.
Then $I_1 \cap I_2$ is also a real interval.

Proof:
Let $x, y \in I_1 \cap I_2$. 
From the definition of a real interval, it suffices to show that:
:for each $z \in \R$ with $x \le z \le y$ we have $z \in I_1 \cap I_2$.
Let $z$ be a real number with:
:$x \le z \le y$
Since $x, y \in I_1$, we have: 
:$z \in I_1$
from the definition of a real interval.
Similarly, since $x, y \in I_2$, we have:
:$z \in I_2$
from the definition of a real interval.
So:
:$z \in I_1 \cap I_2$
as required.
{{qed}}
Theorem: Union of Real Intervals is not necessarily Real Interval

Let $I_1$ and $I_2$ be real intervals.
Then $I_1 \cup I_2$ is not necessarily a real interval.

Proof:
Proof by Counterexample:
Consider the real intervals:
:$I_1 = \left({0 \,.\,.\, 2}\right)$
:$I_2 = \left({4 \,.\,.\, 6}\right)$
Then we have that:
:$1 < 3 < 5$
where:
:$1 \in I_1 \cup I_2$
:$5 \in I_1 \cup I_2$
but:
:$3 \notin I_1 \cup I_2$
Thus $I_1 \cup I_2$ is not a real interval.
{{qed}}
Theorem: Domain of Real Square Function

The domain of the real square function is the entire set of real numbers $\R$.

Proof:
The operation of real multiplication is defined on all real numbers.
Thus:
:$\forall x \in \R: \exists y \in \R: x^2 = y$
Hence the result by definition of domain.
{{qed}}
Theorem: Image of Real Square Function

The image of the real square function is the entire set of positive real numbers $\R_{\ge 0}$.

Proof:
From Square of Real Number is Non-Negative, the image of $f$ is $\R_{\ge 0}$.
From Positive Real has Real Square Root:
:$\forall x \in \R: \exists y \in \R: x^2 = y$
Hence the result by definition of image.
{{qed}}
Theorem: Domain of Real Square Root Function

The domain of the real square root function is the set of positive real numbers $\R_{\ge 0}$:
:$\set{x \in \R: x \ge 0}$

Proof:
From Square of Real Number is Non-Negative:
:$\forall x \in \R: x^2 \ge 0$
Hence the result by definition of domain.
{{qed}}
Theorem: Exponent Combination Laws/Product of Powers/Proof 1

Let $a \in \R_{> 0}$ be a positive real number.
Let $x, y \in \R$ be real numbers.
Let $a^x$ be defined as $a$ to the power of $x$.
Then:
:$a^x a^y = a^{x + y}$

Proof:
{{begin-eqn}}
{{eqn | l = a^{x + y}
      | r = \map \exp {\paren {x + y} \ln a}
      | c = {{Defof|Power to Real Number}}
}}
{{eqn | r = \map \exp {x \ln a + y \ln a}
      | c = 
}}
{{eqn | r = \map \exp {x \ln a} \, \map \exp {y \ln a}
      | c = Exponential of Sum
}}
{{eqn | r = a^x a^y
      | c = {{Defof|Power to Real Number}}
}}
{{end-eqn}}
{{qed}}
Theorem: 2197 is Cube of 13

:$13^3 = 2197$

Proof:
By long multiplication:
<pre>
   13
 x 13
-----
   39
  130
-----
  169
-----
</pre>
then:
<pre>
 x 169
    13
------
   507
  1690
-----
  2197
------
</pre>
{{qed}}
Theorem: Inequality of Product of Unequal Numbers

Let $a, b, c, d \in \R$.
Then:
:$0 < a < b \land 0 < c < d \implies 0 < a c < b d$

Proof:
{{begin-eqn}}
{{eqn | n = 1
      | o = 
      | r = 0 < a < b
      | c = 
}}
{{eqn | n = 2
      | o = \leadsto
      | r = 0 < b
      | c = Ordering is Transitive
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | n = 3
      | o = 
      | r = 0 < c < d
      | c = 
}}
{{eqn | n = 4
      | o = \leadsto
      | r = 0 < c
      | c = Ordering is Transitive
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | o = \leadsto
      | r = 0 < a c < b c
      | c = $(1)$ and $(4)$: {{Real-number-axiom|O2}}
}}
{{eqn | o = 
      | r = 0 < b c < b d
      | c = $(2)$ and $(3)$: {{Real-number-axiom|O2}}
}}
{{eqn | o = \leadsto
      | r = 0 < a c < b d
      | c = Ordering is Transitive
}}
{{end-eqn}}
{{qed}}
Category:Inequalities
Category:Real Multiplication
s7rvvofnn9r2w3qz8d53j55qqk3l9ie
Theorem: Negative of Absolute Value/Corollary 3

Let $y \in \R_{\ge 0}$.
Let $z \in \R$.
Then:
:$\size {x - z} < y \iff z - y < x < z + y$

Proof:
{{begin-eqn}}
{{eqn | l = \size {x - z}
      | o = <
      | m = y
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = -y
      | o = <
      | m = x - z
      | mo= <
      | r = y
      | c = {{Corollary|Negative of Absolute Value|1}}
}}
{{eqn | ll= \leadstoandfrom
      | l = z - y
      | o = <
      | m = x
      | mo= <
      | r = z + y
      | c = Real Number Ordering is Compatible with Addition
}}
{{end-eqn}}
{{qed}}
Category:Negative of Absolute Value
ji3f40avtl2zqo0afi6xm8gejkor0lj
Theorem: Exponent Combination Laws/Product of Powers/Proof 2/Lemma

Let $x_1, x_2, y_1, y_2 \in \R_{>0}$ be strictly positive real numbers.
Let $\epsilon \in \openint 0 {\min \set {y_1, y_2, 1} }$.
Then:
:$\size {x_1 - y_1} < \epsilon \land \size {x_2 - y_2} < \epsilon \implies \size {x_1 x_2 - y_1 y_2} < \epsilon \paren {y_1 + y_2 + 1}$

Proof:
First:
{{begin-eqn}}
{{eqn | l = \epsilon
      | o = <
      | r = \min \set {y_1, y_2, 1}
}}
{{eqn | ll= \leadsto
      | l = \epsilon
      | o = <
      | r = y_1
      | c = {{Defof|Min Operation}}
}}
{{eqn | ll= \leadsto
      | l = \epsilon - \epsilon
      | o = <
      | r = y_1 - \epsilon
      | c = subtracting $\epsilon$ from both sides
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = 0
      | o = <
      | r = y_1 - \epsilon
}}
{{end-eqn}}
The same logic, {{mutatis}}, shows that $0 < y_2 - \epsilon$.
From {{Corollary|Negative of Absolute Value|3}}:
{{begin-eqn}}
{{eqn | l = \size {x_1 - y_1} < \epsilon
      | o = \implies
      | r = y_1 - \epsilon < x_1 < y_1 - \epsilon
}}
{{eqn | l = \size {x_2 - y_2} < \epsilon
      | o = \implies
      | r = y_2 - \epsilon < x_2 < y_2 - \epsilon
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = \paren {y_1 - \epsilon} \paren {y_2 - \epsilon}
      | o = <
      | m = x_1 x_2
      | mo= <
      | r = \paren {y_1 + \epsilon} \paren {y_1 + \epsilon}
      | c = Inequality of Product of Unequal Numbers: from $(1)$
}}
{{eqn | ll= \leadsto
      | l = y_1 y_2 - \epsilon \paren {y_1 + y_2} + \epsilon^2
      | o = <
      | m = x_1 x_2
      | mo= <
      | r = y_1 y_2 + \epsilon \paren {y_1 + y_2} + \epsilon^2
      | c = Distributive Property
}}
{{eqn | ll= \leadsto
      | l = y_1 y_2 - \epsilon \paren {y_1 + y_2} - \epsilon^2
      | o = <
      | m = x_1 x_2
      | mo= <
      | r = y_1 y_2 + \epsilon \paren {y_1 + y_2} + \epsilon^2
      | c = Square of Non-Zero Real Number is Strictly Positive
}}
{{end-eqn}}
Subtracting $y_1 y_2$ from all sections of the inequality:
:$-\epsilon \paren {y_1 + y_2} - \epsilon^2 < x_1 x_2 - y_1 y_2 < \epsilon \paren {y_1 + y_2} + \epsilon^2$
If follows that:
{{begin-eqn}}
{{eqn | l = \size {x_1 x_2 - y_1 y_2}
      | o = <
      | r = \epsilon \paren {y_1 + y_2} + \epsilon^2
      | c = {{Corollary|Negative of Absolute Value|1}}
}}
{{eqn | o = <
      | r = \epsilon \paren {y_1 + y_2} + \epsilon
      | c = Since $\epsilon < \min \size {y_1, y_2, 1} < 1$, we may apply Real Number between Zero and One is Greater than Square
}}
{{eqn | o = <
      | r = \epsilon \paren {y_1 + y_2 + 1}
      | c = Distributive Property
}}
{{end-eqn}}
Hence the result.
{{qed}}
Category:Exponent Combination Laws
7d00dcjw2i0uvtvb8tp2cshhp53ts4y