Metamath Proof Explorer


Theorem gexcl3

Description: If the order of every group element is bounded by N , the group has finite exponent. (Contributed by Mario Carneiro, 24-Apr-2016)

Ref Expression
Hypotheses gexod.1 𝑋 = ( Base ‘ 𝐺 )
gexod.2 𝐸 = ( gEx ‘ 𝐺 )
gexod.3 𝑂 = ( od ‘ 𝐺 )
Assertion gexcl3 ( ( 𝐺 ∈ Grp ∧ ∀ 𝑥𝑋 ( 𝑂𝑥 ) ∈ ( 1 ... 𝑁 ) ) → 𝐸 ∈ ℕ )

Proof

Step Hyp Ref Expression
1 gexod.1 𝑋 = ( Base ‘ 𝐺 )
2 gexod.2 𝐸 = ( gEx ‘ 𝐺 )
3 gexod.3 𝑂 = ( od ‘ 𝐺 )
4 simpl ( ( 𝐺 ∈ Grp ∧ ∀ 𝑥𝑋 ( 𝑂𝑥 ) ∈ ( 1 ... 𝑁 ) ) → 𝐺 ∈ Grp )
5 1 grpbn0 ( 𝐺 ∈ Grp → 𝑋 ≠ ∅ )
6 r19.2z ( ( 𝑋 ≠ ∅ ∧ ∀ 𝑥𝑋 ( 𝑂𝑥 ) ∈ ( 1 ... 𝑁 ) ) → ∃ 𝑥𝑋 ( 𝑂𝑥 ) ∈ ( 1 ... 𝑁 ) )
7 5 6 sylan ( ( 𝐺 ∈ Grp ∧ ∀ 𝑥𝑋 ( 𝑂𝑥 ) ∈ ( 1 ... 𝑁 ) ) → ∃ 𝑥𝑋 ( 𝑂𝑥 ) ∈ ( 1 ... 𝑁 ) )
8 elfzuz2 ( ( 𝑂𝑥 ) ∈ ( 1 ... 𝑁 ) → 𝑁 ∈ ( ℤ ‘ 1 ) )
9 nnuz ℕ = ( ℤ ‘ 1 )
10 8 9 eleqtrrdi ( ( 𝑂𝑥 ) ∈ ( 1 ... 𝑁 ) → 𝑁 ∈ ℕ )
11 10 rexlimivw ( ∃ 𝑥𝑋 ( 𝑂𝑥 ) ∈ ( 1 ... 𝑁 ) → 𝑁 ∈ ℕ )
12 7 11 syl ( ( 𝐺 ∈ Grp ∧ ∀ 𝑥𝑋 ( 𝑂𝑥 ) ∈ ( 1 ... 𝑁 ) ) → 𝑁 ∈ ℕ )
13 12 nnnn0d ( ( 𝐺 ∈ Grp ∧ ∀ 𝑥𝑋 ( 𝑂𝑥 ) ∈ ( 1 ... 𝑁 ) ) → 𝑁 ∈ ℕ0 )
14 13 faccld ( ( 𝐺 ∈ Grp ∧ ∀ 𝑥𝑋 ( 𝑂𝑥 ) ∈ ( 1 ... 𝑁 ) ) → ( ! ‘ 𝑁 ) ∈ ℕ )
15 elfzuzb ( ( 𝑂𝑥 ) ∈ ( 1 ... 𝑁 ) ↔ ( ( 𝑂𝑥 ) ∈ ( ℤ ‘ 1 ) ∧ 𝑁 ∈ ( ℤ ‘ ( 𝑂𝑥 ) ) ) )
16 elnnuz ( ( 𝑂𝑥 ) ∈ ℕ ↔ ( 𝑂𝑥 ) ∈ ( ℤ ‘ 1 ) )
17 dvdsfac ( ( ( 𝑂𝑥 ) ∈ ℕ ∧ 𝑁 ∈ ( ℤ ‘ ( 𝑂𝑥 ) ) ) → ( 𝑂𝑥 ) ∥ ( ! ‘ 𝑁 ) )
18 16 17 sylanbr ( ( ( 𝑂𝑥 ) ∈ ( ℤ ‘ 1 ) ∧ 𝑁 ∈ ( ℤ ‘ ( 𝑂𝑥 ) ) ) → ( 𝑂𝑥 ) ∥ ( ! ‘ 𝑁 ) )
19 15 18 sylbi ( ( 𝑂𝑥 ) ∈ ( 1 ... 𝑁 ) → ( 𝑂𝑥 ) ∥ ( ! ‘ 𝑁 ) )
20 19 adantl ( ( ( 𝐺 ∈ Grp ∧ 𝑥𝑋 ) ∧ ( 𝑂𝑥 ) ∈ ( 1 ... 𝑁 ) ) → ( 𝑂𝑥 ) ∥ ( ! ‘ 𝑁 ) )
21 simpll ( ( ( 𝐺 ∈ Grp ∧ 𝑥𝑋 ) ∧ ( 𝑂𝑥 ) ∈ ( 1 ... 𝑁 ) ) → 𝐺 ∈ Grp )
22 simplr ( ( ( 𝐺 ∈ Grp ∧ 𝑥𝑋 ) ∧ ( 𝑂𝑥 ) ∈ ( 1 ... 𝑁 ) ) → 𝑥𝑋 )
23 10 adantl ( ( ( 𝐺 ∈ Grp ∧ 𝑥𝑋 ) ∧ ( 𝑂𝑥 ) ∈ ( 1 ... 𝑁 ) ) → 𝑁 ∈ ℕ )
24 23 nnnn0d ( ( ( 𝐺 ∈ Grp ∧ 𝑥𝑋 ) ∧ ( 𝑂𝑥 ) ∈ ( 1 ... 𝑁 ) ) → 𝑁 ∈ ℕ0 )
25 24 faccld ( ( ( 𝐺 ∈ Grp ∧ 𝑥𝑋 ) ∧ ( 𝑂𝑥 ) ∈ ( 1 ... 𝑁 ) ) → ( ! ‘ 𝑁 ) ∈ ℕ )
26 25 nnzd ( ( ( 𝐺 ∈ Grp ∧ 𝑥𝑋 ) ∧ ( 𝑂𝑥 ) ∈ ( 1 ... 𝑁 ) ) → ( ! ‘ 𝑁 ) ∈ ℤ )
27 eqid ( .g𝐺 ) = ( .g𝐺 )
28 eqid ( 0g𝐺 ) = ( 0g𝐺 )
29 1 3 27 28 oddvds ( ( 𝐺 ∈ Grp ∧ 𝑥𝑋 ∧ ( ! ‘ 𝑁 ) ∈ ℤ ) → ( ( 𝑂𝑥 ) ∥ ( ! ‘ 𝑁 ) ↔ ( ( ! ‘ 𝑁 ) ( .g𝐺 ) 𝑥 ) = ( 0g𝐺 ) ) )
30 21 22 26 29 syl3anc ( ( ( 𝐺 ∈ Grp ∧ 𝑥𝑋 ) ∧ ( 𝑂𝑥 ) ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑂𝑥 ) ∥ ( ! ‘ 𝑁 ) ↔ ( ( ! ‘ 𝑁 ) ( .g𝐺 ) 𝑥 ) = ( 0g𝐺 ) ) )
31 20 30 mpbid ( ( ( 𝐺 ∈ Grp ∧ 𝑥𝑋 ) ∧ ( 𝑂𝑥 ) ∈ ( 1 ... 𝑁 ) ) → ( ( ! ‘ 𝑁 ) ( .g𝐺 ) 𝑥 ) = ( 0g𝐺 ) )
32 31 ex ( ( 𝐺 ∈ Grp ∧ 𝑥𝑋 ) → ( ( 𝑂𝑥 ) ∈ ( 1 ... 𝑁 ) → ( ( ! ‘ 𝑁 ) ( .g𝐺 ) 𝑥 ) = ( 0g𝐺 ) ) )
33 32 ralimdva ( 𝐺 ∈ Grp → ( ∀ 𝑥𝑋 ( 𝑂𝑥 ) ∈ ( 1 ... 𝑁 ) → ∀ 𝑥𝑋 ( ( ! ‘ 𝑁 ) ( .g𝐺 ) 𝑥 ) = ( 0g𝐺 ) ) )
34 33 imp ( ( 𝐺 ∈ Grp ∧ ∀ 𝑥𝑋 ( 𝑂𝑥 ) ∈ ( 1 ... 𝑁 ) ) → ∀ 𝑥𝑋 ( ( ! ‘ 𝑁 ) ( .g𝐺 ) 𝑥 ) = ( 0g𝐺 ) )
35 1 2 27 28 gexlem2 ( ( 𝐺 ∈ Grp ∧ ( ! ‘ 𝑁 ) ∈ ℕ ∧ ∀ 𝑥𝑋 ( ( ! ‘ 𝑁 ) ( .g𝐺 ) 𝑥 ) = ( 0g𝐺 ) ) → 𝐸 ∈ ( 1 ... ( ! ‘ 𝑁 ) ) )
36 4 14 34 35 syl3anc ( ( 𝐺 ∈ Grp ∧ ∀ 𝑥𝑋 ( 𝑂𝑥 ) ∈ ( 1 ... 𝑁 ) ) → 𝐸 ∈ ( 1 ... ( ! ‘ 𝑁 ) ) )
37 elfznn ( 𝐸 ∈ ( 1 ... ( ! ‘ 𝑁 ) ) → 𝐸 ∈ ℕ )
38 36 37 syl ( ( 𝐺 ∈ Grp ∧ ∀ 𝑥𝑋 ( 𝑂𝑥 ) ∈ ( 1 ... 𝑁 ) ) → 𝐸 ∈ ℕ )