theorem :: GROUP_24:110

for n being non zero Nat
for z being Element of (Dihedral_group n) holds
( z in center (Dihedral_group n) iff for g1 being Element of (INT.Group n) st g1 = 1 holds
for a2 being Element of (INT.Group 2) st a2 = 1 holds
for x, y being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> & y = <*(1_ (INT.Group n)),a2*> holds
( y * z = z * y & ( for i being Nat holds (x |^ i) * z = z * (x |^ i) ) ) )