let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for m being Element of NAT
for x being Element of L st x is_primitive_root_of_degree m holds
for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m & i <> j holds
pow x,(i - j) <> 1. L
let m be Element of NAT ; :: thesis: for x being Element of L st x is_primitive_root_of_degree m holds
for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m & i <> j holds
pow x,(i - j) <> 1. L
let x be Element of L; :: thesis: ( x is_primitive_root_of_degree m implies for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m & i <> j holds
pow x,(i - j) <> 1. L )
assume A1: x is_primitive_root_of_degree m ; :: thesis: for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m & i <> j holds
pow x,(i - j) <> 1. L
let i, j be Nat; :: thesis: ( 1 <= i & i <= m & 1 <= j & j <= m & i <> j implies pow x,(i - j) <> 1. L )
assume A2: ( 1 <= i & i <= m & 1 <= j & j <= m & i <> j ) ; :: thesis: pow x,(i - j) <> 1. L
A3: x <> 0. L by A1, Th30;

per cases ( i > j or i <= j ) ;

suppose A4: i > j ; :: thesis: pow x,(i - j) <> 1. L

then reconsider k = i - j as Element of NAT by INT_1:18;
A5: i - j > j - j by A4, XREAL_1:16;
k <= i - 1 by A2, XREAL_1:15;
then k + 1 <= (i - 1) + 1 by XREAL_1:8;
then k < i by NAT_1:13;
then k < m by A2, XXREAL_0:2;
then x |^ k <> 1. L by A1, A5, Def6;
hence pow x,(i - j) <> 1. L by Def3; :: thesis: verum

end;

suppose i <= j ; :: thesis: pow x,(i - j) <> 1. L

then A6: i < j by A2, XXREAL_0:1;
then A7: i - j < j - j by XREAL_1:16;
then A8: abs (i - j) = - (i - j) by ABSVALUE:def 1;
then reconsider k = - (i - j) as Element of NAT ;
A9: j - i > i - i by A6, XREAL_1:16;
j - i <= j - 1 by A2, XREAL_1:15;
then k + 1 <= (j - 1) + 1 by XREAL_1:8;
then k < j by NAT_1:13;
then A10: k < m by A2, XXREAL_0:2;
then A11: ( x |^ k <> 1. L & x |^ k <> 0. L ) by A1, A3, A9, Def6, Th1;

now

assume (x |^ k) " = 1. L ; :: thesis: contradiction
then 1. L = (x |^ k) * (1. L) by A11, VECTSP_1:def 22
.= x |^ k by VECTSP_1:def 13 ;
hence contradiction by A1, A9, A10, Def6; :: thesis: verum

end;

hence pow x,(i - j) <> 1. L by A7, A8, Def3; :: thesis: verum

end;

end;