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 )