How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
If then iff is an integer multiple of , the powers are distinct, and has exactly elements; if has infinite order then only for
Statement
Let be a group, , and let orders be as in The order of a finite group and the order of an element, with when no positive power of is the identity. Throughout, a natural number written where an integer is expected means its image under the embedding of The naturals embed in the integers.
Finite order. Suppose with , . Then:
- for every , if and only if for some , that is, if and only if (Division with remainder in : for and there are unique with and );
- the powers are pairwise distinct: if with , and , then ;
- and ; so is finite with .
Infinite order. If then for , implies ; so the integer powers of are pairwise distinct and is not finite.
Facts & Assumptions
Given: A group with identity and an element ; , and when , otherwise (The order of a finite group and the order of an element, with when no positive power of is the identity).
Exponent laws: , and for all ; the first also holds for natural exponents in any monoid (Exponent laws in a group: and for all , and when and commute, Powers : natural exponents in a monoid and integer exponents in a group, with ).
Division with remainder: for and there are unique with and (Division with remainder in : for and there are unique with and ).
is injective, preserves addition, multiplication and order, and its image is exactly the nonnegative integers; , (The naturals embed in the integers). The order on is total and antisymmetric and is a commutative ring (The integers form a totally ordered ring, The integers form a commutative ring, Order on the integers, The integers as equivalence classes of pairs of naturals).
Induction on (The principle of mathematical induction).
On : the order is membership, so (On the order is membership: ); means for some (Order on the natural numbers); exactly one of , , holds (Trichotomy of the order on ).
Finiteness and counting: is finite when for some , and that is unique (Finite, countably infinite, countable, uncountable, Equinumerous sets, and , The pigeonhole principle on ); a bijection is an injective and surjective map (Injection, surjection, bijection).
Proof
for every . For natural exponents the set of with contains , since , and is closed under , since ; induction gives it for all naturals. For write ; then .
Assume with . Then , so , and no natural with satisfies , since is the least element of . Also , because and preserves the order.
Infinite order. Assume and suppose with and . Put , so and . Also . By totality one of and is positive; call it , so and with and , hence . Then , contradicting .
The "if" half of claim 1: if for some , then .
The "only if" half. Suppose . Divide: with , legitimate since . Then . Since , we have for a unique , and forces , because otherwise and would give , contradicting antisymmetry. So with .
Claim 2. Let with , and . By trichotomy we may assume , interchanging the names if necessary, and then for some . Now , so by cancellation. Moreover , since , and , so . If then with , impossible; so and .
Therefore in the infinite-order case forces . Moreover is then not finite: a bijection with would make a map , and that map is injective, since is injective, distinct integer exponents give distinct powers by step 1.3, and is injective; but claim 1 of the pigeonhole principle forbids an injection .
In step 2.2 the case is impossible, since it would put in below its least element; hence , so and . With step 2.1 this is claim 1.
Every integer power of is one of : given , divide with , write with and as in step 2.2, and compute .
Claim 3. By [L2] and step 3.2, . The map with is well defined, the elements of the natural number being exactly the naturals ; it is surjective by the displayed description and injective by step 2.3. So is a bijection, , and is finite with , the value being the unique natural equinumerous with .
Claims 1, 2 and 3 are steps 3.1, 2.3 and 4.1, and the infinite-order statement is steps 1.3 and 2.4.
Remarks
-
The division algorithm is exactly what is needed and nothing more. Claim 1 reduces an arbitrary integer exponent to a remainder in ; that reduction is the only place where arithmetic in beyond the ring laws enters, and it is why Division with remainder in : for and there are unique with and is proved on this page.
-
The count in claim 3 starts at exponent . The distinct powers are ; there are of them because , as a von Neumann natural, is the set of exponents used (On the order is membership: ). Reading the list as starting at would give a count off by one.
-
The identity is what makes the order of an element a statement about a subgroup, and is the step on which the later result that the order of an element divides the order of the group rests.
Depends on
The order of a finite group and the order of an element, with when no positive power of is the identity
Powers : natural exponents in a monoid and integer exponents in a group, with
Exponent laws in a group: and for all , and when and commute
Cancellation in a group: or forces ; equivalently left and right translation by are bijections of , so and each have exactly one solution
In a group , and , the order of the last product being essential
, and every cyclic group is abelian
Division with remainder in : for and there are unique with and
The principle of mathematical induction
Finite, countably infinite, countable, uncountable
Equinumerous sets, and
Injection, surjection, bijection
The pigeonhole principle on
The integers as equivalence classes of pairs of naturals
Order on the integers
The integers form a commutative ring
The integers form a totally ordered ring
The naturals embed in the integers
On the order is membership:
Order on the natural numbers
Trichotomy of the order on