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) ;
gcd (A,B,Amp) divides A by Def12;
then consider E being Element of R such that
A2: (gcd (A,B,Amp)) * E = A ;
A3: C * (D * E) = A by A1, A2, GROUP_1:def 3;
gcd (A,B,Amp) divides B by Def12;
then consider E being Element of R such that
A4: (gcd (A,B,Amp)) * E = B ;
C * (D * E) = B by A1, A4, GROUP_1:def 3;
hence ( C divides A & C divides B ) by A3; :: thesis: verum