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 ⊢ 𝑋 = ( Base ‘ 𝐺 )
gexcl2.2 ⊢ 𝐸 = ( gEx ‘ 𝐺 )
Assertion gexcl2 ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) → 𝐸 ∈ ℕ )

Proof

Step Hyp Ref Expression
1 gexcl2.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 gexcl2.2 ⊢ 𝐸 = ( gEx ‘ 𝐺 )
3 eqid ⊢ ( od ‘ 𝐺 ) = ( od ‘ 𝐺 )
4 1 3 odcl2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑥 ∈ 𝑋 ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℕ )
5 1 3 oddvds2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑥 ∈ 𝑋 ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( ♯ ‘ 𝑋 ) )
6 4 nnzd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑥 ∈ 𝑋 ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℤ )
7 1 grpbn0 ⊢ ( 𝐺 ∈ Grp → 𝑋 ≠ ∅ )
8 7 3ad2ant1 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑥 ∈ 𝑋 ) → 𝑋 ≠ ∅ )
9 hashnncl ⊢ ( 𝑋 ∈ Fin → ( ( ♯ ‘ 𝑋 ) ∈ ℕ ↔ 𝑋 ≠ ∅ ) )
10 9 3ad2ant2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑥 ∈ 𝑋 ) → ( ( ♯ ‘ 𝑋 ) ∈ ℕ ↔ 𝑋 ≠ ∅ ) )
11 8 10 mpbird ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑥 ∈ 𝑋 ) → ( ♯ ‘ 𝑋 ) ∈ ℕ )
12 dvdsle ⊢ ( ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℤ ∧ ( ♯ ‘ 𝑋 ) ∈ ℕ ) → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( ♯ ‘ 𝑋 ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ≤ ( ♯ ‘ 𝑋 ) ) )
13 6 11 12 syl2anc ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑥 ∈ 𝑋 ) → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( ♯ ‘ 𝑋 ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ≤ ( ♯ ‘ 𝑋 ) ) )
14 5 13 mpd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑥 ∈ 𝑋 ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ≤ ( ♯ ‘ 𝑋 ) )
15 11 nnzd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑥 ∈ 𝑋 ) → ( ♯ ‘ 𝑋 ) ∈ ℤ )
16 fznn ⊢ ( ( ♯ ‘ 𝑋 ) ∈ ℤ → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( 1 ... ( ♯ ‘ 𝑋 ) ) ↔ ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℕ ∧ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ≤ ( ♯ ‘ 𝑋 ) ) ) )
17 15 16 syl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑥 ∈ 𝑋 ) → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( 1 ... ( ♯ ‘ 𝑋 ) ) ↔ ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℕ ∧ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ≤ ( ♯ ‘ 𝑋 ) ) ) )
18 4 14 17 mpbir2and ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑥 ∈ 𝑋 ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( 1 ... ( ♯ ‘ 𝑋 ) ) )
19 18 3expa ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ 𝑥 ∈ 𝑋 ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( 1 ... ( ♯ ‘ 𝑋 ) ) )
20 19 ralrimiva ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) → ∀ 𝑥 ∈ 𝑋 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( 1 ... ( ♯ ‘ 𝑋 ) ) )
21 1 2 3 gexcl3 ⊢ ( ( 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( 1 ... ( ♯ ‘ 𝑋 ) ) ) → 𝐸 ∈ ℕ )
22 20 21 syldan ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) → 𝐸 ∈ ℕ )