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 ⊢ X = Base G
gexod.2 ⊢ E = gEx ⁡ G
gexod.3 ⊢ O = od ⁡ G
Assertion gexnnod ⊢ G ∈ Grp ∧ E ∈ ℕ ∧ A ∈ X → O ⁡ A ∈ ℕ

Proof

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