let n be non zero even Nat; :: thesis: for k being Nat st n = 2 * k 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
x |^ k in center (Dihedral_group n)
let k be Nat; :: thesis: ( n = 2 * k 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
x |^ k in center (Dihedral_group n) )
assume A1: n = 2 * k ; :: 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
x |^ k in center (Dihedral_group n)
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
x |^ k in center (Dihedral_group n) )
assume A2: g1 = 1 ; :: thesis: for x being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> holds
x |^ k in center (Dihedral_group n)
let x be Element of (Dihedral_group n); :: thesis: ( x = <*g1,(1_ (INT.Group 2))*> implies x |^ k in center (Dihedral_group n) )
assume A3: x = <*g1,(1_ (INT.Group 2))*> ; :: thesis: x |^ k in center (Dihedral_group n)
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;
set z = x |^ k;
A4: y * (x |^ k) = (x |^ (n - k)) * y by A3, Th106
.= (x |^ ((2 * k) - k)) * y by A1
.= (x |^ k) * y ;
for i being Nat holds (x |^ i) * (x |^ k) = (x |^ k) * (x |^ i)

proof

let i be Nat; :: thesis: (x |^ i) * (x |^ k) = (x |^ k) * (x |^ i)
thus (x |^ i) * (x |^ k) = x |^ (i + k) by GROUP_1:33
.= (x |^ k) * (x |^ i) by GROUP_1:33
.= (x |^ k) * (x |^ i) ; :: thesis: verum

end;

hence x |^ k in center (Dihedral_group n) by A2, A3, A4, Th114; :: thesis: verum