Metamath Proof Explorer


Theorem cyggex2

Description: The exponent of a cyclic group is 0 if the group is infinite, otherwise it equals the order of the group. (Contributed by Mario Carneiro, 24-Apr-2016)

Ref Expression
Hypotheses cygctb.1 B=BaseG
cyggex.o E=gExG
Assertion cyggex2 GCycGrpE=ifBFinB0

Proof

Step Hyp Ref Expression
1 cygctb.1 B=BaseG
2 cyggex.o E=gExG
3 eqid G=G
4 eqid xB|rannnGx=B=xB|rannnGx=B
5 1 3 4 iscyg2 GCycGrpGGrpxB|rannnGx=B
6 n0 xB|rannnGx=ByyxB|rannnGx=B
7 ssrab2 xB|rannnGx=BB
8 simpr GGrpyxB|rannnGx=ByxB|rannnGx=B
9 7 8 sselid GGrpyxB|rannnGx=ByB
10 eqid odG=odG
11 1 3 4 10 cyggenod2 GGrpyxB|rannnGx=BodGy=ifBFinB0
12 9 11 jca GGrpyxB|rannnGx=ByBodGy=ifBFinB0
13 12 ex GGrpyxB|rannnGx=ByBodGy=ifBFinB0
14 1 2 gexcl GGrpE0
15 14 adantr GGrpyBodGy=ifBFinB0E0
16 hashcl BFinB0
17 16 adantl GGrpyBodGy=ifBFinB0BFinB0
18 0nn0 00
19 18 a1i GGrpyBodGy=ifBFinB0¬BFin00
20 17 19 ifclda GGrpyBodGy=ifBFinB0ifBFinB00
21 breq2 B=ifBFinB0EBEifBFinB0
22 breq2 0=ifBFinB0E0EifBFinB0
23 1 2 gexdvds3 GGrpBFinEB
24 23 adantlr GGrpyBodGy=ifBFinB0BFinEB
25 15 adantr GGrpyBodGy=ifBFinB0¬BFinE0
26 nn0z E0E
27 dvds0 EE0
28 25 26 27 3syl GGrpyBodGy=ifBFinB0¬BFinE0
29 21 22 24 28 ifbothda GGrpyBodGy=ifBFinB0EifBFinB0
30 simprr GGrpyBodGy=ifBFinB0odGy=ifBFinB0
31 1 2 10 gexod GGrpyBodGyE
32 31 adantrr GGrpyBodGy=ifBFinB0odGyE
33 30 32 eqbrtrrd GGrpyBodGy=ifBFinB0ifBFinB0E
34 dvdseq E0ifBFinB00EifBFinB0ifBFinB0EE=ifBFinB0
35 15 20 29 33 34 syl22anc GGrpyBodGy=ifBFinB0E=ifBFinB0
36 35 ex GGrpyBodGy=ifBFinB0E=ifBFinB0
37 13 36 syld GGrpyxB|rannnGx=BE=ifBFinB0
38 37 exlimdv GGrpyyxB|rannnGx=BE=ifBFinB0
39 6 38 syl5bi GGrpxB|rannnGx=BE=ifBFinB0
40 39 imp GGrpxB|rannnGx=BE=ifBFinB0
41 5 40 sylbi GCycGrpE=ifBFinB0