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

proof

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;

x |^ m = 1. L by A1;
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