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