begin
theorem Th1:
:: deftheorem Def1 defines divides GCD_1:def 1 :
for R being non empty multMagma
for x, y being Element of R holds
( x divides y iff ex z being Element of R st y = x * z );
:: deftheorem Def2 defines unital GCD_1:def 2 :
for R being non empty multLoopStr
for x being Element of R holds
( x is unital iff x divides 1. R );
:: deftheorem Def3 defines is_associated_to GCD_1:def 3 :
for R being non empty multLoopStr
for x, y being Element of R holds
( x is_associated_to y iff ( x divides y & y divides x ) );
:: deftheorem Def4 defines / GCD_1:def 4 :
for R being commutative domRing-like Ring
for x, y being Element of R st y divides x & y <> 0. R holds
for b4 being Element of R holds
( b4 = x / y iff b4 * y = x );
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem
theorem Th14:
theorem Th15:
theorem
theorem Th17:
theorem Th18:
theorem Th19:
begin
:: deftheorem Def5 defines Class GCD_1:def 5 :
for R being non empty multLoopStr
for a being Element of R
for b3 being Subset of R holds
( b3 = Class a iff for b being Element of R holds
( b in b3 iff b is_associated_to a ) );
theorem Th20:
:: deftheorem Def6 defines Classes GCD_1:def 6 :
for R being non empty multLoopStr
for b2 being Subset-Family of R holds
( b2 = Classes R iff for A being Subset of R holds
( A in b2 iff ex a being Element of R st A = Class a ) );
theorem Th21:
:: deftheorem Def7 defines Am GCD_1:def 7 :
for R being non empty associative well-unital multLoopStr
for b2 being non empty Subset of R holds
( b2 is Am of R iff ( ( for a being Element of R ex z being Element of b2 st z is_associated_to a ) & ( for x, y being Element of b2 st x <> y holds
x is_not_associated_to y ) ) );
:: deftheorem Def8 defines AmpleSet GCD_1:def 8 :
for R being non empty associative well-unital multLoopStr
for b2 being non empty Subset of R holds
( b2 is AmpleSet of R iff ( b2 is Am of R & 1. R in b2 ) );
theorem Th22:
theorem
theorem Th24:
:: deftheorem Def9 defines NF GCD_1:def 9 :
for R being non empty associative well-unital multLoopStr
for Amp being AmpleSet of R
for x, b4 being Element of R holds
( b4 = NF (x,Amp) iff ( b4 in Amp & b4 is_associated_to x ) );
theorem Th25:
theorem
:: deftheorem Def10 defines multiplicative GCD_1:def 10 :
for R being non empty associative well-unital multLoopStr
for Amp being AmpleSet of R holds
( Amp is multiplicative iff for x, y being Element of Amp holds x * y in Amp );
theorem Th27:
begin
:: deftheorem Def11 defines gcd-like GCD_1:def 11 :
for R being non empty multLoopStr holds
( R is gcd-like iff for x, y being Element of R ex z being Element of R st
( z divides x & z divides y & ( for zz being Element of R st zz divides x & zz divides y holds
zz divides z ) ) );
:: deftheorem Def12 defines gcd GCD_1:def 12 :
for R being non empty associative well-unital gcd-like multLoopStr
for Amp being AmpleSet of R
for x, y, b5 being Element of R holds
( b5 = gcd (x,y,Amp) iff ( b5 in Amp & b5 divides x & b5 divides y & ( for z being Element of R st z divides x & z divides y holds
z divides b5 ) ) );
theorem
canceled;
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
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 Th36:
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)
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
begin
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 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 Th42:
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
:: deftheorem Def13 defines are_canonical_wrt GCD_1:def 13 :
for R being non empty associative well-unital gcd-like multLoopStr
for Amp being AmpleSet of R
for x, y being Element of R holds
( x,y are_canonical_wrt Amp iff gcd (x,y,Amp) = 1. R );
theorem Th43:
:: deftheorem Def14 defines are_co-prime GCD_1:def 14 :
for R being non empty associative well-unital gcd-like multLoopStr
for x, y being Element of R holds
( x,y are_co-prime iff ex Amp being AmpleSet of R st gcd (x,y,Amp) = 1. R );
theorem Th44:
:: deftheorem Def15 defines are_normalized_wrt GCD_1:def 15 :
for R being non empty associative well-unital gcd-like multLoopStr_0
for Amp being AmpleSet of R
for x, y being Element of R holds
( x,y are_normalized_wrt Amp iff ( gcd (x,y,Amp) = 1. R & y in Amp & y <> 0. R ) );
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)
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem