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