Theorem iscygodd

Description: Show that a group with an element the same order as the group is cyclic. (Contributed by Mario Carneiro, 27-Apr-2016)

	Ref	Expression
Hypotheses	iscygodd.1	|- B = ( Base ` G )
	iscygodd.o	|- O = ( od ` G )
	iscygodd.3	|- ( ph -> G e. Grp )
	iscygodd.4	|- ( ph -> X e. B )
	iscygodd.5	|- ( ph -> ( O ` X ) = ( # ` B ) )
Assertion	iscygodd	|- ( ph -> G e. CycGrp )

Proof

Step	Hyp	Ref	Expression
1		iscygodd.1	|- B = ( Base ` G )
2		iscygodd.o	|- O = ( od ` G )
3		iscygodd.3	|- ( ph -> G e. Grp )
4		iscygodd.4	|- ( ph -> X e. B )
5		iscygodd.5	|- ( ph -> ( O ` X ) = ( # ` B ) )
6	1 2	odcl	|- ( X e. B -> ( O ` X ) e. NN0 )
7	4 6	syl	|- ( ph -> ( O ` X ) e. NN0 )
8	5 7	eqeltrrd	|- ( ph -> ( # ` B ) e. NN0 )
9	1	fvexi	|- B e. _V
10		hashclb	|- ( B e. _V -> ( B e. Fin <-> ( # ` B ) e. NN0 ) )
11	9 10	ax-mp	|- ( B e. Fin <-> ( # ` B ) e. NN0 )
12	8 11	sylibr	|- ( ph -> B e. Fin )
13		eqid	|- ( .g ` G ) = ( .g ` G )
14		eqid	|- { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } = { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B }
15	1 13 14 2	cyggenod	|- ( ( G e. Grp /\ B e. Fin ) -> ( X e. { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } <-> ( X e. B /\ ( O ` X ) = ( # ` B ) ) ) )
16	3 12 15	syl2anc	|- ( ph -> ( X e. { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } <-> ( X e. B /\ ( O ` X ) = ( # ` B ) ) ) )
17	4 5 16	mpbir2and	|- ( ph -> X e. { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } )
18	17	ne0d	|- ( ph -> { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } =/= (/) )
19	1 13 14	iscyg2	|- ( G e. CycGrp <-> ( G e. Grp /\ { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } =/= (/) ) )
20	3 18 19	sylanbrc	|- ( ph -> G e. CycGrp )