let G be finite commutative Group; :: thesis: for m being Nat

for H being finite Subgroup of G st the carrier of H = { x where x is Element of G : x |^ m = 1_ G } holds

for q being Prime st q in support (prime_factorization (card H)) holds

not q,m are_coprime

let m be Nat; :: thesis: for H being finite Subgroup of G st the carrier of H = { x where x is Element of G : x |^ m = 1_ G } holds

for q being Prime st q in support (prime_factorization (card H)) holds

not q,m are_coprime

let H be finite Subgroup of G; :: thesis: ( the carrier of H = { x where x is Element of G : x |^ m = 1_ G } implies for q being Prime st q in support (prime_factorization (card H)) holds

not q,m are_coprime )

assume A1: the carrier of H = { x where x is Element of G : x |^ m = 1_ G } ; :: thesis: for q being Prime st q in support (prime_factorization (card H)) holds

not q,m are_coprime

let q be Prime; :: thesis: ( q in support (prime_factorization (card H)) implies not q,m are_coprime )

assume A2: q in support (prime_factorization (card H)) ; :: thesis: not q,m are_coprime

assume A3: q,m are_coprime ; :: thesis: contradiction

consider a being Element of H such that

A4: ( a <> 1_ H & ord a = q ) by A2, Lm5;

a in { x where x is Element of G : x |^ m = 1_ G } by A1;

then consider x being Element of G such that

A5: ( x = a & x |^ m = 1_ G ) ;

A6: a |^ m = 1_ G by A5, GROUP_4:2;

q gcd m = 1 by A3, INT_2:def 3;

then consider x, y being Integer such that

A7: (x * q) + (y * m) = 1 by NAT_D:68;

a = a |^ 1 by GROUP_1:26

.= (a |^ (q * x)) * (a |^ (m * y)) by GROUP_1:33, A7

.= ((a |^ q) |^ x) * (a |^ (m * y)) by GROUP_1:35

.= ((a |^ q) |^ x) * ((a |^ m) |^ y) by GROUP_1:35

.= ((1_ H) |^ x) * ((a |^ m) |^ y) by A4, GROUP_1:41

.= ((1_ H) |^ x) * ((1_ H) |^ y) by A6, GROUP_2:44

.= (1_ H) * ((1_ H) |^ y) by GROUP_1:31

.= (1_ H) * (1_ H) by GROUP_1:31

.= 1_ H by GROUP_1:def 4

.= 1_ G by GROUP_2:44 ;

hence contradiction by GROUP_2:44, A4; :: thesis: verum

for H being finite Subgroup of G st the carrier of H = { x where x is Element of G : x |^ m = 1_ G } holds

for q being Prime st q in support (prime_factorization (card H)) holds

not q,m are_coprime

let m be Nat; :: thesis: for H being finite Subgroup of G st the carrier of H = { x where x is Element of G : x |^ m = 1_ G } holds

for q being Prime st q in support (prime_factorization (card H)) holds

not q,m are_coprime

let H be finite Subgroup of G; :: thesis: ( the carrier of H = { x where x is Element of G : x |^ m = 1_ G } implies for q being Prime st q in support (prime_factorization (card H)) holds

not q,m are_coprime )

assume A1: the carrier of H = { x where x is Element of G : x |^ m = 1_ G } ; :: thesis: for q being Prime st q in support (prime_factorization (card H)) holds

not q,m are_coprime

let q be Prime; :: thesis: ( q in support (prime_factorization (card H)) implies not q,m are_coprime )

assume A2: q in support (prime_factorization (card H)) ; :: thesis: not q,m are_coprime

assume A3: q,m are_coprime ; :: thesis: contradiction

consider a being Element of H such that

A4: ( a <> 1_ H & ord a = q ) by A2, Lm5;

a in { x where x is Element of G : x |^ m = 1_ G } by A1;

then consider x being Element of G such that

A5: ( x = a & x |^ m = 1_ G ) ;

A6: a |^ m = 1_ G by A5, GROUP_4:2;

q gcd m = 1 by A3, INT_2:def 3;

then consider x, y being Integer such that

A7: (x * q) + (y * m) = 1 by NAT_D:68;

a = a |^ 1 by GROUP_1:26

.= (a |^ (q * x)) * (a |^ (m * y)) by GROUP_1:33, A7

.= ((a |^ q) |^ x) * (a |^ (m * y)) by GROUP_1:35

.= ((a |^ q) |^ x) * ((a |^ m) |^ y) by GROUP_1:35

.= ((1_ H) |^ x) * ((a |^ m) |^ y) by A4, GROUP_1:41

.= ((1_ H) |^ x) * ((1_ H) |^ y) by A6, GROUP_2:44

.= (1_ H) * ((1_ H) |^ y) by GROUP_1:31

.= (1_ H) * (1_ H) by GROUP_1:31

.= 1_ H by GROUP_1:def 4

.= 1_ G by GROUP_2:44 ;

hence contradiction by GROUP_2:44, A4; :: thesis: verum