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 A1: ( gcd r1,r2,Amp = 1. R & gcd s1,s2,Amp = 1. R & r2 <> 0. R & 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;
set d2 = gcd s1,r2,Amp;
A2: gcd r1,s2,Amp <> 0. R by A1, Th34;
A3: gcd s1,r2,Amp <> 0. R by A1, Th34;
set r1' = r1 / (gcd r1,s2,Amp);
set s1' = s1 / (gcd s1,r2,Amp);
set r2' = r2 / (gcd s1,r2,Amp);
set s2' = s2 / (gcd r1,s2,Amp);
gcd r1,s2,Amp divides r1 by Def12;
then (r1 / (gcd r1,s2,Amp)) * (gcd r1,s2,Amp) = r1 by A2, Def4;
then A4: r1 / (gcd r1,s2,Amp) divides r1 by Def1;
gcd s1,r2,Amp divides r2 by Def12;
then (r2 / (gcd s1,r2,Amp)) * (gcd s1,r2,Amp) = r2 by A3, Def4;
then A5: r2 / (gcd s1,r2,Amp) divides r2 by Def1;
A6: gcd (r1 / (gcd r1,s2,Amp)),(r2 / (gcd s1,r2,Amp)),Amp divides r1 / (gcd r1,s2,Amp) by Def12;
A7: gcd (r1 / (gcd r1,s2,Amp)),(r2 / (gcd s1,r2,Amp)),Amp divides r2 / (gcd s1,r2,Amp) by Def12;
A8: gcd (r1 / (gcd r1,s2,Amp)),(r2 / (gcd s1,r2,Amp)),Amp divides r1 by A4, A6, Th2;
gcd (r1 / (gcd r1,s2,Amp)),(r2 / (gcd s1,r2,Amp)),Amp divides r2 by A5, A7, Th2;
then A9: gcd (r1 / (gcd r1,s2,Amp)),(r2 / (gcd s1,r2,Amp)),Amp divides gcd r1,r2,Amp by A8, Def12;
(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 1. R divides gcd (r1 / (gcd r1,s2,Amp)),(r2 / (gcd s1,r2,Amp)),Amp by Def1;
then A10: gcd (r1 / (gcd r1,s2,Amp)),(r2 / (gcd s1,r2,Amp)),Amp is_associated_to 1. R by A1, A9, Def3;
A11: gcd (r1 / (gcd r1,s2,Amp)),(r2 / (gcd s1,r2,Amp)),Amp is Element of Amp by Def12;
1. R is Element of Amp by Def8;
then gcd (r1 / (gcd r1,s2,Amp)),(r2 / (gcd s1,r2,Amp)),Amp = 1. R by A10, A11, Th22;
then A12: gcd (r2 / (gcd s1,r2,Amp)),(r1 / (gcd r1,s2,Amp)),Amp = 1. R by Th30;
gcd r1,s2,Amp divides s2 by Def12;
then (s2 / (gcd r1,s2,Amp)) * (gcd r1,s2,Amp) = s2 by A2, Def4;
then A13: s2 / (gcd r1,s2,Amp) divides s2 by Def1;
gcd s1,r2,Amp divides s1 by Def12;
then (s1 / (gcd s1,r2,Amp)) * (gcd s1,r2,Amp) = s1 by A3, Def4;
then A14: s1 / (gcd s1,r2,Amp) divides s1 by Def1;
A15: gcd (s1 / (gcd s1,r2,Amp)),(s2 / (gcd r1,s2,Amp)),Amp divides s1 / (gcd s1,r2,Amp) by Def12;
A16: gcd (s1 / (gcd s1,r2,Amp)),(s2 / (gcd r1,s2,Amp)),Amp divides s2 / (gcd r1,s2,Amp) by Def12;
A17: gcd (s1 / (gcd s1,r2,Amp)),(s2 / (gcd r1,s2,Amp)),Amp divides s1 by A14, A15, Th2;
gcd (s1 / (gcd s1,r2,Amp)),(s2 / (gcd r1,s2,Amp)),Amp divides s2 by A13, A16, Th2;
then A18: gcd (s1 / (gcd s1,r2,Amp)),(s2 / (gcd r1,s2,Amp)),Amp divides gcd s1,s2,Amp by A17, Def12;
(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 1. R divides gcd (s1 / (gcd s1,r2,Amp)),(s2 / (gcd r1,s2,Amp)),Amp by Def1;
then A19: gcd (s1 / (gcd s1,r2,Amp)),(s2 / (gcd r1,s2,Amp)),Amp is_associated_to 1. R by A1, A18, Def3;
A20: gcd (s1 / (gcd s1,r2,Amp)),(s2 / (gcd r1,s2,Amp)),Amp is Element of Amp by Def12;
1. R is Element of Amp by Def8;
then A21: gcd (s1 / (gcd s1,r2,Amp)),(s2 / (gcd r1,s2,Amp)),Amp = 1. R by A19, A20, Th22;
A22: 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 A2, Th39 ;
A23: gcd (s1 / (gcd s1,r2,Amp)),(r2 / (gcd s1,r2,Amp)),Amp = 1. R by A3, 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 A12, Th38
.= 1. R by A23, 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 A22, Th38
.= 1. R by A21, 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