let p be Prime; Z/Z* p is cyclic Group
consider a being Element of (Z/Z* p);
set ZP = Z/Z* p;
defpred S1[ natural number , Element of (Z/Z* p), Element of (Z/Z* p)] means ord $2 < ord $3;
assume A1:
Z/Z* p is not cyclic Group
; contradiction
A2:
for x being Element of (Z/Z* p) holds ord x < card (Z/Z* p)
A4:
for n being Element of 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
Element of
NAT ;
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);
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:27;
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
set 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;
1_ (gr {x}) in the
carrier of
(gr {x})
;
then
1_ (Z/Z* p) in the
carrier of
(gr {x})
by GROUP_2:53;
then
1
in the
carrier of
(gr {x})
by Th21;
then
z <> 1
by A6, XBOOLE_0:def 5;
then A7:
z <> 1_ (Z/Z* p)
by Th21;
reconsider H =
gr {z} as
strict Subgroup of
Z/Z* p ;
set m =
ord z;
reconsider d =
(ord z) gcd (ord x) as
Nat ;
A8:
card H = ord z
by GR_CY_1:27;
1
<= card H
by GROUP_1:90;
then A9:
1
< ord z
by A8, A7, GROUP_1:85, XXREAL_0:1;
now per cases
( d = 1 or d <> 1 )
;
suppose
d <> 1
;
ex y being Element of the carrier of (Z/Z* p) st ord x < ord yset l =
(ord z) lcm (ord x);
1
<= card (gr {x})
by GROUP_1:90;
then A11:
1
<= ord x
by GR_CY_1:27;
not
ord z divides ord x
then A13:
ord x <> (ord z) lcm (ord x)
by INT_2:25;
1
<= card (gr {z})
by GROUP_1:90;
then A14:
1
<= ord z
by GR_CY_1:27;
then consider m0,
n0 being
Element of
NAT such that A15:
(ord z) lcm (ord x) = n0 * m0
and A16:
n0 gcd m0 = 1
and A17:
n0 divides ord x
and A18:
m0 divides ord z
and A19:
n0 <> 0
and A20:
m0 <> 0
by A11, Th17;
consider j being
Integer such that A21:
ord x = n0 * j
by A17, INT_1:def 9;
consider u being
Integer such that A22:
ord z = m0 * u
by A18, INT_1:def 9;
(ord z) / m0 = u
by A20, A22, XCMPLX_1:90;
then reconsider d2 =
(ord z) / m0 as
Element of
NAT by INT_1:16;
ord z = ((ord z) / m0) * m0
by A20, XCMPLX_1:88;
then A23:
ord (z |^ d2) = m0
by Th30;
(ord x) / n0 = j
by A19, A21, XCMPLX_1:90;
then reconsider d1 =
(ord x) / n0 as
Element of
NAT by INT_1:16;
ord x divides (ord z) lcm (ord x)
by INT_2:25;
then consider j being
Integer such that A24:
(ord z) lcm (ord x) = (ord x) * j
by INT_1:def 9;
take y =
(x |^ d1) * (z |^ d2);
ord x < ord y
ord x = ((ord x) / n0) * n0
by A19, XCMPLX_1:88;
then
ord (x |^ d1) = n0
by Th30;
then A25:
ord y = m0 * n0
by A16, A23, Th25;
((ord z) lcm (ord x)) / (ord x) = j
by A11, A24, XCMPLX_1:90;
then A26:
j is
Element of
NAT
by INT_1:16;
j <> 0
by A11, A14, A24, INT_2:4;
then
(ord x) * 1
<= (ord x) * j
by A26, NAT_1:14, XREAL_1:66;
hence
ord x < ord y
by A15, A25, A13, A24, XXREAL_0:1;
verum end;
hence
ex
y being
Element of
(Z/Z* p) st
S1[
n,
x,
y]
;
verum
end;
consider f being Function of NAT ,the carrier of (Z/Z* p) such that
A27:
( f . 0 = a & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) )
from RECDEF_1:sch 2(A4);
deffunc H1( Element of NAT ) -> Element of NAT = ord (f . $1);
consider g being Function of NAT ,NAT such that
A28:
for k being Element of NAT holds g . k = H1(k)
from FUNCT_2:sch 4();
A31:
for k, m being Element of NAT holds g . k < g . ((k + 1) + m)
A35:
for k, m being Element of NAT st k < m holds
g . k < g . m
then
g is one-to-one
by FUNCT_2:25;
then
dom g, rng g are_equipotent
by WELLORD2:def 4;
then
card (dom g) = card (rng g)
by CARD_1:21;
then A42:
card (rng g) = card NAT
by FUNCT_2:def 1;
rng g c= Segm (card (Z/Z* p))
hence
contradiction
by A42; verum