let R be gcdDomain; for Amp being AmpleSet of R
for a, b, c being Element of R st gcd (a,b,Amp) = 1. R holds
gcd (a,(b * c),Amp) = gcd (a,c,Amp)
let Amp be AmpleSet of R; for a, b, c being Element of R st gcd (a,b,Amp) = 1. R holds
gcd (a,(b * c),Amp) = gcd (a,c,Amp)
let A, B, C be Element of R; ( gcd (A,B,Amp) = 1. R implies gcd (A,(B * C),Amp) = gcd (A,C,Amp) )
assume
gcd (A,B,Amp) = 1. R
; gcd (A,(B * C),Amp) = gcd (A,C,Amp)
then A1:
C * (gcd (A,B,Amp)) = C
;
gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp))
by Th36;
then
gcd (A,C,Amp) is_associated_to gcd (A,(gcd ((A * C),(B * C),Amp)),Amp)
by A1, Th34;
then A2:
gcd (A,C,Amp) is_associated_to gcd ((gcd (A,(A * C),Amp)),(B * C),Amp)
by Th35;
A3: A * (gcd ((1. R),C,Amp)) =
A * (1. R)
by Th32
.=
A
;
gcd ((A * (1. R)),(A * C),Amp) is_associated_to A * (gcd ((1. R),C,Amp))
by Th36;
then
gcd (A,(A * C),Amp) is_associated_to A
by A3;
then A4:
gcd ((gcd (A,(A * C),Amp)),(B * C),Amp) is_associated_to gcd (A,(B * C),Amp)
by Th34;
( gcd (A,(B * C),Amp) is Element of Amp & gcd (A,C,Amp) is Element of Amp )
by Def12;
hence
gcd (A,(B * C),Amp) = gcd (A,C,Amp)
by A2, A4, Th4, Th22; verum