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) |^ 2 = 1_ (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) |^ 2 = 1_ (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) |^ 2 = 1_ (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) |^ 2 = 1_ (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) |^ 2 = 1_ (Dihedral_group n)
let x be Element of (Dihedral_group n); :: thesis: ( x = <*g1,(1_ (INT.Group 2))*> implies (x |^ k) |^ 2 = 1_ (Dihedral_group n) )
assume A3: x = <*g1,(1_ (INT.Group 2))*> ; :: thesis: (x |^ k) |^ 2 = 1_ (Dihedral_group n)
A4: g1 |^ n = n mod n by A2, LmINTGroupOrd3
.= 0 by NAT_D:25
.= 1_ (INT.Group n) by GR_CY_1:14 ;
A5: x |^ n = <*(g1 |^ n),(1_ (INT.Group 2))*> by A3, Th25
.= <*(1_ (INT.Group n)),(1_ (INT.Group 2))*> by A4
.= 1_ (Dihedral_group n) by Th17 ;
thus (x |^ k) |^ 2 = x |^ (k * 2) by GROUP_1:35
.= x |^ n by A1
.= 1_ (Dihedral_group n) by A5 ; :: thesis: verum