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