let n be non zero Nat; :: thesis: 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) ) ) )
let z be Element of (Dihedral_group n); :: thesis: ( 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) ) ) )
thus ( z in center (Dihedral_group n) implies 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) ) ) ) by GROUP_5:77; :: thesis: ( ( 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) ) ) ) implies z in center (Dihedral_group n) )
assume A1: 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) ) ) ; :: thesis: z in center (Dihedral_group n)
for g being Element of (Dihedral_group n) holds z * g = g * z

proof

let g be Element of (Dihedral_group n); :: thesis: z * g = g * z

per cases ( n = 1 or n > 1 ) by NAT_1:53;

suppose n = 1 ; :: thesis: z * g = g * z

then Dihedral_group n is commutative by ThD1Commutative;
hence z * g = g * z ; :: thesis: verum

end;

suppose n > 1 ; :: thesis: z * g = g * z

then 1 in Segm n by NAT_1:44;
then 1 in the carrier of (INT.Group n) by Th76;
then reconsider g1 = 1 as Element of (INT.Group n) ;
1 in INT.Group 2 by EltsOfINTGroup2;
then reconsider a2 = 1 as Element of (INT.Group 2) ;
reconsider x = <*g1,(1_ (INT.Group 2))*>, y = <*(1_ (INT.Group n)),a2*> as Element of (Dihedral_group n) by Th9;
consider k being Nat such that
B1: ( g = (x |^ k) * y or g = x |^ k ) by Th107;

per cases ( g = (x |^ k) * y or g = x |^ k ) by B1;

suppose B2: g = (x |^ k) * y ; :: thesis: z * g = g * z

hence z * g = (z * (x |^ k)) * y by GROUP_1:def 3
.= ((x |^ k) * z) * y by A1
.= (x |^ k) * (z * y) by GROUP_1:def 3
.= (x |^ k) * (y * z) by A1
.= ((x |^ k) * y) * z by GROUP_1:def 3
.= g * z by B2 ;
:: thesis: verum

end;

suppose B3: g = x |^ k ; :: thesis: z * g = g * z

( g1 = 1 & a2 = 1 & x = <*g1,(1_ (INT.Group 2))*> & y = <*(1_ (INT.Group n)),a2*> ) ;
then B4: for i being Nat holds (x |^ i) * z = z * (x |^ i) by A1;
thus z * g = z * (x |^ k) by B3
.= (x |^ k) * z by B4
.= g * z by B3 ; :: thesis: verum

end;

end;

end;

end;

end;

hence z in center (Dihedral_group n) by GROUP_5:77; :: thesis: verum