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 A1: ( C = gcd A,B,Amp & C <> 0. R ) ; :: thesis: gcd (A / C),(B / C),Amp = 1. R
set A1 = A / C;
set B1 = B / C;
C divides A by A1, Def12;
then A2: (A / C) * C = A by A1, Def4;
C divides B by A1, Def12;
then A3: gcd A,B,Amp = gcd ((A / C) * C),((B / C) * C),Amp by A1, A2, Def4;
gcd ((A / C) * C),((B / C) * C),Amp is_associated_to C * (gcd (A / C),(B / C),Amp) by Th37;
then C * (1. R) is_associated_to C * (gcd (A / C),(B / C),Amp) by A1, A3, VECTSP_1:def 13;
then A4: gcd (A / C),(B / C),Amp is_associated_to 1. R by A1, Th19;
A5: gcd (A / C),(B / C),Amp is Element of Amp by Def12;
1. R is Element of Amp by Def8;
hence gcd (A / C),(B / C),Amp = 1. R by A4, A5, Th22; :: thesis: verum