nyuuzyou/wikis huggingface dataset:
Addition Law of Probability/Also presented as

== Addition Law of Probability: Also presented as == 
Some sources present the addition law of probability in the form:
:$\map \Pr {A \cup B} + \map \Pr {A \cap B} = \map \Pr A + \map \Pr B$
== Sources ==
* : $1$: Events and probabilities: $1.4$: Probability spaces: $(15)$
Category:Addition Law of Probability
Addition Law of Probability/Proof 2

== Theorem ==
== Proof ==
From Set Difference and Intersection form Partition:
:$A$ is the union of the two disjoint sets $A \setminus B$ and $A \cap B$
:$B$ is the union of the two disjoint sets $B \setminus A$ and $A \cap B$.
So, by the definition of probability measure:
:$\map \Pr A = \map \Pr {A \setminus B} + \map \Pr {A \cap B}$
:$\map \Pr B = \map \Pr {B \setminus A} + \map \Pr {A \cap B}$
From Set Difference is Disjoint with Reverse:
:$\paren {A \setminus B} \cap \paren {B \setminus A} = \O$
Hence:
Hence the result.
== Sources ==
* : $1$: Events and probabilities: $1.4$: Probability spaces: $(15)$
Category:Addition Law of Probability
Addition Rule for Gaussian Binomial Coefficients

== Theorem ==
Let $\dbinom n m_q$ denote a Gaussian binomial coefficient.
=== Formulation 1 ===
=== Formulation 2 ===
== Sources ==
* : $\S 1.2.6$: Binomial Coefficients: Exercise $58$
Category:Gaussian Binomial Coefficients
Category:Addition Rule for Gaussian Binomial Coefficients
Addition Rule for Gaussian Binomial Coefficients/Formulation 1

== Theorem ==
Let $\dbinom n m_q$ denote a Gaussian binomial coefficient.
Then:
:$\dbinom n m_q = \dbinom {n - 1} m_q + \dbinom {n - 1} {m - 1}_q q^{n - m}$
== Proof ==
By definition of Gaussian binomial coefficient:
Thus:
== Sources ==
* 
* 
* : $\S 1.2.6$: Binomial Coefficients: Exercise $58$
Category:Addition Rule for Gaussian Binomial Coefficients
Addition Rule for Gaussian Binomial Coefficients/Formulation 2

== Theorem ==
Let $\dbinom n m_q$ denote a Gaussian binomial coefficient.
Then:
:$\dbinom n m_q = \dbinom {n - 1} m_q q^m + \dbinom {n - 1} {m - 1}_q$
== Proof ==
By definition of Gaussian binomial coefficient:
Thus:
== Sources ==
* : $\S 1.2.6$: Binomial Coefficients: Exercise $58$
Category:Addition Rule for Gaussian Binomial Coefficients
Addition in Minimally Inductive Set is Unique

== Theorem ==
Let $\omega$ be the minimally inductive set.
Let $A: \omega \times \omega \to \omega$ be the mapping defined as the addition operation:
:$\forall \tuple {x, y} \in \omega \times \omega: \map A {x, y} = \begin {cases} x & : y = 0 \\ \paren {\map A {x, r} }^+ & : y = r^+ \end {cases}$
where $r^+$ is the successor set of $r$.
Then $A$ exists and is unique.
== Proof ==
Recall the Principle of Recursive Definition (Strong Version):
From the von Neumann construction, this $\omega$ is exactly the minimally inductive set as defined in the problem statement.
Let $g: \omega \times \omega \to \omega$ be the mapping defined as:
:$\forall \tuple {x, y} \in \omega \times \omega: \map g {x, y} := y^+$
Hence from the Principle of Recursive Definition (Strong Version), there exists a unique mapping $f: \omega \to \omega$ such that:
:$\forall x \in \omega: \map f x = \begin{cases}
c & : x = \O \\
x^+ & : x = n^+
\end{cases}$
which we get by identifying $\map g {x, y}$ with $y^+$.
Let us fix some arbitrary $x_0 \in \omega$.
== Sources ==
* : Chapter $3$: The Natural Numbers: $\S 8$ Definition by finite recursion: Exercise $8.4 \ \text {(a)}$
Category:Natural Number Addition
Addition is Arithmetically Definable

== Theorem ==
Let $f: \N^2 \to \N$ be defined as:
:$\map f {x, y} = x + y$
Then there exists a WFF $\map \phi {z, x, y}$ of $3$ free variables and containing no quantifiers such that:
:$z = \map f {x, y} \iff \N \models \map \phi {\sqbrk z, \sqbrk x, \sqbrk y}$
where $\sqbrk a$ is the unary representation of $a \in \N$.
== Proof ==
Define:
:$\map \phi {z, x, y} := z = x + y$
Correctness is trivial.
Category:Natural Number Addition
Addition is Primitive Recursive

== Theorem ==
The function $\Add: \N^2 \to \N$, defined as:
:$\map \Add {n, m} = n + m$
is primitive recursive‎.
== Proof ==
We observe that:
:$\map \Add {n, 0} = n + 0 = n$
and that
:$\map \Add {n, m + 1} = n + \paren {m + 1} = \paren {n + m} + 1 = \map \Succ {\map \Add {n, m} }$
where $\Succ$ is the successor function, which is a basic primitive recursive‎ function.
We are to show that $\Add$ is defined by primitive recursion.
So we need to find primitive recursive‎ functions $f: \N \to \N$ and $g: \N^3 \to \N$ such that:
:$\map \Add {n, m} = \begin{cases}
\map f n & : m = 0 \\
\map g {n, m - 1, \map \Add {n, m - 1} } & : m > 0
\end{cases}$
Because $\map \Add {n, 0} = n$, we can see that:
:$\map f n = n$.
That is, $f$ is the basic primitive recursive‎ function $\pr_1^1: \N \to \N$.
Because $\map \Add {n, m + 1} = \map \Succ {\map \Add {n, m} }$, we can see that $g$ needs to be a function which maps the ordered triple $\tuple {n, m, \map \Add {n, m} }$ to $\map \Succ {\map \Add {n, m} }$.
A suitable function is:
:$g: \N^3 \to \N$ where $\map g {n_1, n_2, n_3} = \map \Succ {n_3}$
because then:
:$\map g {n, m, \map \Add {n, m} } = \map \Succ {\map \Add {n, m} }$
It remains to be shown that $g$ is primitive recursive‎.
This is achieved by using the projection function:
:$\map g {n_1, n_2, n_3} = \map \Succ {\map {\pr_3^3} {n_1, n_2, n_3} }$
Thus $g$ is obtained by substitution from the basic primitive recursive‎ functions $\Succ$ and $\pr_3^3$ and so is primitive recursive‎.
So $\Add$ is obtained by primitive recursion from the primitive recursive functions‎ $\pr_1^1$ and $g$, and so is primitive recursive‎.
Category:Primitive Recursive Functions
Addition of 1 in Golden Mean Number System

== Algorithm ==
Let $x \in \R$ be a real number.
The following algorithm performs the operation of addition of $1$ to $x$ in the golden mean number system.
Let $S$ be the representation of $x$ in the golden mean number system in its simplest form.
:Step $1$: Is the digit immediately to the left of the radix point a zero?
:: If Yes, replace that $0$ with $1$. Go to Step $4$.
:: If No, set $m = 2$ and go to Step $2$.
:Step $2$: Does the $m$th place after the radix point contain $0$?
:: If Yes, expand the $100$ in the $3$ places ending in the $m$th place with $011$. Subtract $2$ from $m$. Go to Step $3$.
:: If No, add $2$ to $m$. Repeat Step $2$.
:Step $3$: Is $m = 0$?
:: If Yes, set the digit immediately to the left of the radix point from $0$ to $1$. Go to Step $4$.
:: If No, go to Step $2$.
:Step $4$: Convert $S$ to its simplest form. Stop.
== Proof ==
The above constitutes an algorithm, for the following reasons:
=== Finiteness ===
The only case in which it is possible for the process not to terminate is if the $m$th place never contains $0$.
This can only happen if $S$ ends in an infinite string $01010101 \ldots$
But if this is the case, $S$ is not in its simplest form.
=== Definiteness ===
Each step can be seen to be precisely defined.
=== Inputs ===
The only input to the algorithm is the representation $S$ of $x$.
=== Outputs ===
The only output from the algorithm is the representation $S$ of $x + 1$.
All operations that change $S$ are of the following nature:
:$(1): \quad$ Simplification of $S$, which does not change $x$, which happens if at all in Step $4$.
:$(2): \quad$ Expansion of $S$, which does not change $x$, which happens if at all in Step $2$.
:$(3): \quad$ Setting the digit corresponding to $\phi^0$ to $1$ from $0$, which happens either in Step $1$ or in Step $3$.
:::In either step, it happens only once, after which the algorithm terminates.
=== Effective ===
Each step is basic enough to be done exactly and predictably.
== Sources ==
* 
Category:Golden Mean Number System
Addition of Codewords in Linear Code/Examples/V(2,3)

== Example of Addition of Codewords in $V \paren {2, 3}$ ==
In the master code $V \paren {2, 3}$, the codewords $12$ and $11$ are added thus:
:$12 + 11 = 20$
== Proof ==
Taking the elements of $12$ and $11$ in pairs, successively, we have:
Hence the result.
== Sources ==
* : Chapter $6$: Error-correcting codes
Category:Examples of Linear Codes
Addition of Codewords in Linear Code/Examples/V(3,2)

== Example of Addition of Codewords in $V \paren {3, 2}$ ==
In the master code $V \paren {3, 2}$, the codewords $110$ and $011$ are added thus:
:$110 + 011 = 101$
== Proof ==
Taking the elements of $110$ and $011$ in pairs, successively, we have:
Hence the result.
== Sources ==
* : Chapter $6$: Error-correcting codes
Category:Examples of Linear Codes
Addition of Coordinates on Cartesian Plane under Chebyshev Distance is Continuous Function

== Theorem ==
Let $\R^2$ be the real number plane.
Let $d_\infty$ be the Chebyshev distance on $\R^2$.
Let $f: \R^2 \to \R$ be the real-valued function defined as:
:$\forall \tuple {x_1, x_2} \in \R^2: \map f {x_1, x_2} = x_1 + x_2$
Then $f$ is continuous.
== Proof ==
First we note that:
Let $\epsilon \in \R_{>0}$.
Let $x = \tuple {x_1, x_2} \in \R^2$.
Let $\delta = \dfrac \epsilon 2$.
Then:
Thus it has been demonstrated that:
:$\forall \epsilon \in \R_{>0}: \exists \delta \in \R_{>0}: \forall y \in \R^2: \map {d_\infty} {x, y} < \delta \implies \map d {\map f x, \map f y} < \epsilon$
Hence by definition of continuity at a point, $f$ is continuous at $x$.
As $x$ was chosen arbitrarily, it follows that $f$ is continuous for all $x \in \R^2$.
The result follows by definition of continuous mapping.
== Sources ==
* : Chapter $2$: Metric Spaces: $\S 3$: Continuity: Exercise $3$
Category:Continuous Mappings on Metric Spaces
Category:Chebyshev Distance
Addition of Coordinates on Euclidean Plane is Continuous Function

== Theorem ==
Let $\struct {\R^2, d_2}$ be the real number plane with the usual (Euclidean) metric.
Let $f: \R^2 \to \R$ be the real-valued function defined as:
:$\forall \tuple {x_1, x_2} \in \R^2: \map f {x_1, x_2} = x_1 + x_2$
Then $f$ is continuous.
== Proof ==
First we note that:
Let $\epsilon \in \R_{>0}$.
Let $x = \tuple {x_1, x_2} \in \R^2$.
Let $\delta = \dfrac \epsilon {\sqrt 2}$.
Then:
Thus it has been demonstrated that:
:$\forall \epsilon \in \R_{>0}: \exists \delta \in \R_{>0}: \forall y \in \R^2: \map {d_2} {x, y} < \delta \implies \map d {\map f x, \map f y} < \epsilon$
Hence by definition of continuity at a point, $f$ is continuous at $x$.
As $x$ is chosen arbitrarily, it follows that $f$ is continuous for all $x \in \R^2$.
The result follows by definition of continuous mapping.
== Sources ==
* : Chapter $2$: Metric Spaces: $\S 3$: Continuity: Exercise $3$
Category:Continuous Mappings on Metric Spaces
Category:Real Number Plane with Euclidean Metric
Addition of Cross-Relation Equivalence Classes on Natural Numbers is Cancellable

== Theorem ==
Let $\struct {\N, +}$ be the semigroup of natural numbers under addition.
Let $\struct {\N \times \N, \oplus}$ be the (external) direct product of $\struct {\N, +}$ with itself, where $\oplus$ is the operation on $\N \times \N$ induced by $+$ on $\N$.
Let $\boxtimes$ be the cross-relation defined on $\N \times \N$ by:
:$\tuple {x_1, y_1} \boxtimes \tuple {x_2, y_2} \iff x_1 + y_2 = x_2 + y_1$
Let $\eqclass {x, y} {}$ denote the equivalence class of $\tuple {x, y}$ under $\boxtimes$.
The operation $\oplus$ on these equivalence classes is cancellable, in the sense that:
and similarly:
== Proof ==
== Sources ==
* : $\S 2.5$: Corollary $2.25.1$
Category:Natural Number Addition
Category:Cross-Relations
Category:Equivalence Relations
Addition of Cuts is Associative

== Theorem ==
Let $\alpha$, $\beta$ and $\gamma$ be cuts.
Let the operation of $\alpha + \beta$ be the sum of $\alpha$ and $\beta$.
Then:
:$\paren {\alpha + \beta} + \gamma = \alpha + \paren {\beta + \gamma}$
== Proof ==
$\paren {\alpha + \beta} + \gamma$ is the set of all rational numbers of the form $\paren {p + q} + r$ such that $p \in \alpha$, $q \in \beta$ and $r \in \gamma$.
Similarly, $\alpha + \paren {\beta + \gamma}$ is the set of all rational numbers of the form $p + \paren {q + r}$ such that $p \in \alpha$, $q \in \beta$ and $r \in \gamma$.
From Rational Addition is Associative we have that:
:$\paren {p + q} + r = p + \paren {q + r}$
The result follows.
== Sources ==
* : Chapter $1$: The Real and Complex Number Systems: Dedekind Cuts: $1.14$. Theorem $\text {(b)}$
Category:Cuts
Category:Addition
Category:Examples of Associative Operations‎
Addition of Cuts is Commutative

== Theorem ==
Let $\alpha$ and $\beta$ be cuts.
Let the operation of $\alpha + \beta$ be the sum of $\alpha$ and $\beta$.
Then:
:$\alpha + \beta = \beta + \alpha$
== Proof ==
$\alpha + \beta$ is the set of all rational numbers of the form $p + q$ such that $p \in \alpha$ and $q \in \beta$.
Similarly, $\beta + \alpha$ is the set of all rational numbers of the form $q + p$ such that $p \in \alpha$ and $q \in \beta$.
From Rational Addition is Commutative we have that:
:$p + q = q + p$
The result follows.
== Sources ==
* : Chapter $1$: The Real and Complex Number Systems: Dedekind Cuts: $1.14$. Theorem $\text {(a)}$
Category:Cuts
Category:Addition
Category:Examples of Commutative Operations‎
Addition of Division Products

== Theorem ==
Let $\struct {R, +, \circ}$ be a commutative ring with unity.
Let $\struct {U_R, \circ}$ be the group of units of $\struct {R, +, \circ}$.
Let $a, c \in R, b, d \in U_R$.
Then:
:$\dfrac a b + \dfrac c d = \dfrac {a \circ d + b \circ c} {b \circ d}$
where $\dfrac x z$ is defined as $x \circ \paren {z^{-1} }$, that is, $x$ divided by $z$.
== Proof ==
First we demonstrate the operation has the specified property:
Notice that this works only if $\struct {R, +, \circ}$ is commutative.
== Sources ==
* : Chapter $\text {IV}$: Rings and Fields: $23$. The Field of Rational Numbers: Theorem $23.7 \ (2)$
Category:Commutative Algebra
Addition of Division Products in Field

== Theorem ==
Let $\struct {F, +, \times}$ be a field whose zero is $0$ and whose unity is $1$.
Let $a, b, c, d \in F$ such that $b \ne 0$ and $d \ne 0$.
Then:
:$\dfrac a b + \dfrac c d = \dfrac {a d + b c} {b d}$
where $\dfrac x z$ is defined as $x \paren {z^{-1} }$.
== Proof ==
By definition, a field is a non-trivial division ring whose ring product is commutative.
By definition, a division ring is a ring with unity such that every non-zero element is a unit. 
Hence we can use Addition of Division Products:
:$\dfrac a b + \dfrac c d = \dfrac {a \circ d + b \circ c} {b \circ d}$
which applies to the group of units of a comutative ring with unity.
== Sources ==
* : Chapter $3$: Field Theory: Definition and Examples of Field Structure: $\S 87 \delta$
Category:Field Theory
Addition 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 ==
== Examples ==
== Sources ==
* : $\text {2-2}$ Divisibility: Exercise $7$
* 
* 
* 
* 
Category:Addition of Fractions
Category:Fractions
Category:Addition
Category:Lowest Common Multiple
Category:Greatest Common Divisor
Addition of Integers is Primitive Recursive

== Theorem ==
Let $a : \N^2 \to \N$ be defined as:
:$\map a {m, n} = p$
where:
:$m$ codes an integer $k$
:$n$ codes an integer $\ell$
:$p$ codes the integer $k + \ell$
Then $a$ is a primitive recursive function.
== Proof ==
Define:
:$\map a {m, n} = \begin{cases}
\map {\sgn_\Z} k \times_\Z \paren {\size k + \size \ell}_\Z & : \map {\sgn_\Z} k = \map {\sgn_\Z} \ell \\
\map {\sgn_\Z} k \times_\Z \paren {\size k {\dot -} \size \ell}_\Z & : \map {\sgn_\Z} k \ne \map {\sgn_\Z} \ell \land \size k \ge \size \ell \\
\map {\sgn_\Z} \ell \times_\Z \paren {\size \ell {\dot -} \size k}_\Z & : \map {\sgn_\Z} k \ne \map {\sgn_\Z} \ell \land \size k < \size \ell
\end{cases}$
where:
:$\times_\Z$ denotes integer multiplication
:$N_\Z$ denotes the code number for $N : \Z$
:$\sgn_\Z$ denotes the signum function on $\Z$
:$\dot -$ denotes cut-off subtraction
By:
* Ordering Relations are Primitive Recursive
* Equality Relation is Primitive Recursive
* Set Operations on Primitive Recursive Relations
* Signum Function on Integers is Primitive Recursive
* Multiplication of Integers is Primitive Recursive
* Absolute Value of Integer is Primitive Recursive
* Addition is Primitive Recursive
* Cut-Off Subtraction is Primitive Recursive
* Definition by Cases is Primitive Recursive
it follows that $a$ is primitive recursive.
Now, we will show that $a$ satisfies the definition in the theorem statement.
First, suppose:
:$\size k > \size \ell$
Then:
:$\map {\sgn_\Z} {k + \ell} = \map {\sgn_\Z} k$.
If the signs of $k$ and $\ell$ match, then:
:$\size {k + \ell} = \size k + \size \ell$
If they differ, then either:
:$\ell = 0$
or:
$k$ and $\ell$ have opposite signs.
Then:
:$\size {k + \ell} = \size k - \size \ell$ 
in either case.
But since:
:$\size k > \size \ell$
We have:
:$\size k - \size \ell = \size k {\dot -} \size \ell$
In both of those cases, $\map a {m, n}$ matches the value.
It can be seen that, when:
:$\size k < \size \ell$
the above holds with the roles of the two variables swapped.
Now, suppose:
:$\size k = \size \ell$
If:
:$\map {\sgn_\Z} k = \map {\sgn_\Z} \ell$
then:
:$\map {\sgn_\Z} {k + \ell} = \map {\sgn_\Z} k = \map {\sgn_\Z} \ell$
and:
:$\size {k + \ell} = \size k + \size \ell$
If:
:$\map {\sgn_\Z} k \ne \map {\sgn_\Z} \ell$
then either:
:One of the two is zero
or:
:One is positive, and the other is negative
In either of the two cases, we can again use cut-off subtraction to get the correct result.
Since, in every case, the defined $a : \N^2 \to \N$ satisfies the definition, the result follows.
Category:Primitive Recursive Functions
Addition of Linear Transformations

== Theorem ==
Let $\struct {G, +_G}$ and $\struct {H, +_H}$ be abelian groups.
Let $\struct {R, +_R, \times_R}$ be a ring.
Let $\struct {G, +_G, \circ_G}$ and $\struct {H, +_H, \circ_H}$ be $R$-modules.
Let $\map {\LL_R} {G, H}$ be the set of all linear transformations from $G$ to $H$.
Let $\oplus_H$ be defined as pointwise addition on $\map {\LL_R} {G, H}$:
:$\forall \phi, \psi \in \map {\LL_R} {G, H}: \forall x \in G: \map {\paren {\phi \oplus_H \psi} } x := \map \phi x +_H \map \psi x$
Then $\phi \oplus_H \psi: G \to H$ is a linear transformation.
== Proof ==
From the definition of a module, the group $\struct {H, +_H}$ is abelian.
Hence $\struct {H, +_H}$ is a commutative semigroup.
Therefore we can apply Homomorphism on Induced Structure to Commutative Semigroup to show that $\phi +_H \psi: G \to H$ is a homomorphism.
Let $\lambda \in R, x \in G$.
Then:
== Sources ==
* : Chapter $\text {V}$: Vector Spaces: $\S 28$. Linear Transformations
Category:Linear Transformations
Addition of Natural Numbers is Provable

== Theorem ==
Let $x, y \in \N$ be natural numbers.
Then there exists formal proof of:
:$\sqbrk x + \sqbrk y = \sqbrk {x + y}$
in minimal arithmetic, where $\sqbrk a$ is the unary representation of $a$.
=== General Form ===
== Proof ==
By Unary Representation of Natural Number, let $\sqbrk a$ denote the term $\map s {\dots \map s 0}$, where there are $a$ applications of the successor mapping to the constant $0$.
Proceed by induction on $y$.
=== Base Case ===
Let $y = 0$.
Then $\sqbrk y = 0$.
The following is a formal proof:
But $x + 0 = x$.
Therefore, $\sqbrk {x + 0} = \sqbrk x$.
Thus, the proof above is a formal proof of $\sqbrk x + 0 = \sqbrk {x + 0}$.
=== Induction Step ===
Let there exist a formal proof of $\sqbrk x + \sqbrk y = \sqbrk {x + y}$.
Then, the following is a formal proof:
Therefore, there exists a formal proof of $\sqbrk x + \map s {\sqbrk y} = \map s {\sqbrk {x + y} }$.
But as:
:$\sqbrk a$
consists of $a$ applications of the successor mapping to the constant $0$, it follows that:
:$\map s {\sqbrk y} = \sqbrk {\map s y}$
consists of $a + 1 = \map s a$ applications of $s$ to $0$.
But that is the unary representation of $\map s a$.
Therefore:
:$\map s {\sqbrk y} = \sqbrk {\map s y}$
and
:$\map s {\sqbrk {x + y} } = \sqbrk {\map s {x + y} }$
By the definition of addition, $x + \map s y = \map s {x + y}$.
Thus:
:$\sqbrk {\map s {x + y} } = \sqbrk {x + \map s y}$
It follows that the proof above is also a proof of:
:$\sqbrk x + \sqbrk {\map s y} = \sqbrk {x + \map s y}$
Thus, by the Principle of Mathematical Induction, there exists such a formal proof for every $y \in \N$.
As $x$ was arbitrary, there exists such a formal proof for every $x, y \in \N$.
Category:Natural Number Addition
Category:Proofs by Induction
Addition of Natural Numbers is Provable/General Form

== Theorem ==
Let $y \in \N$ be a natural number.
Let $s^a$ denote the application of the successor mapping $a$ times.
Let $\sqbrk a$ denote $\map {s^a} 0$.
Then there exists a formal proof of:
:$\forall x: x + \sqbrk y = \map {s^y} x$
in minimal arithmetic.
== Proof ==
Proceed by induction on $y$.
=== Basis for the Induction ===
Let $y = 0$.
Then $\sqbrk y = 0$ by definition.
Then the theorem to prove is:
:$\forall x: x + 0 = x$
But that is Axiom $\text M 3$ of minimal arithmetic.
=== Induction Hypothesis ===
Fix some $y \in \N$.
Suppose that there is a formal proof of:
:$\forall x: x + \sqbrk y = \map {s^y} x$
=== Induction Step ===
The following is a formal proof:
By expanding the definitions of $\sqbrk y$ and $\map {s^y} x$, the proven result is syntactically identical to:
:$\forall x: x + \sqbrk {\map s y} \map {s^{\map s y} } x$
which was the theorem to be proven.
Thus, by the Principle of Mathematical Induction, there is such a formal proof for every $y \in \N$.
Category:Natural Number Addition
Category:Proofs by Induction
Addition of Numbers is not Distributive over Multiplication

== Theorem ==
Addition of numbers is not distributive over multiplication.
That is, for numbers $a$, $b$ and $c$ it is not necessarily the case that $a + \paren {b \times c} = \paren {a + b} \times \paren {a + c}$.
== Proof ==
Proof by Counterexample:
== Sources ==
* 
* 
* 
Category:Examples of Distributive Operations
Addition of Order Types/Examples/Example Ordering on Integers

== Examples of Addition of Order Types ==
Let $\preccurlyeq$ denote the relation on the set of integers $\Z$ defined as:
:$a \preccurlyeq b$ $0 \le a \le b \text { or } b \le a < 0 \text { or } a < 0 \le b$
where $\le$ is the usual ordering on $\Z$.
Then the order type of $\struct {\Z, \preccurlyeq}$ is:
:$\map \ot {\Z, \preccurlyeq} = \omega + \omega$
where $\omega$ denotes the order type of the natural numbers.
== Proof ==
Consider the following mappings:
:$i_\N: \N \to \Z_{\ge 0}: x \mapsto x$
:$\phi: \N \to \Z_{<0}: x \mapsto -\paren {x + 1}$
These are seen to be order isomorphisms.
We have that:
:$\struct {\N, \le} \oplus \struct {\N, \le} \cong \struct {\Z, \preccurlyeq}$
== Sources ==
* : Part $1$: Not Entirely Naive Set Theory: Chapter $2$: Partial Order Relations
Category:Examples of Order Type Addition
Addition of Real and Imaginary Parts

== Theorem ==
Let $z_0, z_1 \in \C$ be two complex numbers.
Then:
:$\map \Re {z_0 + z_1} = \map \Re {z_0} + \map \Re {z_1}$
and:
:$\map \Im {z_0 + z_1} = \map \Im {z_0} + \map \Im {z_1}$
Here, $\map \Re {z_0}$ denotes the real part of $z_0$, and $\map \Im {z_0}$ denotes the imaginary part of $z_0$.
== Proof ==
We have:
Category:Complex Addition