let R be gcdDomain; :: thesis: for Amp being AmpleSet of R
for r1, r2, s1, s2 being Element of R st gcd r1,r2,Amp = 1. R & gcd s1,s2,Amp = 1. R & r2 <> 0. R holds
gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(r2 * (s2 / (gcd r2,s2,Amp))),Amp = gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(gcd r2,s2,Amp),Amp
let Amp be AmpleSet of R; :: thesis: for r1, r2, s1, s2 being Element of R st gcd r1,r2,Amp = 1. R & gcd s1,s2,Amp = 1. R & r2 <> 0. R holds
gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(r2 * (s2 / (gcd r2,s2,Amp))),Amp = gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(gcd r2,s2,Amp),Amp
let r1, r2, s1, s2 be Element of R; :: thesis: ( gcd r1,r2,Amp = 1. R & gcd s1,s2,Amp = 1. R & r2 <> 0. R implies gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(r2 * (s2 / (gcd r2,s2,Amp))),Amp = gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(gcd r2,s2,Amp),Amp )
assume that
A1: gcd r1,r2,Amp = 1. R and
A2: gcd s1,s2,Amp = 1. R and
A3: r2 <> 0. R ; :: thesis: gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(r2 * (s2 / (gcd r2,s2,Amp))),Amp = gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(gcd r2,s2,Amp),Amp
set d = gcd r2,s2,Amp;
set r = r2 / (gcd r2,s2,Amp);
set s = s2 / (gcd r2,s2,Amp);
A4: gcd r2,s2,Amp <> 0. R by A3, Th34;
then A5: gcd (r2 / (gcd r2,s2,Amp)),(s2 / (gcd r2,s2,Amp)),Amp = 1. R by Th39;
A6: gcd r2,s2,Amp divides s2 by Def12;
gcd (s2 / (gcd r2,s2,Amp)),s1,Amp = 1. R

proof

gcd (s2 / (gcd r2,s2,Amp)),s1,Amp divides s2 / (gcd r2,s2,Amp) by Def12;
then consider e being Element of R such that
A7: (gcd (s2 / (gcd r2,s2,Amp)),s1,Amp) * e = s2 / (gcd r2,s2,Amp) by Def1;
(gcd (s2 / (gcd r2,s2,Amp)),s1,Amp) * (e * (gcd r2,s2,Amp)) = (s2 / (gcd r2,s2,Amp)) * (gcd r2,s2,Amp) by A7, GROUP_1:def 4
.= s2 by A6, A4, Def4 ;
then A8: gcd (s2 / (gcd r2,s2,Amp)),s1,Amp divides s2 by Def1;
A9: ( gcd (s2 / (gcd r2,s2,Amp)),s1,Amp is Element of Amp & 1. R is Element of Amp ) by Def8, Def12;
(1. R) * (gcd (s2 / (gcd r2,s2,Amp)),s1,Amp) = gcd (s2 / (gcd r2,s2,Amp)),s1,Amp by VECTSP_1:def 19;
then A10: 1. R divides gcd (s2 / (gcd r2,s2,Amp)),s1,Amp by Def1;
gcd (s2 / (gcd r2,s2,Amp)),s1,Amp divides s1 by Def12;
then gcd (s2 / (gcd r2,s2,Amp)),s1,Amp divides gcd s1,s2,Amp by A8, Def12;
then gcd (s2 / (gcd r2,s2,Amp)),s1,Amp is_associated_to 1. R by A2, A10, Def3;
hence gcd (s2 / (gcd r2,s2,Amp)),s1,Amp = 1. R by A9, Th22; :: thesis: verum

end;

then A11: gcd (s2 / (gcd r2,s2,Amp)),(s1 * (r2 / (gcd r2,s2,Amp))),Amp = gcd (s2 / (gcd r2,s2,Amp)),(r2 / (gcd r2,s2,Amp)),Amp by Th38;
gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(s2 / (gcd r2,s2,Amp)),Amp = gcd (s1 * (r2 / (gcd r2,s2,Amp))),(s2 / (gcd r2,s2,Amp)),Amp by Th40;
then A12: gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(s2 / (gcd r2,s2,Amp)),Amp = gcd (s2 / (gcd r2,s2,Amp)),(s1 * (r2 / (gcd r2,s2,Amp))),Amp by Th30
.= 1. R by A11, A5, Th30 ;
A13: gcd r2,s2,Amp divides (gcd r2,s2,Amp) * r2 by Th6;
A14: gcd r2,s2,Amp divides r2 by Def12;
gcd (r2 / (gcd r2,s2,Amp)),r1,Amp = 1. R

proof

gcd (r2 / (gcd r2,s2,Amp)),r1,Amp divides r2 / (gcd r2,s2,Amp) by Def12;
then consider e being Element of R such that
A15: (gcd (r2 / (gcd r2,s2,Amp)),r1,Amp) * e = r2 / (gcd r2,s2,Amp) by Def1;
(gcd (r2 / (gcd r2,s2,Amp)),r1,Amp) * (e * (gcd r2,s2,Amp)) = (r2 / (gcd r2,s2,Amp)) * (gcd r2,s2,Amp) by A15, GROUP_1:def 4
.= r2 by A14, A4, Def4 ;
then A16: gcd (r2 / (gcd r2,s2,Amp)),r1,Amp divides r2 by Def1;
A17: ( gcd (r2 / (gcd r2,s2,Amp)),r1,Amp is Element of Amp & 1. R is Element of Amp ) by Def8, Def12;
(1. R) * (gcd (r2 / (gcd r2,s2,Amp)),r1,Amp) = gcd (r2 / (gcd r2,s2,Amp)),r1,Amp by VECTSP_1:def 19;
then A18: 1. R divides gcd (r2 / (gcd r2,s2,Amp)),r1,Amp by Def1;
gcd (r2 / (gcd r2,s2,Amp)),r1,Amp divides r1 by Def12;
then gcd (r2 / (gcd r2,s2,Amp)),r1,Amp divides gcd r1,r2,Amp by A16, Def12;
then gcd (r2 / (gcd r2,s2,Amp)),r1,Amp is_associated_to 1. R by A1, A18, Def3;
hence gcd (r2 / (gcd r2,s2,Amp)),r1,Amp = 1. R by A17, Th22; :: thesis: verum

end;

then A19: gcd (r2 / (gcd r2,s2,Amp)),(r1 * (s2 / (gcd r2,s2,Amp))),Amp = gcd (r2 / (gcd r2,s2,Amp)),(s2 / (gcd r2,s2,Amp)),Amp by Th38;
A20: gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(r2 / (gcd r2,s2,Amp)),Amp = gcd (r1 * (s2 / (gcd r2,s2,Amp))),(r2 / (gcd r2,s2,Amp)),Amp by Th40;
gcd (r2 / (gcd r2,s2,Amp)),(s2 / (gcd r2,s2,Amp)),Amp = 1. R by A4, Th39;
then A21: gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),((gcd r2,s2,Amp) * (r2 / (gcd r2,s2,Amp))),Amp = gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(gcd r2,s2,Amp),Amp by A20, A19, Th30, Th38;
r2 * (s2 / (gcd r2,s2,Amp)) = ((1. R) * r2) * (s2 / (gcd r2,s2,Amp)) by VECTSP_1:def 19
.= (((gcd r2,s2,Amp) / (gcd r2,s2,Amp)) * r2) * (s2 / (gcd r2,s2,Amp)) by A4, Th9
.= (((gcd r2,s2,Amp) * r2) / (gcd r2,s2,Amp)) * (s2 / (gcd r2,s2,Amp)) by A4, A13, Th11
.= (s2 / (gcd r2,s2,Amp)) * ((gcd r2,s2,Amp) * (r2 / (gcd r2,s2,Amp))) by A14, A4, A13, Th11 ;
hence gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(r2 * (s2 / (gcd r2,s2,Amp))),Amp = gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(gcd r2,s2,Amp),Amp by A12, A21, Th38; :: thesis: verum