let R be gcdDomain; 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; 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; ( 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
; ( 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; verum