let R be gcdDomain; :: thesis: for Amp being AmpleSet of R
for a, b, c being Element of R st b is_associated_to c holds
( gcd (a,b,Amp) is_associated_to gcd (a,c,Amp) & gcd (b,a,Amp) is_associated_to gcd (c,a,Amp) )
let Amp be AmpleSet of R; :: thesis: for a, b, c being Element of R st b is_associated_to c holds
( gcd (a,b,Amp) is_associated_to gcd (a,c,Amp) & gcd (b,a,Amp) is_associated_to gcd (c,a,Amp) )
let A, B, C be Element of R; :: thesis: ( B is_associated_to C implies ( gcd (A,B,Amp) is_associated_to gcd (A,C,Amp) & gcd (B,A,Amp) is_associated_to gcd (C,A,Amp) ) )
A1: gcd (A,B,Amp) divides B by Def12;
A2: gcd (A,B,Amp) divides A by Def12;
A3: gcd (A,C,Amp) divides A by Def12;
A4: gcd (A,C,Amp) divides C by Def12;
A5: gcd (A,B,Amp) = gcd (B,A,Amp) by Th29;
assume A6: B is_associated_to C ; :: thesis: ( gcd (A,B,Amp) is_associated_to gcd (A,C,Amp) & gcd (B,A,Amp) is_associated_to gcd (C,A,Amp) )
then C divides B ;
then gcd (A,C,Amp) divides B by A4, Th2;
then A7: gcd (A,C,Amp) divides gcd (A,B,Amp) by A3, Def12;
B divides C by A6;
then gcd (A,B,Amp) divides C by A1, Th2;
then gcd (A,B,Amp) divides gcd (A,C,Amp) by A2, Def12;
then gcd (A,B,Amp) is_associated_to gcd (A,C,Amp) by A7;
hence ( gcd (A,B,Amp) is_associated_to gcd (A,C,Amp) & gcd (B,A,Amp) is_associated_to gcd (C,A,Amp) ) by A5, Th29; :: thesis: verum