# 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 𝑋 = ( Base ‘ 𝐺 )
gexex.2 𝐸 = ( gEx ‘ 𝐺 )
gexex.3 𝑂 = ( od ‘ 𝐺 )
Assertion gexex ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) → ∃ 𝑥𝑋 ( 𝑂𝑥 ) = 𝐸 )

### Proof

Step Hyp Ref Expression
1 gexex.1 𝑋 = ( Base ‘ 𝐺 )
2 gexex.2 𝐸 = ( gEx ‘ 𝐺 )
3 gexex.3 𝑂 = ( od ‘ 𝐺 )
4 simpll ( ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) ∧ ( 𝑥𝑋 ∧ ( 𝑂𝑥 ) = sup ( ran 𝑂 , ℝ , < ) ) ) → 𝐺 ∈ Abel )
5 simplr ( ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) ∧ ( 𝑥𝑋 ∧ ( 𝑂𝑥 ) = sup ( ran 𝑂 , ℝ , < ) ) ) → 𝐸 ∈ ℕ )
6 simprl ( ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) ∧ ( 𝑥𝑋 ∧ ( 𝑂𝑥 ) = sup ( ran 𝑂 , ℝ , < ) ) ) → 𝑥𝑋 )
7 1 3 odf 𝑂 : 𝑋 ⟶ ℕ0
8 frn ( 𝑂 : 𝑋 ⟶ ℕ0 → ran 𝑂 ⊆ ℕ0 )
9 7 8 ax-mp ran 𝑂 ⊆ ℕ0
10 nn0ssz 0 ⊆ ℤ
11 9 10 sstri ran 𝑂 ⊆ ℤ
12 nnz ( 𝐸 ∈ ℕ → 𝐸 ∈ ℤ )
13 12 adantl ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) → 𝐸 ∈ ℤ )
14 ablgrp ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
15 14 adantr ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) → 𝐺 ∈ Grp )
16 1 2 3 gexod ( ( 𝐺 ∈ Grp ∧ 𝑥𝑋 ) → ( 𝑂𝑥 ) ∥ 𝐸 )
17 15 16 sylan ( ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) ∧ 𝑥𝑋 ) → ( 𝑂𝑥 ) ∥ 𝐸 )
18 1 3 odcl ( 𝑥𝑋 → ( 𝑂𝑥 ) ∈ ℕ0 )
19 18 adantl ( ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) ∧ 𝑥𝑋 ) → ( 𝑂𝑥 ) ∈ ℕ0 )
20 19 nn0zd ( ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) ∧ 𝑥𝑋 ) → ( 𝑂𝑥 ) ∈ ℤ )
21 simplr ( ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) ∧ 𝑥𝑋 ) → 𝐸 ∈ ℕ )
22 dvdsle ( ( ( 𝑂𝑥 ) ∈ ℤ ∧ 𝐸 ∈ ℕ ) → ( ( 𝑂𝑥 ) ∥ 𝐸 → ( 𝑂𝑥 ) ≤ 𝐸 ) )
23 20 21 22 syl2anc ( ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) ∧ 𝑥𝑋 ) → ( ( 𝑂𝑥 ) ∥ 𝐸 → ( 𝑂𝑥 ) ≤ 𝐸 ) )
24 17 23 mpd ( ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) ∧ 𝑥𝑋 ) → ( 𝑂𝑥 ) ≤ 𝐸 )
25 24 ralrimiva ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) → ∀ 𝑥𝑋 ( 𝑂𝑥 ) ≤ 𝐸 )
26 ffn ( 𝑂 : 𝑋 ⟶ ℕ0𝑂 Fn 𝑋 )
27 7 26 ax-mp 𝑂 Fn 𝑋
28 breq1 ( 𝑦 = ( 𝑂𝑥 ) → ( 𝑦𝐸 ↔ ( 𝑂𝑥 ) ≤ 𝐸 ) )
29 28 ralrn ( 𝑂 Fn 𝑋 → ( ∀ 𝑦 ∈ ran 𝑂 𝑦𝐸 ↔ ∀ 𝑥𝑋 ( 𝑂𝑥 ) ≤ 𝐸 ) )
30 27 29 ax-mp ( ∀ 𝑦 ∈ ran 𝑂 𝑦𝐸 ↔ ∀ 𝑥𝑋 ( 𝑂𝑥 ) ≤ 𝐸 )
31 25 30 sylibr ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) → ∀ 𝑦 ∈ ran 𝑂 𝑦𝐸 )
32 brralrspcev ( ( 𝐸 ∈ ℤ ∧ ∀ 𝑦 ∈ ran 𝑂 𝑦𝐸 ) → ∃ 𝑛 ∈ ℤ ∀ 𝑦 ∈ ran 𝑂 𝑦𝑛 )
33 13 31 32 syl2anc ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) → ∃ 𝑛 ∈ ℤ ∀ 𝑦 ∈ ran 𝑂 𝑦𝑛 )
34 33 ad2antrr ( ( ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) ∧ ( 𝑥𝑋 ∧ ( 𝑂𝑥 ) = sup ( ran 𝑂 , ℝ , < ) ) ) ∧ 𝑦𝑋 ) → ∃ 𝑛 ∈ ℤ ∀ 𝑦 ∈ ran 𝑂 𝑦𝑛 )
35 27 a1i ( ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) ∧ ( 𝑥𝑋 ∧ ( 𝑂𝑥 ) = sup ( ran 𝑂 , ℝ , < ) ) ) → 𝑂 Fn 𝑋 )
36 fnfvelrn ( ( 𝑂 Fn 𝑋𝑦𝑋 ) → ( 𝑂𝑦 ) ∈ ran 𝑂 )
37 35 36 sylan ( ( ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) ∧ ( 𝑥𝑋 ∧ ( 𝑂𝑥 ) = sup ( ran 𝑂 , ℝ , < ) ) ) ∧ 𝑦𝑋 ) → ( 𝑂𝑦 ) ∈ ran 𝑂 )
38 suprzub ( ( ran 𝑂 ⊆ ℤ ∧ ∃ 𝑛 ∈ ℤ ∀ 𝑦 ∈ ran 𝑂 𝑦𝑛 ∧ ( 𝑂𝑦 ) ∈ ran 𝑂 ) → ( 𝑂𝑦 ) ≤ sup ( ran 𝑂 , ℝ , < ) )
39 11 34 37 38 mp3an2i ( ( ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) ∧ ( 𝑥𝑋 ∧ ( 𝑂𝑥 ) = sup ( ran 𝑂 , ℝ , < ) ) ) ∧ 𝑦𝑋 ) → ( 𝑂𝑦 ) ≤ sup ( ran 𝑂 , ℝ , < ) )
40 simplrr ( ( ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) ∧ ( 𝑥𝑋 ∧ ( 𝑂𝑥 ) = sup ( ran 𝑂 , ℝ , < ) ) ) ∧ 𝑦𝑋 ) → ( 𝑂𝑥 ) = sup ( ran 𝑂 , ℝ , < ) )
41 39 40 breqtrrd ( ( ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) ∧ ( 𝑥𝑋 ∧ ( 𝑂𝑥 ) = sup ( ran 𝑂 , ℝ , < ) ) ) ∧ 𝑦𝑋 ) → ( 𝑂𝑦 ) ≤ ( 𝑂𝑥 ) )
42 1 2 3 4 5 6 41 gexexlem ( ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) ∧ ( 𝑥𝑋 ∧ ( 𝑂𝑥 ) = sup ( ran 𝑂 , ℝ , < ) ) ) → ( 𝑂𝑥 ) = 𝐸 )
43 1 grpbn0 ( 𝐺 ∈ Grp → 𝑋 ≠ ∅ )
44 15 43 syl ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) → 𝑋 ≠ ∅ )
45 7 fdmi dom 𝑂 = 𝑋
46 45 eqeq1i ( dom 𝑂 = ∅ ↔ 𝑋 = ∅ )
47 dm0rn0 ( dom 𝑂 = ∅ ↔ ran 𝑂 = ∅ )
48 46 47 bitr3i ( 𝑋 = ∅ ↔ ran 𝑂 = ∅ )
49 48 necon3bii ( 𝑋 ≠ ∅ ↔ ran 𝑂 ≠ ∅ )
50 44 49 sylib ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) → ran 𝑂 ≠ ∅ )
51 suprzcl2 ( ( ran 𝑂 ⊆ ℤ ∧ ran 𝑂 ≠ ∅ ∧ ∃ 𝑛 ∈ ℤ ∀ 𝑦 ∈ ran 𝑂 𝑦𝑛 ) → sup ( ran 𝑂 , ℝ , < ) ∈ ran 𝑂 )
52 11 50 33 51 mp3an2i ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) → sup ( ran 𝑂 , ℝ , < ) ∈ ran 𝑂 )
53 fvelrnb ( 𝑂 Fn 𝑋 → ( sup ( ran 𝑂 , ℝ , < ) ∈ ran 𝑂 ↔ ∃ 𝑥𝑋 ( 𝑂𝑥 ) = sup ( ran 𝑂 , ℝ , < ) ) )
54 27 53 ax-mp ( sup ( ran 𝑂 , ℝ , < ) ∈ ran 𝑂 ↔ ∃ 𝑥𝑋 ( 𝑂𝑥 ) = sup ( ran 𝑂 , ℝ , < ) )
55 52 54 sylib ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) → ∃ 𝑥𝑋 ( 𝑂𝑥 ) = sup ( ran 𝑂 , ℝ , < ) )
56 42 55 reximddv ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) → ∃ 𝑥𝑋 ( 𝑂𝑥 ) = 𝐸 )
{"found_math": false, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 0, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "url": "http://metamath.tirix.org/mpeuni/gexex", "fetch_time": 1721766750000000000, "content_mime_type": "text/html", "warc_filename": "crawl-data/CC-MAIN-2024-30/segments/1720763518115.82/warc/CC-MAIN-20240723194208-20240723224208-00021.warc.gz", "warc_record_offset": 20370085, "warc_record_length": 3961, "token_count": 2556, "char_count": 4021, "score": 3.78125, "int_score": 4, "crawl": "CC-MAIN-2024-30", "snapshot_type": "latest", "language": "en", "language_score": 0.6330750584602356, "file_path": "/sailhome/yjruan/project/latent-lm/data/processed/finemath-4plus/finemath-4plus/train-00030-of-00064.parquet"}