:: The correctness of the Generic Algorithms of Brown and Henrici
:: concerning Addition and Multiplication in Fraction Fields
:: by Christoph Schwarzweller
::
:: Received June 16, 1997
:: Copyright (c) 1997-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies BINOP_1, VECTSP_1, XBOOLE_0, ALGSTR_0, SUBSET_1, MESFUNC1,
RELAT_1, LATTICES, ARYTM_3, FUNCSDOM, VECTSP_2, SUPINF_2, CARD_1,
STRUCT_0, RLVECT_1, ARYTM_1, GROUP_1, EQREL_1, TARSKI, SETFAM_1,
MSSUBFAM, INT_2, GCD_1, FUNCT_7, NUMBERS;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, STRUCT_0, ALGSTR_0,
RLVECT_1, GROUP_1, VECTSP_2, VECTSP_1;
constructors BINOP_2, VECTSP_2, MONOID_0;
registrations XBOOLE_0, SUBSET_1, MEMBERED, STRUCT_0, VECTSP_1, MONOID_0,
XREAL_0;
requirements SUBSET, BOOLE;
begin :: Basics
reserve X,Y for set;
:: Theorems about Integral Domains
registration
cluster commutative right_unital -> left_unital for non empty multLoopStr;
end;
registration
cluster commutative right-distributive -> distributive for non empty
doubleLoopStr;
cluster commutative left-distributive -> distributive for non empty
doubleLoopStr;
end;
registration
cluster -> well-unital for Ring;
end;
registration
cluster F_Real -> domRing-like;
end;
registration
cluster strict Abelian add-associative right_zeroed right_complementable
associative commutative domRing-like distributive well-unital non degenerated
almost_left_invertible for non empty doubleLoopStr;
end;
reserve R for domRing-like commutative Ring;
reserve c for Element of R;
theorem :: GCD_1:1
for R being domRing-like commutative Ring for a,b,c being Element
of R holds a <> 0.R implies (a * b = a * c implies b = c) & (b * a = c * a
implies b = c);
:: Definition of Divisibility
definition
let R be non empty multMagma;
let x,y be Element of R;
pred x divides y means
:: GCD_1:def 1
ex z being Element of R st y = x * z;
end;
definition
let R be right_unital non empty multLoopStr;
let x,y be Element of R;
redefine pred x divides y;
reflexivity;
end;
definition
let R be non empty multLoopStr;
let x be Element of R;
attr x is unital means
:: GCD_1:def 2
x divides 1.R;
end;
definition
let R be non empty multLoopStr;
let x,y be Element of R;
pred x is_associated_to y means
:: GCD_1:def 3
x divides y & y divides x;
symmetry;
end;
notation
let R be non empty multLoopStr;
let x,y be Element of R;
antonym x is_not_associated_to y for x is_associated_to y;
end;
definition
let R be well-unital non empty multLoopStr;
let x,y be Element of R;
redefine pred x is_associated_to y;
reflexivity;
end;
definition
let R be domRing-like commutative Ring;
let x,y be Element of R;
assume
y divides x;
assume
y <> 0.R;
func x/y -> Element of R means
:: GCD_1:def 4
it * y = x;
end;
:: Some Lemmata about Divisibility
theorem :: GCD_1:2
for R being associative non empty multLoopStr for a,b,c being
Element of R holds a divides b & b divides c implies a divides c;
theorem :: GCD_1:3
for R being commutative associative non empty multLoopStr for a
,b,c,d being Element of R holds (b divides a & d divides c) implies (b * d)
divides (a * c);
theorem :: GCD_1:4
for R being associative non empty multLoopStr for a,b,c being
Element of R holds a is_associated_to b & b is_associated_to c implies a
is_associated_to c;
theorem :: GCD_1:5
for R being associative non empty multLoopStr for a,b,c being
Element of R holds a divides b implies c * a divides c * b;
theorem :: GCD_1:6
for R being non empty multLoopStr for a,b being Element of R
holds a divides a * b & (R is commutative implies b divides a * b);
theorem :: GCD_1:7
for R being associative non empty multLoopStr for a,b,c being
Element of R holds a divides b implies a divides b * c;
theorem :: GCD_1:8
for a,b being Element of R holds b divides a & b <> 0.R implies (
a/b = 0.R iff a = 0.R);
theorem :: GCD_1:9
for a being Element of R holds a <> 0.R implies a/a = 1.R;
theorem :: GCD_1:10
for R being non degenerated domRing-like commutative Ring for a
being Element of R holds a/1.R = a;
theorem :: GCD_1:11
for a,b,c being Element of R holds c <> 0.R implies ( c divides
(a * b) & c divides a implies (a * b) / c = (a / c) * b) & ( c divides (a * b)
& c divides b implies (a * b) / c = a * (b / c));
theorem :: GCD_1:12
for a,b,c being Element of R holds c <> 0.R & c divides a & c
divides b & c divides (a + b) implies (a/c) + (b/c) = (a + b)/c;
theorem :: GCD_1:13
for a,b,c being Element of R holds c <> 0.R & c divides a & c divides
b implies (a/c = b/c iff a = b);
theorem :: GCD_1:14
for a,b,c,d being Element of R holds b <> 0.R & d <> 0.R & b
divides a & d divides c implies (a/b) * (c/d) = (a * c) / (b * d);
theorem :: GCD_1:15
for a,b,c being Element of R holds a <> 0.R & (a * b) divides (a
* c) implies b divides c;
theorem :: GCD_1:16
for a being Element of R holds a is_associated_to 0.R implies a = 0.R;
theorem :: GCD_1:17
for a,b being Element of R holds a <> 0.R & a * b = a implies b = 1.R;
theorem :: GCD_1:18
for a,b being Element of R holds a is_associated_to b iff ex c
st c is unital & a * c = b;
theorem :: GCD_1:19
for a,b,c being Element of R holds c <> 0.R & c * a
is_associated_to c * b implies a is_associated_to b;
begin
:: Definition of Ample Set
definition
let R be non empty multLoopStr;
let a be Element of R;
func Class a -> Subset of R means
:: GCD_1:def 5
for b being Element of R holds b in it iff b is_associated_to a;
end;
registration
let R be well-unital non empty multLoopStr;
let a be Element of R;
cluster Class a -> non empty;
end;
theorem :: GCD_1:20
for R being associative non empty multLoopStr for a,b being
Element of R holds Class a meets Class b implies Class a = Class b;
definition
let R be non empty multLoopStr;
func Classes R -> Subset-Family of R means
:: GCD_1:def 6
for A being Subset of R
holds A in it iff ex a being Element of R st A = Class a;
end;
registration
let R be non empty multLoopStr;
cluster Classes R -> non empty;
end;
theorem :: GCD_1:21
for R being well-unital non empty multLoopStr for X being
Subset of R holds X in Classes R implies X is non empty;
definition
let R be associative well-unital non empty multLoopStr;
mode Am of R -> non empty Subset of R means
:: GCD_1:def 7
(for a being Element of R
ex z being Element of it st z is_associated_to a) & for x,y being Element of it
holds x <> y implies x is_not_associated_to y;
end;
definition
let R be associative well-unital non empty multLoopStr;
mode AmpleSet of R -> non empty Subset of R means
:: GCD_1:def 8
it is Am of R & 1.R in it;
end;
theorem :: GCD_1:22
for R being associative well-unital non empty multLoopStr for
Amp being AmpleSet of R holds (1.R in Amp) & (for a being Element of R ex z
being Element of Amp st z is_associated_to a) & (for x,y being Element of Amp
holds x <> y implies x is_not_associated_to y);
theorem :: GCD_1:23
for R being associative well-unital non empty multLoopStr for Amp
being AmpleSet of R for x,y being Element of Amp holds x is_associated_to y
implies x = y;
theorem :: GCD_1:24
for Amp being AmpleSet of R holds 0.R is Element of Amp;
:: Definition of Normalform
definition
let R be associative well-unital non empty multLoopStr;
let Amp be AmpleSet of R;
let x be Element of R;
func NF(x,Amp) -> Element of R means
:: GCD_1:def 9
it in Amp & it is_associated_to x;
end;
theorem :: GCD_1:25
for Amp being AmpleSet of R holds NF(0.R,Amp) = 0.R & NF(1.R,Amp ) = 1.R;
theorem :: GCD_1:26
for Amp being AmpleSet of R for a being Element of R holds a in Amp
iff a = NF(a,Amp);
:: Definition of multiplicative AmpleSet
definition
let R be associative well-unital non empty multLoopStr;
let Amp be AmpleSet of R;
attr Amp is multiplicative means
:: GCD_1:def 10
for x,y being Element of Amp holds x * y in Amp;
end;
theorem :: GCD_1:27
for Amp being AmpleSet of R holds Amp is multiplicative implies
for x,y being Element of Amp holds y divides x & y <> 0.R implies x/y in Amp;
begin
:: Definition of GCD-Domain
definition
let R be non empty multLoopStr;
attr R is gcd-like means
:: GCD_1:def 11
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;
end;
registration
cluster gcd-like for domRing;
end;
registration
cluster gcd-like associative commutative well-unital for
non empty multLoopStr;
end;
registration
cluster gcd-like associative commutative well-unital for non empty
multLoopStr_0;
end;
registration
cluster -> gcd-like for almost_left_invertible add-associative right_zeroed
right_complementable left_unital well-unital left-distributive
right-distributive commutative non empty doubleLoopStr;
end;
registration
cluster gcd-like associative commutative well-unital domRing-like unital
distributive non degenerated Abelian add-associative right_zeroed
right_complementable for non empty doubleLoopStr;
end;
definition
mode gcdDomain is gcd-like domRing-like non degenerated commutative Ring;
end;
definition
let R be gcd-like associative well-unital non empty multLoopStr;
let Amp be AmpleSet of R;
let x,y be Element of R;
func gcd(x,y,Amp) -> Element of R means
:: GCD_1:def 12
it in Amp & it divides x &
it divides y & for z being Element of R st z divides x & z divides y holds z
divides it;
end;
reserve R for gcdDomain;
:: Lemmata about GCD
theorem :: GCD_1:28
for Amp being AmpleSet of R for a,b,c being Element of R holds c
divides gcd(a,b,Amp) implies c divides a & c divides b;
theorem :: GCD_1:29
for Amp being AmpleSet of R for a,b being Element of R holds gcd
(a,b,Amp) = gcd(b,a,Amp);
theorem :: GCD_1:30
for Amp being AmpleSet of R for a being Element of R holds gcd(a
,0.R,Amp) = NF(a,Amp) & gcd(0.R,a,Amp) = NF(a,Amp);
theorem :: GCD_1:31
for Amp being AmpleSet of R holds gcd(0.R,0.R,Amp) = 0.R;
theorem :: GCD_1:32
for Amp being AmpleSet of R for a being Element of R holds gcd(a
,1.R,Amp) = 1.R & gcd(1.R,a,Amp) = 1.R;
theorem :: GCD_1:33
for Amp being AmpleSet of R for a,b being Element of R holds gcd
(a,b,Amp) = 0.R iff a = 0.R & b = 0.R;
theorem :: GCD_1:34
for Amp being AmpleSet of R for a,b,c being Element of R holds b
is_associated_to c implies gcd(a,b,Amp) is_associated_to gcd(a,c,Amp) & gcd(b,a
,Amp) is_associated_to gcd(c,a,Amp);
:: Main Theorems
theorem :: GCD_1:35
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 :: GCD_1:36
for Amp being AmpleSet of R for a,b,c being Element of R holds
gcd(a * c,b * c,Amp) is_associated_to (c * gcd(a,b,Amp));
theorem :: GCD_1:37
for Amp being AmpleSet of R for a,b,c being Element of R holds
gcd(a,b,Amp) = 1.R implies gcd(a,(b * c),Amp) = gcd(a,c,Amp);
theorem :: GCD_1:38
for Amp being AmpleSet of R for a,b,c being Element of R holds c
= gcd(a,b,Amp) & c <> 0.R implies gcd((a/c),(b/c),Amp) = 1.R;
theorem :: GCD_1:39
for Amp being AmpleSet of R for a,b,c being Element of R holds
gcd((a + (b * c)),c,Amp) = gcd(a,c,Amp);
begin
:: Brown & Henrici
::$N Brown Theorem
theorem :: GCD_1:40
for Amp being AmpleSet of R for r1,r2,s1,s2 being Element of R
holds 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);
::$N Henrici Theorem
theorem :: GCD_1:41
for Amp being AmpleSet of R for r1,r2,s1,s2 being Element of R
holds 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;
begin
:: Properties of the Algorithms
definition
let R be gcd-like associative well-unital non empty multLoopStr;
let Amp be AmpleSet of R;
let x,y be Element of R;
pred x,y are_canonical_wrt Amp means
:: GCD_1:def 13
gcd(x,y,Amp) = 1.R;
end;
theorem :: GCD_1:42
for Amp,Amp9 being AmpleSet of R for x,y being Element of R st x
,y are_canonical_wrt Amp holds x,y are_canonical_wrt Amp9;
definition
let R be gcd-like associative well-unital non empty multLoopStr;
let x,y be Element of R;
pred x,y are_co-prime means
:: GCD_1:def 14
ex Amp being AmpleSet of R st gcd(x,y, Amp) = 1.R;
end;
definition
let R be gcdDomain;
let x,y be Element of R;
redefine pred x,y are_co-prime;
symmetry;
end;
theorem :: GCD_1:43
for Amp being AmpleSet of R for x,y being Element of R holds x,y
are_co-prime implies gcd(x,y,Amp) = 1.R;
definition
let R be gcd-like associative well-unital non empty multLoopStr_0;
let Amp be AmpleSet of R;
let x,y be Element of R;
pred x,y are_normalized_wrt Amp means
:: GCD_1:def 15
gcd(x,y,Amp) = 1.R & y in Amp & y <> 0.R;
end;
:: Addition
definition
let R be gcdDomain;
let Amp be AmpleSet of R;
let r1,r2,s1,s2 be Element of R;
assume that
r1,r2 are_co-prime and
s1,s2 are_co-prime and
r2 = NF(r2,Amp) and
s2 = NF(s2,Amp);
func add1(r1,r2,s1,s2,Amp) -> Element of R equals
:: GCD_1:def 16
s1 if r1 = 0.R, r1
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);
end;
definition
let R be gcdDomain;
let Amp be AmpleSet of R;
let r1,r2,s1,s2 be Element of R;
assume that
r1,r2 are_co-prime and
s1,s2 are_co-prime and
r2 = NF(r2,Amp) and
s2 = NF(s2,Amp);
func add2(r1,r2,s1,s2,Amp) -> Element of R equals
:: GCD_1:def 17
s2 if r1 = 0.R, r2
if s1 = 0.R, r2 * 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);
end;
theorem :: GCD_1:44
for Amp being AmpleSet of R for r1,r2,s1,s2 being Element of R holds
Amp is multiplicative & r1,r2 are_normalized_wrt Amp & s1,s2 are_normalized_wrt
Amp implies add1(r1,r2,s1,s2,Amp),add2(r1,r2,s1,s2,Amp) are_normalized_wrt Amp;
theorem :: GCD_1:45
for Amp being AmpleSet of R for r1,r2,s1,s2 being Element of R holds
r1,r2 are_normalized_wrt Amp & s1,s2 are_normalized_wrt Amp implies add1(r1,r2,
s1,s2,Amp) * (r2 * s2) = add2(r1,r2,s1,s2,Amp) * ((r1 * s2) + (s1 * r2));
:: Multiplication
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
:: GCD_1:def 18
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));
end;
definition
let R be gcdDomain;
let Amp be AmpleSet of R;
let r1,r2,s1,s2 be Element of R;
assume that
r1,r2 are_co-prime and
s1,s2 are_co-prime and
r2 = NF(r2,Amp) and
s2 = NF(s2,Amp);
func mult2(r1,r2,s1,s2,Amp) -> Element of R equals
:: GCD_1:def 19
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));
end;
theorem :: GCD_1:46
for Amp being AmpleSet of R for r1,r2,s1,s2 being Element of R holds
Amp is multiplicative & r1,r2 are_normalized_wrt Amp & s1,s2 are_normalized_wrt
Amp implies mult1(r1,r2,s1,s2,Amp),mult2(r1,r2,s1,s2,Amp) are_normalized_wrt
Amp;
theorem :: GCD_1:47
for Amp being AmpleSet of R for r1,r2,s1,s2 being Element of R holds
r1,r2 are_normalized_wrt Amp & s1,s2 are_normalized_wrt Amp implies mult1(r1,r2
,s1,s2,Amp) * (r2 * s2) = mult2(r1,r2,s1,s2,Amp) * (r1 * s1);
theorem :: GCD_1:48
for F be add-associative right_zeroed right_complementable Abelian
distributive non empty doubleLoopStr, x,y being Element of F holds (-x)*y = -
x*y & x*(-y) = -x*y;
theorem :: GCD_1:49
for F being almost_left_invertible commutative Ring for a, b being
Element of F st a <> 0.F & b <> 0.F holds a"*b" = (b*a)";