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	|- .x. = ( .g ` G )
	odid.4	|- .0. = ( 0g ` G )
Assertion	oddvdsi	|- ( ( G e. Grp /\ A e. X /\ ( O ` A ) || N ) -> ( N .x. A ) = .0. )

Proof

Step	Hyp	Ref	Expression
1		odcl.1	|- X = ( Base ` G )
2		odcl.2	|- O = ( od ` G )
3		odid.3	|- .x. = ( .g ` G )
4		odid.4	|- .0. = ( 0g ` G )
5		simp3	|- ( ( G e. Grp /\ A e. X /\ ( O ` A ) || N ) -> ( O ` A ) || N )
6		dvdszrcl	|- ( ( O ` A ) || N -> ( ( O ` A ) e. ZZ /\ N e. ZZ ) )
7	6	simprd	|- ( ( O ` A ) || N -> N e. ZZ )
8	1 2 3 4	oddvds	|- ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> ( ( O ` A ) || N <-> ( N .x. A ) = .0. ) )
9	7 8	syl3an3	|- ( ( G e. Grp /\ A e. X /\ ( O ` A ) || N ) -> ( ( O ` A ) || N <-> ( N .x. A ) = .0. ) )
10	5 9	mpbid	|- ( ( G e. Grp /\ A e. X /\ ( O ` A ) || N ) -> ( N .x. A ) = .0. )