let p be Prime; 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
; contradiction
A2:
for x being Element of (Z/Z* p) holds ord x < card (Z/Z* p)
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;
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: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 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:45;
then A7:
1
<= ord x
by GR_CY_1:7;
not
ord z divides ord x
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);
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;
verum end;
hence
ex
y being
Element of
(Z/Z* p) st
S1[
n,
x,
y]
;
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)
A26:
now for k being Nat holds g . k < g . (k + 1)end;
A28:
for k, m being Element of NAT holds g . k < g . ((k + 1) + m)
A32:
for k, m being Element of NAT st k < m holds
g . k < g . m
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))
hence
contradiction
by A39; verum