avewright/proofwiki-math huggingface dataset:
Theorem: Universal Affirmative and Negative are both False iff Particular Affirmative and Negative are both True

Consider the categorical statements:
{{begin-axiom}}
{{axiom | q = \map {\mathbf A} {S, P}
        | lc= The universal affirmative:
        | ml= \forall x: \map S x
        | mo= \implies
        | mr= \map P x
}}
{{axiom | q = \map {\mathbf E} {S, P}
        | lc= The universal negative:
        | ml= \forall x: \map S x
        | mo= \implies
        | mr= \neg \map P x
}}
{{axiom | q = \map {\mathbf I} {S, P}
        | lc= The particular affirmative:
        | ml= \exists x: \map S x
        | mo= \land 
        | mr= \map P x
}}
{{axiom | q = \map {\mathbf O} {S, P}
        | lc= The particular negative:
        | ml= \exists x: \map S x
        | mo= \land 
        | mr= \neg \map P x
}}
{{end-axiom}}
Then:
:$\map {\mathbf A} {S, P}$ and $\map {\mathbf E} {S, P}$ are both false
{{iff}}:
:$\map {\mathbf I} {S, P}$ and $\map {\mathbf O} {S, P}$ are both true.

Proof:
=== Necessary Condition ===
Let $\map {\mathbf A} {S, P}$ and $\map {\mathbf E} {S, P}$ both be false.
{{begin-eqn}}
{{eqn | n = 1
      | l = \neg \map {\mathbf A} {S, P}
      | o = \land
      | r = \neg \map {\mathbf E} {S, P}
}}
{{eqn | n = 2
      | ll= \leadsto
      | l = \neg \map {\mathbf A} {S, P}
      | o =
      | c = Rule of Simplification: from $(1)$
}}
{{eqn | n = 3
      | ll= \leadsto
      | l = \map {\mathbf O} {S, P}
      | o =
      | c = Universal Affirmative and Particular Negative are Contradictory: from $(2)$
}}
{{eqn | n = 4
      | ll= \leadsto
      | l = \neg \map {\mathbf E} {S, P}
      | o =
      | c = Rule of Simplification: from $(1)$
}}
{{eqn | n = 5
      | ll= \leadsto
      | l = \map {\mathbf I} {S, P}
      | o =
      | c = Particular Affirmative and Universal Negative are Contradictory: from $(4)$
}}
{{eqn | n = 6
      | ll= \leadsto
      | l = \map {\mathbf I} {S, P}
      | o = \land
      | r = \map {\mathbf O} {S, P}
      | c = Rule of Conjunction: from $(5)$ and $(3)$
}}
{{end-eqn}}
Hence $\map {\mathbf I} {S, P}$ and $\map {\mathbf O} {S, P}$ are both true.
{{qed|lemma}}
Theorem: Law of Simple Conversion of I

Consider the particular affirmative categorical statement ''Some $S$ is $P$'':
:$\map {\mathbf I} {S, P}: \exists x: \map S x \land  \map P x$
Then ''Some $P$ is $S$'':
:$\map {\mathbf I} {P, S}$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = \map {\mathbf I} {S, P}
      | c = 
}}
{{eqn | ll= \leadsto
      | o = 
      | q = \exists x
      | r = \map S x \land \map P x
      | c = {{Defof|Particular Affirmative}}
}}
{{eqn | ll= \leadsto
      | o = 
      | q = \exists x
      | r = \map P x \land \map S x
      | c = Conjunction is Commutative
}}
{{eqn | ll= \leadsto
      | o = 
      | r = \map {\mathbf I} {P, S}
      | c = {{Defof|Particular Affirmative}}
}}
{{end-eqn}}
{{qed}}
Theorem: Law of Simple Conversion of E

Consider the universal negative categorical statement ''No $S$ is $P$'':
:$\map {\mathbf E} {S, P}: \forall x: \map S x \implies \neg \map P x$
Then ''No $P$ is $S$'':
:$\map {\mathbf E} {P, S}$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = \map {\mathbf E} {S, P}
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \forall x
      | o = 
      | r = \map S x \implies \neg \map P x
      | c = {{Defof|Universal Negative}}
}}
{{eqn | ll= \leadsto
      | q = \forall x
      | o = 
      | r = \neg \paren {\map S x \land \map P x}
      | c = Modus Ponendo Tollens
}}
{{eqn | ll= \leadsto
      | q = \forall x
      | o = 
      | r = \neg \paren {\map P x \land \map S x}
      | c = Conjunction is Commutative
}}
{{eqn | ll= \leadsto
      | q = \forall x
      | o = 
      | r = \map P x \implies \neg \map S x
      | c = Modus Ponendo Tollens
}}
{{eqn | ll= \leadsto
      | o = 
      | r = \map {\mathbf E} {P, S}
      | c = {{Defof|Universal Negative}}
}}
{{end-eqn}}
{{qed}}
Theorem: Conversion per Accidens

Consider the categorical statements:
{{begin-axiom}}
{{axiom | ll = \map {\mathbf A} {S, P}:
        | lc= The universal affirmative:
        | q = \forall x
        | m = \map S x \implies \map P x
}}
{{axiom | ll= \map {\mathbf I} {P, S}:
        | lc= The particular affirmative:
        | q = \exists x
        | m = \map P x \land \map S x
}}
{{end-axiom}}
Then:
:$\map {\mathbf A} {S, P} \implies \map {\mathbf I} {P, S}$
{{iff}}:
:$\exists x: \map S x$
Using the symbology of predicate logic:
:$\exists x: \map S x \iff \paren {\paren {\forall x: \map S x \implies \map P x} \implies \paren {\exists x: \map P x \land \map S x} }$
This law has the traditional name '''conversion per accidens of $\mathbf A$'''.
Thus the $\mathbf A$ form '''converts per accidens''' to the $\mathbf I$ form.

Proof:
From Universal Affirmative implies Particular Affirmative iff First Predicate is not Vacuous:
:$\exists x: \map S x \iff \paren {\paren {\forall x: \map S x \implies \map P x} \implies \paren {\exists x: \map S x \land \map P x} }$
From Law of Simple Conversion of I:
:$\paren {\exists x: \map S x \land \map P x} \implies \paren {\exists x: \map P x \land \map S x}$
Hence the result.
{{qed}}
Theorem: Number of Standard Instances of Categorical Syllogism

There are $256$ distinct standard instances of the categorical syllogism.

Proof:
Recall the four figures of the categorical syllogism:
:<nowiki>$\begin{array}{r|rl}
\text I & & \\
\hline \\
\text{Major Premise}: & \mathbf \Phi_1 & \tuple {M, P} \\
\text{Minor Premise}: & \mathbf \Phi_2 & \tuple {S, M} \\
\hline \\
\text{Conclusion}: & \mathbf \Phi_3 & \tuple {S, P} \\
\end{array}
\qquad
\begin{array}{r|rl}
\text {II} & & \\
\hline \\
\text{Major Premise}: & \mathbf \Phi_1 & \tuple {P, M} \\
\text{Minor Premise}: & \mathbf \Phi_2 & \tuple {S, M} \\
\hline \\
\text{Conclusion}: & \mathbf \Phi_3 & \tuple {S, P} \\
\end{array}$</nowiki>
:<nowiki>$\begin{array}{r|rl}
\text {III} & & \\
\hline \\
\text{Major Premise}: & \mathbf \Phi_1 & \tuple {M, P} \\
\text{Minor Premise}: & \mathbf \Phi_2 & \tuple {M, S} \\
\hline \\
\text{Conclusion}: & \mathbf \Phi_3 & \tuple {S, P} \\
\end{array}
\qquad
\begin{array}{r|rl}
\text {IV} & & \\
\hline \\
\text{Major Premise}: & \mathbf \Phi_1 & \tuple {P, M} \\
\text{Minor Premise}: & \mathbf \Phi_2 & \tuple {M, S} \\
\hline \\
\text{Conclusion}: & \mathbf \Phi_3 & \tuple {S, P} \\
\end{array}$</nowiki>
By the definition of a categorical syllogism, the following are fixed:
:$(1): \quad$ The order of the categorical statements: major premise, then minor premise, then conclusion.
:$(2): \quad$ The structure of the conclusion: the secondary term then the primary term.
:$(3): \quad$ The content of the two premises: the major premise contains the primary term and the middle term, while the minor premise contains the middle term and the secondary term.
The things that can be varied are:
:$(A): \quad$ The specific nature of each of the categorical statements: each can be any of four types: $\mathbf A$, $\mathbf E$, $\mathbf I$ or $\mathbf O$.
:$(B): \quad$ Within the major and minor premises, the order of the two terms: the middle term can come either first or second.
The order of the terms within the premises determines the figure of the categorical syllogism.
For each of the two premises there are two options for the position of the middle term.
By the Product Rule for Counting it follows that there are $2 \times 2 = 4$ figures.
In each figure, there are $3$ categorical statements.
Each can be of any of $4$ types.
Hence by the Product Rule for Counting, there are $4 \times 4 \times 4 = 64$ possible standard instances for each figure.
For all $4$ figures, by the Product Rule for Counting, it follows that there are $4 \times 64 = 256$ standard instances in total.
{{qed}}
Theorem: Valid Patterns of Categorical Syllogism

The following categorical syllogisms are valid:
:<nowiki>$\begin{array}{rl}
\text{I} & AAA \\
\text{I} & AII \\
\text{I} & EAE \\
\text{I} & EIO \\
* \text{I} & AAI \\
* \text{I} & EAO \\
\end{array}
\qquad
\begin{array}{rl}
\text{II} & EAE \\
\text{II} & AEE \\
\text{II} & AOO \\
\text{II} & EIO \\
* \text{II} & EAO \\
* \text{II} & AEO \\
\end{array}
\qquad
\begin{array}{rl}
\dagger \text{III} & AAI \\
\text{III} & AII \\
\text{III} & IAI \\
\dagger \text{III} & EAO \\
\text{III} & EIO \\
\text{III} & OAO \\
\end{array}
\qquad
\begin{array}{rl}
\S \text{IV} & AAI \\
\text{IV} & AEE \\
\dagger \text{IV} & EAO \\
\text{IV} & EIO \\
\text{IV} & IAI \\
* \text{IV} & AEO \\
\end{array}$</nowiki>
In the above:
:$\text{I}, \text{II}, \text{III}, \text{IV}$ denote the four figures of the categorical syllogisms.
:$A, E, I, O$ denote the universal affirmative, universal negative, particular affirmative and particular negative respectively: see Shorthand for Categorical Syllogism.
:Syllogisms marked $*$ require the assumption that $\exists x: \map S x$, that is, that there exists an object fulfilling the secondary predicate.
:Syllogisms marked $\dagger$ require the assumption that $\exists x: \map M x$, that is, that there exists an object fulfilling the middle predicate.
:Syllogisms marked $\S$ require the assumption that $\exists x: \map P x$, that is, that there exists an object fulfilling the primary predicate.

Proof:
From Elimination of all but 24 Categorical Syllogisms as Invalid, all but these $24$ patterns have been shown to be invalid.
It remains to be shown that these remaining syllogisms are in fact valid.
{{ProofWanted|Considerable work to be done yet.}}
Theorem: No Valid Categorical Syllogism contains two Particular Premises

Let $Q$ be a valid categorical syllogism.
Then at least one of the premises of $Q$ is universal.

Proof:
Suppose both premises of $Q$ are particular.
Then the pattern of $Q$ is one of $\text{II}x$, $\text{IO}x$, $\text{OI}x$ or $\text{OO}x$, where $x$ is the conclusion.
$\text{I}$ is neither universal nor negative.
Thus the $\text{II}x$ pattern does not distribute the middle term of $Q$.
So $\text{II}x$ violates the rule Middle Term of Valid Categorical Syllogism is Distributed at least Once.
$\text{O}$ is negative.
Thus $\text{OO}x$ violates the rule No Valid Categorical Syllogism contains two Negative Premises.
It remains to investigate $\text{IO}x$ and $\text{OI}x$.
By Conclusion of Valid Categorical Syllogism is Negative iff one Premise is Negative, the conclusion of $Q$ is negative, either $\text{E}$ or $\text{O}$.
By the definition of Distributed Predicate of Categorical Syllogism, the predicate of the conclusion of $Q$ is distributed.
Thus, by construction, the primary term $P$ of $Q$ is distributed.
By Distributed Term of Conclusion of Valid Categorical Syllogism is Distributed in Premise, it follows that $P$ is distributed in the major premise of $Q$.
This eliminates $\text{IO}x$ as the particular affirmative $\text{I}$ distributes neither its subject nor its predicate.
The final pattern to be investigated is $\text{OI}x$.
By definition, $\text{O}$ distributes only its predicate.
As $\text{O}$ needs to distribute the primary term $P$, it cannot also distribute the middle term $M$ of $Q$.
But the particular affirmative $\text{I}$ (as has been seen above) also does not distribute $M$.
Thus $M$ remains undistributed, so violating the rule Middle Term of Valid Categorical Syllogism is Distributed at least Once.
This eliminates $\text{OI}x$.
{{qed}}
Theorem: No Valid Categorical Syllogism with Particular Premise has Universal Conclusion

Let $Q$ be a valid categorical syllogism.
Let one of the premises of $Q$ be particular.
Then the conclusion of $Q$ is also particular.

Proof:
Let the major premise of $Q$ be denoted $\text{Maj}$.
Let the minor premise of $Q$ be denoted $\text{Min}$.
Let the conclusion of $Q$ be denoted $\text{C}$.
From No Valid Categorical Syllogism contains two Particular Premises, either $\text{Maj}$ or $\text{Min}$ has to be universal.
Let the other premise of $Q$ be particular.
Suppose $\text{C}$ is the universal affirmative $\map {\mathbf A} {S, P}$.
From Conclusion of Valid Categorical Syllogism is Negative iff one Premise is Negative it follows that $\text{Maj}$ and $\text{Min}$ are also both affirmative.
The only patterns fitting the criteria are $\text{AI}x$ and $\text{IA}x$, both of which distribute only one term in $Q$.
We have that $\text{C}$ distributes $S$.
From Distributed Term of Conclusion of Valid Categorical Syllogism is Distributed in Premise, $S$ must also be distributed in $\text{Min}$.
From Middle Term of Valid Categorical Syllogism is Distributed at least Once, the middle term $M$ of $Q$ needs to be distributed.
Thus we require two distributed terms in the premises for $\text{C}$ to be the universal affirmative.
So if $\text{C}$ is affirmative, neither premise of $Q$ can be particular.
From this contradiction it follows that $\text{C}$ is not $\map {\mathbf A} {S, P}$.
Suppose $\text{C}$ is the universal negative $\map {\mathbf E} {S, P}$.
In this case, both $S$ and $P$ are distributed in $C$, as the universal negative distributes both $S$ and $P$.
By Middle Term of Valid Categorical Syllogism is Distributed at least Once, the middle term $M$ of $Q$ needs to be distributed.
Thus there are three terms needing to be distributed in two premises.
So at least one premises needs to be the universal negative.
The other premise is not $\mathbf O$ as this violates No Valid Categorical Syllogism contains two Negative Premises.
But it also is not $\mathbf I$, as $\mathbf I$ does not distribute any terms.
So if $\text{C}$ is the universal negative, neither premise can be particular.
From this contradiction it follows that $\text{C}$ is not $\map {\mathbf E} {S, P}$.
{{qed}}
Theorem: Conjunction implies Disjunction

:$\vdash \paren {p \land q} \implies \paren {p \lor q}$

Proof:
{{BeginTableau|\paren {p \land q} \implies \paren {p \lor q} }}
{{Assumption|1|p \land q}}
{{Simplification|2|1|p|1|1}}
{{Addition|3|1|p \lor q|2|1}}
{{Implication|4||\paren {p \land q} \implies \paren {p \lor q}|1|3}}
{{EndTableau}}
{{qed}}
Theorem: Conjunction implies Disjunction

:$\vdash \paren {p \land q} \implies \paren {p \lor q}$

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connective is true for all boolean interpretations.
:<nowiki>$\begin{array}{|ccc|c|ccc|} \hline
(p & \land & q) & \implies & (p & \lor & q) \\
\hline
\F & \F & \F & \T & \F & \F & \F \\
\F & \F & \T & \T & \F & \T & \T \\
\T & \F & \F & \T & \T & \T & \F \\
\T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Angle Bisector Vector

Let $\mathbf u$ and $\mathbf v$ be vectors of non-zero length.
Let $\norm {\mathbf u}$ and $\norm {\mathbf v}$ be their respective lengths.
Then $\norm {\mathbf u} \mathbf v + \norm {\mathbf v} \mathbf u$ is the angle bisector of $\mathbf u$ and $\mathbf v$.

Proof:
Let $\mathbf a = \norm {\mathbf u} \mathbf v + \norm {\mathbf v} \mathbf u$.
Then:
{{begin-eqn}}
{{eqn | l = \cos \angle \mathbf u, \mathbf a
      | r = \frac {\mathbf u \cdot \mathbf a} {\norm {\mathbf u} \norm {\mathbf a} }
      | c = Cosine Formula for Dot Product
}}
{{eqn | r = \frac {\mathbf u \cdot \paren {\norm {\mathbf u} \mathbf v + \norm {\mathbf v} \mathbf u} } {\norm {\mathbf u} \norm {\mathbf a} }
      | c = $\mathbf a = \norm {\mathbf u} \mathbf v + \norm {\mathbf v} \mathbf u$
}}
{{eqn | r = \frac {\norm {\mathbf u} \paren {\mathbf u \cdot \mathbf v} + \norm {\mathbf v} \paren {\mathbf u \cdot \mathbf u} } {\norm {\mathbf u} \norm{\mathbf a} }
      | c = Dot Product Associates with Scalar Multiplication
}}
{{eqn | r = \frac {\norm {\mathbf u} \paren {\mathbf u \cdot \mathbf v} + \norm {\mathbf v} \norm {\mathbf u}^2} {\norm {\mathbf u} \norm {\mathbf a} }
      | c = Dot Product of Vector with Itself
}}
{{eqn | r = \frac {\mathbf u \cdot \mathbf v + \norm {\mathbf u} \norm {\mathbf v} } {\norm {\mathbf a} }
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \cos \angle \mathbf a, \mathbf v
      | r = \frac {\mathbf v \cdot \mathbf a} {\norm {\mathbf v} \norm{\mathbf a} }
      | c = Cosine Formula for Dot Product
}}
{{eqn | r = \frac {\mathbf v \cdot \paren {\norm {\mathbf u} \mathbf v + \norm {\mathbf v} \mathbf u} } {\norm {\mathbf v} \norm {\mathbf a} }
      | c = $\mathbf a = \norm {\mathbf u} \mathbf v + \norm {\mathbf v} \mathbf u$
}}
{{eqn | r = \frac {\norm {\mathbf u} \paren {\mathbf v \cdot \mathbf v} + \norm {\mathbf v} \paren {\mathbf u \cdot \mathbf v} } {\norm {\mathbf v} \norm {\mathbf a} }
      | c = Dot Product Associates with Scalar Multiplication
}}
{{eqn | r = \frac {\norm {\mathbf v} \paren {\mathbf u \cdot \mathbf v} + \norm {\mathbf u} \norm {\mathbf v}^2} {\norm {\mathbf v} \norm {\mathbf a} }
      | c = Dot Product of Vector with Itself
}}
{{eqn | r = \frac {\mathbf u \cdot \mathbf v + \norm {\mathbf u} \norm {\mathbf v} } {\norm {\mathbf a} }
}}
{{end-eqn}}
Comparing the two expressions gives us:
:$\cos \angle \mathbf u, \mathbf a = \cos \angle \mathbf a, \mathbf v$
Since the angle used in the dot product is always taken to be between $0$ and $\pi$ and cosine is injective on this interval (from Shape of Cosine Function):
:$\angle \mathbf u, \mathbf a = \angle \mathbf a, \mathbf v$
The result follows.
{{qed}}
Theorem: Angle Bisector Vector

Let $\mathbf u$ and $\mathbf v$ be vectors of non-zero length.
Let $\norm {\mathbf u}$ and $\norm {\mathbf v}$ be their respective lengths.
Then $\norm {\mathbf u} \mathbf v + \norm {\mathbf v} \mathbf u$ is the angle bisector of $\mathbf u$ and $\mathbf v$.

Proof:
:400px
As shown above:
:Let $\gamma$ be the angle between $\mathbf u$ and $\mathbf v$.
:Let $\alpha$ be the angle between $\norm {\mathbf u} \mathbf v$ and $\norm {\mathbf v} \mathbf u$.
:Let $\beta$ be the angle between $\mathbf u$ and $\norm {\mathbf u} \mathbf v + \norm {\mathbf v} \mathbf u$.
Note that $\norm {\mathbf u} \mathbf v$ is $\mathbf v$ multiplied by the length of $\mathbf u$.
By Vector Times Magnitude Same Length As Magnitude Times Vector the vectors $\norm {\mathbf u} \mathbf v$ and $\norm {\mathbf v} \mathbf u$ have equal length.
So $\norm {\mathbf u} \mathbf v$, $\norm {\mathbf v} \mathbf u$ and $\norm {\mathbf u} \mathbf v + \norm {\mathbf v} \mathbf u$ make an isosceles triangle.
Therefore:
{{begin-eqn}}
{{eqn | l = 2 \beta + \alpha
      | r = 180 \degrees
}}
{{eqn | l = \beta
      | r = 90 \degrees - \frac 1 2 \alpha
}}
{{eqn | l = 2 \beta
      | r = 180 \degrees - \alpha
}}
{{end-eqn}}
But since $\mathbf v$ and $\norm {\mathbf u} \mathbf v$ are parallel, we also have:
{{begin-eqn}}
{{eqn | l = \delta
      | r = \alpha
      | c = Parallelism implies Equal Corresponding Angles
}}
{{eqn | l = \delta + \gamma
      | r = 180 \degrees
}}
{{eqn | l = \alpha + \gamma
      | r = 180 \degrees
}}
{{eqn | l = \gamma
      | r = 180 \degrees - \alpha
}}
{{end-eqn}}
Thus $\gamma = 2 \beta$, and the result follows.
{{qed}}
Theorem: Angle Bisector Vector

Let $\mathbf u$ and $\mathbf v$ be vectors of non-zero length.
Let $\norm {\mathbf u}$ and $\norm {\mathbf v}$ be their respective lengths.
Then $\norm {\mathbf u} \mathbf v + \norm {\mathbf v} \mathbf u$ is the angle bisector of $\mathbf u$ and $\mathbf v$.

Proof:
The vectors $\norm {\mathbf u} \mathbf v$ and $\norm {\mathbf v} \mathbf u$ have equal length from Vector Times Magnitude Same Length As Magnitude Times Vector.
Thus $\norm {\mathbf u} \mathbf v + \norm {\mathbf v} \mathbf u$ is the diagonal of a rhombus.
The result follows from Diagonals of Rhombus Bisect Angles.
{{qed}}
Theorem: Subgroup of Order 1 is Trivial

Let $\struct {G, \circ}$ be a group.
Then $\struct {G, \circ}$ has exactly $1$ subgroup of order $1$: the trivial subgroup.

Proof:
From Trivial Subgroup is Subgroup, $\struct {\set e, \circ}$ is a subgroup of $\struct {G, \circ}$.
Suppose $\struct {\set g, \circ}$ is a subgroup of $\struct {G, \circ}$.
From Group is not Empty, $e \in \set g$.
Thus it follows trivially that $\struct {\set g, \circ} = \struct {\set e, \circ}$.
That is, $\struct {\set e, \circ}$ is the only subgroup of $\struct {G, \circ}$ of order $1$.
{{qed}}
Theorem: Injection from Finite Set to Itself is Surjection/Corollary

Let $S$ be a finite set.
Let $f: S \to S$ be an injection.
Then $f$ is a permutation.

Proof:
From Injection from Finite Set to Itself is Surjection, $f$ is a surjection.
As $f$ is thus both an injection and a surjection, $f$ is a bijection by definition.
Thus as $f$ is a bijection to itself, it is by definition a permutation.
{{qed}}
Theorem: Surjection from Finite Set to Itself is Permutation

Let $S$ be a finite set.
Let $f: S \to S$ be an surjection.
Then $f$ is a permutation.

Proof:
From Surjection iff Right Inverse, $f$ has a right inverse $g: S \to S$.
From Right Inverse Mapping is Injection, $g$ is an injection.
From Injection from Finite Set to Itself is Permutation, $g$ is a permutation and so a bijection.
From Inverse of Bijection is Bijection, $f$ is also a bijection.
Thus as $f$ is a bijection to itself, it is by definition a permutation.
{{qed}}
Theorem: Order of Power of Group Element

Let $\struct {G, \circ}$ be a group whose identity is $e$.
Let $g \in G$ be an element of $G$ such that:
:$\order g = n$
where $\order g$ denotes the order of $g$.
Then:
:$\forall m \in \Z: \order {g^m} = \dfrac n {\gcd \set {m, n} }$
where $\gcd \set {m, n}$ denotes the greatest common divisor of $m$ and $n$.

Proof:
Let $\gcd \set {m, n} = d$.
From Integers Divided by GCD are Coprime: there exists $m', n' \in \Z$ such that $m = d m'$, $n = d n'$.
Then:
{{begin-eqn}}
{{eqn | l = \paren {g^m}^{n'}
      | r = \paren {g^{d m'} }^{n'}
      | c = Definition of $m'$
}}
{{eqn | r = \paren {g^{d n'} }^{m'}
      | c = 
}}
{{eqn | r = \paren {g^n}^{m'}
      | c = Definition of $n'$
}}
{{eqn | r = e^{m'}
      | c = $n$ is the order of $g$
}}
{{eqn | r = e
      | c = 
}}
{{end-eqn}}
By Element to Power of Multiple of Order is Identity:
:$\order {g^m} \divides n'$.
{{AimForCont}} $\order {g^m} = n' ' < n'$.
By Bézout's Identity:
:$\exists x, y \in \Z: m x + n y = d$
{{begin-eqn}}
{{eqn | l = g^{d n' '}
      | r = g^{\paren {m x + n y} n' '}
      | c = 
}}
{{eqn | r = \paren {g^{m n' '} }^x \paren {g^n}^{y n' '}
      | c = 
}}
{{eqn | r = e^x \paren {g^n}^{y n' '}
      | c = $n' '$ is the order of $g^m$
}}
{{eqn | r = e^x e^{y n' '}
      | c = $n$ is the order of $g$
}}
{{eqn | r = e
      | c = 
}}
{{end-eqn}}
But $d n' ' < d n' = n$, contradicting the fact that $n$ is the order of $g$.
Therefore:
:$\order {g^m} = n'$
Recalling the definition of $n'$:
:$\order {g^m} = \dfrac n {\gcd \set {m, n} }$
as required.
{{qed}}
Theorem: Existence of Group of Finite Order

Let $n \in \Z_{>0}$.
Then there exists at least one group whose order is $n$.

Proof:
From Existence of Cyclic Group of Order n, there exists a cyclic group whose order is $n$.
In particular, a concrete example of such a group is demonstrated in Roots of Unity under Multiplication form Cyclic Group.
{{qed}}