let R be gcdDomain; :: thesis: for Amp being AmpleSet of R
for a, b, c being Element of R holds gcd ((gcd (a,b,Amp)),c,Amp) = gcd (a,(gcd (b,c,Amp)),Amp)
let Amp be AmpleSet of R; :: thesis: for a, b, c being Element of R holds gcd ((gcd (a,b,Amp)),c,Amp) = gcd (a,(gcd (b,c,Amp)),Amp)
let A, B, C be Element of R; :: thesis: gcd ((gcd (A,B,Amp)),C,Amp) = gcd (A,(gcd (B,C,Amp)),Amp)
set D = gcd ((gcd (A,B,Amp)),C,Amp);
set E = gcd (A,(gcd (B,C,Amp)),Amp);
A1: gcd ((gcd (A,B,Amp)),C,Amp) divides C by Def12;
A2: gcd (A,(gcd (B,C,Amp)),Amp) divides A by Def12;
A3: gcd (A,(gcd (B,C,Amp)),Amp) divides gcd (B,C,Amp) by Def12;
then A4: gcd (A,(gcd (B,C,Amp)),Amp) divides C by Th28;
gcd (A,(gcd (B,C,Amp)),Amp) divides B by A3, Th28;
then gcd (A,(gcd (B,C,Amp)),Amp) divides gcd (A,B,Amp) by A2, Def12;
then A5: gcd (A,(gcd (B,C,Amp)),Amp) divides gcd ((gcd (A,B,Amp)),C,Amp) by A4, Def12;
A6: ( gcd ((gcd (A,B,Amp)),C,Amp) is Element of Amp & gcd (A,(gcd (B,C,Amp)),Amp) is Element of Amp ) by Def12;
A7: gcd ((gcd (A,B,Amp)),C,Amp) divides gcd (A,B,Amp) by Def12;
then A8: gcd ((gcd (A,B,Amp)),C,Amp) divides A by Th28;
gcd ((gcd (A,B,Amp)),C,Amp) divides B by A7, Th28;
then gcd ((gcd (A,B,Amp)),C,Amp) divides gcd (B,C,Amp) by A1, Def12;
then gcd ((gcd (A,B,Amp)),C,Amp) divides gcd (A,(gcd (B,C,Amp)),Amp) by A8, Def12;
then gcd ((gcd (A,B,Amp)),C,Amp) is_associated_to gcd (A,(gcd (B,C,Amp)),Amp) by A5;
hence gcd ((gcd (A,B,Amp)),C,Amp) = gcd (A,(gcd (B,C,Amp)),Amp) by A6, Th22; :: thesis: verum