let L be non empty non degenerated right_complementable right-distributive well-unital add-associative right_zeroed doubleLoopStr ; :: thesis: for n being Element of NAT holds not 0. L is_primitive_root_of_degree n

let n be Element of NAT ; :: thesis: not 0. L is_primitive_root_of_degree n

defpred S_{1}[ Nat] means (0. L) |^ $1 = 0. L;

A1: for j being Nat st 1 <= j & S_{1}[j] holds

S_{1}[j + 1]
_{1}[1]
by BINOM:8;

A3: for m being Nat st 1 <= m holds

S_{1}[m]
from NAT_1:sch 8(A2, A1);

assume A4: 0. L is_primitive_root_of_degree n ; :: thesis: contradiction

then n <> 0 ;

then 0 + 1 < n + 1 by XREAL_1:8;

then 1 <= n by NAT_1:13;

then (0. L) |^ n <> 1. L by A3;

hence contradiction by A4; :: thesis: verum

let n be Element of NAT ; :: thesis: not 0. L is_primitive_root_of_degree n

defpred S

A1: for j being Nat st 1 <= j & S

S

proof

A2:
S
let j be Nat; :: thesis: ( 1 <= j & S_{1}[j] implies S_{1}[j + 1] )

assume 1 <= j ; :: thesis: ( not S_{1}[j] or S_{1}[j + 1] )

assume S_{1}[j]
; :: thesis: S_{1}[j + 1]

(0. L) |^ (j + 1) = ((0. L) |^ j) * (0. L) by GROUP_1:def 7

.= 0. L ;

hence S_{1}[j + 1]
; :: thesis: verum

end;assume 1 <= j ; :: thesis: ( not S

assume S

(0. L) |^ (j + 1) = ((0. L) |^ j) * (0. L) by GROUP_1:def 7

.= 0. L ;

hence S

A3: for m being Nat st 1 <= m holds

S

assume A4: 0. L is_primitive_root_of_degree n ; :: thesis: contradiction

then n <> 0 ;

then 0 + 1 < n + 1 by XREAL_1:8;

then 1 <= n by NAT_1:13;

then (0. L) |^ n <> 1. L by A3;

hence contradiction by A4; :: thesis: verum