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
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, Def6;
hence (x " ) |^ i <> 1. L by A2, Lm11; :: thesis: verum

end;

x |^ m = 1. L by A1, Def6;
then A4: (x " ) |^ m = 1. L by A2, Lm10;
m <> 0 by A1, Def6;
hence x " is_primitive_root_of_degree m by A4, A3, Def6; :: thesis: verum