let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative 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

then A2: x <> 0. L by Th30;

let i, j be Nat; :: thesis: ( 1 <= i & i <= m & 1 <= j & j <= m & i <> j implies pow (x,(i - j)) <> 1. L )

assume that

A3: 1 <= i and

A4: i <= m and

A5: 1 <= j and

A6: j <= m and

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

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

then A2: x <> 0. L by Th30;

let i, j be Nat; :: thesis: ( 1 <= i & i <= m & 1 <= j & j <= m & i <> j implies pow (x,(i - j)) <> 1. L )

assume that

A3: 1 <= i and

A4: i <= m and

A5: 1 <= j and

A6: j <= m and

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

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

end;

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

then reconsider k = i - j as Element of NAT by INT_1:5;

k <= i - 1 by A5, XREAL_1:13;

then k + 1 <= (i - 1) + 1 by XREAL_1:6;

then k < i by NAT_1:13;

then A9: k < m by A4, XXREAL_0:2;

i - j > j - j by A8, XREAL_1:14;

then x |^ k <> 1. L by A1, A9;

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

end;k <= i - 1 by A5, XREAL_1:13;

then k + 1 <= (i - 1) + 1 by XREAL_1:6;

then k < i by NAT_1:13;

then A9: k < m by A4, XXREAL_0:2;

i - j > j - j by A8, XREAL_1:14;

then x |^ k <> 1. L by A1, A9;

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

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

then A10:
i < j
by A7, XXREAL_0:1;

then A11: j - i > i - i by XREAL_1:14;

A12: i - j < j - j by A10, XREAL_1:14;

then A13: |.(i - j).| = - (i - j) by ABSVALUE:def 1;

then reconsider k = - (i - j) as Element of NAT ;

j - i <= j - 1 by A3, XREAL_1:13;

then k + 1 <= (j - 1) + 1 by XREAL_1:6;

then k < j by NAT_1:13;

then A14: k < m by A6, XXREAL_0:2;

A15: x |^ k <> 0. L by A2, Th1;

end;then A11: j - i > i - i by XREAL_1:14;

A12: i - j < j - j by A10, XREAL_1:14;

then A13: |.(i - j).| = - (i - j) by ABSVALUE:def 1;

then reconsider k = - (i - j) as Element of NAT ;

j - i <= j - 1 by A3, XREAL_1:13;

then k + 1 <= (j - 1) + 1 by XREAL_1:6;

then k < j by NAT_1:13;

then A14: k < m by A6, XXREAL_0:2;

A15: x |^ k <> 0. L by A2, Th1;

now :: thesis: not (x |^ k) " = 1. L

hence
pow (x,(i - j)) <> 1. L
by A12, A13, Def2; :: thesis: verumassume
(x |^ k) " = 1. L
; :: thesis: contradiction

then 1. L = (x |^ k) * (1. L) by A15, VECTSP_1:def 10

.= x |^ k ;

hence contradiction by A1, A11, A14; :: thesis: verum

end;then 1. L = (x |^ k) * (1. L) by A15, VECTSP_1:def 10

.= x |^ k ;

hence contradiction by A1, A11, A14; :: thesis: verum