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 =/= (/) ) )