This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gexod

Description: Any group element is annihilated by any multiple of the group exponent. (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 gexod ⊢ G ∈ Grp ∧ A ∈ X → O ⁡ A ∥ E

Proof

Step Hyp Ref Expression
1 gexod.1 ⊢ X = Base G
2 gexod.2 ⊢ E = gEx ⁡ G
3 gexod.3 ⊢ O = od ⁡ G
4 eqid ⊢ ⋅ G = ⋅ G
5 eqid ⊢ 0 G = 0 G
6 1 2 4 5 gexid ⊢ A ∈ X → E ⋅ G A = 0 G
7 6 adantl ⊢ G ∈ Grp ∧ A ∈ X → E ⋅ G A = 0 G
8 1 2 gexcl ⊢ G ∈ Grp → E ∈ ℕ 0
9 8 adantr ⊢ G ∈ Grp ∧ A ∈ X → E ∈ ℕ 0
10 9 nn0zd ⊢ G ∈ Grp ∧ A ∈ X → E ∈ ℤ
11 1 3 4 5 oddvds ⊢ G ∈ Grp ∧ A ∈ X ∧ E ∈ ℤ → O ⁡ A ∥ E ↔ E ⋅ G A = 0 G
12 10 11 mpd3an3 ⊢ G ∈ Grp ∧ A ∈ X → O ⁡ A ∥ E ↔ E ⋅ G A = 0 G
13 7 12 mpbird ⊢ G ∈ Grp ∧ A ∈ X → O ⁡ A ∥ E