begin
begin
begin
theorem Th34:
for
R being
gcdDomain for
Amp being
AmpleSet of
R for
a,
b,
c being
Element of
R st
b is_associated_to c holds
(
gcd (
a,
b,
Amp)
is_associated_to gcd (
a,
c,
Amp) &
gcd (
b,
a,
Amp)
is_associated_to gcd (
c,
a,
Amp) )
theorem Th35:
for
R being
gcdDomain for
Amp being
AmpleSet of
R for
a,
b,
c being
Element of
R holds
gcd (
(gcd (a,b,Amp)),
c,
Amp)
= gcd (
a,
(gcd (b,c,Amp)),
Amp)
begin
theorem Th40:
for
R being
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)
theorem Th41:
for
R being
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 &
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
begin
definition
let R be
gcdDomain;
let Amp be
AmpleSet of
R;
let r1,
r2,
s1,
s2 be
Element of
R;
assume that A1:
r1,
r2 are_co-prime
and A2:
s1,
s2 are_co-prime
and A3:
r2 = NF (
r2,
Amp)
and A4:
s2 = NF (
s2,
Amp)
;
func add1 (
r1,
r2,
s1,
s2,
Amp)
-> Element of
R equals :
Def16:
s1 if r1 = 0. Rr1 if s1 = 0. R(r1 * s2) + (r2 * s1) if gcd (
r2,
s2,
Amp)
= 1. R 0. R if (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R otherwise ((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))) / (gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp));
coherence
( ( r1 = 0. R implies s1 is Element of R ) & ( s1 = 0. R implies r1 is Element of R ) & ( gcd (r2,s2,Amp) = 1. R implies (r1 * s2) + (r2 * s1) is Element of R ) & ( (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies 0. R is Element of R ) & ( not r1 = 0. R & not s1 = 0. R & not gcd (r2,s2,Amp) = 1. R & not (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies ((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))) / (gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp)) is Element of R ) )
;
consistency
for b1 being Element of R holds
( ( r1 = 0. R & s1 = 0. R implies ( b1 = s1 iff b1 = r1 ) ) & ( r1 = 0. R & gcd (r2,s2,Amp) = 1. R implies ( b1 = s1 iff b1 = (r1 * s2) + (r2 * s1) ) ) & ( r1 = 0. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies ( b1 = s1 iff b1 = 0. R ) ) & ( s1 = 0. R & gcd (r2,s2,Amp) = 1. R implies ( b1 = r1 iff b1 = (r1 * s2) + (r2 * s1) ) ) & ( s1 = 0. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies ( b1 = r1 iff b1 = 0. R ) ) & ( gcd (r2,s2,Amp) = 1. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies ( b1 = (r1 * s2) + (r2 * s1) iff b1 = 0. R ) ) )
end;
::
deftheorem Def16 defines
add1 GCD_1:def 16 :
for R being gcdDomain
for Amp being AmpleSet of R
for r1, r2, s1, s2 being Element of R st r1,r2 are_co-prime & s1,s2 are_co-prime & r2 = NF (r2,Amp) & s2 = NF (s2,Amp) holds
( ( r1 = 0. R implies add1 (r1,r2,s1,s2,Amp) = s1 ) & ( s1 = 0. R implies add1 (r1,r2,s1,s2,Amp) = r1 ) & ( gcd (r2,s2,Amp) = 1. R implies add1 (r1,r2,s1,s2,Amp) = (r1 * s2) + (r2 * s1) ) & ( (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies add1 (r1,r2,s1,s2,Amp) = 0. R ) & ( not r1 = 0. R & not s1 = 0. R & not gcd (r2,s2,Amp) = 1. R & not (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies add1 (r1,r2,s1,s2,Amp) = ((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))) / (gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp)) ) );
definition
let R be
gcdDomain;
let Amp be
AmpleSet of
R;
let r1,
r2,
s1,
s2 be
Element of
R;
assume that A1:
r1,
r2 are_co-prime
and A2:
s1,
s2 are_co-prime
and A3:
r2 = NF (
r2,
Amp)
and A4:
s2 = NF (
s2,
Amp)
;
func add2 (
r1,
r2,
s1,
s2,
Amp)
-> Element of
R equals :
Def17:
s2 if r1 = 0. Rr2 if s1 = 0. Rr2 * s2 if gcd (
r2,
s2,
Amp)
= 1. R 1. R if (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R otherwise (r2 * (s2 / (gcd (r2,s2,Amp)))) / (gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp));
coherence
( ( r1 = 0. R implies s2 is Element of R ) & ( s1 = 0. R implies r2 is Element of R ) & ( gcd (r2,s2,Amp) = 1. R implies r2 * s2 is Element of R ) & ( (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies 1. R is Element of R ) & ( not r1 = 0. R & not s1 = 0. R & not gcd (r2,s2,Amp) = 1. R & not (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies (r2 * (s2 / (gcd (r2,s2,Amp)))) / (gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp)) is Element of R ) )
;
consistency
for b1 being Element of R holds
( ( r1 = 0. R & s1 = 0. R implies ( b1 = s2 iff b1 = r2 ) ) & ( r1 = 0. R & gcd (r2,s2,Amp) = 1. R implies ( b1 = s2 iff b1 = r2 * s2 ) ) & ( r1 = 0. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies ( b1 = s2 iff b1 = 1. R ) ) & ( s1 = 0. R & gcd (r2,s2,Amp) = 1. R implies ( b1 = r2 iff b1 = r2 * s2 ) ) & ( s1 = 0. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies ( b1 = r2 iff b1 = 1. R ) ) & ( gcd (r2,s2,Amp) = 1. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies ( b1 = r2 * s2 iff b1 = 1. R ) ) )
end;
::
deftheorem Def17 defines
add2 GCD_1:def 17 :
for R being gcdDomain
for Amp being AmpleSet of R
for r1, r2, s1, s2 being Element of R st r1,r2 are_co-prime & s1,s2 are_co-prime & r2 = NF (r2,Amp) & s2 = NF (s2,Amp) holds
( ( r1 = 0. R implies add2 (r1,r2,s1,s2,Amp) = s2 ) & ( s1 = 0. R implies add2 (r1,r2,s1,s2,Amp) = r2 ) & ( gcd (r2,s2,Amp) = 1. R implies add2 (r1,r2,s1,s2,Amp) = r2 * s2 ) & ( (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies add2 (r1,r2,s1,s2,Amp) = 1. R ) & ( not r1 = 0. R & not s1 = 0. R & not gcd (r2,s2,Amp) = 1. R & not (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies add2 (r1,r2,s1,s2,Amp) = (r2 * (s2 / (gcd (r2,s2,Amp)))) / (gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp)) ) );
theorem
for
R being
gcdDomain for
Amp being
AmpleSet of
R for
r1,
r2,
s1,
s2 being
Element of
R st
Amp is
multiplicative &
r1,
r2 are_normalized_wrt Amp &
s1,
s2 are_normalized_wrt Amp holds
add1 (
r1,
r2,
s1,
s2,
Amp),
add2 (
r1,
r2,
s1,
s2,
Amp)
are_normalized_wrt Amp
theorem
for
R being
gcdDomain for
Amp being
AmpleSet of
R for
r1,
r2,
s1,
s2 being
Element of
R st
r1,
r2 are_normalized_wrt Amp &
s1,
s2 are_normalized_wrt Amp holds
(add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2))
definition
let R be
gcdDomain;
let Amp be
AmpleSet of
R;
let r1,
r2,
s1,
s2 be
Element of
R;
func mult1 (
r1,
r2,
s1,
s2,
Amp)
-> Element of
R equals :
Def18:
0. R if (
r1 = 0. R or
s1 = 0. R )
r1 * s1 if (
r2 = 1. R &
s2 = 1. R )
(r1 * s1) / (gcd (r1,s2,Amp)) if (
s2 <> 0. R &
r2 = 1. R )
(r1 * s1) / (gcd (s1,r2,Amp)) if (
r2 <> 0. R &
s2 = 1. R )
otherwise (r1 / (gcd (r1,s2,Amp))) * (s1 / (gcd (s1,r2,Amp)));
coherence
( ( ( r1 = 0. R or s1 = 0. R ) implies 0. R is Element of R ) & ( r2 = 1. R & s2 = 1. R implies r1 * s1 is Element of R ) & ( s2 <> 0. R & r2 = 1. R implies (r1 * s1) / (gcd (r1,s2,Amp)) is Element of R ) & ( r2 <> 0. R & s2 = 1. R implies (r1 * s1) / (gcd (s1,r2,Amp)) is Element of R ) & ( r1 = 0. R or s1 = 0. R or ( r2 = 1. R & s2 = 1. R ) or ( s2 <> 0. R & r2 = 1. R ) or ( r2 <> 0. R & s2 = 1. R ) or (r1 / (gcd (r1,s2,Amp))) * (s1 / (gcd (s1,r2,Amp))) is Element of R ) )
;
consistency
for b1 being Element of R holds
( ( ( r1 = 0. R or s1 = 0. R ) & r2 = 1. R & s2 = 1. R implies ( b1 = 0. R iff b1 = r1 * s1 ) ) & ( ( r1 = 0. R or s1 = 0. R ) & s2 <> 0. R & r2 = 1. R implies ( b1 = 0. R iff b1 = (r1 * s1) / (gcd (r1,s2,Amp)) ) ) & ( ( r1 = 0. R or s1 = 0. R ) & r2 <> 0. R & s2 = 1. R implies ( b1 = 0. R iff b1 = (r1 * s1) / (gcd (s1,r2,Amp)) ) ) & ( r2 = 1. R & s2 = 1. R & s2 <> 0. R & r2 = 1. R implies ( b1 = r1 * s1 iff b1 = (r1 * s1) / (gcd (r1,s2,Amp)) ) ) & ( r2 = 1. R & s2 = 1. R & r2 <> 0. R & s2 = 1. R implies ( b1 = r1 * s1 iff b1 = (r1 * s1) / (gcd (s1,r2,Amp)) ) ) & ( s2 <> 0. R & r2 = 1. R & r2 <> 0. R & s2 = 1. R implies ( b1 = (r1 * s1) / (gcd (r1,s2,Amp)) iff b1 = (r1 * s1) / (gcd (s1,r2,Amp)) ) ) )
end;
::
deftheorem Def18 defines
mult1 GCD_1:def 18 :
for R being gcdDomain
for Amp being AmpleSet of R
for r1, r2, s1, s2 being Element of R holds
( ( ( r1 = 0. R or s1 = 0. R ) implies mult1 (r1,r2,s1,s2,Amp) = 0. R ) & ( r2 = 1. R & s2 = 1. R implies mult1 (r1,r2,s1,s2,Amp) = r1 * s1 ) & ( s2 <> 0. R & r2 = 1. R implies mult1 (r1,r2,s1,s2,Amp) = (r1 * s1) / (gcd (r1,s2,Amp)) ) & ( r2 <> 0. R & s2 = 1. R implies mult1 (r1,r2,s1,s2,Amp) = (r1 * s1) / (gcd (s1,r2,Amp)) ) & ( r1 = 0. R or s1 = 0. R or ( r2 = 1. R & s2 = 1. R ) or ( s2 <> 0. R & r2 = 1. R ) or ( r2 <> 0. R & s2 = 1. R ) or mult1 (r1,r2,s1,s2,Amp) = (r1 / (gcd (r1,s2,Amp))) * (s1 / (gcd (s1,r2,Amp))) ) );
definition
let R be
gcdDomain;
let Amp be
AmpleSet of
R;
let r1,
r2,
s1,
s2 be
Element of
R;
assume that A1:
r1,
r2 are_co-prime
and A2:
s1,
s2 are_co-prime
and A3:
r2 = NF (
r2,
Amp)
and A4:
s2 = NF (
s2,
Amp)
;
func mult2 (
r1,
r2,
s1,
s2,
Amp)
-> Element of
R equals :
Def19:
1. R if (
r1 = 0. R or
s1 = 0. R )
1. R if (
r2 = 1. R &
s2 = 1. R )
s2 / (gcd (r1,s2,Amp)) if (
s2 <> 0. R &
r2 = 1. R )
r2 / (gcd (s1,r2,Amp)) if (
r2 <> 0. R &
s2 = 1. R )
otherwise (r2 / (gcd (s1,r2,Amp))) * (s2 / (gcd (r1,s2,Amp)));
coherence
( ( ( r1 = 0. R or s1 = 0. R ) implies 1. R is Element of R ) & ( r2 = 1. R & s2 = 1. R implies 1. R is Element of R ) & ( s2 <> 0. R & r2 = 1. R implies s2 / (gcd (r1,s2,Amp)) is Element of R ) & ( r2 <> 0. R & s2 = 1. R implies r2 / (gcd (s1,r2,Amp)) is Element of R ) & ( r1 = 0. R or s1 = 0. R or ( r2 = 1. R & s2 = 1. R ) or ( s2 <> 0. R & r2 = 1. R ) or ( r2 <> 0. R & s2 = 1. R ) or (r2 / (gcd (s1,r2,Amp))) * (s2 / (gcd (r1,s2,Amp))) is Element of R ) )
;
consistency
for b1 being Element of R holds
( ( ( r1 = 0. R or s1 = 0. R ) & r2 = 1. R & s2 = 1. R implies ( b1 = 1. R iff b1 = 1. R ) ) & ( ( r1 = 0. R or s1 = 0. R ) & s2 <> 0. R & r2 = 1. R implies ( b1 = 1. R iff b1 = s2 / (gcd (r1,s2,Amp)) ) ) & ( ( r1 = 0. R or s1 = 0. R ) & r2 <> 0. R & s2 = 1. R implies ( b1 = 1. R iff b1 = r2 / (gcd (s1,r2,Amp)) ) ) & ( r2 = 1. R & s2 = 1. R & s2 <> 0. R & r2 = 1. R implies ( b1 = 1. R iff b1 = s2 / (gcd (r1,s2,Amp)) ) ) & ( r2 = 1. R & s2 = 1. R & r2 <> 0. R & s2 = 1. R implies ( b1 = 1. R iff b1 = r2 / (gcd (s1,r2,Amp)) ) ) & ( s2 <> 0. R & r2 = 1. R & r2 <> 0. R & s2 = 1. R implies ( b1 = s2 / (gcd (r1,s2,Amp)) iff b1 = r2 / (gcd (s1,r2,Amp)) ) ) )
end;
::
deftheorem Def19 defines
mult2 GCD_1:def 19 :
for R being gcdDomain
for Amp being AmpleSet of R
for r1, r2, s1, s2 being Element of R st r1,r2 are_co-prime & s1,s2 are_co-prime & r2 = NF (r2,Amp) & s2 = NF (s2,Amp) holds
( ( ( r1 = 0. R or s1 = 0. R ) implies mult2 (r1,r2,s1,s2,Amp) = 1. R ) & ( r2 = 1. R & s2 = 1. R implies mult2 (r1,r2,s1,s2,Amp) = 1. R ) & ( s2 <> 0. R & r2 = 1. R implies mult2 (r1,r2,s1,s2,Amp) = s2 / (gcd (r1,s2,Amp)) ) & ( r2 <> 0. R & s2 = 1. R implies mult2 (r1,r2,s1,s2,Amp) = r2 / (gcd (s1,r2,Amp)) ) & ( r1 = 0. R or s1 = 0. R or ( r2 = 1. R & s2 = 1. R ) or ( s2 <> 0. R & r2 = 1. R ) or ( r2 <> 0. R & s2 = 1. R ) or mult2 (r1,r2,s1,s2,Amp) = (r2 / (gcd (s1,r2,Amp))) * (s2 / (gcd (r1,s2,Amp))) ) );
theorem
for
R being
gcdDomain for
Amp being
AmpleSet of
R for
r1,
r2,
s1,
s2 being
Element of
R st
Amp is
multiplicative &
r1,
r2 are_normalized_wrt Amp &
s1,
s2 are_normalized_wrt Amp holds
mult1 (
r1,
r2,
s1,
s2,
Amp),
mult2 (
r1,
r2,
s1,
s2,
Amp)
are_normalized_wrt Amp
theorem
for
R being
gcdDomain for
Amp being
AmpleSet of
R for
r1,
r2,
s1,
s2 being
Element of
R st
r1,
r2 are_normalized_wrt Amp &
s1,
s2 are_normalized_wrt Amp holds
(mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1)