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

Proof

Step	Hyp	Ref	Expression
1		odmulgid.1	|- X = ( Base ` G )
2		odmulgid.2	|- O = ( od ` G )
3		odmulgid.3	|- .x. = ( .g ` G )
4	1 2	odcl	|- ( A e. X -> ( O ` A ) e. NN0 )
5	4	nn0zd	|- ( A e. X -> ( O ` A ) e. ZZ )
6	5	3ad2ant2	|- ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> ( O ` A ) e. ZZ )
7		simp3	|- ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> N e. ZZ )
8		dvdsmul1	|- ( ( ( O ` A ) e. ZZ /\ N e. ZZ ) -> ( O ` A ) || ( ( O ` A ) x. N ) )
9	6 7 8	syl2anc	|- ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> ( O ` A ) || ( ( O ` A ) x. N ) )
10	1 2 3	odmulgid	|- ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. ZZ ) -> ( ( O ` ( N .x. A ) ) || ( O ` A ) <-> ( O ` A ) || ( ( O ` A ) x. N ) ) )
11	6 10	mpdan	|- ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> ( ( O ` ( N .x. A ) ) || ( O ` A ) <-> ( O ` A ) || ( ( O ` A ) x. N ) ) )
12	9 11	mpbird	|- ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> ( O ` ( N .x. A ) ) || ( O ` A ) )