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 | |
|
cyggex.o | |
||
Assertion | cyggex2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cygctb.1 | |
|
2 | cyggex.o | |
|
3 | eqid | |
|
4 | eqid | |
|
5 | 1 3 4 | iscyg2 | |
6 | n0 | |
|
7 | ssrab2 | |
|
8 | simpr | |
|
9 | 7 8 | sselid | |
10 | eqid | |
|
11 | 1 3 4 10 | cyggenod2 | |
12 | 9 11 | jca | |
13 | 12 | ex | |
14 | 1 2 | gexcl | |
15 | 14 | adantr | |
16 | hashcl | |
|
17 | 16 | adantl | |
18 | 0nn0 | |
|
19 | 18 | a1i | |
20 | 17 19 | ifclda | |
21 | breq2 | |
|
22 | breq2 | |
|
23 | 1 2 | gexdvds3 | |
24 | 23 | adantlr | |
25 | 15 | adantr | |
26 | nn0z | |
|
27 | dvds0 | |
|
28 | 25 26 27 | 3syl | |
29 | 21 22 24 28 | ifbothda | |
30 | simprr | |
|
31 | 1 2 10 | gexod | |
32 | 31 | adantrr | |
33 | 30 32 | eqbrtrrd | |
34 | dvdseq | |
|
35 | 15 20 29 33 34 | syl22anc | |
36 | 35 | ex | |
37 | 13 36 | syld | |
38 | 37 | exlimdv | |
39 | 6 38 | syl5bi | |
40 | 39 | imp | |
41 | 5 40 | sylbi | |