let R be gcdDomain; :: thesis: for Amp being AmpleSet of R
for a, b, c being Element of R st c divides gcd a,b,Amp holds
( c divides a & c divides b )
let Amp be AmpleSet of R; :: thesis: for a, b, c being Element of R st c divides gcd a,b,Amp holds
( c divides a & c divides b )
let A, B, C be Element of R; :: thesis: ( C divides gcd A,B,Amp implies ( C divides A & C divides B ) )
assume C divides gcd A,B,Amp ; :: thesis: ( C divides A & C divides B )
then consider D being Element of R such that
A1: C * D = gcd A,B,Amp by Def1;
gcd A,B,Amp divides A by Def12;
then consider E being Element of R such that
A2: (gcd A,B,Amp) * E = A by Def1;
A3: C * (D * E) = A by A1, A2, GROUP_1:def 4;
gcd A,B,Amp divides B by Def12;
then consider E being Element of R such that
A4: (gcd A,B,Amp) * E = B by Def1;
C * (D * E) = B by A1, A4, GROUP_1:def 4;
hence ( C divides A & C divides B ) by A3, Def1; :: thesis: verum