let p be Prime; :: thesis: for a, b being Element of (Z/Z* p)
for n being Nat st 0 < n & ord a = n & b |^ n = 1 holds
b is Element of (gr {a})
let a, b be Element of (Z/Z* p); :: thesis: for n being Nat st 0 < n & ord a = n & b |^ n = 1 holds
b is Element of (gr {a})
let n be Nat; :: thesis: ( 0 < n & ord a = n & b |^ n = 1 implies b is Element of (gr {a}) )
assume that
A1: 0 < n and
A2: ord a = n and
A3: b |^ n = 1 ; :: thesis: b is Element of (gr {a})
reconsider XX = the carrier of (gr {a}) as finite set ;
A4: ex D being finite set st
( D = the carrier of (gr {a}) & card (gr {a}) = card D ) ;
reconsider L = INT.Ring p as non empty unital doubleLoopStr ;
consider f being Polynomial of L such that
A5: deg f = n and
A6: for x being Element of L
for xz being Element of (Z/Z* p)
for xn being Element of (INT.Ring p) st x = xz & xn = xz |^ n holds
eval (f,x) = xn - (1_ (INT.Ring p)) by A1, Lm14;
consider m, n0 being Element of NAT such that
A7: n0 = deg f and
A8: m = card (Roots f) and
A9: m <= n0 by A5, Th27;
assume b is not Element of (gr {a}) ; :: thesis: contradiction
then card ( the carrier of (gr {a}) \/ {b}) = (card XX) + 1 by CARD_2:41
.= n0 + 1 by A2, A5, A7, A4, GR_CY_1:7 ;
then A10: card (n0 + 1) = card ( the carrier of (gr {a}) \/ {b}) ;
A11: 1 < p by INT_2:def 4;
A12: for x being Element of (Z/Z* p) st x |^ n = 1 holds
x in Roots f

proof

let x1 be Element of (Z/Z* p); :: thesis: ( x1 |^ n = 1 implies x1 in Roots f )
assume x1 |^ n = 1 ; :: thesis: x1 in Roots f
then A13: x1 |^ n = 1_ (Z/Z* p) by Th21
.= 1_ (INT.Ring p) by Th21 ;
x1 |^ n in Segm0 p ;
then x1 |^ n in (Segm p) \ {0} by A11, Def2;
then reconsider x2 = x1 |^ n as Element of (INT.Ring p) by XBOOLE_0:def 5;
x1 in Segm0 p ;
then x1 in (Segm p) \ {0} by A11, Def2;
then reconsider x3 = x1 as Element of L by XBOOLE_0:def 5;
eval (f,x3) = x2 - (1_ (INT.Ring p)) by A6
.= 0. L by A13, RLVECT_1:15 ;
then x3 is_a_root_of f by POLYNOM5:def 7;
hence x1 in Roots f by POLYNOM5:def 10; :: thesis: verum

end;

A14: the carrier of (gr {a}) c= Roots f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (gr {a}) or x in Roots f )
assume A15: x in the carrier of (gr {a}) ; :: thesis: x in Roots f
then x in gr {a} ;
then x in Z/Z* p by GROUP_2:40;
then reconsider x1 = x as Element of (Z/Z* p) ;
x1 in gr {a} by A15;
then consider j being Integer such that
A16: x1 = a |^ j by GR_CY_1:5;
x1 |^ n = a |^ (j * n) by A16, GROUP_1:35
.= (a |^ n) |^ j by GROUP_1:35
.= (1_ (Z/Z* p)) |^ j by A2, GROUP_1:41
.= 1_ (Z/Z* p) by GROUP_1:31
.= 1 by Th21 ;
hence x in Roots f by A12; :: thesis: verum

end;

b in Roots f by A3, A12;
then {b} c= Roots f by ZFMISC_1:31;
then the carrier of (gr {a}) \/ {b} c= Roots f by A14, XBOOLE_1:8;
then A17: card ( the carrier of (gr {a}) \/ {b}) c= card (Roots f) by CARD_1:11;
card m = card (Roots f) by A8;
then Segm (n0 + 1) c= Segm m by A17, A10;
then n0 + 1 <= m by NAT_1:39;
hence contradiction by A9, NAT_1:16, XXREAL_0:2; :: thesis: verum