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 ⊢ 𝑋 = ( Base ‘ 𝐺 )
gexod.2 ⊢ 𝐸 = ( gEx ‘ 𝐺 )
gexod.3 ⊢ 𝑂 = ( od ‘ 𝐺 )
Assertion gexod ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ 𝐴 ) ∥ 𝐸 )

Proof

Step Hyp Ref Expression
1 gexod.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 gexod.2 ⊢ 𝐸 = ( gEx ‘ 𝐺 )
3 gexod.3 ⊢ 𝑂 = ( od ‘ 𝐺 )
4 eqid ⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
5 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
6 1 2 4 5 gexid ⊢ ( 𝐴 ∈ 𝑋 → ( 𝐸 ( .g ‘ 𝐺 ) 𝐴 ) = ( 0g ‘ 𝐺 ) )
7 6 adantl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐸 ( .g ‘ 𝐺 ) 𝐴 ) = ( 0g ‘ 𝐺 ) )
8 1 2 gexcl ⊢ ( 𝐺 ∈ Grp → 𝐸 ∈ ℕ0 )
9 8 adantr ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → 𝐸 ∈ ℕ0 )
10 9 nn0zd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → 𝐸 ∈ ℤ )
11 1 3 4 5 oddvds ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐸 ∈ ℤ ) → ( ( 𝑂 ‘ 𝐴 ) ∥ 𝐸 ↔ ( 𝐸 ( .g ‘ 𝐺 ) 𝐴 ) = ( 0g ‘ 𝐺 ) ) )
12 10 11 mpd3an3 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑂 ‘ 𝐴 ) ∥ 𝐸 ↔ ( 𝐸 ( .g ‘ 𝐺 ) 𝐴 ) = ( 0g ‘ 𝐺 ) ) )
13 7 12 mpbird ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ 𝐴 ) ∥ 𝐸 )