begin
theorem Th1:
:: deftheorem Def1 defines divides GCD_1:def 1 :
:: deftheorem Def2 defines unital GCD_1:def 2 :
:: deftheorem Def3 defines is_associated_to GCD_1:def 3 :
:: deftheorem Def4 defines / GCD_1:def 4 :
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 :
theorem Th20:
:: deftheorem Def6 defines Classes GCD_1:def 6 :
theorem Th21:
:: deftheorem Def7 defines Am GCD_1:def 7 :
:: deftheorem Def8 defines AmpleSet GCD_1:def 8 :
theorem Th22:
theorem
theorem Th24:
:: deftheorem Def9 defines NF GCD_1:def 9 :
theorem Th25:
theorem
:: deftheorem Def10 defines multiplicative GCD_1:def 10 :
theorem Th27:
begin
:: deftheorem Def11 defines gcd-like GCD_1:def 11 :
:: deftheorem Def12 defines gcd GCD_1:def 12 :
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 :
theorem Th43:
:: deftheorem Def14 defines are_co-prime GCD_1:def 14 :
theorem Th44:
:: deftheorem Def15 defines are_normalized_wrt GCD_1:def 15 :
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