let R be gcdDomain; :: thesis: for Amp being AmpleSet of R
for a, b being Element of R holds
( gcd (a,b,Amp) = 0. R iff ( a = 0. R & b = 0. R ) )
let Amp be AmpleSet of R; :: thesis: for a, b being Element of R holds
( gcd (a,b,Amp) = 0. R iff ( a = 0. R & b = 0. R ) )
let A, B be Element of R; :: thesis: ( gcd (A,B,Amp) = 0. R iff ( A = 0. R & B = 0. R ) )
A1: now :: thesis: ( gcd (A,B,Amp) = 0. R & gcd (A,B,Amp) = 0. R implies ( A = 0. R & B = 0. R ) )
assume A2: gcd (A,B,Amp) = 0. R ; :: thesis: ( gcd (A,B,Amp) = 0. R implies ( A = 0. R & B = 0. R ) )
then 0. R divides B by Def12;
then A3: ex E being Element of R st (0. R) * E = B ;
0. R divides A by A2, Def12;
then ex D being Element of R st (0. R) * D = A ;
hence ( gcd (A,B,Amp) = 0. R implies ( A = 0. R & B = 0. R ) ) by A3; :: thesis: verum
end;
( A = 0. R & B = 0. R implies gcd (A,B,Amp) = 0. R )
proof
assume that
A4: A = 0. R and
A5: B = 0. R ; :: thesis: gcd (A,B,Amp) = 0. R
gcd (A,B,Amp) = NF (A,Amp) by A5, Th30;
hence gcd (A,B,Amp) = 0. R by A4, Th25; :: thesis: verum
end;
hence ( gcd (A,B,Amp) = 0. R iff ( A = 0. R & B = 0. R ) ) by A1; :: thesis: verum