let p be Prime; :: thesis: for a, b being Element of (Z/Z* p)
for n being natural number 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 natural number st 0 < n & ord a = n & b |^ n = 1 holds
b is Element of (gr {a})
let n be natural number ; :: thesis: ( 0 < n & ord a = n & b |^ n = 1 implies b is Element of (gr {a}) )
assume A1: ( 0 < n & ord a = n & b |^ n = 1 ) ; :: thesis: b is Element of (gr {a})
A2: 1 < p by INT_2:def 5;
assume A3: b is not Element of (gr {a}) ; :: thesis: contradiction
reconsider L = INT.Ring p as non empty unital doubleLoopStr ;
consider f being Polynomial of L such that
A4: ( deg f = n & ( 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;
A5: 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 A6: x1 |^ n = 1 ; :: thesis: x1 in Roots f
x1 in Segm0 p ;
then x1 in (Segm p) \ {0 } by A2, Def2;
then reconsider x3 = x1 as Element of L by XBOOLE_0:def 5;
A7: x1 |^ n = 1_ (Z/Z* p) by A6, Th21
.= 1_ (INT.Ring p) by Th21 ;
x1 |^ n in Segm0 p ;
then x1 |^ n in (Segm p) \ {0 } by A2, Def2;
then reconsider x2 = x1 |^ n as Element of (INT.Ring p) by XBOOLE_0:def 5;
eval f,x3 = x2 - (1_ (INT.Ring p)) by A4
.= 0. L by A7, RLVECT_1:28 ;
then x3 is_a_root_of f by POLYNOM5:def 6;
hence x1 in Roots f by POLYNOM5:def 9; :: thesis: verum

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (gr {a}) or x in Roots f )
assume A9: x in the carrier of (gr {a}) ; :: thesis: x in Roots f
then x in gr {a} by STRUCT_0:def 5;
then x in Z/Z* p by GROUP_2:49;
then reconsider x1 = x as Element of (Z/Z* p) by STRUCT_0:def 5;
x1 in gr {a} by A9, STRUCT_0:def 5;
then consider j being Integer such that
A10: x1 = a |^ j by GR_CY_1:25;
x1 |^ n = a |^ (j * n) by A10, GROUP_1:69
.= (a |^ n) |^ j by GROUP_1:68
.= (1_ (Z/Z* p)) |^ j by A1, GROUP_1:82
.= 1_ (Z/Z* p) by GROUP_1:61
.= 1 by Th21 ;
hence x in Roots f by A5; :: thesis: verum

end;

reconsider RF = Roots f as finite set ;
consider m, n0 being Element of NAT such that
A11: ( n0 = deg f & m = card (Roots f) & m <= n0 ) by A4, Th27;
A12: ex D being finite set st
( D = the carrier of (gr {a}) & card (gr {a}) = card D ) ;
b in Roots f by A1, A5;
then {b} c= Roots f by ZFMISC_1:37;
then A13: the carrier of (gr {a}) \/ {b} c= Roots f by A8, XBOOLE_1:8;
reconsider XX = the carrier of (gr {a}) as finite set ;
A14: card (the carrier of (gr {a}) \/ {b}) = (card XX) + 1 by A3, CARD_2:54
.= n0 + 1 by A1, A4, A11, A12, GR_CY_1:27 ;
A15: card (the carrier of (gr {a}) \/ {b}) c= card (Roots f) by A13, CARD_1:27;
A16: card m = card (Roots f) by A11;
card (n0 + 1) = card (the carrier of (gr {a}) \/ {b}) by A14;
then n0 + 1 c= m by A15, A16, CARD_1:72;
then n0 + 1 <= m by NAT_1:40;
hence contradiction by A11, NAT_1:16, XXREAL_0:2; :: thesis: verum