avewright/proofwiki-math huggingface dataset:
Theorem: Infinite Sequence Property of Well-Founded Relation/Forward Implication

Let $\struct {S, \RR}$ be a relational structure.
Let $\RR$ be a well-founded relation.
Then there exists no infinite sequence $\sequence {a_n}$ of elements of $S$ such that:
:$\forall n \in \N: \paren {a_{n + 1} \mathrel \RR a_n} \text { and } \paren {a_{n + 1} \ne a_n}$

Proof:
Let $\RR$ be a well-founded relation.
{{AimForCont}} there exists an infinite sequence $\sequence {a_n}$ in $S$ such that:
:$\forall n \in \N: \paren {a_{n + 1} \mathrel \RR a_n} \text { and } \paren {a_{n + 1} \ne a_n}$
Let $T = \set {a_0, a_1, a_2, \ldots}$.
Let $a_k \in T$ be a minimal element of $T$.
That is:
:$\forall y \in T \setminus \set {a_k}: \neg \paren {y \mathrel \RR a_k}$
But we have that:
:$a_{k + 1} \mathrel \RR a_k$ and $a_{k + 1} \ne a_k$.
So $a_k$ is not a minimal element.
It follows by Proof by Contradiction that such an infinite sequence cannot exist.
Theorem: Extendability Theorem for Function Continuous on Open Interval

Let $f$ be a continuous real function that is defined on an open interval $\openint a b$.
Let $g$ be a real function that satisfies:
:$g$ is defined on $\closedint a b$
:$g$ is continuous on $\closedint a b$
:$g = f$ on $\openint a b$.
Then $g$ exists {{iff}} $\ds \lim_{x \mathop \to a^+} \map f x$ and $\ds \lim_{x \mathop \to b^-} \map f x$ exist.

Proof:
=== Necessary Condition ===
Assume that $g$ exists.
We need to prove that the limits $\ds \lim_{x \mathop \to a^+} \map f x$ and $\ds \lim_{x \mathop \to b^-} \map f x$ exist.
$g$ is continuous at the end points $a$ and $b$ of its domain as $g$ is continuous on $\closedint a b$.
$g$ is right-continuous at $a$ and left-continuous at $b$.
This means that $\map g a = \ds \lim_{x \mathop \to a^+} \map g x$ and $\map g b = \ds \lim_{x \mathop \to b^-} \map g x$.
In turn, this means that the expressions $\ds \lim_{x \mathop \to a^+} \map g x$ and $\ds \lim_{x \mathop \to b^-} \map g x$ exist.
The two $x$ parameters as being part of the two limiting processes in these expressions can be considered confined to $\openint a b$.
Therefore, $g$ in these two expressions can be replaced by $f$ as $g = f$ on $\openint a b$.
We conclude that $\ds \lim_{x \mathop \to a^+} \map f x$ and $\ds \lim_{x \mathop \to b^-} \map f x$ exist.
{{qed|lemma}}
Theorem: Integrability Theorem for Functions Continuous on Open Intervals

Let $f$ be a real function defined on a closed interval $\closedint a b$ such that $a < b$.
Let $f$ be continuous on $\openint a b$.
Let the one-sided limits $\ds \lim_{x \mathop \to a^+} \map f x$ and $\ds \lim_{x \mathop \to b^-} \map f x$ exist.
Then $f$ is Darboux integrable on $\closedint a b$.

Proof:
We start by showing that $f$ is bounded.
A real function $g$ defined on $\closedint a b$ exists by Extendability Theorem for Function Continuous on Open Interval such that:
:$g$ equals $f$ on $\openint a b$
:$g$ is continuous on $\closedint a b$
Therefore:
:$g$ is bounded on $\closedint a b$ by Continuous Function on Compact Subspace of Euclidean Space is Bounded and Closed Real Interval is Compact in Metric Space
Accordingly, $g$ is bounded on $\openint a b$ as $\openint a b$ is a subset of $\closedint a b$.
Therefore, $f$ is bounded on $\openint a b$ as $f = g$ on $\openint a b$.
Also, $f$ is bounded on the set $\set {a, b}$ by the maximum $\map \max {\size {\map f a}, \size {\map f b} }$.
Therefore:
:$f$ is bounded on $\closedint a b$
We have:
:$f$ is bounded on $\closedint a b$
:$f$ is continuous on $\openint a b$
Therefore:
:$f$ is Darboux integrable on $\closedint a b$ by Bounded Function Continuous on Open Interval is Darboux Integrable.
{{qed}}
Category:Integral Calculus
2imrgmi3u96mqctm0lf64rmei5f0l3j
Theorem: Set of Rational Numbers whose Numerator Divisible by p is Closed under Multiplication

Let $p$ be a prime number.
Let $A_p$ be the set of all rational numbers which, when expressed in canonical form has a numerator which is divisible by $p$.
Then $A_p$ is closed under rational multiplication.

Proof:
Let $a, b \in A_p$.
Then $a = \dfrac {p n_1} {d_1}, b = \dfrac {p n_1} {d_1}$ where:
:$n_1, n_2 \in \Z$
:$d_1, d_2 \in \Z_{>0}$
:$p n_1 \perp d_1, p n_2 \perp d_2$
Then:
{{begin-eqn}}
{{eqn | l = a \times b
      | r = \frac {p n_1} {d_1} \times \frac {p n_2} {d_2}
      | c = 
}}
{{eqn | r = \frac {p n_1 p n_2} {d_1 d_2}
      | c = {{Defof|Rational Multiplication}}
}}
{{eqn | r = \frac {p^2 \paren {n_1 n_2} } {d_1 d_2}
      | c = 
}}
{{end-eqn}}
From Euclid's Lemma for Prime Divisors, if $p \divides d_1 d_2$ then either $p \divides d_1$ or $p \divides d_2$.
But neither of these is the case, so $p \nmid d_1 d_2$.
Hence by Prime not Divisor implies Coprime:
:$p \perp d_1 d_2$
where $\perp$ denotes coprimeness.
So when $\dfrac {p^2 \paren {n_1 n_2} } {d_1 d_2}$ is expressed in canonical form, $p$ will still be a divisor of the numerator.
Hence the result.
{{qed}}
Theorem: Integer Less One divides Power Less One

Let $q, n \in \Z_{>0}$.
Then:
:$\paren {q - 1} \divides \paren {q^n - 1}$
where $\divides$ denotes divisibility.

Proof:
From Sum of Geometric Sequence:
:$\ds \frac {q^n - 1} {q - 1} = \sum_{k \mathop = 0}^{n - 1} q^k$
That is:
:$q^n - 1 = r \paren {q - 1}$
where $r = 1 + q + q^2 + \cdots + q^{n - 1}$.
As Integer Addition is Closed and Integer Multiplication is Closed, it follows that $r \in \Z$.
Hence the result by definition of divisor of integer.
{{qed}}
Theorem: Number Plus One divides Power Plus One iff Odd

Let $q, n \in \Z_{>0}$.
Then:
:$\paren {q + 1} \divides \paren {q^n + 1}$
{{iff}} $n$ is odd.
In the above, $\divides$ denotes divisibility.

Proof:
Let $n$ be odd.
Then from Sum of Odd Positive Powers:
:$\ds q^n + 1 = \paren {q + 1} \sum_{k \mathop = 1}^n \paren {-1}^k q^{k - 1}$
Let $n$ be even.
Consider the equation:
:$q^n + 1 = 0$
We have:
:$\paren {-1}^n + 1 = 2$
So $-1$ is not a root of $q^n + 1 = 0$.
By Polynomial Factor Theorem, $q + 1$ is not a divisor of $q^n + 1$ when $n$ is even.
{{qed}}
Theorem: Mapping is Bounded on Union iff Bounded on Each Component/Real-Valued Function

Let $f$ be a real-valued function.
Then:
:$f$ is bounded on the union of a finite number of sets within the domain of $f$
{{iff}}:
:$f$ is bounded on each of the sets.

Proof:
Let $S_i$, $i \in \set {1, \ldots, n}$, $n \in \N_{>0}$, denote sets within the domain of $f$.
Define $S = \ds \bigcup_{i \mathop = 1}^n S_i$.
Theorem: Parity of Integer equals Parity of Positive Power

Let $p \in \Z$ be an integer.
Let $n \in \Z_{>0}$ be a strictly positive integer.
Then $p$ is even {{iff}} $p^n$ is even.
That is, the parity of an integer equals the parity of all its (strictly) positive powers.

Proof:
Proof by induction:
For all $n \in \Z_{> 0}$, let $P \left({n}\right)$ be the proposition:
:For all $p \in \Z$, $p$ is even {{iff}} $p^n$ is even.
First it is worth confirming that $P \left({0}\right)$ does not hold:
:$\forall p \in \Z: p^0 = 1$
which is not even whatever the parity of $p$.
$P \left({1}\right)$ is true, as this just says:
: $p$ is even {{iff}} $p$ is even
which is a tautology.
Theorem: Two divides Power Plus One iff Odd

Let $q, n \in \Z_{>0}$.
Then:
:$2 \divides \paren {q^n + 1}$
{{iff}} $q$ is odd.
In the above, $\divides$ denotes divisibility.

Proof:
By Parity of Integer equals Parity of Positive Power, $q^n$ is even {{iff}} $q$ is even.
Thus it follows that $q^n + 1$ is even {{iff}} $q$ is odd.
The result follows by definition of even integer.
{{qed}}
Theorem: Primes of form Power plus One

Let $q, n \in \Z_{>0}$ such that $q > 1$.
Then $q^n + 1$ is prime only if:
:$(1): \quad q$ is even
and
:$(2): \quad n$ is of the form $2^m$ for some positive integer $m$.

Proof:
Note that if $q = 1$ then $q^n + 1 = 2$ which ''is'' prime.
Hence the condition on $q$ in the statement of the theorem.
So by hypothesis $q > 1$.
Let $q$ be odd.
Then by Two divides Power Plus One iff Odd, $q^n + 1$ is not prime.
Let $q$ be even.
Let $n$ be expressed in the form $r 2^m$ where $r$ is odd.
Then $q^n + 1$ can be expressed in the form:
: $q^{r 2^m} + 1 = \left({q^{2^m}}\right)^r + 1$
By Number Plus One divides Power Plus One iff Odd, $q^{2^m} + 1$ is a divisor of $\left({q^{2^m}}\right)^r + 1$.
So for all $r > 1$ it follows that $\left({q^{2^m}}\right)^r + 1$ is composite.
Hence the result.
{{qed}}
Theorem: Fermat Number whose Index is Sum of Integers

Let $F_n = 2^{\left({2^n}\right)} + 1$ be the $n$th Fermat number.
Let $k \in \Z_{>0}$.
Then:
:$F_{n + k} - 1 = \left({F_n - 1}\right)^{2^k}$

Proof:
By the definition of Fermat number
{{begin-eqn}}
{{eqn | l = F_{n + k} - 1
      | r = 2^{2^{n + k} }
      | c = {{Defof|Fermat Number}}
}}
{{eqn | r = 2^{2^n 2^k}
      | c = 
}}
{{eqn | r = \left({2^{2^n} }\right)^{2^k}
      | c = 
}}
{{eqn | r = \left({F_n - 1}\right)^{2^k}
      | c = {{Defof|Fermat Number}}
}}
{{end-eqn}}
{{qed}}
Theorem: Number of Boolean Interpretations for Finite Set of Variables

Let $\PP_0$ be the vocabulary of language of propositional logic.
Let $S \subseteq \PP_0$ be a finite set of $n$ letters from $\PP_0$.
Then there are $2^n$ different partial boolean interpretations for $S$.

Proof:
A partial boolean interpretation for $S$ is a mapping from $S$ to the Boolean domain $\set {T, F}$.
By Cardinality of Set of All Mappings, the total number of mappings from $S$ to $T$ is:
:$\card {T^S} = \card T^{\card S}$
The result follows directly.
{{qed}}
Theorem: Integers under Addition form Monoid

The set of integers under addition $\struct {\Z, +}$ forms a monoid.

Proof:
Follows directly from Integers under Addition form Abelian Group.
By definition, an abelian group is a group.
Also by definition, a group is a monoid.
Hence the result.
{{qed}}
Theorem: Rational Numbers under Addition form Monoid

The set of rational numbers under addition $\struct {\Q, +}$ forms a monoid.

Proof:
Follows directly from Rational Numbers under Addition form Infinite Abelian Group.
By definition, an abelian group is a group.
Also by definition, a group is a monoid.
Hence the result.
{{qed}}
Theorem: Real Numbers form Field

The set of real numbers $\R$ forms a field under addition and multiplication: $\struct {\R, +, \times}$.

Proof:
From Real Numbers under Addition form Infinite Abelian Group, we have that $\struct {\R, +}$ forms an abelian group.
From Non-Zero Real Numbers under Multiplication form Abelian Group, we have that $\struct {\R_{\ne 0}, \times}$ forms an abelian group.
Next we have that Real Multiplication Distributes over Addition.
Thus all the criteria are fulfilled, and $\struct {\R, +, \times}$ is a field.
{{qed}}
Theorem: Rational Numbers form Field

Consider the algebraic structure $\struct {\Q, +, \times}$, where:
:$\Q$ is the set of all rational numbers
:$+$ is the operation of rational addition
:$\times$ is the operation of rational multiplication.
Then $\struct {\Q, +, \times}$ forms a field.

Proof:
This is demonstrated in the formal definition of rational numbers.
{{Qed}}
Theorem: Real Numbers under Addition form Monoid

The set of real numbers under addition $\struct {\R, +}$ forms a monoid.

Proof:
Taking the monoid axioms in turn:
Theorem: Integers Modulo m under Addition form Abelian Group

Let $\Z_m$ is the set of integers modulo $m$
Let $+_m$ be the operation of addition modulo $m$.
Then the structure $\struct {\Z_m, +_m}$ is an abelian group.

Proof:
From Integers Modulo m under Addition form Cyclic Group, $\struct {\Z_m, +_m}$ is a cyclic group.
The result follows from Cyclic Group is Abelian.
{{Qed}}
Theorem: Complex Numbers under Addition form Monoid

The set of complex numbers under addition $\left({\C, +}\right)$ forms a monoid.

Proof:
Taking the monoid axioms in turn:
Theorem: Rational Numbers under Multiplication form Monoid

The set of rational numbers under multiplication $\struct {\Q, \times}$ forms a monoid.

Proof:
Taking the monoid axioms in turn:
Theorem: Real Numbers under Multiplication form Monoid

The set of real numbers under multiplication $\struct {\R, \times}$ forms a monoid.

Proof:
Taking the monoid axioms in turn:
Theorem: Complex Numbers under Multiplication form Monoid

The set of complex numbers under multiplication $\struct {\C, \times}$ forms a monoid.

Proof:
Taking the monoid axioms in turn:
Theorem: Non-Zero Natural Numbers under Multiplication form Commutative Monoid

Let $\N_{>0}$ be the set of natural numbers without zero, i.e. $\N_{>0} = \N \setminus \set 0$.
The structure $\struct{\N_{>0}, \times}$ forms a commutative monoid.

Proof:
From Non-Zero Natural Numbers under Multiplication form Commutative Semigroup, $\struct {\N_{>0}, \times}$ forms a commutative semigroup.
From Identity Element of Natural Number Multiplication is One, $\struct {\N_{>0}, \times}$ has an identity element which is $1$.
Hence the result, by definition of commutative monoid.
{{qed}}
Theorem: Non-Zero Natural Numbers under Addition do not form Monoid

Let $\N_{>0}$ be the set of natural numbers without zero, i.e. $\N_{>0} = \N \setminus \set 0$.
The structure $\struct {\N_{>0}, +}$ does ''not'' form a monoid.

Proof:
From Natural Numbers under Addition form Commutative Monoid, $\struct {\N, +}$ forms a commutative monoid.
From Natural Numbers Bounded Below under Addition form Commutative Semigroup, $\struct {\N_{>0}, +}$ forms a commutative semigroup.
From Identity Element of Natural Number Addition is Zero, $0$ is the identity of $\struct {\N, +}$ 
From Natural Number Addition is Cancellable, all elements of $\struct {\N, +}$ are cancellable.
{{AimForCont}} $\struct {\N_{>0}, +}$ is a monoid.
Then by definition $\struct {\N_{>0}, +}$ has an identity $e$.
From Identity of Cancellable Monoid is Identity of Submonoid, $e$ the same as the identity of $\struct {\N, +}$.
That is:
:$e = 0$
But $0 \notin \N_{>0}$.
Thus it follows that $\struct {\N_{>0}, +}$ has no identity.
Hence by Proof by Contradiction it follows that $\struct {\N_{>0}, +}$ is not a monoid.
{{qed}}
Theorem: Natural Numbers Bounded Below under Addition form Commutative Semigroup

Let $m \in \N$ where $\N$ is the set of natural numbers.
Let $M \subseteq \N$ be defined as:
:$M := \set {x \in \N: x \ge m}$
That is, $M$ is the set of all natural numbers greater than or equal to $m$.
Then the algebraic structure $\struct {M, +}$ is a commutative semigroup.

Proof:
We have that:
:Natural Number Addition is Associative
:Natural Number Addition is Commutative
From Restriction of Associative Operation is Associative, $+$ is associative on $\struct {M, +}$.
From Restriction of Commutative Operation is Commutative, $+$ is commutative on $\struct {M, +}$.
It remains to be shown that $+$ is closed on $\struct {M, +}$.
Let $a, b \in M$.
Then $\exists r, s \in \N: a = m + r, b = m + s$.
Thus:
{{begin-eqn}}
{{eqn | l = a + b
      | r = \paren {m + r} + \paren {m + s}
      | c = 
}}
{{eqn | r = m + \paren {m + r + s}
      | c = 
}}
{{eqn | o = \ge
      | r = m
      | c = 
}}
{{end-eqn}}
So $a + b \in M$ and so $+$ is closed on $\struct {M, +}$.
{{qed}}
Category:Examples of Commutative Semigroups
Category:Natural Number Addition
tnz2ewm7ni5rqma58fqlxgnyvsgn6qt
Theorem: Positive Real Numbers under Max Operation form Monoid

Let $\R_{\ge 0}$ be the set of positive (that is, non-negative) real numbers.
Let $\max: \R_{\ge 0}^2 \to \R_{\ge 0}$ be the max operation on $\R_{\ge 0}$.
Then $\struct {\R_{\ge 0}, \max}$ is a monoid whose identity is $0$.

Proof:
From Real Numbers are Totally Ordered, $\R$ is a totally ordered set.
From Max Operation on Toset forms Semigroup, $\struct {\R_{\ge 0}, \max}$ is a semigroup.
By definition of $\R_{\ge 0}$:
:$\forall x \in \R_{\ge 0}: 0 \le x$
Thus by definition of the max operation:
:$\forall x \in \R_{\ge 0}: \map \max {0, x} = x = \map \max {x, 0}$
So $0$ is the identity of $\struct {\R_{\ge 0}, \max}$ by definition.
The result follows by definition of monoid.
{{qed}}
Theorem: Free Commutative Monoid on One Element is Isomorphic to Natural Numbers under Addition

Let $X = \set x$ be a singleton.
Let $M$ be the free commutative monoid on $X$.
Then $M$ is isomorphic to the additive monoid of natural numbers.

Proof:
By definition, the free commutative monoid $M$ on $\set x$ is:
:$M = \set {e, x, x^2, x^3, \ldots}$
where $e$ denotes the null sequence of elements of $X$.
Let $\phi$ denote the mapping from $M$ to $\N$ as:
:$\forall a \in M: \map \phi a = \begin{cases}
0 & : a = e \\
n & : a = x^n \end{cases}$
By definition of $\phi$:
:$\phi$ is injective: $\map \phi a = \map \phi b \implies a = b$
:$\phi$ is surjective: $\forall a \in \N: \exists b \in M: \map \phi b = a$
:$\phi$ is a monoid homomorphism: $\map \phi {a b} = \map \phi {a + b} = \map \phi a + \map \phi b$
Hence the result, by definition of isomorphism.
{{qed}}
Theorem: Finite Monoid with Right Cancellable Operation is Group

Let $\struct {S, \circ}$ be a finite monoid.
Let $\circ$ be a right cancellable operation.
Then $\struct {S, \circ}$ is a group.

Proof:
{{Group-axiom|0}}, {{Group-axiom|1}} and {{Group-axiom|2}} are satisfied by dint of $\struct {S, \circ}$ being a monoid.
Recall the definition of right cancellable operation:
:$\forall a, b, c \in S: a \circ c = b \circ c \implies a = b$
Let $\rho_c: S \to S$ be the right regular representation of $\struct {S, \circ}$ with respect to $c$.
By Right Cancellable iff Right Regular Representation Injective, $\rho_c$ is an injection.
By Right Regular Representation wrt Right Cancellable Element on Finite Semigroup is Bijection, $\rho_c$ is a bijection.
Thus $a \circ b = e$ has a unique solution for all $a \in S$.
That is, {{Group-axiom|3}} holds on $S$.
{{qed}}
Theorem: Finite Monoid with Left Cancellable Operation is Group

Let $\struct {S, \circ}$ be a finite monoid.
Let $\circ$ be a left cancellable operation.
Then $\struct {S, \circ}$ is a group.

Proof:
{{Group-axiom|0}}, {{Group-axiom|1}} and {{Group-axiom|2}} are satisfied by dint of $\paren {S, \circ}$ being a monoid.
Recall the definition of left cancellable operation:
:$\forall a, b, c \in S: c \circ a = c \circ b \implies a = b$
Let $\lambda_c: S \to S$ be the left regular representation of $\struct {S, \circ}$ with respect to $c$.
By Left Cancellable iff Left Regular Representation Injective, $\lambda_c$ is an injection.
By Left Regular Representation wrt Left Cancellable Element on Finite Semigroup is Bijection, $\lambda_c$ is a bijection.
Thus $a \circ b = e$ has a unique solution for all $a \in S$.
That is, {{Group-axiom|3}} holds on $S$.
{{qed}}
Theorem: Multiplicative Group of Field is Abelian Group

Let $\struct {F, +, \times}$ be a field.
Let $F^* := F \setminus \set 0$ be the set $F$ less its zero.
The algebraic structure $\struct {F^*, \times}$ is an abelian group.

Proof:
From the field axioms:
{{begin-axiom}}
{{axiom | n = \text M 0
        | lc= Closure under product
        | q = \forall x, y \in F
        | m = x \circ y \in F
}}
{{axiom | n = \text M 1
        | lc= Associativity of product
        | q = \forall x, y, z \in F
        | m = \paren {x \circ y} \circ z = x \circ \paren {y \circ z}
}}
{{axiom | n = \text M 2
        | lc= Commutativity of product
        | q = \forall x, y \in F
        | m = x \circ y = y \circ x
}}
{{axiom | n = \text M 3
        | lc= Identity element for product
        | q = \exists 1_F \in F, 1_F \ne 0_F: \forall x \in F
        | m = x \circ 1_F = x = 1_F \circ x
        | rc= $1_F$ is called the unity
}}
{{axiom | n = \text M 4
        | lc= Inverse elements for product
        | q = \forall x \in F^*: \exists x^{-1} \in F^*
        | m = x \circ x^{-1} = 1_F = x^{-1} \circ x
}}
{{end-axiom}}
Hence the result.
{{qed}}
Theorem: Multiplicative Group of Field is Abelian Group

Let $\struct {F, +, \times}$ be a field.
Let $F^* := F \setminus \set 0$ be the set $F$ less its zero.
The algebraic structure $\struct {F^*, \times}$ is an abelian group.

Proof:
Recall that a field is a non-trivial commutative division ring.
The result follows from Non-Zero Elements of Division Ring form Group.
{{qed}}
Theorem: One and Minus One form Subgroup of Multiplicative Group of Rational Numbers

Let $\struct {\Q_{\ne 0}, \times}$ be the multiplicative group of rational numbers.
Let $S \subseteq \Q$ where $S = \set {1, -1}$.
Then $\struct {S, \times}$ is a subgroup of $\struct {\Q_{\ne 0}, \times}$.

Proof:
By hypothesis, $S$ is not empty.
As $0 \notin S$, it follows that $S \subseteq \Q_{\ne 0}$.
Recall that $-1 \times -1 = 1$ and also $1 \times 1 = 1$.
Thus:
:$\forall x \in S: x \times y^{-1} \in S$
The result follows from the One-Step Subgroup Test.
{{qed}}
Theorem: Symmetric Group is not Abelian

Let $S_n$ be the symmetric group of order $n$ where $n \ge 3$.
Then $S_n$ is not abelian.

Proof:
Let $\alpha \in S_n$ such that $\alpha$ is not the identity mapping.
From Center of Symmetric Group is Trivial, $\alpha$ is not in the center $\map Z {S_n}$ of $S_n$.
Thus $S_n \ne \map Z {S_n}$.
The result follows by definition of abelian group.
{{qed}}
Theorem: Symmetric Group is not Abelian

Let $S_n$ be the symmetric group of order $n$ where $n \ge 3$.
Then $S_n$ is not abelian.

Proof:
Let $a, b, c \in S$.
Let $\alpha$ be the transposition on $S$ which exchanges $a$ and $b$.
Let $\beta$ be the transposition on $S$ which exchanges $b$ and $c$.
Then:
:$\alpha \circ \beta$ maps $\tuple {a, b, c}$ to $\tuple {c, a, b}$
while:
:$\beta \circ \alpha$ maps $\tuple {a, b, c}$ to $\tuple {b, c, a}$
Thus $\alpha, \beta \in S_n$ such that $\alpha$ does not commute with $\beta$.
Hence the result by definition of abelian group.
{{qed}}
Theorem: Möbius Function is Multiplicative/Corollary

Let $\gcd \set {m, n} > 1$.
Then:
:$\map \mu {m n} = 0$

Proof:
Let $\gcd \set {m, n} = k$ where $k > 1$.
Then $m = k r$ and $n = k s$ for some $r, s \in \Z$.
Thus $m n = k^2 r s$.
From Integer is Expressible as Product of Primes there exists $p \in \Z$ such that $p$ is prime and $p \divides k$.
That is:
:$\exists t \in \Z: k = p t$
and so:
:$m n = p^2 t^2 r s$
That is:
:$p^2 \divides m $
Hence the result by definition of the Möbius function.
{{qed}}
Category:Multiplicative Functions
Category:Möbius Function
oxry1u2cq5rmz4yamh7ls14ie4hb64z
Theorem: Affine Group of One Dimension is Group

Let $\map {\operatorname {Af}_1} \R$ be the $1$-dimensional affine group on $\R$.
Then $\map {\operatorname {Af}_1} \R$ is a group.

Proof:
Taking the group axioms in turn:
=== {{Group-axiom|0|nolink}} ===
Let :
:$a, c \in \R_{\ne 0} \land b, d \in \R$
Let:
:$f_{ab}, f_{cd} \in \map {\operatorname {Af}_1} \R$
Then:
{{begin-eqn}}
{{eqn | l = \map {\paren {f_{ab} \circ f_{cd} } } x
      | r = \map {f_{ab} } {\map {f_{cd} } x}
      | c = {{Defof|Composition of Mappings}}
}}
{{eqn | r = \map {f_{ab} } {c x + d}
      | c = {{Defof|Affine Group of One Dimension}}
}}
{{eqn | r = a \paren {c x + d} + b
      | c = {{Defof|Affine Group of One Dimension}}
}}
{{eqn | r = \paren {a c x + a d} + b
      | c = {{Real-number-axiom|A1}}
}}
{{eqn | r = \paren {a c x} + \paren {a d + b}
      | c = {{Real-number-axiom|A1}}
}}
{{eqn | r = \paren {a c} x + \paren {a d + b}
      | c = {{Real-number-axiom|M1}}
}}
{{end-eqn}}
By the field axioms:
:$a c \in \R_{\ne 0} \land a d + b \in \R$
Thus $f_{ab} \circ f_{cd} \in \map {\operatorname {Af}_1} \R$ and so $\map {\operatorname {Af}_1} \R$ is closed.
{{qed|lemma}}
=== {{Group-axiom|1|nolink}} ===
From Composition of Mappings is Associative, it follows directly that $\circ$ is associative on $\map {\operatorname {Af}_1} \R$.
{{qed|lemma}}
=== {{Group-axiom|2|nolink}} ===
By Identity of Affine Group of One Dimension, $\map {\operatorname {Af}_1} \R$ has $f_{1, 0}$ as an identity element.
{{qed|lemma}}
=== {{Group-axiom|3|nolink}} ===
By Inverse in Affine Group of One Dimension, every element $f_{a b}$ of $\map {\operatorname {Af}_1} \R$ has an inverse $f_{c d}$ where $c = \dfrac 1 a$ and $d = \dfrac {-b} a$.
{{qed|lemma}}
All the group axioms are thus seen to be fulfilled, and so $\map {\operatorname {Af}_1} \R$ is a group.
{{qed}}
Theorem: Affine Group of One Dimension is Group

Let $\map {\operatorname {Af}_1} \R$ be the $1$-dimensional affine group on $\R$.
Then $\map {\operatorname {Af}_1} \R$ is a group.

Proof:
The result follows from Affine Group of One Dimension as Semidirect Product and Semidirect Product of Groups is Group.
{{qed}}