nyuuzyou/wikis huggingface dataset:
Substitution Theorem for Terms

== Theorem ==
Let $\beta, \tau$ be terms.
Let $x \in \mathrm {VAR}$ be a variable.
Let $\map \beta {x \gets \tau}$ be the substitution instance of $\beta$ substituting $\tau$ for $x$.
Let $\AA$ be a structure for predicate logic.
Let $\sigma$ be an assignment for $\beta$ and $\tau$.
Suppose that:
:$\map {\operatorname{val}_\AA} \tau \sqbrk \sigma = a$
where $\map {\operatorname{val}_\AA} \tau \sqbrk \sigma$ is the value of $\tau$ under $\sigma$.
Then:
:$\map {\operatorname{val}_\AA} {\map \beta {x \gets \tau} } \sqbrk \sigma = \map {\operatorname{val}_\AA} \beta \sqbrk {\sigma + \paren {x / a} }$
where $\sigma + \paren {x / a}$ is the extension of $\sigma$ by mapping $x$ to $a$.
== Proof ==
Proceed by the Principle of Structural Induction on the definition of term, applied to $\beta$.
If $\beta = y$ for some variable $y$, then:
:$\map \beta {x \gets \tau} = \begin {cases} \tau & : \text{if $y = x$} \\ y & : \text {otherwise} \end {cases}$
In the first case:
In the second case:
as desired.
If $\beta = \map f {\tau_1, \ldots, \tau_n}$ and the induction hypothesis holds for $\tau_1, \ldots, \tau_n$, then:
:$\map \beta {x \gets \tau} = \map f {\map {\tau_1} {x \gets \tau}, \ldots, \map {\tau_n} {x \gets \tau} }$
Now:
as desired.
The result follows by the Principle of Structural Induction.
== Sources ==
* : $\text {II}.8$ Further Semantic Notions: Lemma $\text {II}.8.7$
Category:Named Theorems
Category:Predicate Logic
Substitution Theorem for Well-Formed Formulas/Corollary

== Corollary to Substitution Theorem for Well-Formed Formulas ==
Let $\map {\mathbf A} {x_1, \ldots, x_n}$ be a WFF whose free variables are among $x_1, \ldots, x_n$.
Let $\tau_1, \ldots, \tau_n$ be closed terms, and let each $\tau_i$ be freely substitutable for $x_i$.
Let $a_i = \map {\operatorname{val}_\AA} {\tau_i}$, where $\operatorname{val}_\AA$ denotes the value of $\tau$ in $\AA$.
Then:
:$\AA \models_{\mathrm{PL}} \map {\mathbf A} {\tau_1, \ldots, \tau_n}$ $\AA \models_{\mathrm{PL_A}} \mathbf A \sqbrk {a_1, \ldots, a_n}$
where $\models_{\mathrm{PL}}$ denotes model of sentence, and $\models_{\mathrm{PL_A}}$ denotes model of formula.
== Proof ==
Applying the Substitution Theorem for Well-Formed Formulas $n$ times:
The result follows from the definitions of model of sentence and model of formula.
== Sources ==
* : $\mathrm{II}.8$ Further Semantic Notions: Lemma $\mathrm{II.8.13}$
Category:Predicate Logic
Substitution for Equivalent Subformula is Equivalent

== Theorem ==
Let $\mathbf B$ a WFF of propositional logic.
Let $\mathbf A, \mathbf A'$ be equivalent WFFs.
Let $\mathbf A$ be a subformula of $\mathbf B$.
Let $\mathbf B' = \map {\mathbf B} {\mathbf A \,//\, \mathbf A'}$ be the substitution of $\mathbf A'$ for $\mathbf A$ in $\mathbf B$.
Then $\mathbf B$ and $\mathbf B'$ are equivalent.
== Proof ==
Let $v$ be an arbitrary boolean interpretation.
Then $\map v {\mathbf A} = \map v {\mathbf A'}$.
It is to be shown that $\map v {\mathbf B} = \map v {\mathbf B'}$.
We proceed by induction.
Let $\map n {\mathbf B}$ be the number of WFFs $\mathbf C$ such that:
:$\mathbf A$ is a subformula of $\mathbf C$, and $\mathbf C$ is a subformula of $\mathbf B$.
Note that $\map n {\mathbf B} \ne 0$, for $\mathbf C = \mathbf A$ is a valid choice.
Suppose now that $\map n {\mathbf B} = 1$.
Because we have the valid choices $\mathbf C = \mathbf A$ and $\mathbf C = \mathbf B$, it follows that these choices must be identical, i.e. $\mathbf A = \mathbf B$.
Hence $\mathbf B' = \mathbf A'$, and so:
:$\map v {\mathbf B} = \map v {\mathbf B'}$
Suppose now that the assertion is true for all $\mathbf B$ with $\map n {\mathbf B} \le n$.
Let $\map n {\mathbf B} = n + 1$.
Suppose $\mathbf B = \neg \mathbf B_1$.
Then obviously $\map n {\mathbf B_1} = n$, so by hypothesis:
:$\map v {\mathbf B_1} = \map v {\map {\mathbf B_1} {\mathbf A \,//\, \mathbf A'} }$
Also, by definition of substitution:
:$\mathbf B' = \neg \map {\mathbf B_1} {\mathbf A \,//\, \mathbf A'}$
Now, by definition of boolean interpretation:
Suppose now that $\mathbf B = \mathbf B_1 \mathbin{\mathsf B} \mathbf B_2$ for a binary connective $\mathsf B$.
Then $\map n {\mathbf B_1}, \map n {\mathbf B_2} \le n$, so:
:$\map v {\mathbf B_1} = \map v {\map {\mathbf B_1} {\mathbf A \,//\, \mathbf A'} }$
:$\map v {\mathbf B_2} = \map v {\map {\mathbf B_2} {\mathbf A \,//\, \mathbf A'} }$
This follows by either the induction hypothesis, or when $\mathbf A$ is not a subformula of $\mathbf B_1$ or $\mathbf B_2$, is entirely trivial, considering the substitution does not change anything.
Also, by definition of substitution:
:$\mathbf B' = \map {\mathbf B_1} {\mathbf A \,//\, \mathbf A'} \mathbin {\mathsf B} \map {\mathbf B_2} {\mathbf A \,//\, \mathbf A'}$
Now, by definition of boolean interpretation:
By definition of the language of propositional logic, $\mathbf B$ must have either of the above forms.
Hence the result, from the Second Principle of Mathematical Induction.
== Sources ==
* : $\S 2.3.2$: Theorem $2.34$
Category:Boolean Interpretations
Category:Propositional Logic
Substitution in Big-O Estimate/General Result

== Theorem ==
Let $X$ and $Y$ be topological spaces.
Let $V$ be a normed vector space over $\R$ or $\C$ with norm $\norm {\,\cdot\,}$.
Let $x_0 \in X$ and $y_0 \in Y$.
Let $f: X \to Y$ be a function with $\map f {x_0} = y_0$ that is continuous at $x_0$.
Let $g, h: Y \to V$ be functions.
Suppose $\map g y = \map O {\map h y}$ as $y \to y_0$, where $O$ denotes big-O notation.
Then $\map {\paren {g \circ f} } x = \map O {\map {\paren {h \circ f} } x}$ as $x \to x_0$.
== Proof ==
Because $g = \map O h$, there exists a neighborhood $V$ of $y_0$ and a real number $c$ such that:
:$\norm {\map g x} \le c \cdot \norm {\map h x}$ for all $y \in V$.
By definition of continuity, there exists a neighborhood $U$ of $x_0$ with $\map f U \subset V$.
For $x \in U$, we have:
:$\norm {\map g {\map f x} } \le c \cdot \norm {\map h {\map f x} }$
Thus $g \circ f = \map O {h \circ f}$ as $x \to x_0$.
Category:Big-O Notation
Substitution in Big-O Estimate/Real Analysis

== Theorem ==
Let $f$ and $g$ be real-valued or complex-valued functions defined on a neighborhood of $+ \infty$ in $\R$.
Let $f = \map \OO g$, where $\OO$ denotes big-O notation.
Let $h$ be a real-valued defined on a neighborhood of $+ \infty$ in $\R$.
Let $\ds \lim_{x \mathop \to +\infty} \map h x = +\infty$.
Then:
:$f \circ h = \map \OO {g \circ h}$ as $x \to +\infty$.
== Proof ==
Category:Big-O Notation
Substitution in Big-O Estimate/Sequences

== Theorem ==
Let $\sequence {a_n}$ and $\sequence {b_n}$ be sequences of real or complex numbers.
Let $a_n = \map \OO {b_n}$ where $\OO$ denotes big-O notation.
Let $\sequence {n_k}$ be a diverging sequence of natural numbers.
Then $a_{n_k} = \map \OO {b_{n_k} }$.
== Proof ==
Because $a_n = \map \OO {b_n}$, there exists $M \ge 0$ and $n_0 \in \N$ such that $\size {a_n} \le M \cdot \size {b_n}$ for $n \ge n_0$.
Because $n_k$ diverges, there exists $k_0 \in \N$ such that $n_k \ge n_0$ for $k \ge k_0$.
Then $\size {a_{n_k} } \le M \cdot \size {b_{n_k} }$ for $k \ge k_0$.
Thus:
:$a_{n_k} = \map \OO {b_{n_k} }$
Category:Big-O Notation
Substitution of Arithmetically Definable Functions is Arithmetically Definable

== Theorem ==
Let $f: \N^t \to \N$ and $g_1, g_2, \dotsc, g_t: \N^k \to \N$ be partial functions.
Let $h: \N^k \to \N$ be defined by substitution as:
:$\map h {x_1, \dotsc, x_k} \approx \map f {\map {g_1} {x_1, \dotsc, x_k}, \dotsc, \map {g_t} {x_1, \dotsc, x_k} }$ 
Suppose that there exists a $\Sigma_1$ WFF of $t + 1$ free variables:
:$\map {\phi_f} {y, x_1, \dotsc, x_t}$
such that:
:$y = \map f {x_1, \dotsc, x_t} \iff \N \models \map {\phi_f} {\sqbrk y, \sqbrk {x_1}, \dotsc, \sqbrk {x_t} }$
where $\sqbrk a$ denotes the unary representation of $a \in \N$.
Suppose also that there exist $\Sigma_1$ WFFs of $k + 1$ free variables:
:$\map {\phi_{g_1} } {y, x_1, \dotsc, x_k}$
:$\dots$
:$\map {\phi_{g_t} } {y, x_1, \dotsc, x_k}$
such that:
:$y = \map {g_i} {x_1, \dotsc, x_k} \iff \N \models \map {\phi_{g_i} } {\sqbrk y, \sqbrk {x_1}, \dotsc, \sqbrk {x_k} }$
for each $1 \le i \le t$.
Then there exists a $\Sigma_1$ WFF of $k + 1$ free variables:
:$\map {\phi_h} {y, x_1, \dotsc, x_k}$
such that:
:$y = \map h {x_1, \dotsc, x_k} \iff \N \models \map {\phi_h} {\sqbrk y, \sqbrk {x_1}, \dotsc, \sqbrk {x_k} }$
== Proof ==
Define:
:$\map {\phi_h} {y, x_1, \dotsc, x_k} := \exists s_1: \dotsm \exists s_t: \map {\phi_f} {y, s_1, \dotsc, s_t} \land \map {\phi_{g_1} } {s_1, x_1, \dotsc, x_k} \land \dotso \land \map {\phi_{g_t} } {s_t, x_1, \dotsc, x_k}$
Correctness is apparent.
That $\phi_h$ is $\Sigma_1$ follows from Conjunction of Existential Quantifier.
Category:Primitive Recursive Functions
Substitution of Constant yields Primitive Recursive Function

== Theorem ==
Let $f: \N^{k + 1} \to \N$ be a primitive recursive function‎.
Then $g: \N^k \to \N$ given by:
:$\map g {n_1, n_2, \ldots, n_k} = \map f {n_1, n_2, \ldots, n_{i - 1}, a, n_i \ldots, n_k}$
is primitive recursive.
== Proof ==
Let $n = \tuple {n_1, n_2, \ldots, n_{i - 1}, n_i \ldots, n_k}$.
We see that:
:$\map g {n_1, n_2, \ldots, n_k} = \map f {\map {\pr^k_1} n, \map {\pr^k_2} n, \ldots, \map {\pr^k_{i - 1} } n, \map {f_a} n, \map {\pr^k_i} n, \ldots, \map {\pr^k_k} n}$
We have that:
* $\pr^k_j$ is a basic primitive recursive‎ function for all $j$ such that $1 \ne j \le k$
* $f_a$ is a primitive recursive‎ function.
So $g$ is obtained by substitution from primitive recursive‎ functions and so is primitive recursive‎.
Category:Primitive Recursive Functions
Substitution of Elements

== Theorem ==
Let $a$, $b$, and $x$ be sets.
:$a = b \implies \paren {a \in x \iff b \in x}$
== Proof ==
By the Axiom of Extension:
:$a = b \implies \paren {a \in x \implies b \in x}$
Equality is Symmetric, so also by the Axiom of Extension:
:$a = b \implies \paren {b \in x \implies a \in x}$
== Sources ==
* : $\S 3.3$
Category:Set Theory
Substitutivity of Class Equality

== Theorem ==
Let $A$ and $B$ be classes.
Let $\map P A$ be a well-formed formula of the language of set theory.
Let $\map P B$ be the same proposition $\map P A$ with all instances of $A$ replaced with instances of $B$.
Let $=$ denote class equality.
:$A = B \implies \paren {\map P A \iff \map P B}$
== Proof ==
By induction on the well-formed parts of $\map P A$.
The proof shall use $\implies$ and $\neg$ as the primitive connectives.
=== Atoms ===
First, to prove the statement if $A$ and $B$ are elements of some other class $C$:
Then, if $A$ and $B$ have $C$ as an element:
Recall that for $A \in B$ it has to be the case that $A$ is not a proper class, but a set.
=== Inductive Step for $\implies$ ===
Suppose that $\map P A$ is of the form $\map Q A \implies \map R A$
Furthermore, suppose that:
:$A = B \implies \paren {\map Q A \iff \map Q B}$
and:
:$A = B \implies \paren {\map R A \iff \map R B}$
It follows that:
:$A = B \implies \paren {\paren {\map Q A \implies \map R A} \iff \paren {\map Q B \implies \map R B} }$
:$A = B \implies \paren {\map P A \iff \map P B}$
=== Inductive Step for $\neg$ ===
Suppose that $\map P A$ is of the form $\neg \map Q A$
Furthermore, suppose that:
:$A = B \implies \paren {\map Q A \iff \map Q B}$
It follows that:
:$A = B \implies \paren {\neg \map Q A \iff \neg \map Q B}$
:$A = B \implies \paren {\map P A \iff \map P B}$
=== Inductive Step for $\forall x:$ ===
Suppose that $\map P A$ is of the form $\forall z: \map Q {x, z}$
If $x$ and $z$ are the same variable, then $x$ is a bound variable and the theorem holds trivially.
If $x$ and $z$ are distinct, then:
== Also see ==
* Axiom:Leibniz's Law
== Sources ==
* : $\S 4.8$
Category:Class Theory
Substitutivity of Equality

== Theorem ==
Let $x$ and $y$ be sets.
Let $\map P x$ be a well-formed formula of the language of set theory.
Let $\map P y$ be the same proposition $\map P x$ with some (not necessarily all) free instances of $x$ replaced with free instances of $y$.
Let $=$ denote set equality.
:$x = y \implies \paren {\map P x \iff \map P y}$
== Proof ==
By induction on the well-formed parts of $\map P x$.
The proof shall use $\implies$ and $\neg$ as the primitive connectives.
=== Atoms ===
:$x = y \implies \paren {x \in z \iff y \in z}$ by Substitution of Elements.
:$x = y \implies \paren {z \in x \iff z \in y}$ by definition of Set Equality.
=== Inductive Step for $\implies$ ===
Suppose that $\map P x$ is of the form $\map Q x \implies \map R x$
Furthermore, suppose that:
:$x = y \implies \paren {\map Q x \iff \map Q y}$
and:
:$x = y \implies \paren {\map R x \iff \map R y}$
It follows that:
:$x = y \implies \paren {\paren {\map Q x \implies \map R x} \iff \paren {\map Q y \implies \map R y} }$
:$x = y \implies \paren {\map P x \iff \map P y}$
=== Inductive Step for $\neg$ ===
Suppose that $\map P x$ is of the form $\neg \map Q x$
Furthermore, suppose that:
:$x = y \implies \paren {\map Q x \iff \map Q y}$
It follows that:
:$x = y \implies \paren { \neg \map Q x \iff \neg \map Q y}$
:$x = y \implies \paren {\map P x \iff \map P y}$
=== Inductive Step for $\forall x:$ ===
Suppose that $\map P x$ is of the form $\forall z: \map Q {x, z}$
If $x$ and $z$ are the same variable, then $x$ is a bound variable and the theorem holds trivially.
If $x$ and $z$ are distinct, then:
== Also see ==
* Axiom:Leibniz's Law
== Sources ==
* : $\S 3.4$
Category:Set Theory
Category:Equality
Substructure of Entropic Structure is Entropic

== Theorem ==
Let $\struct {S, \odot}$ be an entropic structure:
:$\forall a, b, c, d \in S: \paren {a \odot b} \odot \paren {c \odot d} = \paren {a \odot c} \odot \paren {b \odot d}$
Let $\struct {T, \odot_T}$ be a substructure of $\struct {S, \odot}$.
Then $\struct {T, \odot_T}$ is also an entropic structure.
== Proof ==
Category:Entropic Structures
Subtract Half is Replicative Function

== Theorem ==
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 ==
Hence the result by definition of replicative function.
== Sources ==
* : $\S 1.2.4$: Integer Functions and Elementary Number Theory: Exercise $39 \ \text{a)}$
Category:Replicative Functions
Subtraction Formulas for Hyperbolic Functions

== Theorem ==
=== Hyperbolic Sine of Difference ===
=== Hyperbolic Cosine of Difference ===
=== Hyperbolic Tangent of Difference ===
=== Hyperbolic Cotangent of Difference ===
== Also see ==
* Addition Formulas for Hyperbolic Functions
* Subtraction Formulas
* Addition Formulas
Category:Subtraction Formulas for Hyperbolic Functions
Category:Hyperbolic Identities
Subtraction has no Identity Element

== Theorem ==
The operation of subtraction on numbers of any kind has no identity.
== Proof ==
 there exists an identity $e$ in one of the standard number systems $\GF$.
That is:
:$\forall x \in \GF: x = e$
But from Identity is Unique, if $e$ is an identity then there can be only one such.
From Proof by Contradiction it follows that $\GF$ has no such $e$.
== Sources ==
* : $\S 4.3$. Units and zeros: Example $72$
Category:Numbers
Category:Subtraction
Category:Examples of Identity Elements
Subtraction of Complex Numbers

== Theorem ==
Let $z_1 := a_1 + i b_1$ and $z_2 := a_2 + i b_2$ be complex numbers.
The subtraction operation on $z_1$ and $z_2$ is:
:$z_1 - z_2 = \paren {a_1 - a_2} + i \paren {b_1 - b_2}$
== Proof ==
== Sources ==
* : $\S 1.2$. The Algebraic Theory
* : $\S 6$: Complex Numbers: Subtraction of Complex Numbers: $6.3$
* : $1$: Complex Numbers: Fundamental Operations with Complex Numbers: $2$. Subtraction
* : $\S 4$: Complex Numbers: Arithmetic of Complex Numbers: $4.3.$
Category:Complex Subtraction
Subtraction of Divisors obeys Distributive Law

== Theorem ==
In modern algebraic language:
:$a = \dfrac 1 n b, c = \dfrac 1 n d \implies a - c = \dfrac 1 n \paren {b - d}$
== Euclid's Proof ==
== Modern Proof ==
Category:Algebra
Category:Subtraction of Divisors obeys Distributive Law
Subtraction of Divisors obeys Distributive Law/Proof 1

== Theorem ==
== Proof ==
Let $AB$ be that aliquot part of the (natural) number $CD$ which $AE$ subtracted is of $CF$ subtracted.
We need to show that the remainder $EB$ is also the same part of the number $CD$ which $AE$ subtracted is of $CF$ subtracted.
:
Whatever part $AE$ is of $CF$, let the same part $EB$ be of $CG$.
Then from , whatever aliquot part $AE$ is of $CF$, the same aliquot part also is $AB$ of $GF$.
But whatever aliquot part $AE$ is of $CF$, the same aliquot part also is $AB$ of $CD$, by hypothesis.
Therefore, whatever aliquot part $AB$ is of $GF$, the same aliquot part is it of $CD$ also.
Therefore $GF = CD$.
Let $CF$ be subtracted from each.
Therefore $GC = FD$.
We have that whatever aliquot part $AE$ is of $CF$, the same aliquot part also is $EB$ of $CG$
Therefore whatever aliquot part $AE$ is of $CF$, the same aliquot part also is $EB$ of $FD$.
But whatever aliquot part $AE$ is of $CF$, the same aliquot part also is $AB$ of $CD$.
Therefore the remainder $EB$ is the same aliquot part of the remainder $FD$ that the whole $AB$ is of the whole $CD$.
== Sources ==
* : Book $\text{VII}$. Propositions
Category:Subtraction of Divisors obeys Distributive Law
Subtraction of Fractions

== Theorem ==
Let $a, b, c, d \in \Z$ such that $b d \ne 0$.
Then:
:$\dfrac a b - \dfrac c d = \dfrac {a D - B c} {\lcm \set {b, d} }$
where:
:$B = \dfrac b {\gcd \set {b, d} }$
:$D = \dfrac d {\gcd \set {b, d} }$
:$\lcm$ denotes lowest common multiple
:$\gcd$ denotes greatest common divisor.
== Proof ==
== Sources ==
* 
* 
Category:Fractions
Category:Subtraction
Category:Lowest Common Multiple
Category:Greatest Common Divisor
Subtraction of Multiples of Divisors obeys Distributive Law

== Theorem ==
In modern algebraic language:
:$a = \dfrac m n b, c = \dfrac m n d \implies a - c = \dfrac m n \paren {b - d}$
== Euclid's Proof ==
== Modern Proof ==
Category:Algebra
Category:Divisors
Category:Subtraction
Category:Subtraction of Multiples of Divisors obeys Distributive Law
Subtraction of Multiples of Divisors obeys Distributive Law/Proof 1

== Theorem ==
== Proof ==
Let the (natural) number $AB$ be the same aliquant part of the (natural) number $CD$ that $AE$ subtracted is of $CF$ subtracted.
We need to show that $EB$ is also the same aliquant part of the remainder $FD$ that the whole $AB$ is of the whole $CD$.
:
Let $GH = AB$.
Then whatever aliquant part $GH$ is of $CD$, the same aliquant part also is $AE$ of $CF$.
Let $GH$ be divided into the aliquant parts of $CD$, namely $GK + KH$, and $AE$ into the aliquant parts of $CF$, namely $AL + LE$.
Thus the multitude of $GK, KH$ will be equal to the multitude of $AL, LE$.
We have that whatever aliquot part $GK$ is of $CD$, the same aliquot part also is $AL$ of $CF$.
We also have that $CD > CF$.
Therefore $GK > AL$.
Now let $GM = AL$.
Then whatever aliquot part $GK$ is of $CD$, the same aliquot part also is $GM$ of $CF$.
Therefore from Subtraction of Divisors obeys Distributive Law the remainder $MK$ is of the same aliquot part of the remainder $FD$ that the whole $GK$ is of the whole $CD$.
Again, we have that whatever aliquot part $KH$ is of $CD$, the same aliquot part also is $EL$ of $CF$.
We also have that $CD > CF$.
Therefore $HK > EL$.
Let $KN = EL$.
Then whatever aliquot part $KH$ is of $CD$, the same aliquot part also is $KN$ of $CF$.
Therefore from Subtraction of Divisors obeys Distributive Law the remainder $NH$ is of the same aliquot part of the remainder $FD$ that the whole $KH$ is of the whole $CD$.
But $MK$ was proved to be the same aliquot part of $FD$ that $GK$ is of $CD$.
Therefore $MK + NH$ is the same aliquant part of $DF$ that $HG$ is of $CD$.
But $MK + NH = EB$ and $HG = BA$.
Therefore $EB$ is the same aliquant part of $FD$ that $AB$ is of $CD$.
== Sources ==
* : Book $\text{VII}$. Propositions
Category:Subtraction of Multiples of Divisors obeys Distributive Law
Subtraction of Subring is Subtraction of Ring

== Theorem ==
Let $\struct {R, +, \circ}$ be an ring.
For each $x, y \in R$ let $x - y$ denote the subtraction of $x$ and $y$ in $R$.
Let $\struct {S, + {\restriction_S}, \circ {\restriction_S}}$ be a subring of $R$.
For each $x, y \in S$ let $x \sim y$ denote the subtraction of $x$ and $y$ in $S$.
Then:
:$\forall x, y \in S: x \sim y = x - y$
== Proof ==
Let $x, y \in S$.
Let $-x$ denote the ring negative of $x$ in $R$.
Let $\mathbin \sim x$ denote the ring negative of $x$ in $S$.
Then:
Category:Ring Theory
Subtraction on Integers is Extension of Natural Numbers

== Theorem ==
Integer subtraction is an extension of the definition of subtraction on the natural numbers.
== Proof ==
Let $m, n \in \N: m \le n$.
From natural number subtraction, $\exists p \in \N: m + p = n$ such that $n - m = p$.
As $m, n, p \in \N$, it follows that $m, n, p \in \Z$ as well.
However, as $\Z$ is the inverse completion of $\N$, it follows that $-m \in \Z$ as well, so it makes sense to express the following:
Thus, as all elements of $\Z$ are cancellable, it follows that $n + \paren {-m} = n - m$.
So:
: $\forall m, n \in \Z, m \le n: n + \paren {-m} = n - m = n -_\N m$
and the result follows.
Category:Integers
Category:Subtraction
Subtraction on Numbers is Anticommutative

== Theorem ==
The operation of subtraction on the numbers is anticommutative.
That is:
:$a - b = b - a \iff a = b$
== Proof ==
=== Natural Numbers ===
=== Integers, Rationals, Reals, Complex Numbers ===
== Also see ==
* Definition:Natural Number Subtraction
== Sources ==
* : $\S 4.2$. Commutative and associative operations: Example $61$
* : Part $\text I$: Prologue: Chapter $1$: Basic Properties of Numbers
* 
Category:Numbers
Category:Subtraction
Category:Examples of Anticommutativity
Category:Subtraction on Numbers is Anticommutative
Subtraction on Numbers is Anticommutative/Integral Domains

== Theorem ==
The operation of subtraction on the numbers is anticommutative.
That is:
:$a - b = b - a \iff a = b$
== Proof ==
Let $a, b$ be elements of one of the standard number sets: $\Z, \Q, \R, \C$.
Each of those systems is an integral domain, and so is closed under the operation of subtraction.
=== Necessary Condition ===
Let $a = b$.
Then $a - b = 0 = b - a$.
=== Sufficient Condition ===
Let $a - b = b - a$.
Then:
We have that:
:$a - b = b - a$
So from the above:
:$b - a = - \paren {b - a}$
That is:
:$b - a = 0$
and so:
:$a = b$
== Also see ==
* Definition:Natural Number Subtraction
== Sources ==
* : Chapter $\text I$: Algebraic Structures: $\S 2$: Compositions: Example $2.1$
* : $\S 28$. Associativity and commutativity: Definition $2$
Category:Subtraction on Numbers is Anticommutative
Subtraction on Numbers is Anticommutative/Natural Numbers

== Theorem ==
The operation of subtraction on the natural numbers $\N$ is anticommutative, and defined only when $a = b$:
That is:
:$a - b = b - a \iff a = b$
== Proof ==
$a - b$ is defined on $\N$ only if $a \ge b$.
If $a > b$, then although $a - b$ is defined, $b - a$ is not.
So for $a - b = b - a$ it is necessary for both to be defined.
This happens only when $a = b$.
Hence the result.
Category:Subtraction on Numbers is Anticommutative
Subtraction on Numbers is Not Associative

== Theorem ==
The operation of subtraction on the numbers is not associative.
That is, in general:
:$a - \paren {b - c} \ne \paren {a - b} - c$
== Proof ==
By definition of subtraction:
So we see that:
:$a - \paren {b - c} = \paren {a - b} - c \iff c = 0$
and so in general:
:$a - \paren {b - c} \ne \paren {a - b} - c$
== Examples ==
== Sources ==
* : $\S 4.2$. Commutative and associative operations: Example $64$
* : Chapter $\text I$: Algebraic Structures: $\S 2$: Compositions: Example $2.1$
* : $\S 28$. Associativity and commutativity
* 
* 
Category:Subtraction on Numbers is Not Associative
Category:Numbers
Category:Subtraction
Category:Examples of Associative Operations‎
Succeed is Dual to Precede

== Theorem ==
Let $\left({S, \preceq}\right)$ be an ordered set.
Let $a, b \in S$.
The following are dual statements:
:$a$ succeeds $b$
:$a$ precedes $b$
== Proof ==
By definition, $a$ succeeds $b$ :
:$b \preceq a$
The dual of this statement is:
:$a \preceq b$
by Dual Pairs (Order Theory).
By definition, this means $a$ precedes $b$.
The converse follows from Dual of Dual Statement (Order Theory).
== Also see ==
* Duality Principle (Order Theory)
* Strictly Succeed is Dual to Strictly Precede
Category:Dual Pairs (Order Theory)