let R be gcdDomain; 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; 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; ( 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
; 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;
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;
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; verum