Metamath Proof Explorer

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 CycGrp B Fin E = B


Step Hyp Ref Expression
1 cygctb.1 B = Base G
2 cyggex.o E = gEx G
3 1 2 cyggex2 G CycGrp E = if B Fin B 0
4 iftrue B Fin if B Fin B 0 = B
5 3 4 sylan9eq G CycGrp B Fin E = B