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

Metamath Proof Explorer

Theorem odmulg2

Description: The order of a multiple divides the order of the base point. (Contributed by Stefan O'Rear, 6-Sep-2015)

Ref Expression
Hypotheses odmulgid.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
odmulgid.2 ⊢ 𝑂 = ( od ‘ 𝐺 )
odmulgid.3 ⊢ · = ( .g ‘ 𝐺 )
Assertion odmulg2 ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ∥ ( 𝑂 ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 odmulgid.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 odmulgid.2 ⊢ 𝑂 = ( od ‘ 𝐺 )
3 odmulgid.3 ⊢ · = ( .g ‘ 𝐺 )
4 1 2 odcl ⊢ ( 𝐴 ∈ 𝑋 → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
5 4 nn0zd ⊢ ( 𝐴 ∈ 𝑋 → ( 𝑂 ‘ 𝐴 ) ∈ ℤ )
6 5 3ad2ant2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → ( 𝑂 ‘ 𝐴 ) ∈ ℤ )
7 simp3 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℤ )
8 dvdsmul1 ⊢ ( ( ( 𝑂 ‘ 𝐴 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑂 ‘ 𝐴 ) ∥ ( ( 𝑂 ‘ 𝐴 ) · 𝑁 ) )
9 6 7 8 syl2anc ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → ( 𝑂 ‘ 𝐴 ) ∥ ( ( 𝑂 ‘ 𝐴 ) · 𝑁 ) )
10 1 2 3 odmulgid ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℤ ) → ( ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ∥ ( 𝑂 ‘ 𝐴 ) ↔ ( 𝑂 ‘ 𝐴 ) ∥ ( ( 𝑂 ‘ 𝐴 ) · 𝑁 ) ) )
11 6 10 mpdan ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → ( ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ∥ ( 𝑂 ‘ 𝐴 ) ↔ ( 𝑂 ‘ 𝐴 ) ∥ ( ( 𝑂 ‘ 𝐴 ) · 𝑁 ) ) )
12 9 11 mpbird ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ∥ ( 𝑂 ‘ 𝐴 ) )