TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17

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.

Sylow I: every finite group has a Sylow $p$ -subgroup

Statement

Let $G$ be finite, let $p$ be prime, and write $∣ G ∣ = p^{a} m$ with $p ∤ m$ . Then $G$ has a subgroup of order $p^{a}$ , hence a Sylow $p$ -subgroup (Sylow $p$ -subgroups of a finite group). See Sylow $p$ -subgroups of a finite group.

Facts & Assumptions

Given: The hypotheses and objects in the Statement.

[L1]

Let $G$ be a finite group, let $p$ be prime, and write $∣ G ∣ = p^{a} m$ with $a \in N$ and $p ∤ m$ . A subgroup $P \leq G$ is a Sylow $p$ -subgroup when $∣ P ∣ = p^{a}$ . Equivalently, its order is the largest power of $p$ dividing $∣ G ∣$ . This is a property of a subgroup and does not presume that such a subgroup exists; existence is proved in thm-sylow-first-theorem. (Sylow $p$ -subgroups of a finite group).

[L2]

Let $p$ be prime and let $a, m \in N$ satisfy $p ∤ m$ . Then $v_{p} ⁣ ((\binom{p^{a} m}{p^{a}})) = 0.$ The valuation is applied only to nonzero integers. (If $∣ G ∣ = p^{a} m$ with $p ∤ m$ , then $v_{p} (\binom{p^{a} m}{p^{a}}) = 0$ ).

[L3]

Let $G$ act on $X$ and let $x \in X$ . The rule $Φ : G / G_{x} ⟶ G \cdot x, Φ (g G_{x}) = g \cdot x,$ is well-defined and bijective. Thus every orbit is naturally in bijection with the left cosets of its stabilizer. (Orbit-stabiliser: $G / G_{x} \to G \cdot x$ , $g G_{x} \mapsto g \cdot x$ , is a well-defined bijection).

[L4]

For an action of $G$ on $X$ and $x \in X$ , $∣ G \cdot x ∣ = [G : G_{x}]$ whenever either side is finite. In particular, if $G$ is finite, then $∣ G ∣ = ∣ G_{x} ∣ ∣ G \cdot x ∣ .$ . (Orbit-stabiliser cardinality: $∣ G \cdot x ∣ = [G : G_{x}]$ whenever either side is finite, and $∣ G ∣ = ∣ G_{x} ∣ ∣ G \cdot x ∣$ for finite $G$ ).

[L5]

Let $G$ be a finite group and $H \leq G$ . Then $∣ G ∣ = [G : H] ∣ H ∣ .$ Consequently, under the canonical embedding $ι : N \to Z$ , $∣ H ∣$ divides $∣ G ∣$ . (Lagrange's theorem: $∣ G ∣ = [G : H] ∣ H ∣$ for every subgroup $H$ of a finite group $G$ ).

[L6]

Let $P$ be a property of naturals such that for every $n \in N$ , if $P (m)$ holds for all $m < n$ then $P (n)$ . Then $P (n)$ holds for all $n \in N$ . (At $n = 0$ the hypothesis is vacuous, so $P (0)$ is forced.). (Strong (complete) induction).

[L7]

For a left action of $G$ on $X$ , the relation $x \sim y$ defined by $y = g \cdot x$ for some $g \in G$ is an equivalence relation whose class at $x$ is $G \cdot x$ , and the distinct orbits partition $X$ (The orbits of a group action are the equivalence classes of $x \sim y$ iff $y = g \cdot x$ for some $g$ , and hence partition the acted-on set).

Proof

technique · direct

1.1

Argue by strong induction [L6] on $∣ G ∣$ , the induction statement being that every finite group of order $n$ has a subgroup of order $p^{a}$ whenever $n = p^{a} m$ with $p ∤ m$ . Let $Ω$ be the set of subsets of $G$ of size $p^{a}$ and let $G$ act on $Ω$ by left translation, $g \cdot A : = g A$ ; this is an action, and $∣ g A ∣ = ∣ A ∣$ because left translation is a bijection of $G$ . Counting subsets gives $∣ Ω ∣ = (\binom{p^{a} m}{p^{a}})$ , so [L2] yields $v_{p} (∣ Ω ∣) = 0$ , that is $p ∤ ∣ Ω ∣$ .

L2L6givenalgebra

2.1

By [L7] the orbits partition $Ω$ , so $∣ Ω ∣$ is the sum of the orbit sizes. Were $p$ to divide every orbit size it would divide $∣ Ω ∣$ , so some orbit $O$ has $p ∤ ∣ O ∣$ . Choose $A \in O$ and put $H = G_{A} = {g \in G : g A = A}$ . The bijection of [L3] between $G / H$ and $O$ gives $∣ O ∣ = [G : H]$ , so [L4] gives $p^{a} m = ∣ G ∣ = ∣ H ∣ ∣ O ∣$ ; since $p ∤ ∣ O ∣$ , the full power $p^{a}$ divides $∣ H ∣$ .

step 1.1L3L4L7choose

3.1

Suppose $H = G$ . Then $g A = A$ for every $g \in G$ , so for any $x \in A$ the set $A$ contains $G x = G$ , whence $A = G$ and $p^{a} = ∣ A ∣ = ∣ G ∣ = p^{a} m$ . Thus $m = 1$ and $G$ itself is a subgroup of order $p^{a}$ .

step 2.1givenalgebra

3.2

Suppose instead $H \neq G$ , so $∣ H ∣ < ∣ G ∣$ . By [L5], $∣ H ∣$ divides $p^{a} m$ ; writing $∣ H ∣ = p^{b} m^{'}$ with $p ∤ m^{'}$ , step 2.1 gives $b \geq a$ , while $p^{b} ∣ p^{a} m$ with $p ∤ m$ gives $b \leq a$ . Hence $∣ H ∣ = p^{a} m^{'}$ with $p ∤ m^{'}$ , and the induction hypothesis applied to $H$ supplies a subgroup of $H$ of order $p^{a}$ , which is a subgroup of $G$ .

step 2.1L5L6givenalgebra

4.1

Steps 3.1 and 3.2 are exhaustive, so $G$ has a subgroup $P$ of order $p^{a}$ , and $∣ P ∣$ is the largest power of $p$ dividing $∣ G ∣$ , so $P$ is a Sylow $p$ -subgroup by [L1]. At $a = 0$ the argument returns the trivial subgroup, of order $p^{0} = 1$ ; for the trivial group $∣ G ∣ = 1$ this is $G$ itself, and $m = 1$ is the case settled in step 3.1.

L1step 3.1step 3.2given∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 111 results over 25 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Amin Idelhaj, The Sylow Theorems and Their Applications, Section 3, Lemma 3.6 and the proof of Sylow's first theorem (standard reference, not scraped)
Keith Conrad, The Sylow Theorems, Section 2, Proof of Sylow I (standard reference, not scraped)

Sylow I: every finite group has a Sylow pp-subgroup