# Metamath Proof Explorer

## Theorem iscyg2

Description: A cyclic group is a group which contains a generator. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypotheses iscyg.1
`|- B = ( Base ` G )`
iscyg.2
`|- .x. = ( .g ` G )`
iscyg3.e
`|- E = { x e. B | ran ( n e. ZZ |-> ( n .x. x ) ) = B }`
Assertion iscyg2
`|- ( G e. CycGrp <-> ( G e. Grp /\ E =/= (/) ) )`

### Proof

Step Hyp Ref Expression
1 iscyg.1
` |-  B = ( Base ` G )`
2 iscyg.2
` |-  .x. = ( .g ` G )`
3 iscyg3.e
` |-  E = { x e. B | ran ( n e. ZZ |-> ( n .x. x ) ) = B }`
4 1 2 iscyg
` |-  ( G e. CycGrp <-> ( G e. Grp /\ E. x e. B ran ( n e. ZZ |-> ( n .x. x ) ) = B ) )`
5 3 neeq1i
` |-  ( E =/= (/) <-> { x e. B | ran ( n e. ZZ |-> ( n .x. x ) ) = B } =/= (/) )`
6 rabn0
` |-  ( { x e. B | ran ( n e. ZZ |-> ( n .x. x ) ) = B } =/= (/) <-> E. x e. B ran ( n e. ZZ |-> ( n .x. x ) ) = B )`
7 5 6 bitri
` |-  ( E =/= (/) <-> E. x e. B ran ( n e. ZZ |-> ( n .x. x ) ) = B )`
8 7 anbi2i
` |-  ( ( G e. Grp /\ E =/= (/) ) <-> ( G e. Grp /\ E. x e. B ran ( n e. ZZ |-> ( n .x. x ) ) = B ) )`
9 4 8 bitr4i
` |-  ( G e. CycGrp <-> ( G e. Grp /\ E =/= (/) ) )`