Theorem cyggex

Description: The exponent of a finite cyclic group is the order of the group. (Contributed by Mario Carneiro, 24-Apr-2016)

	Ref	Expression
Hypotheses	cygctb.1	|- B = ( Base ` G )
	cyggex.o	|- E = ( gEx ` G )
Assertion	cyggex	|- ( ( G e. CycGrp /\ B e. Fin ) -> E = ( # ` B ) )

Proof

Step	Hyp	Ref	Expression
1		cygctb.1	|- B = ( Base ` G )
2		cyggex.o	|- E = ( gEx ` G )
3	1 2	cyggex2	|- ( G e. CycGrp -> E = if ( B e. Fin , ( # ` B ) , 0 ) )
4		iftrue	|- ( B e. Fin -> if ( B e. Fin , ( # ` B ) , 0 ) = ( # ` B ) )
5	3 4	sylan9eq	|- ( ( G e. CycGrp /\ B e. Fin ) -> E = ( # ` B ) )