# 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}={\mathrm{Base}}_{{G}}$
gexcl2.2 ${⊢}{E}=\mathrm{gEx}\left({G}\right)$
Assertion gexcl2 ${⊢}\left({G}\in \mathrm{Grp}\wedge {X}\in \mathrm{Fin}\right)\to {E}\in ℕ$

### Proof

Step Hyp Ref Expression
1 gexcl2.1 ${⊢}{X}={\mathrm{Base}}_{{G}}$
2 gexcl2.2 ${⊢}{E}=\mathrm{gEx}\left({G}\right)$
3 eqid ${⊢}\mathrm{od}\left({G}\right)=\mathrm{od}\left({G}\right)$
4 1 3 odcl2 ${⊢}\left({G}\in \mathrm{Grp}\wedge {X}\in \mathrm{Fin}\wedge {x}\in {X}\right)\to \mathrm{od}\left({G}\right)\left({x}\right)\in ℕ$
5 1 3 oddvds2 ${⊢}\left({G}\in \mathrm{Grp}\wedge {X}\in \mathrm{Fin}\wedge {x}\in {X}\right)\to \mathrm{od}\left({G}\right)\left({x}\right)\parallel \left|{X}\right|$
6 4 nnzd ${⊢}\left({G}\in \mathrm{Grp}\wedge {X}\in \mathrm{Fin}\wedge {x}\in {X}\right)\to \mathrm{od}\left({G}\right)\left({x}\right)\in ℤ$
7 1 grpbn0 ${⊢}{G}\in \mathrm{Grp}\to {X}\ne \varnothing$
8 7 3ad2ant1 ${⊢}\left({G}\in \mathrm{Grp}\wedge {X}\in \mathrm{Fin}\wedge {x}\in {X}\right)\to {X}\ne \varnothing$
9 hashnncl ${⊢}{X}\in \mathrm{Fin}\to \left(\left|{X}\right|\in ℕ↔{X}\ne \varnothing \right)$
10 9 3ad2ant2 ${⊢}\left({G}\in \mathrm{Grp}\wedge {X}\in \mathrm{Fin}\wedge {x}\in {X}\right)\to \left(\left|{X}\right|\in ℕ↔{X}\ne \varnothing \right)$
11 8 10 mpbird ${⊢}\left({G}\in \mathrm{Grp}\wedge {X}\in \mathrm{Fin}\wedge {x}\in {X}\right)\to \left|{X}\right|\in ℕ$
12 dvdsle ${⊢}\left(\mathrm{od}\left({G}\right)\left({x}\right)\in ℤ\wedge \left|{X}\right|\in ℕ\right)\to \left(\mathrm{od}\left({G}\right)\left({x}\right)\parallel \left|{X}\right|\to \mathrm{od}\left({G}\right)\left({x}\right)\le \left|{X}\right|\right)$
13 6 11 12 syl2anc ${⊢}\left({G}\in \mathrm{Grp}\wedge {X}\in \mathrm{Fin}\wedge {x}\in {X}\right)\to \left(\mathrm{od}\left({G}\right)\left({x}\right)\parallel \left|{X}\right|\to \mathrm{od}\left({G}\right)\left({x}\right)\le \left|{X}\right|\right)$
14 5 13 mpd ${⊢}\left({G}\in \mathrm{Grp}\wedge {X}\in \mathrm{Fin}\wedge {x}\in {X}\right)\to \mathrm{od}\left({G}\right)\left({x}\right)\le \left|{X}\right|$
15 11 nnzd ${⊢}\left({G}\in \mathrm{Grp}\wedge {X}\in \mathrm{Fin}\wedge {x}\in {X}\right)\to \left|{X}\right|\in ℤ$
16 fznn ${⊢}\left|{X}\right|\in ℤ\to \left(\mathrm{od}\left({G}\right)\left({x}\right)\in \left(1\dots \left|{X}\right|\right)↔\left(\mathrm{od}\left({G}\right)\left({x}\right)\in ℕ\wedge \mathrm{od}\left({G}\right)\left({x}\right)\le \left|{X}\right|\right)\right)$
17 15 16 syl ${⊢}\left({G}\in \mathrm{Grp}\wedge {X}\in \mathrm{Fin}\wedge {x}\in {X}\right)\to \left(\mathrm{od}\left({G}\right)\left({x}\right)\in \left(1\dots \left|{X}\right|\right)↔\left(\mathrm{od}\left({G}\right)\left({x}\right)\in ℕ\wedge \mathrm{od}\left({G}\right)\left({x}\right)\le \left|{X}\right|\right)\right)$
18 4 14 17 mpbir2and ${⊢}\left({G}\in \mathrm{Grp}\wedge {X}\in \mathrm{Fin}\wedge {x}\in {X}\right)\to \mathrm{od}\left({G}\right)\left({x}\right)\in \left(1\dots \left|{X}\right|\right)$
19 18 3expa ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge {X}\in \mathrm{Fin}\right)\wedge {x}\in {X}\right)\to \mathrm{od}\left({G}\right)\left({x}\right)\in \left(1\dots \left|{X}\right|\right)$
20 19 ralrimiva ${⊢}\left({G}\in \mathrm{Grp}\wedge {X}\in \mathrm{Fin}\right)\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\mathrm{od}\left({G}\right)\left({x}\right)\in \left(1\dots \left|{X}\right|\right)$
21 1 2 3 gexcl3 ${⊢}\left({G}\in \mathrm{Grp}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\mathrm{od}\left({G}\right)\left({x}\right)\in \left(1\dots \left|{X}\right|\right)\right)\to {E}\in ℕ$
22 20 21 syldan ${⊢}\left({G}\in \mathrm{Grp}\wedge {X}\in \mathrm{Fin}\right)\to {E}\in ℕ$