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 ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ∥ ( 𝑂 ‘ 𝐴 ) )