let n be non zero even Nat; :: thesis: for k being Nat st n = 2 * k & n > 2 holds
for g1 being Element of (INT.Group n) st g1 = 1 holds
for x being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> holds
for g being Element of (Dihedral_group n) holds
( g in center (Dihedral_group n) iff ( g = 1_ (Dihedral_group n) or g = x |^ k ) )
let k be Nat; :: thesis: ( n = 2 * k & n > 2 implies for g1 being Element of (INT.Group n) st g1 = 1 holds
for x being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> holds
for g being Element of (Dihedral_group n) holds
( g in center (Dihedral_group n) iff ( g = 1_ (Dihedral_group n) or g = x |^ k ) ) )
assume A1: n = 2 * k ; :: thesis: ( not n > 2 or for g1 being Element of (INT.Group n) st g1 = 1 holds
for x being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> holds
for g being Element of (Dihedral_group n) holds
( g in center (Dihedral_group n) iff ( g = 1_ (Dihedral_group n) or g = x |^ k ) ) )
assume A2: n > 2 ; :: thesis: for g1 being Element of (INT.Group n) st g1 = 1 holds
for x being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> holds
for g being Element of (Dihedral_group n) holds
( g in center (Dihedral_group n) iff ( g = 1_ (Dihedral_group n) or g = x |^ k ) )
let g1 be Element of (INT.Group n); :: thesis: ( g1 = 1 implies for x being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> holds
for g being Element of (Dihedral_group n) holds
( g in center (Dihedral_group n) iff ( g = 1_ (Dihedral_group n) or g = x |^ k ) ) )
assume A3: g1 = 1 ; :: thesis: for x being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> holds
for g being Element of (Dihedral_group n) holds
( g in center (Dihedral_group n) iff ( g = 1_ (Dihedral_group n) or g = x |^ k ) )
let x be Element of (Dihedral_group n); :: thesis: ( x = <*g1,(1_ (INT.Group 2))*> implies for g being Element of (Dihedral_group n) holds
( g in center (Dihedral_group n) iff ( g = 1_ (Dihedral_group n) or g = x |^ k ) ) )
assume A4: x = <*g1,(1_ (INT.Group 2))*> ; :: thesis: for g being Element of (Dihedral_group n) holds
( g in center (Dihedral_group n) iff ( g = 1_ (Dihedral_group n) or g = x |^ k ) )
1 in INT.Group 2 by EltsOfINTGroup2;
then reconsider a2 = 1 as Element of (INT.Group 2) ;
reconsider y = <*(1_ (INT.Group n)),a2*> as Element of (Dihedral_group n) by Th9;
let g be Element of (Dihedral_group n); :: thesis: ( g in center (Dihedral_group n) iff ( g = 1_ (Dihedral_group n) or g = x |^ k ) )
thus ( not g in center (Dihedral_group n) or g = 1_ (Dihedral_group n) or g = x |^ k ) :: thesis: ( ( g = 1_ (Dihedral_group n) or g = x |^ k ) implies g in center (Dihedral_group n) )

proof

assume A5: g in center (Dihedral_group n) ; :: thesis: ( g = 1_ (Dihedral_group n) or g = x |^ k )
assume A6: not g = 1_ (Dihedral_group n) ; :: thesis: g = x |^ k
consider j being Nat such that
A7: j < n and
A8: ( g = (x |^ j) * y or g = x |^ j ) by A3, A4, Th108;

per cases ( g = (x |^ j) * y or g = x |^ j ) by A8;

suppose A9: g = (x |^ j) * y ; :: thesis: g = x |^ k

A10: x |^ 2 = 1_ (Dihedral_group n)

proof

B1: g * x = ((x |^ j) * y) * x by A9
.= ((x |^ j) * y) * (x |^ 1) by GROUP_1:26
.= (x |^ ((n + j) - 1)) * y by A4, Th109
.= (x |^ (j + (n - 1))) * y
.= ((x |^ j) * (x |^ (n - 1))) * y by GROUP_1:33 ;
B2: x * g = x * ((x |^ j) * y) by A9
.= (x |^ 1) * ((x |^ j) * y) by GROUP_1:26
.= ((x |^ 1) * (x |^ j)) * y by GROUP_1:def 3
.= (x |^ (1 + j)) * y by GROUP_1:33
.= ((x |^ j) * x) * y by GROUP_1:34 ;
x * g = g * x by A5, GROUP_5:77
.= ((x |^ j) * (x |^ (n - 1))) * y by B1 ;
then ((x |^ j) * x) * y = ((x |^ j) * (x |^ (n - 1))) * y by B2;
then (x |^ j) * x = (x |^ j) * (x |^ (n - 1)) by GROUP_1:6;
then x = x |^ (n - 1) by GROUP_1:6;
then x * x = x |^ ((n - 1) + 1) by GROUP_1:34
.= 1_ (Dihedral_group n) by A4, Th101 ;
hence x |^ 2 = 1_ (Dihedral_group n) by GROUP_1:27; :: thesis: verum

end;

x |^ 2 <> 1_ (Dihedral_group n) by A2, A3, A4, Th102;
then contradiction by A10;
hence g = x |^ k ; :: thesis: verum

end;

suppose A12: g = x |^ j ; :: thesis: g = x |^ k

A13: g |^ 2 = 1_ (Dihedral_group n)

proof

B1: y * g = y * (x |^ j) by A12
.= (x |^ (n - j)) * y by A4, Th106 ;
B2: g * y = (x |^ j) * y by A12;
y * g = g * y by A5, GROUP_5:77
.= (x |^ j) * y by B2 ;
then (x |^ (n - j)) * y = (x |^ j) * y by B1;
then x |^ j = x |^ (n - j) by GROUP_1:6
.= x |^ (n + (- j))
.= (x |^ n) * (x |^ (- j)) by GROUP_1:33
.= (1_ (Dihedral_group n)) * (x |^ (- j)) by A4, Th101
.= x |^ (- j) by GROUP_1:def 4 ;
then (x |^ j) * (x |^ j) = x |^ ((- j) + j) by GROUP_1:33
.= 1_ (Dihedral_group n) by GROUP_1:25 ;
hence 1_ (Dihedral_group n) = (x |^ j) |^ 2 by GROUP_1:27
.= g |^ 2 by A12 ;
:: thesis: verum

end;

g1 |^ (2 * j) = g1 |^ 0

proof

g |^ 2 = (x |^ j) |^ 2 by A12
.= x |^ (j * 2) by GROUP_1:35
.= <*(g1 |^ (2 * j)),(1_ (INT.Group 2))*> by A4, Th25 ;
then <*(g1 |^ (2 * j)),(1_ (INT.Group 2))*> = 1_ (Dihedral_group n) by A13
.= <*(1_ (INT.Group n)),(1_ (INT.Group 2))*> by Th17 ;
hence g1 |^ (2 * j) = 1_ (INT.Group n) by FINSEQ_1:77
.= g1 |^ 0 by GROUP_1:25 ;
:: thesis: verum

end;

then (2 * j) mod n = 0 mod n by A3, ThINTGroupOrd3
.= 0 by NAT_D:26 ;
then A14: 2 * j = (n * ((2 * j) div n)) + 0 by NAT_D:2;
( (2 * j) div n = 0 or (2 * j) div n = 1 ) by A7, Th121, NAT_1:23;

per cases then ( (2 * j) div n = 0 or (2 * j) div n = 1 ) ;

suppose (2 * j) div n = 0 ; :: thesis: g = x |^ k

then 2 * j = (n * 0) + 0 by A14
.= 0 ;
then A15: j = 0 ;
g = x |^ j by A12
.= x |^ 0 by A15
.= 1_ (Dihedral_group n) by GROUP_1:25 ;
then contradiction by A6;
hence g = x |^ k ; :: thesis: verum

end;

suppose (2 * j) div n = 1 ; :: thesis: g = x |^ k

then 2 * j = (n * 1) + 0 by A14
.= 2 * k by A1 ;
hence g = x |^ k by A12; :: thesis: verum

end;

end;

end;

end;

end;

assume ( g = 1_ (Dihedral_group n) or g = x |^ k ) ; :: thesis: g in center (Dihedral_group n)

per cases then ( g = 1_ (Dihedral_group n) or g = x |^ k ) ;

suppose g = 1_ (Dihedral_group n) ; :: thesis: g in center (Dihedral_group n)

hence g in center (Dihedral_group n) by GROUP_2:46; :: thesis: verum

end;

suppose g = x |^ k ; :: thesis: g in center (Dihedral_group n)

hence g in center (Dihedral_group n) by A1, A3, A4, Th120; :: thesis: verum

end;

end;