let F be commutative Skew-Field; for G being finite Subgroup of MultGroup F holds G is cyclic Group
let G be finite Subgroup of MultGroup F; G is cyclic Group
set a = the Element of G;
defpred S1[ Nat, Element of G, Element of G] means ord $2 < ord $3;
assume
G is not cyclic Group
; contradiction
then A1:
for x being Element of G holds not ord x = card G
by GR_CY_1:19;
A2:
for x being Element of G holds ord x < card G
A3:
for n being Nat
for x being Element of G ex y being Element of G st S1[n,x,y]
proof
let n be
Nat;
for x being Element of G ex y being Element of G st S1[n,x,y]let x be
Element of
G;
ex y being Element of G st S1[n,x,y]
set n =
ord x;
ord x < card G
by A2;
then A4:
card (gr {x}) <> card G
by GR_CY_1:7;
the
carrier of
(gr {x}) c= the
carrier of
G
by GROUP_2:def 5;
then
the
carrier of
(gr {x}) c< the
carrier of
G
by A4, XBOOLE_0:def 8;
then
the
carrier of
G \ the
carrier of
(gr {x}) <> {}
by XBOOLE_1:105;
then consider z being
object such that A5:
z in the
carrier of
G \ the
carrier of
(gr {x})
by XBOOLE_0:def 1;
reconsider z =
z as
Element of
G by A5;
set m =
ord z;
set l =
(ord z) lcm (ord x);
ord x divides (ord z) lcm (ord x)
by INT_2:def 1;
then consider j being
Integer such that A6:
(ord z) lcm (ord x) = (ord x) * j
by INT_1:def 3;
A7:
1
<= card (gr {x})
by GROUP_1:45;
then A8:
1
<= ord x
by GR_CY_1:7;
then
((ord z) lcm (ord x)) / (ord x) = j
by A6, XCMPLX_1:89;
then A9:
j is
Element of
NAT
by INT_1:3;
not
ord z divides ord x
then A12:
ord x <> (ord z) lcm (ord x)
by INT_2:def 1;
A13:
1
<= card (gr {z})
by GROUP_1:45;
then A14:
ord z <> 0
by GR_CY_1:7;
1
<= ord z
by A13, GR_CY_1:7;
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 A8, INT_7:17;
ex
u being
Integer st
ord z = m0 * u
by A18, INT_1:def 3;
then
(ord z) / m0 is
Integer
by A20, XCMPLX_1:89;
then reconsider d2 =
(ord z) / m0 as
Element of
NAT by INT_1:3;
ex
j being
Integer st
ord x = n0 * j
by A17, INT_1:def 3;
then
(ord x) / n0 is
Integer
by A19, XCMPLX_1:89;
then reconsider d1 =
(ord x) / n0 as
Element of
NAT by INT_1:3;
set y =
(x |^ d1) * (z |^ d2);
ord z = d2 * m0
by A20, XCMPLX_1:87;
then A21:
ord (z |^ d2) = m0
by INT_7:30;
ord x <> 0
by A7, GR_CY_1:7;
then
j <> 0
by A14, A6, INT_2:4;
then
(ord x) * 1
<= (ord x) * j
by A9, NAT_1:14, XREAL_1:64;
then A22:
ord x < (ord z) lcm (ord x)
by A12, A6, XXREAL_0:1;
ord x = d1 * n0
by A19, XCMPLX_1:87;
then
ord (x |^ d1) = n0
by INT_7:30;
then
ord ((x |^ d1) * (z |^ d2)) = m0 * n0
by A16, A21, INT_7:25;
hence
ex
y being
Element of
G st
ord x < ord y
by A15, A22;
verum
end;
consider f being sequence of the carrier of G such that
A23:
( f . 0 = the Element of G & ( for n being Nat holds S1[n,f . n,f . (n + 1)] ) )
from RECDEF_1:sch 2(A3);
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 G)
hence
contradiction
by A39; verum