let n be non zero Nat; :: 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
for z being Element of (Dihedral_group n) ex k being Nat st
( z = (x |^ k) * y or z = x |^ k )
let g1 be Element of (INT.Group n); :: thesis: ( g1 = 1 implies 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
for z being Element of (Dihedral_group n) ex k being Nat st
( z = (x |^ k) * y or z = x |^ k ) )
assume A1: g1 = 1 ; :: thesis: 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
for z being Element of (Dihedral_group n) ex k being Nat st
( z = (x |^ k) * y or z = x |^ k )
let a2 be Element of (INT.Group 2); :: thesis: ( a2 = 1 implies for x, y being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> & y = <*(1_ (INT.Group n)),a2*> holds
for z being Element of (Dihedral_group n) ex k being Nat st
( z = (x |^ k) * y or z = x |^ k ) )
assume A2: a2 = 1 ; :: thesis: for x, y being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> & y = <*(1_ (INT.Group n)),a2*> holds
for z being Element of (Dihedral_group n) ex k being Nat st
( z = (x |^ k) * y or z = x |^ k )
let x, y be Element of (Dihedral_group n); :: thesis: ( x = <*g1,(1_ (INT.Group 2))*> & y = <*(1_ (INT.Group n)),a2*> implies for z being Element of (Dihedral_group n) ex k being Nat st
( z = (x |^ k) * y or z = x |^ k ) )
assume A3: x = <*g1,(1_ (INT.Group 2))*> ; :: thesis: ( not y = <*(1_ (INT.Group n)),a2*> or for z being Element of (Dihedral_group n) ex k being Nat st
( z = (x |^ k) * y or z = x |^ k ) )
assume A4: y = <*(1_ (INT.Group n)),a2*> ; :: thesis: for z being Element of (Dihedral_group n) ex k being Nat st
( z = (x |^ k) * y or z = x |^ k )
let z be Element of (Dihedral_group n); :: thesis: ex k being Nat st
( z = (x |^ k) * y or z = x |^ k )
consider g being Element of (INT.Group n), a being Element of (INT.Group 2) such that
A6: z = <*g,a*> by Th12;
consider k being Nat such that
A7: ( g = g1 |^ k & g = k mod n ) by A1, ThINTGroupOrd;
take k ; :: thesis: ( z = (x |^ k) * y or z = x |^ k )
assume A8: z <> (x |^ k) * y ; :: thesis: z = x |^ k
A9: x |^ k = <*(g1 |^ k),(1_ (INT.Group 2))*> by A3, Th25
.= <*g,(1_ (INT.Group 2))*> by A7 ;
a in INT.Group 2 ;
then ( a = 0 or a = 1 ) by EltsOfINTGroup2;

per cases then ( a = 0 or a = 1 ) ;

suppose A10: a = 0 ; :: thesis: z = x |^ k

x |^ k = <*g,(1_ (INT.Group 2))*> by A9
.= z by A6, A10, GR_CY_1:14 ;
hence z = x |^ k ; :: thesis: verum

end;

suppose a = 1 ; :: thesis: z = x |^ k

then a = a2 by A2;
then (x |^ k) * y = z by A4, A6, A9, Th16;
then contradiction by A8;
hence z = x |^ k ; :: thesis: verum

end;

end;