let G be finite cyclic Group; :: thesis: for n, m being Nat st card G = n * m holds
ex a being Element of G st
( ord a = n & gr {a} is strict Subgroup of G )
let n, m be Nat; :: thesis: ( card G = n * m implies ex a being Element of G st
( ord a = n & gr {a} is strict Subgroup of G ) )
consider g being Element of G such that
A1: ord g = card G by GR_CY_1:19;
A2: m in NAT by ORDINAL1:def 12;
A3: n in NAT by ORDINAL1:def 12;
assume card G = n * m ; :: thesis: ex a being Element of G st
( ord a = n & gr {a} is strict Subgroup of G )
then ord (g |^ m) = n by A1, A2, A3, INT_7:30;
then consider a being Element of G such that
A4: ord a = n ;
take a ; :: thesis: ( ord a = n & gr {a} is strict Subgroup of G )
thus ( ord a = n & gr {a} is strict Subgroup of G ) by A4; :: thesis: verum