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
( k < n & ( 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
( k < n & ( 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
( k < n & ( 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
( k < n & ( 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
( k < n & ( 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
( k < n & ( 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
( k < n & ( 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
( k < n & ( z = (x |^ k) * y or z = x |^ k ) )
let z be Element of (Dihedral_group n); :: thesis: ex k being Nat st
( k < n & ( z = (x |^ k) * y or z = x |^ k ) )
consider k being Nat such that
A5: ( z = (x |^ k) * y or z = x |^ k ) by A1, A2, A3, A4, Th107;
reconsider k1 = k mod n as Nat ;
take k1 ; :: thesis: ( k1 < n & ( z = (x |^ k1) * y or z = x |^ k1 ) )
thus k1 < n by NAT_D:1; :: thesis: ( z = (x |^ k1) * y or z = x |^ k1 )
assume A6: not z = (x |^ k1) * y ; :: thesis: z = x |^ k1
k1 mod n = k mod n by NAT_D:65;
then A7: g1 |^ k1 = g1 |^ k by A1, ThINTGroupOrd3;
A8: x |^ k1 = <*(g1 |^ k1),(1_ (INT.Group 2))*> by A3, Th25
.= <*(g1 |^ k),(1_ (INT.Group 2))*> by A7
.= x |^ k by A3, Th25 ;
then not z = (x |^ k) * y by A6;
hence x |^ k1 = z by A8, A5; :: thesis: verum