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

Metamath Proof Explorer

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	$⊢ X = {Base}_{G}$
		odcl.2	$⊢ O = od (G)$
		odid.3	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
		odid.4	$⊢ \underset{˙}{0} = 0_{G}$
	Assertion	oddvdsi	$⊢ (G \in Grp \land A \in X \land O (A) ∥ N) \to N \underset{˙}{\cdot} A = \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		odcl.1	$⊢ X = {Base}_{G}$
2		odcl.2	$⊢ O = od (G)$
3		odid.3	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
4		odid.4	$⊢ \underset{˙}{0} = 0_{G}$
5		simp3	$⊢ (G \in Grp \land A \in X \land O (A) ∥ N) \to O (A) ∥ N$
6		dvdszrcl	$⊢ O (A) ∥ N \to (O (A) \in ℤ \land N \in ℤ)$
7	6	simprd	$⊢ O (A) ∥ N \to N \in ℤ$
8	1 2 3 4	oddvds	$⊢ (G \in Grp \land A \in X \land N \in ℤ) \to (O (A) ∥ N \leftrightarrow N \underset{˙}{\cdot} A = \underset{˙}{0})$
9	7 8	syl3an3	$⊢ (G \in Grp \land A \in X \land O (A) ∥ N) \to (O (A) ∥ N \leftrightarrow N \underset{˙}{\cdot} A = \underset{˙}{0})$
10	5 9	mpbid	$⊢ (G \in Grp \land A \in X \land O (A) ∥ N) \to N \underset{˙}{\cdot} A = \underset{˙}{0}$