%--------------------------------------------------------------------------
% File     : GRP102e1.0-001 : TSTP v2.4.1; Released v1.0.0;
% Domain   : Group Theory
% Problem  : let p prime, q prime, p<q, q<>1 (mod p), |G| = p*q;
%                   Then G is a cyclic group
% Language : English
% Version  :
% System   :

% Refs     :
% Source   :
% Date     :

% Results  :
% Comments :
%--------------------------------------------------------------------------
english(f1,hypothesis,
    'p is prime',
    file('tptp/grp/GRP102.p',f1)).

english(f2,hypothesis,
    'q is prime',
    file('tptp/grp/GRP102.p',f2)).

english(f3,hypothesis,
    'p<q',
    file('tptp/grp/GRP102.p',f3)).

english(f4,hypothesis,
    q<>1 (mod p)',
    file('tptp/grp/GRP102.p',f4)).

english(f5,hypothesis,
    '|G|= p*q',
    file('tptp/grp/GRP102.p',f5)).

english(f6,knowledge,
    'let A<G, B<G, LargestCommonFactor(|A|,|B|)=1; then the Intersection(A,B)={1}',
    creator('sasha',[])).

english(f7,knowledge,
    'let IsMember(a,G), IsMember(b,G), a*b=b*a; the,order(a*b)=order(a)order(b)',
    creator('sasha',[])).

english(f8,definition,
    'let |G| = pow(p,a)*m for a>=1, p prime and p does not divide m. Set Sylow(p,G)={P< G: |P|=pow(p,a)}.',
    creator('sasha',[])).

english(f9,knowledge,
    'let n(p)=|sylow(p,G)|=1, IsMember(x,P), IsMember(P,sylow(p,G)); then IsMember(x*a*pow(x,-1),P)',
    creator('sasha',[])).

english(f10,knowledge,
    'let |A|=r, r is prime then there exists c such that IsMember(c,A) and order(c)=r',
    creator('sasha',[])).

english(f11,knowledge,
    'let n(p)=|sylow(p,G)|, then n(p)|m',
    creator('sasha',[])).

english(f12,knowledge,
    'let n(p)=|sylow(p,G)|, then n(p)=1 (mod p)',
    creator('sasha',[])).

english(f13,knowledge,
    'let p is prime, s|p; then s=1 or s=p ',
    creator('sasha',[])).

english(f14,knowledge,
    'let |G|=s, IsMember(x,G), order(x)=s; then G is a cyclic group',
    creator('sasha',[])).

english(f15,definition,
    'let G is a group, IsMember(a,G); then IsMember(pow(a,-1),G)',
    file('tptp/grp/GRP001.ax',f1)).

english(f16,definition,
    'let G is a group, IsMember(a,G), IsMember(b,G); then IsMember(a*b,G)',
    file('tptp/grp/GRP001.ax',f2)).

english(f17,infered,
    'n(p)|q',
    inference(deduction,[f5,f8,f11])).

english(f18,infered,
    'n(q)|p',
    inference(deduction,[f5,f8,f11])).

english(f19,infered,
    'n(p)=1 or n(p)=q',
    inference(deduction,[f2,f13,f17])).

english(f20,infered,
    'n(q)=1 or n(q)=p',
    inference(deduction,[f1,f13,f18])).

english(f21,infered,
    'n(p)=1',
    inference(deduction,[f4,f8,f12,f19])).

english(f22,infered,
    'n(q)=1',
    inference(deduction,[f3,f8,f12,f20])).

english(f23,infered,
    '|sylow(p,G)|=1 and sylow(p,G)={P | |P|=p}',
    inference(rewrite,f21])).

english(f24,infered,
    '|sylow(q,G)|=1 and sylow(q,G)={Q | |Q|=q}',
    inference(rewrite,f22])).

english(f25,infered,
    'there exists a such that IsMember(a,P), order(a)=p',
    inference(deduction,[f9,f23])).

english(f26,infered,
    'there exists b such that IsMember(b,Q), order(b)=q',
    inference(deduction,[f9,f24])).

english(f27,infered,
    'if IsMember(b,G) then IsMember(b*pow(a,-1)*pow(b,-1),P)',
    inference(deduction,[f8,f15,f23,f25])).

english(f28,infered,
    'if IsMember(b,G) then IsMember(a*b*pow(a,-1),Q)',
    inference(deduction,[f8,f24,f26])).

english(f29,infered,
    'IsMember(a*b*pow(a,-1)*pow(b,-1),P)',
    inference(deduction,[f16,f25,f27])).

english(f30,infered,
    'IsMember(a*b*pow(a,-1)*pow(b,-1),Q)',
    inference(deduction,[f15,f16,f26,f28])).

english(f31,infered,
    'a*b*pow(a,-1)*pow(b,-1)=1',
    inference(deduction,[f1,f2,f6,f23,f24,f29,f30])).

english(f32,infered,
    'a*b=b*a',
    inference(rewrite,f31])).

english(f33,infered,
    'order(a*b)=p*q',
    inference(deduction,[f7,f25,f26,f32])).

english(f34,infered,
    'G is a cyclic group',
    inference(deduction,[f5,f14,f16,f33])).
%--------------------------------------------------------------------------