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 Th37;
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, VECTSP_1:def 13;
hence gcd (A / C),(B / C),Amp = 1. R by A2, A5, Th19, Th22; :: thesis: verum