Metamath Proof Explorer

Theorem gexdvds3

Description: The exponent of a finite group divides the order (cardinality) of the group. Corollary of Lagrange's theorem for the order of a subgroup. (Contributed by Mario Carneiro, 24-Apr-2016)

Ref Expression
Hypotheses gexcl2.1 ⊢ X = Base G
gexcl2.2 ⊢ E = gEx ⁡ G
Assertion gexdvds3 ⊢ G ∈ Grp ∧ X ∈ Fin → E ∥ X

Proof

Step Hyp Ref Expression
1 gexcl2.1 ⊢ X = Base G
2 gexcl2.2 ⊢ E = gEx ⁡ G
3 eqid ⊢ od ⁡ G = od ⁡ G
4 1 3 oddvds2 ⊢ G ∈ Grp ∧ X ∈ Fin ∧ x ∈ X → od ⁡ G ⁡ x ∥ X
5 4 3expa ⊢ G ∈ Grp ∧ X ∈ Fin ∧ x ∈ X → od ⁡ G ⁡ x ∥ X
6 5 ralrimiva ⊢ G ∈ Grp ∧ X ∈ Fin → ∀ x ∈ X od ⁡ G ⁡ x ∥ X
7 hashcl ⊢ X ∈ Fin → X ∈ ℕ 0
8 7 adantl ⊢ G ∈ Grp ∧ X ∈ Fin → X ∈ ℕ 0
9 8 nn0zd ⊢ G ∈ Grp ∧ X ∈ Fin → X ∈ ℤ
10 1 2 3 gexdvds2 ⊢ G ∈ Grp ∧ X ∈ ℤ → E ∥ X ↔ ∀ x ∈ X od ⁡ G ⁡ x ∥ X
11 9 10 syldan ⊢ G ∈ Grp ∧ X ∈ Fin → E ∥ X ↔ ∀ x ∈ X od ⁡ G ⁡ x ∥ X
12 6 11 mpbird ⊢ G ∈ Grp ∧ X ∈ Fin → E ∥ X