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, Th33;
then A5: gcd ((r2 / (gcd (r2,s2,Amp))),(s2 / (gcd (r2,s2,Amp))),Amp) = 1. R by Th38;
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)) ;
(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 3
.= s2 by A6, A4, Def4 ;
then A8: gcd ((s2 / (gcd (r2,s2,Amp))),s1,Amp) divides s2 ;
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) ;
then A10: 1. R divides gcd ((s2 / (gcd (r2,s2,Amp))),s1,Amp) ;
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;
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 Th37;
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 Th39;
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 Th29
.= 1. R by A11, A5, Th29 ;
A13: gcd (r2,s2,Amp) divides (gcd (r2,s2,Amp)) * r2 ;
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)) ;
(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 3
.= r2 by A14, A4, Def4 ;
then A16: gcd ((r2 / (gcd (r2,s2,Amp))),r1,Amp) divides r2 ;
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) ;
then A18: 1. R divides gcd ((r2 / (gcd (r2,s2,Amp))),r1,Amp) ;
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;
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 Th37;
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 Th39;
gcd ((r2 / (gcd (r2,s2,Amp))),(s2 / (gcd (r2,s2,Amp))),Amp) = 1. R by A4, Th38;
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, Th29, Th37;
r2 * (s2 / (gcd (r2,s2,Amp))) = ((1. R) * r2) * (s2 / (gcd (r2,s2,Amp)))
.= (((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, Th37; :: thesis: verum