let p be Prime; :: thesis: Z/Z* p is cyclic Group
set a = the Element of (Z/Z* p);
set ZP = Z/Z* p;
defpred S1[ Nat, Element of (Z/Z* p), Element of (Z/Z* p)] means ord $2 < ord $3;
assume A1: Z/Z* p is not cyclic Group ; :: thesis: contradiction
A2: for x being Element of (Z/Z* p) holds ord x < card (Z/Z* p)
proof
let x be Element of (Z/Z* p); :: thesis: ord x < card (Z/Z* p)
A3: ord x <= card (Z/Z* p) by GR_CY_1:8, NAT_D:7;
ord x <> card (Z/Z* p) by A1, GR_CY_1:19;
hence ord x < card (Z/Z* p) by A3, XXREAL_0:1; :: thesis: verum
end;
A4: for n being Nat
for x being Element of (Z/Z* p) ex y being Element of (Z/Z* p) st S1[n,x,y]
proof
let n be Nat; :: thesis: for x being Element of (Z/Z* p) ex y being Element of (Z/Z* p) st S1[n,x,y]
let x be Element of (Z/Z* p); :: thesis: ex y being Element of (Z/Z* p) st S1[n,x,y]
set n = ord x;
ord x < card (Z/Z* p) by A2;
then A5: card (gr {x}) <> card (Z/Z* p) by GR_CY_1:7;
the carrier of (gr {x}) c= the carrier of (Z/Z* p) by GROUP_2:def 5;
then the carrier of (gr {x}) c< the carrier of (Z/Z* p) by A5, XBOOLE_0:def 8;
then the carrier of (Z/Z* p) \ the carrier of (gr {x}) <> {} by XBOOLE_1:105;
then consider z being object such that
A6: z in the carrier of (Z/Z* p) \ the carrier of (gr {x}) by XBOOLE_0:def 1;
reconsider z = z as Element of (Z/Z* p) by A6;
set m = ord z;
now :: thesis: ex y being Element of the carrier of (Z/Z* p) st ord x < ord y
set l = (ord z) lcm (ord x);
1 <= card (gr {x}) by GROUP_1:45;
then A7: 1 <= ord x by GR_CY_1:7;
not ord z divides ord x
proof
assume ord z divides ord x ; :: thesis: contradiction
then consider j being Integer such that
A8: ord x = (ord z) * j by INT_1:def 3;
z |^ (ord x) = (z |^ (ord z)) |^ j by A8, GROUP_1:35
.= (1_ (Z/Z* p)) |^ j by GROUP_1:41
.= 1_ (Z/Z* p) by GROUP_1:31
.= 1 by Th21 ;
then z is Element of (gr {x}) by A7, Th29;
hence contradiction by A6, XBOOLE_0:def 5; :: thesis: verum
end;
then A9: ord x <> (ord z) lcm (ord x) by INT_2:18;
1 <= card (gr {z}) by GROUP_1:45;
then A10: 1 <= ord z by GR_CY_1:7;
then consider m0, n0 being Element of NAT such that
A11: (ord z) lcm (ord x) = n0 * m0 and
A12: n0 gcd m0 = 1 and
A13: n0 divides ord x and
A14: m0 divides ord z and
A15: n0 <> 0 and
A16: m0 <> 0 by A7, Th17;
consider j being Integer such that
A17: ord x = n0 * j by A13, INT_1:def 3;
consider u being Integer such that
A18: ord z = m0 * u by A14, INT_1:def 3;
(ord z) / m0 = u by A16, A18, XCMPLX_1:89;
then reconsider d2 = (ord z) / m0 as Element of NAT by INT_1:3;
ord z = ((ord z) / m0) * m0 by A16, XCMPLX_1:87;
then A19: ord (z |^ d2) = m0 by Th30;
(ord x) / n0 = j by A15, A17, XCMPLX_1:89;
then reconsider d1 = (ord x) / n0 as Element of NAT by INT_1:3;
ord x divides (ord z) lcm (ord x) by INT_2:18;
then consider j being Integer such that
A20: (ord z) lcm (ord x) = (ord x) * j by INT_1:def 3;
take y = (x |^ d1) * (z |^ d2); :: thesis: ord x < ord y
ord x = ((ord x) / n0) * n0 by A15, XCMPLX_1:87;
then ord (x |^ d1) = n0 by Th30;
then A21: ord y = m0 * n0 by A12, A19, Th25;
((ord z) lcm (ord x)) / (ord x) = j by A7, A20, XCMPLX_1:89;
then A22: j is Element of NAT by INT_1:3;
j <> 0 by A7, A10, A20, INT_2:4;
then (ord x) * 1 <= (ord x) * j by A22, NAT_1:14, XREAL_1:64;
hence ord x < ord y by A11, A21, A9, A20, XXREAL_0:1; :: thesis: verum
end;
hence ex y being Element of (Z/Z* p) st S1[n,x,y] ; :: thesis: verum
end;
consider f being sequence of the carrier of (Z/Z* p) such that
A23: ( f . 0 = the Element of (Z/Z* p) & ( for n being Nat holds S1[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch 2(A4);
 deffunc H1( Nat) -> Element of NAT = ord (f . $1);
consider g being sequence of NAT such that
A24: for k being Element of NAT holds g . k = H1(k) from FUNCT_2:sch 4();
 A25: for k being Nat holds g . k = H1(k)
proof
let k be Nat; :: thesis: g . k = H1(k)
k in NAT by ORDINAL1:def 12;
hence g . k = H1(k) by A24; :: thesis: verum
end;
A26: now :: thesis: for k being Nat holds g . k < g . (k + 1)
let k be Nat; :: thesis: g . k < g . (k + 1)
A27: g . (k + 1) = ord (f . (k + 1)) by A25;
g . k = ord (f . k) by A25;
hence g . k < g . (k + 1) by A23, A27; :: thesis: verum
end;
A28: for k, m being Element of NAT holds g . k < g . ((k + 1) + m)
proof
let k be Element of NAT ; :: thesis: for m being Element of NAT holds g . k < g . ((k + 1) + m)
defpred S2[ Nat] means g . k < g . ((k + 1) + $1);
A29: now :: thesis: for m being Nat st S2[m] holds
S2[m + 1]
let m be Nat; :: thesis: ( S2[m] implies S2[m + 1] )
assume A30: S2[m] ; :: thesis: S2[m + 1]
g . ((k + 1) + m) < g . (((k + 1) + m) + 1) by A26;
hence S2[m + 1] by A30, XXREAL_0:2; :: thesis: verum
end;
A31: S2[ 0 ] by A26;
for m being Nat holds S2[m] from NAT_1:sch 2(A31, A29);
 hence for m being Element of NAT holds g . k < g . ((k + 1) + m) ; :: thesis: verum
end;
A32: for k, m being Element of NAT st k < m holds
g . k < g . m
proof
let k, m be Element of NAT ; :: thesis: ( k < m implies g . k < g . m )
assume A33: k < m ; :: thesis: g . k < g . m
then m - k is Element of NAT by INT_1:5;
then reconsider mk = m - k as Nat ;
m - k <> 0 by A33;
then consider n0 being Nat such that
A34: mk = n0 + 1 by NAT_1:6;
reconsider n = n0 as Element of NAT by ORDINAL1:def 12;
m = (k + 1) + n by A34;
hence g . k < g . m by A28; :: thesis: verum
end;
now :: thesis: for x1, x2 being object st x1 in NAT & x2 in NAT & g . x1 = g . x2 holds
x2 = x1
let x1, x2 be object ; :: thesis: ( x1 in NAT & x2 in NAT & g . x1 = g . x2 implies x2 = x1 )
assume that
A35: x1 in NAT and
A36: x2 in NAT and
A37: g . x1 = g . x2 ; :: thesis: x2 = x1
reconsider xx1 = x1, xx2 = x2 as Element of NAT by A35, A36;
A38: xx2 <= xx1 by A32, A37;
xx1 <= xx2 by A32, A37;
hence x2 = x1 by A38, XXREAL_0:1; :: thesis: verum
end;
then g is one-to-one by FUNCT_2:19;
then dom g, rng g are_equipotent by WELLORD2:def 4;
then card (dom g) = card (rng g) by CARD_1:5;
then A39: card (rng g) = card NAT by FUNCT_2:def 1;
rng g c= Segm (card (Z/Z* p))
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng g or y in Segm (card (Z/Z* p)) )
assume y in rng g ; :: thesis: y in Segm (card (Z/Z* p))
then consider x being object such that
A40: x in NAT and
A41: y = g . x by FUNCT_2:11;
reconsider x = x as Element of NAT by A40;
reconsider gg = g . x as Element of NAT ;
g . x = ord (f . x) by A25;
then gg < card (Z/Z* p) by A2;
hence y in Segm (card (Z/Z* p)) by A41, NAT_1:44; :: thesis: verum
end;
hence contradiction by A39; :: thesis: verum