let n be non zero odd Nat; :: 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 i being Nat holds
( not i < n or i = 0 or x |^ i <> x |^ (n - i) )
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 i being Nat holds
( not i < n or i = 0 or x |^ i <> x |^ (n - i) ) )
assume A1: g1 = 1 ; :: thesis: for x being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> holds
for i being Nat holds
( not i < n or i = 0 or x |^ i <> x |^ (n - i) )
let x be Element of (Dihedral_group n); :: thesis: ( x = <*g1,(1_ (INT.Group 2))*> implies for i being Nat holds
( not i < n or i = 0 or x |^ i <> x |^ (n - i) ) )
assume A2: x = <*g1,(1_ (INT.Group 2))*> ; :: thesis: for i being Nat holds
( not i < n or i = 0 or x |^ i <> x |^ (n - i) )
let i be Nat; :: thesis: ( not i < n or i = 0 or x |^ i <> x |^ (n - i) )
assume A3: i < n ; :: thesis: ( i = 0 or x |^ i <> x |^ (n - i) )
assume A4: i <> 0 ; :: thesis: x |^ i <> x |^ (n - i)
A5: for j being Nat holds g1 |^ j = j mod n by A1, LmINTGroupOrd3;
g1 |^ i <> g1 |^ (n - i)

proof

assume B1: g1 |^ i = g1 |^ (n - i) ; :: thesis: contradiction
B2: g1 |^ i = i mod n by A5
.= i by A3, NAT_D:24 ;
B3: ( 0 < n - i & n - i < n )

proof

i - i < n - i by A3, XREAL_1:9;
hence 0 < n - i ; :: thesis: n - i < n
i > 0 by A4;
hence n - i < n by XREAL_1:44; :: thesis: verum

end;

then n - i in NAT by INT_1:3;
then g1 |^ (n - i) = (n - i) mod n by A5
.= n - i by B3, NAT_D:24 ;
then i = n - i by B1, B2;
then 2 * i = n + 0 ;
then n is even ;
hence contradiction ; :: thesis: verum

end;

then g1 |^ i <> g1 |^ (n - i) ;
then <*(g1 |^ i),(1_ (INT.Group 2))*> <> <*(g1 |^ (n - i)),(1_ (INT.Group 2))*> by FINSEQ_1:77;
then x |^ i <> <*(g1 |^ (n - i)),(1_ (INT.Group 2))*> by A2, Th25;
hence x |^ i <> x |^ (n - i) by A2, Th25; :: thesis: verum