let R be gcdDomain; 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; 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; ( 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; verum