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

x " is_primitive_root_of_degree m

let m be Element of NAT ; :: thesis: for x being Element of L st x is_primitive_root_of_degree m holds

x " is_primitive_root_of_degree m

let x be Element of L; :: thesis: ( x is_primitive_root_of_degree m implies x " is_primitive_root_of_degree m )

assume A1: x is_primitive_root_of_degree m ; :: thesis: x " is_primitive_root_of_degree m

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

A3: for i being Element of NAT st 0 < i & i < m holds

(x ") |^ i <> 1. L

then A4: (x ") |^ m = 1. L by A2, Lm10;

m <> 0 by A1;

hence x " is_primitive_root_of_degree m by A4, A3; :: thesis: verum

for x being Element of L st x is_primitive_root_of_degree m holds

x " is_primitive_root_of_degree m

let m be Element of NAT ; :: thesis: for x being Element of L st x is_primitive_root_of_degree m holds

x " is_primitive_root_of_degree m

let x be Element of L; :: thesis: ( x is_primitive_root_of_degree m implies x " is_primitive_root_of_degree m )

assume A1: x is_primitive_root_of_degree m ; :: thesis: x " is_primitive_root_of_degree m

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

A3: for i being Element of NAT st 0 < i & i < m holds

(x ") |^ i <> 1. L

proof

x |^ m = 1. L
by A1;
let i be Element of NAT ; :: thesis: ( 0 < i & i < m implies (x ") |^ i <> 1. L )

assume ( 0 < i & i < m ) ; :: thesis: (x ") |^ i <> 1. L

then x |^ i <> 1. L by A1;

hence (x ") |^ i <> 1. L by A2, Lm11; :: thesis: verum

end;assume ( 0 < i & i < m ) ; :: thesis: (x ") |^ i <> 1. L

then x |^ i <> 1. L by A1;

hence (x ") |^ i <> 1. L by A2, Lm11; :: thesis: verum

then A4: (x ") |^ m = 1. L by A2, Lm10;

m <> 0 by A1;

hence x " is_primitive_root_of_degree m by A4, A3; :: thesis: verum