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 ⊢ X = Base G
odmulgid.2 ⊢ O = od ⁡ G
odmulgid.3 ⊢ · ˙ = ⋅ G
Assertion odmulg2 ⊢ G ∈ Grp ∧ A ∈ X ∧ N ∈ ℤ → O ⁡ N · ˙ A ∥ O ⁡ A

Proof

Step Hyp Ref Expression
1 odmulgid.1 ⊢ X = Base G
2 odmulgid.2 ⊢ O = od ⁡ G
3 odmulgid.3 ⊢ · ˙ = ⋅ G
4 1 2 odcl ⊢ A ∈ X → O ⁡ A ∈ ℕ 0
5 4 nn0zd ⊢ A ∈ X → O ⁡ A ∈ ℤ
6 5 3ad2ant2 ⊢ G ∈ Grp ∧ A ∈ X ∧ N ∈ ℤ → O ⁡ A ∈ ℤ
7 simp3 ⊢ G ∈ Grp ∧ A ∈ X ∧ N ∈ ℤ → N ∈ ℤ
8 dvdsmul1 ⊢ O ⁡ A ∈ ℤ ∧ N ∈ ℤ → O ⁡ A ∥ O ⁡ A ⋅ N
9 6 7 8 syl2anc ⊢ G ∈ Grp ∧ A ∈ X ∧ N ∈ ℤ → O ⁡ A ∥ O ⁡ A ⋅ N
10 1 2 3 odmulgid ⊢ G ∈ Grp ∧ A ∈ X ∧ N ∈ ℤ ∧ O ⁡ A ∈ ℤ → O ⁡ N · ˙ A ∥ O ⁡ A ↔ O ⁡ A ∥ O ⁡ A ⋅ N
11 6 10 mpdan ⊢ G ∈ Grp ∧ A ∈ X ∧ N ∈ ℤ → O ⁡ N · ˙ A ∥ O ⁡ A ↔ O ⁡ A ∥ O ⁡ A ⋅ N
12 9 11 mpbird ⊢ G ∈ Grp ∧ A ∈ X ∧ N ∈ ℤ → O ⁡ N · ˙ A ∥ O ⁡ A