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	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
Assertion	odmulg2	$⊢ (G \in Grp \land A \in X \land N \in ℤ) \to O (N \underset{˙}{\cdot} A) ∥ O (A)$

Step	Hyp	Ref	Expression
1		odmulgid.1	$⊢ X = {Base}_{G}$
2		odmulgid.2	$⊢ O = od (G)$
3		odmulgid.3	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
4	1 2	odcl	$⊢ A \in X \to O (A) \in ℕ_{0}$
5	4	nn0zd	$⊢ A \in X \to O (A) \in ℤ$
6	5	3ad2ant2	$⊢ (G \in Grp \land A \in X \land N \in ℤ) \to O (A) \in ℤ$
7		simp3	$⊢ (G \in Grp \land A \in X \land N \in ℤ) \to N \in ℤ$
8		dvdsmul1	$⊢ (O (A) \in ℤ \land N \in ℤ) \to O (A) ∥ O (A) \cdot N$
9	6 7 8	syl2anc	$⊢ (G \in Grp \land A \in X \land N \in ℤ) \to O (A) ∥ O (A) \cdot N$
10	1 2 3	odmulgid	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℤ) \to (O (N \underset{˙}{\cdot} A) ∥ O (A) \leftrightarrow O (A) ∥ O (A) \cdot N)$
11	6 10	mpdan	$⊢ (G \in Grp \land A \in X \land N \in ℤ) \to (O (N \underset{˙}{\cdot} A) ∥ O (A) \leftrightarrow O (A) ∥ O (A) \cdot N)$
12	9 11	mpbird	$⊢ (G \in Grp \land A \in X \land N \in ℤ) \to O (N \underset{˙}{\cdot} A) ∥ O (A)$

Metamath Proof Explorer