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 = Base G
gexcl2.2 ⊢ E = gEx ⁡ G
Assertion gexcl2 ⊢ G ∈ Grp ∧ X ∈ Fin → E ∈ ℕ

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 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 ∈ X od ⁡ G ⁡ x ∈ 1 … X
21 1 2 3 gexcl3 ⊢ G ∈ Grp ∧ ∀ x ∈ X od ⁡ G ⁡ x ∈ 1 … X → E ∈ ℕ
22 20 21 syldan ⊢ G ∈ Grp ∧ X ∈ Fin → E ∈ ℕ