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

Metamath Proof Explorer

Theorem oddvdsi

Description: Any group element is annihilated by any multiple of its order. (Contributed by Stefan O'Rear, 5-Sep-2015) (Revised by Mario Carneiro, 23-Sep-2015)

Ref Expression
Hypotheses odcl.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
odcl.2 ⊢ 𝑂 = ( od ‘ 𝐺 )
odid.3 ⊢ · = ( .g ‘ 𝐺 )
odid.4 ⊢ 0 = ( 0g ‘ 𝐺 )
Assertion oddvdsi ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∥ 𝑁 ) → ( 𝑁 · 𝐴 ) = 0 )

Proof

Step Hyp Ref Expression
1 odcl.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 odcl.2 ⊢ 𝑂 = ( od ‘ 𝐺 )
3 odid.3 ⊢ · = ( .g ‘ 𝐺 )
4 odid.4 ⊢ 0 = ( 0g ‘ 𝐺 )
5 simp3 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∥ 𝑁 ) → ( 𝑂 ‘ 𝐴 ) ∥ 𝑁 )
6 dvdszrcl ⊢ ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑁 → ( ( 𝑂 ‘ 𝐴 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
7 6 simprd ⊢ ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑁 → 𝑁 ∈ ℤ )
8 1 2 3 4 oddvds ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑁 ↔ ( 𝑁 · 𝐴 ) = 0 ) )
9 7 8 syl3an3 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∥ 𝑁 ) → ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑁 ↔ ( 𝑁 · 𝐴 ) = 0 ) )
10 5 9 mpbid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∥ 𝑁 ) → ( 𝑁 · 𝐴 ) = 0 )