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={\mathrm{Base}}_G$$
	cyggex.o	$$⊢E=\mathrm{gEx}\left(G\right)$$
Assertion	cyggex	$$⊢\left(G\in \mathrm{CycGrp}\wedge B\in \mathrm{Fin}\right)\to E=\left|B\right|$$

Proof

Step	Hyp	Ref	Expression
1		cygctb.1	$$⊢B={\mathrm{Base}}_G$$
2		cyggex.o	$$⊢E=\mathrm{gEx}\left(G\right)$$
3	1 2	cyggex2	$$⊢G\in \mathrm{CycGrp}\to E=if\left(B\in \mathrm{Fin},\left|B\right|,0\right)$$
4		iftrue	$$⊢B\in \mathrm{Fin}\to if\left(B\in \mathrm{Fin},\left|B\right|,0\right)=\left|B\right|$$
5	3 4	sylan9eq	$$⊢\left(G\in \mathrm{CycGrp}\wedge B\in \mathrm{Fin}\right)\to E=\left|B\right|$$