let R be gcdDomain; for Amp being AmpleSet of R
for a, b, c being Element of R st c divides gcd (a,b,Amp) holds
( c divides a & c divides b )
let Amp be AmpleSet of R; for a, b, c being Element of R st c divides gcd (a,b,Amp) holds
( c divides a & c divides b )
let A, B, C be Element of R; ( C divides gcd (A,B,Amp) implies ( C divides A & C divides B ) )
assume
C divides gcd (A,B,Amp)
; ( C divides A & C divides B )
then consider D being Element of R such that
A1:
C * D = gcd (A,B,Amp)
;
gcd (A,B,Amp) divides A
by Def12;
then consider E being Element of R such that
A2:
(gcd (A,B,Amp)) * E = A
;
A3:
C * (D * E) = A
by A1, A2, GROUP_1:def 3;
gcd (A,B,Amp) divides B
by Def12;
then consider E being Element of R such that
A4:
(gcd (A,B,Amp)) * E = B
;
C * (D * E) = B
by A1, A4, GROUP_1:def 3;
hence
( C divides A & C divides B )
by A3; verum