# Metamath Proof Explorer

## Theorem gexex

Description: In an abelian group with finite exponent, there is an element in the group with order equal to the exponent. In other words, all orders of elements divide the largest order of an element of the group. This fails if E = 0 , for example in an infinite p-group, where there are elements of arbitrarily large orders (so E is zero) but no elements of infinite order. (Contributed by Mario Carneiro, 24-Apr-2016)

Ref Expression
Hypotheses gexex.1 ${⊢}{X}={\mathrm{Base}}_{{G}}$
gexex.2 ${⊢}{E}=\mathrm{gEx}\left({G}\right)$
gexex.3 ${⊢}{O}=\mathrm{od}\left({G}\right)$
Assertion gexex ${⊢}\left({G}\in \mathrm{Abel}\wedge {E}\in ℕ\right)\to \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{O}\left({x}\right)={E}$

### Proof

Step Hyp Ref Expression
1 gexex.1 ${⊢}{X}={\mathrm{Base}}_{{G}}$
2 gexex.2 ${⊢}{E}=\mathrm{gEx}\left({G}\right)$
3 gexex.3 ${⊢}{O}=\mathrm{od}\left({G}\right)$
4 simpll ${⊢}\left(\left({G}\in \mathrm{Abel}\wedge {E}\in ℕ\right)\wedge \left({x}\in {X}\wedge {O}\left({x}\right)=sup\left(\mathrm{ran}{O},ℝ,<\right)\right)\right)\to {G}\in \mathrm{Abel}$
5 simplr ${⊢}\left(\left({G}\in \mathrm{Abel}\wedge {E}\in ℕ\right)\wedge \left({x}\in {X}\wedge {O}\left({x}\right)=sup\left(\mathrm{ran}{O},ℝ,<\right)\right)\right)\to {E}\in ℕ$
6 simprl ${⊢}\left(\left({G}\in \mathrm{Abel}\wedge {E}\in ℕ\right)\wedge \left({x}\in {X}\wedge {O}\left({x}\right)=sup\left(\mathrm{ran}{O},ℝ,<\right)\right)\right)\to {x}\in {X}$
7 1 3 odf ${⊢}{O}:{X}⟶{ℕ}_{0}$
8 frn ${⊢}{O}:{X}⟶{ℕ}_{0}\to \mathrm{ran}{O}\subseteq {ℕ}_{0}$
9 7 8 ax-mp ${⊢}\mathrm{ran}{O}\subseteq {ℕ}_{0}$
10 nn0ssz ${⊢}{ℕ}_{0}\subseteq ℤ$
11 9 10 sstri ${⊢}\mathrm{ran}{O}\subseteq ℤ$
12 nnz ${⊢}{E}\in ℕ\to {E}\in ℤ$
13 12 adantl ${⊢}\left({G}\in \mathrm{Abel}\wedge {E}\in ℕ\right)\to {E}\in ℤ$
14 ablgrp ${⊢}{G}\in \mathrm{Abel}\to {G}\in \mathrm{Grp}$
15 14 adantr ${⊢}\left({G}\in \mathrm{Abel}\wedge {E}\in ℕ\right)\to {G}\in \mathrm{Grp}$
16 1 2 3 gexod ${⊢}\left({G}\in \mathrm{Grp}\wedge {x}\in {X}\right)\to {O}\left({x}\right)\parallel {E}$
17 15 16 sylan ${⊢}\left(\left({G}\in \mathrm{Abel}\wedge {E}\in ℕ\right)\wedge {x}\in {X}\right)\to {O}\left({x}\right)\parallel {E}$
18 1 3 odcl ${⊢}{x}\in {X}\to {O}\left({x}\right)\in {ℕ}_{0}$
19 18 adantl ${⊢}\left(\left({G}\in \mathrm{Abel}\wedge {E}\in ℕ\right)\wedge {x}\in {X}\right)\to {O}\left({x}\right)\in {ℕ}_{0}$
20 19 nn0zd ${⊢}\left(\left({G}\in \mathrm{Abel}\wedge {E}\in ℕ\right)\wedge {x}\in {X}\right)\to {O}\left({x}\right)\in ℤ$
21 simplr ${⊢}\left(\left({G}\in \mathrm{Abel}\wedge {E}\in ℕ\right)\wedge {x}\in {X}\right)\to {E}\in ℕ$
22 dvdsle ${⊢}\left({O}\left({x}\right)\in ℤ\wedge {E}\in ℕ\right)\to \left({O}\left({x}\right)\parallel {E}\to {O}\left({x}\right)\le {E}\right)$
23 20 21 22 syl2anc ${⊢}\left(\left({G}\in \mathrm{Abel}\wedge {E}\in ℕ\right)\wedge {x}\in {X}\right)\to \left({O}\left({x}\right)\parallel {E}\to {O}\left({x}\right)\le {E}\right)$
24 17 23 mpd ${⊢}\left(\left({G}\in \mathrm{Abel}\wedge {E}\in ℕ\right)\wedge {x}\in {X}\right)\to {O}\left({x}\right)\le {E}$
25 24 ralrimiva ${⊢}\left({G}\in \mathrm{Abel}\wedge {E}\in ℕ\right)\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{O}\left({x}\right)\le {E}$
26 ffn ${⊢}{O}:{X}⟶{ℕ}_{0}\to {O}Fn{X}$
27 7 26 ax-mp ${⊢}{O}Fn{X}$
28 breq1 ${⊢}{y}={O}\left({x}\right)\to \left({y}\le {E}↔{O}\left({x}\right)\le {E}\right)$
29 28 ralrn ${⊢}{O}Fn{X}\to \left(\forall {y}\in \mathrm{ran}{O}\phantom{\rule{.4em}{0ex}}{y}\le {E}↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{O}\left({x}\right)\le {E}\right)$
30 27 29 ax-mp ${⊢}\forall {y}\in \mathrm{ran}{O}\phantom{\rule{.4em}{0ex}}{y}\le {E}↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{O}\left({x}\right)\le {E}$
31 25 30 sylibr ${⊢}\left({G}\in \mathrm{Abel}\wedge {E}\in ℕ\right)\to \forall {y}\in \mathrm{ran}{O}\phantom{\rule{.4em}{0ex}}{y}\le {E}$
32 brralrspcev ${⊢}\left({E}\in ℤ\wedge \forall {y}\in \mathrm{ran}{O}\phantom{\rule{.4em}{0ex}}{y}\le {E}\right)\to \exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{O}\phantom{\rule{.4em}{0ex}}{y}\le {n}$
33 13 31 32 syl2anc ${⊢}\left({G}\in \mathrm{Abel}\wedge {E}\in ℕ\right)\to \exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{O}\phantom{\rule{.4em}{0ex}}{y}\le {n}$
34 33 ad2antrr ${⊢}\left(\left(\left({G}\in \mathrm{Abel}\wedge {E}\in ℕ\right)\wedge \left({x}\in {X}\wedge {O}\left({x}\right)=sup\left(\mathrm{ran}{O},ℝ,<\right)\right)\right)\wedge {y}\in {X}\right)\to \exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{O}\phantom{\rule{.4em}{0ex}}{y}\le {n}$
35 27 a1i ${⊢}\left(\left({G}\in \mathrm{Abel}\wedge {E}\in ℕ\right)\wedge \left({x}\in {X}\wedge {O}\left({x}\right)=sup\left(\mathrm{ran}{O},ℝ,<\right)\right)\right)\to {O}Fn{X}$
36 fnfvelrn ${⊢}\left({O}Fn{X}\wedge {y}\in {X}\right)\to {O}\left({y}\right)\in \mathrm{ran}{O}$
37 35 36 sylan ${⊢}\left(\left(\left({G}\in \mathrm{Abel}\wedge {E}\in ℕ\right)\wedge \left({x}\in {X}\wedge {O}\left({x}\right)=sup\left(\mathrm{ran}{O},ℝ,<\right)\right)\right)\wedge {y}\in {X}\right)\to {O}\left({y}\right)\in \mathrm{ran}{O}$
38 suprzub ${⊢}\left(\mathrm{ran}{O}\subseteq ℤ\wedge \exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{O}\phantom{\rule{.4em}{0ex}}{y}\le {n}\wedge {O}\left({y}\right)\in \mathrm{ran}{O}\right)\to {O}\left({y}\right)\le sup\left(\mathrm{ran}{O},ℝ,<\right)$
39 11 34 37 38 mp3an2i ${⊢}\left(\left(\left({G}\in \mathrm{Abel}\wedge {E}\in ℕ\right)\wedge \left({x}\in {X}\wedge {O}\left({x}\right)=sup\left(\mathrm{ran}{O},ℝ,<\right)\right)\right)\wedge {y}\in {X}\right)\to {O}\left({y}\right)\le sup\left(\mathrm{ran}{O},ℝ,<\right)$
40 simplrr ${⊢}\left(\left(\left({G}\in \mathrm{Abel}\wedge {E}\in ℕ\right)\wedge \left({x}\in {X}\wedge {O}\left({x}\right)=sup\left(\mathrm{ran}{O},ℝ,<\right)\right)\right)\wedge {y}\in {X}\right)\to {O}\left({x}\right)=sup\left(\mathrm{ran}{O},ℝ,<\right)$
41 39 40 breqtrrd ${⊢}\left(\left(\left({G}\in \mathrm{Abel}\wedge {E}\in ℕ\right)\wedge \left({x}\in {X}\wedge {O}\left({x}\right)=sup\left(\mathrm{ran}{O},ℝ,<\right)\right)\right)\wedge {y}\in {X}\right)\to {O}\left({y}\right)\le {O}\left({x}\right)$
42 1 2 3 4 5 6 41 gexexlem ${⊢}\left(\left({G}\in \mathrm{Abel}\wedge {E}\in ℕ\right)\wedge \left({x}\in {X}\wedge {O}\left({x}\right)=sup\left(\mathrm{ran}{O},ℝ,<\right)\right)\right)\to {O}\left({x}\right)={E}$
43 1 grpbn0 ${⊢}{G}\in \mathrm{Grp}\to {X}\ne \varnothing$
44 15 43 syl ${⊢}\left({G}\in \mathrm{Abel}\wedge {E}\in ℕ\right)\to {X}\ne \varnothing$
45 7 fdmi ${⊢}\mathrm{dom}{O}={X}$
46 45 eqeq1i ${⊢}\mathrm{dom}{O}=\varnothing ↔{X}=\varnothing$
47 dm0rn0 ${⊢}\mathrm{dom}{O}=\varnothing ↔\mathrm{ran}{O}=\varnothing$
48 46 47 bitr3i ${⊢}{X}=\varnothing ↔\mathrm{ran}{O}=\varnothing$
49 48 necon3bii ${⊢}{X}\ne \varnothing ↔\mathrm{ran}{O}\ne \varnothing$
50 44 49 sylib ${⊢}\left({G}\in \mathrm{Abel}\wedge {E}\in ℕ\right)\to \mathrm{ran}{O}\ne \varnothing$
51 suprzcl2 ${⊢}\left(\mathrm{ran}{O}\subseteq ℤ\wedge \mathrm{ran}{O}\ne \varnothing \wedge \exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{O}\phantom{\rule{.4em}{0ex}}{y}\le {n}\right)\to sup\left(\mathrm{ran}{O},ℝ,<\right)\in \mathrm{ran}{O}$
52 11 50 33 51 mp3an2i ${⊢}\left({G}\in \mathrm{Abel}\wedge {E}\in ℕ\right)\to sup\left(\mathrm{ran}{O},ℝ,<\right)\in \mathrm{ran}{O}$
53 fvelrnb ${⊢}{O}Fn{X}\to \left(sup\left(\mathrm{ran}{O},ℝ,<\right)\in \mathrm{ran}{O}↔\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{O}\left({x}\right)=sup\left(\mathrm{ran}{O},ℝ,<\right)\right)$
54 27 53 ax-mp ${⊢}sup\left(\mathrm{ran}{O},ℝ,<\right)\in \mathrm{ran}{O}↔\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{O}\left({x}\right)=sup\left(\mathrm{ran}{O},ℝ,<\right)$
55 52 54 sylib ${⊢}\left({G}\in \mathrm{Abel}\wedge {E}\in ℕ\right)\to \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{O}\left({x}\right)=sup\left(\mathrm{ran}{O},ℝ,<\right)$
56 42 55 reximddv ${⊢}\left({G}\in \mathrm{Abel}\wedge {E}\in ℕ\right)\to \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{O}\left({x}\right)={E}$