Volume 9, 1997

University of Bialystok

Copyright (c) 1997 Association of Mizar Users

### The abstract of the Mizar article:

### The Correctness of the Generic Algorithms of Brown and Henrici Concerning Addition and Multiplication in Fraction Fields

**by****Christoph Schwarzweller**- Received June 16, 1997
- MML identifier: GCD_1

- [ Mizar article, MML identifier index ]

environ vocabulary BINOP_1, VECTSP_1, LATTICES, ALGSTR_2, VECTSP_2, FUNCSDOM, RLVECT_1, FUNCT_1, ARYTM_3, ARYTM_1, GROUP_1, EQREL_1, BOOLE, SETFAM_1, COHSP_1, INT_2, RELAT_1, GCD_1; notation TARSKI, XBOOLE_0, SUBSET_1, REAL_1, STRUCT_0, RLVECT_1, VECTSP_2, VECTSP_1, FUNCSDOM, BINOP_1; constructors FUNCSDOM, ALGSTR_2, VECTSP_2, REAL_1, MEMBERED; clusters STRUCT_0, VECTSP_1, VECTSP_2, SUBSET_1, ALGSTR_1, XBOOLE_0, MEMBERED; requirements SUBSET, BOOLE; begin :: Basics reserve X,Y for set; :: Theorems about Integral Domains :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: definition cluster commutative right_unital -> left_unital (non empty multLoopStr); end; definition cluster commutative right-distributive -> distributive (non empty doubleLoopStr); cluster commutative left-distributive -> distributive (non empty doubleLoopStr); end; definition cluster -> well-unital Ring; end; definition cluster F_Real -> domRing-like; end; definition cluster strict Abelian add-associative right_zeroed right_complementable associative commutative domRing-like distributive well-unital non degenerated Field-like (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 HGrStr; 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 well-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; antonym x is_not_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; definition 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; definition 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; definition cluster gcd-like domRing; end; definition cluster gcd-like associative commutative well-unital (non empty multLoopStr); end; definition cluster gcd-like associative commutative well-unital (non empty multLoopStr_0); end; definition cluster -> gcd-like (Field-like add-associative right_zeroed right_complementable left_unital right_unital left-distributive right-distributive commutative (non empty doubleLoopStr)); end; definition cluster gcd-like associative commutative well-unital domRing-like well-unital distributive non degenerated Abelian add-associative right_zeroed right_complementable (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 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: canceled; theorem :: GCD_1:29 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:30 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:31 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:32 for Amp being AmpleSet of R holds gcd(0.R,0.R,Amp) = 0.R; theorem :: GCD_1:33 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:34 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:35 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:36 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:37 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:38 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:39 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:40 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 :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 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 * (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 :: GCD_1:42 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:43 for Amp,Amp' being AmpleSet of R for x,y being Element of R holds x,y are_canonical_wrt Amp iff x,y are_canonical_wrt Amp'; 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:44 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 r1,r2 are_co-prime & s1,s2 are_co-prime & r2 = NF(r2,Amp) & 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 r1,r2 are_co-prime & s1,s2 are_co-prime & r2 = NF(r2,Amp) & 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:45 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: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 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 r1,r2 are_co-prime & s1,s2 are_co-prime & r2 = NF(r2,Amp) & 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:47 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:48 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) * (r2 * s2) = mult2(r1,r2,s1,s2,Amp) * (r1 * s1); canceled 2; theorem :: GCD_1:51 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; canceled; theorem :: GCD_1:53 for F being Field-like commutative Ring for a, b being Element of F st a <> 0.F & b <> 0.F holds a"*b" = (b*a)";

Back to top