Metamath Proof Explorer

Theorem gexcl2

Description: The exponent of a finite group is finite. (Contributed by Mario Carneiro, 24-Apr-2016)

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

Proof

Step Hyp Ref Expression
1 gexcl2.1 ⊢X=BaseG
2 gexcl2.2 ⊢E=gEx⁡G
3 eqid ⊢od⁡G=od⁡G
4 1 3 odcl2 ⊢G∈Grp∧X∈Fin∧x∈X→od⁡G⁡x∈ℕ
5 1 3 oddvds2 ⊢G∈Grp∧X∈Fin∧x∈X→od⁡G⁡x∥X
6 4 nnzd ⊢G∈Grp∧X∈Fin∧x∈X→od⁡G⁡x∈ℤ
7 1 grpbn0 ⊢G∈Grp→X≠∅
8 7 3ad2ant1 ⊢G∈Grp∧X∈Fin∧x∈X→X≠∅
9 hashnncl ⊢X∈Fin→X∈ℕ↔X≠∅
10 9 3ad2ant2 ⊢G∈Grp∧X∈Fin∧x∈X→X∈ℕ↔X≠∅
11 8 10 mpbird ⊢G∈Grp∧X∈Fin∧x∈X→X∈ℕ
12 dvdsle ⊢od⁡G⁡x∈ℤ∧X∈ℕ→od⁡G⁡x∥X→od⁡G⁡x≤X
13 6 11 12 syl2anc ⊢G∈Grp∧X∈Fin∧x∈X→od⁡G⁡x∥X→od⁡G⁡x≤X
14 5 13 mpd ⊢G∈Grp∧X∈Fin∧x∈X→od⁡G⁡x≤X
15 11 nnzd ⊢G∈Grp∧X∈Fin∧x∈X→X∈ℤ
16 fznn ⊢X∈ℤ→od⁡G⁡x∈1…X↔od⁡G⁡x∈ℕ∧od⁡G⁡x≤X
17 15 16 syl ⊢G∈Grp∧X∈Fin∧x∈X→od⁡G⁡x∈1…X↔od⁡G⁡x∈ℕ∧od⁡G⁡x≤X
18 4 14 17 mpbir2and ⊢G∈Grp∧X∈Fin∧x∈X→od⁡G⁡x∈1…X
19 18 3expa ⊢G∈Grp∧X∈Fin∧x∈X→od⁡G⁡x∈1…X
20 19 ralrimiva ⊢G∈Grp∧X∈Fin→∀x∈Xod⁡G⁡x∈1…X
21 1 2 3 gexcl3 ⊢G∈Grp∧∀x∈Xod⁡G⁡x∈1…X→E∈ℕ
22 20 21 syldan ⊢G∈Grp∧X∈Fin→E∈ℕ