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 & s2 <> 0. R holds
gcd (((r1 / (gcd (r1,s2,Amp))) * (s1 / (gcd (s1,r2,Amp)))),((r2 / (gcd (s1,r2,Amp))) * (s2 / (gcd (r1,s2,Amp)))),Amp) = 1. R
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 & s2 <> 0. R holds
gcd (((r1 / (gcd (r1,s2,Amp))) * (s1 / (gcd (s1,r2,Amp)))),((r2 / (gcd (s1,r2,Amp))) * (s2 / (gcd (r1,s2,Amp)))),Amp) = 1. R
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 & s2 <> 0. R implies gcd (((r1 / (gcd (r1,s2,Amp))) * (s1 / (gcd (s1,r2,Amp)))),((r2 / (gcd (s1,r2,Amp))) * (s2 / (gcd (r1,s2,Amp)))),Amp) = 1. R )
assume that
A1: gcd (r1,r2,Amp) = 1. R and
A2: gcd (s1,s2,Amp) = 1. R and
A3: r2 <> 0. R and
A4: s2 <> 0. R ; :: thesis: gcd (((r1 / (gcd (r1,s2,Amp))) * (s1 / (gcd (s1,r2,Amp)))),((r2 / (gcd (s1,r2,Amp))) * (s2 / (gcd (r1,s2,Amp)))),Amp) = 1. R
set d1 = gcd (r1,s2,Amp);
A5: gcd (r1,s2,Amp) <> 0. R by A4, Th34;
set d2 = gcd (s1,r2,Amp);
set s19 = s1 / (gcd (s1,r2,Amp));
set r29 = r2 / (gcd (s1,r2,Amp));
A6: gcd (s1,r2,Amp) <> 0. R by A3, Th34;
then A7: gcd ((s1 / (gcd (s1,r2,Amp))),(r2 / (gcd (s1,r2,Amp))),Amp) = 1. R by Th39;
set r19 = r1 / (gcd (r1,s2,Amp));
A8: gcd ((r1 / (gcd (r1,s2,Amp))),(r2 / (gcd (s1,r2,Amp))),Amp) divides r2 / (gcd (s1,r2,Amp)) by Def12;
gcd (s1,r2,Amp) divides r2 by Def12;
then (r2 / (gcd (s1,r2,Amp))) * (gcd (s1,r2,Amp)) = r2 by A6, Def4;
then r2 / (gcd (s1,r2,Amp)) divides r2 by Def1;
then A9: gcd ((r1 / (gcd (r1,s2,Amp))),(r2 / (gcd (s1,r2,Amp))),Amp) divides r2 by A8, Th2;
A10: ( gcd ((r1 / (gcd (r1,s2,Amp))),(r2 / (gcd (s1,r2,Amp))),Amp) is Element of Amp & 1. R is Element of Amp ) by Def8, Def12;
gcd (r1,s2,Amp) divides r1 by Def12;
then (r1 / (gcd (r1,s2,Amp))) * (gcd (r1,s2,Amp)) = r1 by A5, Def4;
then A11: r1 / (gcd (r1,s2,Amp)) divides r1 by Def1;
(1. R) * (gcd ((r1 / (gcd (r1,s2,Amp))),(r2 / (gcd (s1,r2,Amp))),Amp)) = gcd ((r1 / (gcd (r1,s2,Amp))),(r2 / (gcd (s1,r2,Amp))),Amp) by VECTSP_1:def 19;
then A12: 1. R divides gcd ((r1 / (gcd (r1,s2,Amp))),(r2 / (gcd (s1,r2,Amp))),Amp) by Def1;
gcd ((r1 / (gcd (r1,s2,Amp))),(r2 / (gcd (s1,r2,Amp))),Amp) divides r1 / (gcd (r1,s2,Amp)) by Def12;
then gcd ((r1 / (gcd (r1,s2,Amp))),(r2 / (gcd (s1,r2,Amp))),Amp) divides r1 by A11, Th2;
then gcd ((r1 / (gcd (r1,s2,Amp))),(r2 / (gcd (s1,r2,Amp))),Amp) divides gcd (r1,r2,Amp) by A9, Def12;
then gcd ((r1 / (gcd (r1,s2,Amp))),(r2 / (gcd (s1,r2,Amp))),Amp) is_associated_to 1. R by A1, A12, Def3;
then gcd ((r1 / (gcd (r1,s2,Amp))),(r2 / (gcd (s1,r2,Amp))),Amp) = 1. R by A10, Th22;
then A13: gcd ((r2 / (gcd (s1,r2,Amp))),(r1 / (gcd (r1,s2,Amp))),Amp) = 1. R by Th30;
set s29 = s2 / (gcd (r1,s2,Amp));
A14: gcd ((s1 / (gcd (s1,r2,Amp))),(s2 / (gcd (r1,s2,Amp))),Amp) divides s2 / (gcd (r1,s2,Amp)) by Def12;
gcd (r1,s2,Amp) divides s2 by Def12;
then (s2 / (gcd (r1,s2,Amp))) * (gcd (r1,s2,Amp)) = s2 by A5, Def4;
then s2 / (gcd (r1,s2,Amp)) divides s2 by Def1;
then A15: gcd ((s1 / (gcd (s1,r2,Amp))),(s2 / (gcd (r1,s2,Amp))),Amp) divides s2 by A14, Th2;
A16: ( gcd ((s1 / (gcd (s1,r2,Amp))),(s2 / (gcd (r1,s2,Amp))),Amp) is Element of Amp & 1. R is Element of Amp ) by Def8, Def12;
gcd (s1,r2,Amp) divides s1 by Def12;
then (s1 / (gcd (s1,r2,Amp))) * (gcd (s1,r2,Amp)) = s1 by A6, Def4;
then A17: s1 / (gcd (s1,r2,Amp)) divides s1 by Def1;
(1. R) * (gcd ((s1 / (gcd (s1,r2,Amp))),(s2 / (gcd (r1,s2,Amp))),Amp)) = gcd ((s1 / (gcd (s1,r2,Amp))),(s2 / (gcd (r1,s2,Amp))),Amp) by VECTSP_1:def 19;
then A18: 1. R divides gcd ((s1 / (gcd (s1,r2,Amp))),(s2 / (gcd (r1,s2,Amp))),Amp) by Def1;
gcd ((s1 / (gcd (s1,r2,Amp))),(s2 / (gcd (r1,s2,Amp))),Amp) divides s1 / (gcd (s1,r2,Amp)) by Def12;
then gcd ((s1 / (gcd (s1,r2,Amp))),(s2 / (gcd (r1,s2,Amp))),Amp) divides s1 by A17, Th2;
then gcd ((s1 / (gcd (s1,r2,Amp))),(s2 / (gcd (r1,s2,Amp))),Amp) divides gcd (s1,s2,Amp) by A15, Def12;
then gcd ((s1 / (gcd (s1,r2,Amp))),(s2 / (gcd (r1,s2,Amp))),Amp) is_associated_to 1. R by A2, A18, Def3;
then A19: gcd ((s1 / (gcd (s1,r2,Amp))),(s2 / (gcd (r1,s2,Amp))),Amp) = 1. R by A16, Th22;
A20: gcd ((s2 / (gcd (r1,s2,Amp))),(r1 / (gcd (r1,s2,Amp))),Amp) = gcd ((r1 / (gcd (r1,s2,Amp))),(s2 / (gcd (r1,s2,Amp))),Amp) by Th30
.= 1. R by A5, Th39 ;
gcd (((r1 / (gcd (r1,s2,Amp))) * (s1 / (gcd (s1,r2,Amp)))),(r2 / (gcd (s1,r2,Amp))),Amp) = gcd ((r2 / (gcd (s1,r2,Amp))),((r1 / (gcd (r1,s2,Amp))) * (s1 / (gcd (s1,r2,Amp)))),Amp) by Th30
.= gcd ((r2 / (gcd (s1,r2,Amp))),(s1 / (gcd (s1,r2,Amp))),Amp) by A13, Th38
.= 1. R by A7, Th30 ;
then gcd (((r1 / (gcd (r1,s2,Amp))) * (s1 / (gcd (s1,r2,Amp)))),((r2 / (gcd (s1,r2,Amp))) * (s2 / (gcd (r1,s2,Amp)))),Amp) = gcd (((r1 / (gcd (r1,s2,Amp))) * (s1 / (gcd (s1,r2,Amp)))),(s2 / (gcd (r1,s2,Amp))),Amp) by Th38
.= gcd ((s2 / (gcd (r1,s2,Amp))),((r1 / (gcd (r1,s2,Amp))) * (s1 / (gcd (s1,r2,Amp)))),Amp) by Th30
.= gcd ((s2 / (gcd (r1,s2,Amp))),(s1 / (gcd (s1,r2,Amp))),Amp) by A20, Th38
.= 1. R by A19, Th30 ;
hence gcd (((r1 / (gcd (r1,s2,Amp))) * (s1 / (gcd (s1,r2,Amp)))),((r2 / (gcd (s1,r2,Amp))) * (s2 / (gcd (r1,s2,Amp)))),Amp) = 1. R ; :: thesis: verum