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 ... 𝑁 ) ) → 𝐸 ∈ ℕ )