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 () 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 () 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 () 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 () holds
not q,m are_coprime

let q be Prime; :: thesis: ( q in support () implies not q,m are_coprime )
assume A2: q in support () ; :: 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 ;
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 ;
q gcd m = 1 by ;
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
.= ((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
.= ((1_ H) |^ x) * ((1_ H) |^ y) by
.= (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