Description: A cyclic group with n elements is isomorphic to ZZ / n ZZ , and an infinite cyclic group is isomorphic to ZZ / 0 ZZ ~ZZ . (Contributed by Mario Carneiro, 21-Apr-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cygzn.b | |
|
cygzn.n | |
||
cygzn.y | |
||
Assertion | cygzn | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cygzn.b | |
|
2 | cygzn.n | |
|
3 | cygzn.y | |
|
4 | eqid | |
|
5 | eqid | |
|
6 | 1 4 5 | iscyg2 | |
7 | 6 | simprbi | |
8 | n0 | |
|
9 | 7 8 | sylib | |
10 | eqid | |
|
11 | simpl | |
|
12 | simpr | |
|
13 | eqid | |
|
14 | 1 2 3 4 10 5 11 12 13 | cygznlem3 | |
15 | 9 14 | exlimddv | |