Metamath Proof Explorer

Theorem gexnnod

Description: Every group element has finite order if the exponent is finite. (Contributed by Mario Carneiro, 24-Apr-2016)

Ref Expression
Hypotheses gexod.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
gexod.2 ⊢ 𝐸 = ( gEx ‘ 𝐺 )
gexod.3 ⊢ 𝑂 = ( od ‘ 𝐺 )
Assertion gexnnod ( ( 𝐺 ∈ Grp ∧ 𝐸 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ )

Proof

Step Hyp Ref Expression
1 gexod.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 gexod.2 ⊢ 𝐸 = ( gEx ‘ 𝐺 )
3 gexod.3 ⊢ 𝑂 = ( od ‘ 𝐺 )
4 nnne0 ⊢ ( 𝐸 ∈ ℕ → 𝐸 ≠ 0 )
5 4 3ad2ant2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐸 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → 𝐸 ≠ 0 )
6 nnz ⊢ ( 𝐸 ∈ ℕ → 𝐸 ∈ ℤ )
7 6 3ad2ant2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐸 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → 𝐸 ∈ ℤ )
8 0dvds ⊢ ( 𝐸 ∈ ℤ → ( 0 ∥ 𝐸 ↔ 𝐸 = 0 ) )
9 7 8 syl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐸 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( 0 ∥ 𝐸 ↔ 𝐸 = 0 ) )
10 9 necon3bbid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐸 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ¬ 0 ∥ 𝐸 ↔ 𝐸 ≠ 0 ) )
11 5 10 mpbird ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐸 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ¬ 0 ∥ 𝐸 )
12 1 2 3 gexod ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ 𝐴 ) ∥ 𝐸 )
13 12 3adant2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐸 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ 𝐴 ) ∥ 𝐸 )
14 breq1 ⊢ ( ( 𝑂 ‘ 𝐴 ) = 0 → ( ( 𝑂 ‘ 𝐴 ) ∥ 𝐸 ↔ 0 ∥ 𝐸 ) )
15 13 14 syl5ibcom ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐸 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑂 ‘ 𝐴 ) = 0 → 0 ∥ 𝐸 ) )
16 11 15 mtod ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐸 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ¬ ( 𝑂 ‘ 𝐴 ) = 0 )
17 1 3 odcl ⊢ ( 𝐴 ∈ 𝑋 → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
18 17 3ad2ant3 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐸 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
19 elnn0 ⊢ ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 ↔ ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ ∨ ( 𝑂 ‘ 𝐴 ) = 0 ) )
20 18 19 sylib ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐸 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ ∨ ( 𝑂 ‘ 𝐴 ) = 0 ) )
21 20 ord ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐸 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( ¬ ( 𝑂 ‘ 𝐴 ) ∈ ℕ → ( 𝑂 ‘ 𝐴 ) = 0 ) )
22 16 21 mt3d ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐸 ∈ ℕ ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ )