let R be gcdDomain; :: thesis: for Amp being AmpleSet of R
for a being Element of R holds
( gcd (a,(0. R),Amp) = NF (a,Amp) & gcd ((0. R),a,Amp) = NF (a,Amp) )
let Amp be AmpleSet of R; :: thesis: for a being Element of R holds
( gcd (a,(0. R),Amp) = NF (a,Amp) & gcd ((0. R),a,Amp) = NF (a,Amp) )
let A be Element of R; :: thesis: ( gcd (A,(0. R),Amp) = NF (A,Amp) & gcd ((0. R),A,Amp) = NF (A,Amp) )
A1: NF (A,Amp) in Amp by Def9;
(NF (A,Amp)) * (0. R) = 0. R ;
then A2: NF (A,Amp) divides 0. R ;
A3: NF (A,Amp) is_associated_to A by Def9;
A4: for z being Element of R st z divides A & z divides 0. R holds
z divides NF (A,Amp) by A3, Th2;
NF (A,Amp) divides A by A3;
then gcd (A,(0. R),Amp) = NF (A,Amp) by A2, A4, A1, Def12;
hence ( gcd (A,(0. R),Amp) = NF (A,Amp) & gcd ((0. R),A,Amp) = NF (A,Amp) ) by Th29; :: thesis: verum