let R be gcdDomain; :: thesis: for Amp being AmpleSet of R
for a, b, c being Element of R st c = gcd (a,b,Amp) & c <> 0. R holds
gcd ((a / c),(b / c),Amp) = 1. R
let Amp be AmpleSet of R; :: thesis: for a, b, c being Element of R st c = gcd (a,b,Amp) & c <> 0. R holds
gcd ((a / c),(b / c),Amp) = 1. R
let A, B, C be Element of R; :: thesis: ( C = gcd (A,B,Amp) & C <> 0. R implies gcd ((A / C),(B / C),Amp) = 1. R )
assume that
A1: C = gcd (A,B,Amp) and
A2: C <> 0. R ; :: thesis: gcd ((A / C),(B / C),Amp) = 1. R
set A1 = A / C;
C divides A by A1, Def12;
then A3: (A / C) * C = A by A2, Def4;
set B1 = B / C;
A4: gcd (((A / C) * C),((B / C) * C),Amp) is_associated_to C * (gcd ((A / C),(B / C),Amp)) by Th36;
A5: ( gcd ((A / C),(B / C),Amp) is Element of Amp & 1. R is Element of Amp ) by Def8, Def12;
C divides B by A1, Def12;
then gcd (A,B,Amp) = gcd (((A / C) * C),((B / C) * C),Amp) by A2, A3, Def4;
then C * (1. R) is_associated_to C * (gcd ((A / C),(B / C),Amp)) by A1, A4;
hence gcd ((A / C),(B / C),Amp) = 1. R by A2, A5, Th19, Th22; :: thesis: verum