:: 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-2012 Association of Mizar Users begin :: Theorems about Integral Domains registration cluster non empty commutative right_unital -> non empty left_unital for multLoopStr ; coherence for b1 being non empty multLoopStr st b1 is commutative & b1 is right_unital holds b1 is left_unital proofend; end; registration cluster non empty commutative right-distributive -> non empty distributive for doubleLoopStr ; coherence for b1 being non empty doubleLoopStr st b1 is commutative & b1 is right-distributive holds b1 is distributive proofend; cluster non empty commutative left-distributive -> non empty distributive for doubleLoopStr ; coherence for b1 being non empty doubleLoopStr st b1 is commutative & b1 is left-distributive holds b1 is distributive proofend; end; registration cluster non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed -> for doubleLoopStr ; coherence for b1 being Ring holds b1 is well-unital ; end; registration cluster F_Real -> domRing-like ; coherence F_Real is domRing-like proofend; end; registration cluster non empty non degenerated right_complementable almost_left_invertible strict associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like for doubleLoopStr ; existence ex b1 being non empty doubleLoopStr st ( b1 is strict & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is associative & b1 is commutative & b1 is domRing-like & b1 is distributive & b1 is well-unital & not b1 is degenerated & b1 is almost_left_invertible ) proofend; end; theorem Th1: :: GCD_1:1 for R being commutative domRing-like Ring for a, b, c being Element of R st a <> 0. R holds ( ( a * b = a * c implies b = c ) & ( b * a = c * a implies b = c ) ) proofend; :: Definition of Divisibility definition let R be non empty multMagma ; let x, y be Element of R; predx divides y means :Def1: :: GCD_1:def 1 ex z being Element of R st y = x * z; end; :: 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 ); definition let R be non empty right_unital multLoopStr ; let x, y be Element of R; :: original:divides redefine predx divides y; reflexivity for x being Element of R holds (R,b1,b1) proofend; end; definition let R be non empty multLoopStr ; let x be Element of R; attrx is unital means :Def2: :: GCD_1:def 2 x divides 1. R; end; :: 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 ); definition let R be non empty multLoopStr ; let x, y be Element of R; predx is_associated_to y means :Def3: :: GCD_1:def 3 ( x divides y & y divides x ); symmetry for x, y being Element of R st x divides y & y divides x holds ( y divides x & x divides y ) ; end; :: 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 ) ); 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 non empty well-unital multLoopStr ; let x, y be Element of R; :: original:is_associated_to redefine predx is_associated_to y; reflexivity for x being Element of R holds (R,b1,b1) proofend; end; definition let R be commutative domRing-like Ring; let x, y be Element of R; assume A1: y divides x ; assume A2: y <> 0. R ; funcx / y -> Element of R means :Def4: :: GCD_1:def 4 it * y = x; existence ex b1 being Element of R st b1 * y = x proofend; uniqueness for b1, b2 being Element of R st b1 * y = x & b2 * y = x holds b1 = b2 by A2, Th1; end; :: 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 ); :: Some Lemmata about Divisibility theorem Th2: :: GCD_1:2 for R being non empty associative multLoopStr for a, b, c being Element of R st a divides b & b divides c holds a divides c proofend; theorem Th3: :: GCD_1:3 for R being non empty associative commutative multLoopStr for a, b, c, d being Element of R st b divides a & d divides c holds b * d divides a * c proofend; theorem Th4: :: GCD_1:4 for R being non empty associative multLoopStr for a, b, c being Element of R st a is_associated_to b & b is_associated_to c holds a is_associated_to c proofend; theorem Th5: :: GCD_1:5 for R being non empty associative multLoopStr for a, b, c being Element of R st a divides b holds c * a divides c * b proofend; theorem Th6: :: 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 ) ) proofend; theorem Th7: :: GCD_1:7 for R being non empty associative multLoopStr for a, b, c being Element of R st a divides b holds a divides b * c proofend; theorem Th8: :: GCD_1:8 for R being commutative domRing-like Ring for a, b being Element of R st b divides a & b <> 0. R holds ( a / b = 0. R iff a = 0. R ) proofend; theorem Th9: :: GCD_1:9 for R being commutative domRing-like Ring for a being Element of R st a <> 0. R holds a / a = 1. R proofend; theorem Th10: :: GCD_1:10 for R being non degenerated commutative domRing-like Ring for a being Element of R holds a / (1. R) = a proofend; theorem Th11: :: GCD_1:11 for R being commutative domRing-like Ring for a, b, c being Element of R st c <> 0. R holds ( ( 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) ) ) proofend; theorem Th12: :: GCD_1:12 for R being commutative domRing-like Ring for a, b, c being Element of R st c <> 0. R & c divides a & c divides b & c divides a + b holds (a / c) + (b / c) = (a + b) / c proofend; theorem :: GCD_1:13 for R being commutative domRing-like Ring for a, b, c being Element of R st c <> 0. R & c divides a & c divides b holds ( a / c = b / c iff a = b ) proofend; theorem Th14: :: GCD_1:14 for R being commutative domRing-like Ring for a, b, c, d being Element of R st b <> 0. R & d <> 0. R & b divides a & d divides c holds (a / b) * (c / d) = (a * c) / (b * d) proofend; theorem Th15: :: GCD_1:15 for R being commutative domRing-like Ring for a, b, c being Element of R st a <> 0. R & a * b divides a * c holds b divides c proofend; theorem :: GCD_1:16 for R being commutative domRing-like Ring for a being Element of R st a is_associated_to 0. R holds a = 0. R proofend; theorem Th17: :: GCD_1:17 for R being commutative domRing-like Ring for a, b being Element of R st a <> 0. R & a * b = a holds b = 1. R proofend; theorem Th18: :: GCD_1:18 for R being commutative domRing-like Ring for a, b being Element of R holds ( a is_associated_to b iff ex c being Element of R st ( c is unital & a * c = b ) ) proofend; theorem Th19: :: GCD_1:19 for R being commutative domRing-like Ring for a, b, c being Element of R st c <> 0. R & c * a is_associated_to c * b holds a is_associated_to b proofend; 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 :Def5: :: GCD_1:def 5 for b being Element of R holds ( b in it iff b is_associated_to a ); existence ex b1 being Subset of R st for b being Element of R holds ( b in b1 iff b is_associated_to a ) proofend; uniqueness for b1, b2 being Subset of R st ( for b being Element of R holds ( b in b1 iff b is_associated_to a ) ) & ( for b being Element of R holds ( b in b2 iff b is_associated_to a ) ) holds b1 = b2 proofend; end; :: 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 ) ); registration let R be non empty well-unital multLoopStr ; let a be Element of R; cluster Class a -> non empty ; coherence not Class a is empty proofend; end; theorem Th20: :: GCD_1:20 for R being non empty associative multLoopStr for a, b being Element of R st Class a meets Class b holds Class a = Class b proofend; definition let R be non empty multLoopStr ; func Classes R -> Subset-Family of R means :Def6: :: 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 ); existence ex b1 being Subset-Family of R st for A being Subset of R holds ( A in b1 iff ex a being Element of R st A = Class a ) proofend; uniqueness for b1, b2 being Subset-Family of R st ( for A being Subset of R holds ( A in b1 iff ex a being Element of R st A = Class a ) ) & ( for A being Subset of R holds ( A in b2 iff ex a being Element of R st A = Class a ) ) holds b1 = b2 proofend; end; :: 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 ) ); registration let R be non empty multLoopStr ; cluster Classes R -> non empty ; coherence not Classes R is empty proofend; end; theorem Th21: :: GCD_1:21 for R being non empty well-unital multLoopStr for X being Subset of R st X in Classes R holds not X is empty proofend; definition let R be non empty associative well-unital multLoopStr ; mode Am of R -> non empty Subset of R means :Def7: :: 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 st x <> y holds x is_not_associated_to y ) ); existence ex b1 being non empty Subset of R st ( ( for a being Element of R ex z being Element of b1 st z is_associated_to a ) & ( for x, y being Element of b1 st x <> y holds x is_not_associated_to y ) ) proofend; end; :: 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 ) ) ); definition let R be non empty associative well-unital multLoopStr ; mode AmpleSet of R -> non empty Subset of R means :Def8: :: GCD_1:def 8 ( it is Am of R & 1. R in it ); existence ex b1 being non empty Subset of R st ( b1 is Am of R & 1. R in b1 ) proofend; end; :: 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: :: GCD_1:22 for R being non empty associative well-unital 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 st x <> y holds x is_not_associated_to y ) ) proofend; theorem :: GCD_1:23 for R being non empty associative well-unital multLoopStr for Amp being AmpleSet of R for x, y being Element of Amp st x is_associated_to y holds x = y by Th22; theorem Th24: :: GCD_1:24 for R being commutative domRing-like Ring for Amp being AmpleSet of R holds 0. R is Element of Amp proofend; :: Definition of Normalform definition let R be non empty associative well-unital multLoopStr ; let Amp be AmpleSet of R; let x be Element of R; func NF (x,Amp) -> Element of R means :Def9: :: GCD_1:def 9 ( it in Amp & it is_associated_to x ); existence ex b1 being Element of R st ( b1 in Amp & b1 is_associated_to x ) proofend; uniqueness for b1, b2 being Element of R st b1 in Amp & b1 is_associated_to x & b2 in Amp & b2 is_associated_to x holds b1 = b2 by Th4, Th22; end; :: 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: :: GCD_1:25 for R being commutative domRing-like Ring for Amp being AmpleSet of R holds ( NF ((0. R),Amp) = 0. R & NF ((1. R),Amp) = 1. R ) proofend; theorem :: GCD_1:26 for R being commutative domRing-like Ring for Amp being AmpleSet of R for a being Element of R holds ( a in Amp iff a = NF (a,Amp) ) by Def9; :: Definition of multiplicative AmpleSet definition let R be non empty associative well-unital multLoopStr ; let Amp be AmpleSet of R; attrAmp is multiplicative means :Def10: :: GCD_1:def 10 for x, y being Element of Amp holds x * y in Amp; end; :: 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: :: GCD_1:27 for R being commutative domRing-like Ring for Amp being AmpleSet of R st Amp is multiplicative holds for x, y being Element of Amp st y divides x & y <> 0. R holds x / y in Amp proofend; begin :: Definition of GCD-Domain definition let R be non empty multLoopStr ; attrR is gcd-like means :Def11: :: 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; :: 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 ) ) ); Lm1: now__::_thesis:_for_F_being_Field for_x,_y_being_Element_of_F_ex_z_being_Element_of_F_st_ (_z_divides_x_&_z_divides_y_&_(_for_zz_being_Element_of_F_st_zz_divides_x_&_zz_divides_y_holds_ zz_divides_z_)_) let F be Field; ::_thesis: for x, y being Element of F ex z being Element of F st ( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds zz divides z ) ) let x, y be Element of F; ::_thesis: ex z being Element of F st ( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds zz divides z ) ) now__::_thesis:_(_(_x_<>_0._F_&_y_<>_0._F_&_ex_z_being_Element_of_F_st_ (_z_divides_x_&_z_divides_y_&_(_for_zz_being_Element_of_F_st_zz_divides_x_&_zz_divides_y_holds_ zz_divides_z_)_)_)_or_(_x_=_0._F_&_ex_z_being_Element_of_F_st_ (_z_divides_x_&_z_divides_y_&_(_for_zz_being_Element_of_F_st_zz_divides_x_&_zz_divides_y_holds_ zz_divides_z_)_)_)_or_(_y_=_0._F_&_ex_z_being_Element_of_F_st_ (_z_divides_x_&_z_divides_y_&_(_for_zz_being_Element_of_F_st_zz_divides_x_&_zz_divides_y_holds_ zz_divides_z_)_)_)_) percases ( ( x <> 0. F & y <> 0. F ) or x = 0. F or y = 0. F ) ; caseA1: ( x <> 0. F & y <> 0. F ) ; ::_thesis: ex z being Element of F st ( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds zz divides z ) ) A2: for zz being Element of F st zz divides x & zz divides y holds zz divides 1_ F proof let zz be Element of F; ::_thesis: ( zz divides x & zz divides y implies zz divides 1_ F ) assume that A3: zz divides x and zz divides y ; ::_thesis: zz divides 1_ F now__::_thesis:_(_(_zz_<>_0._F_&_zz_divides_1__F_)_or_(_zz_=_0._F_&_(_zz_divides_x_implies_zz_divides_1__F_)_)_) percases ( zz <> 0. F or zz = 0. F ) ; case zz <> 0. F ; ::_thesis: zz divides 1_ F then ex zz9 being Element of F st zz9 * zz = 1_ F by VECTSP_1:def_9; hence zz divides 1_ F by Def1; ::_thesis: verum end; caseA4: zz = 0. F ; ::_thesis: ( zz divides x implies zz divides 1_ F ) assume zz divides x ; ::_thesis: zz divides 1_ F then ex d being Element of F st zz * d = x by Def1; hence zz divides 1_ F by A1, A4, VECTSP_1:7; ::_thesis: verum end; end; end; hence zz divides 1_ F by A3; ::_thesis: verum end; y = (1_ F) * y by VECTSP_1:def_6; then A5: 1_ F divides y by Def1; x = (1_ F) * x by VECTSP_1:def_6; then 1_ F divides x by Def1; hence ex z being Element of F st ( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds zz divides z ) ) by A5, A2; ::_thesis: verum end; caseA6: x = 0. F ; ::_thesis: ex z being Element of F st ( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds zz divides z ) ) y * (0. F) = 0. F by VECTSP_1:7; then A7: y divides 0. F by Def1; for z being Element of F st z divides 0. F & z divides y holds z divides y ; hence ex z being Element of F st ( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds zz divides z ) ) by A6, A7; ::_thesis: verum end; caseA8: y = 0. F ; ::_thesis: ex z being Element of F st ( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds zz divides z ) ) x * (0. F) = 0. F by VECTSP_1:7; then A9: x divides 0. F by Def1; for z being Element of F st z divides x & z divides 0. F holds z divides x ; hence ex z being Element of F st ( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds zz divides z ) ) by A8, A9; ::_thesis: verum end; end; end; hence ex z being Element of F st ( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds zz divides z ) ) ; ::_thesis: verum end; registration cluster non empty non degenerated V46() right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like gcd-like for doubleLoopStr ; existence ex b1 being domRing st b1 is gcd-like proofend; end; registration cluster non empty associative commutative well-unital gcd-like for multLoopStr ; existence ex b1 being non empty multLoopStr st ( b1 is gcd-like & b1 is associative & b1 is commutative & b1 is well-unital ) proofend; end; registration cluster non empty associative commutative well-unital gcd-like for multLoopStr_0 ; existence ex b1 being non empty multLoopStr_0 st ( b1 is gcd-like & b1 is associative & b1 is commutative & b1 is well-unital ) proofend; end; registration cluster non empty right_complementable almost_left_invertible commutative right-distributive left-distributive well-unital left_unital add-associative right_zeroed -> non empty right_complementable almost_left_invertible commutative right-distributive left-distributive well-unital left_unital add-associative right_zeroed gcd-like for doubleLoopStr ; coherence for b1 being non empty right_complementable almost_left_invertible commutative right-distributive left-distributive well-unital left_unital add-associative right_zeroed doubleLoopStr holds b1 is gcd-like proofend; end; registration cluster non empty non degenerated right_complementable unital associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like gcd-like for doubleLoopStr ; existence ex b1 being non empty doubleLoopStr st ( b1 is gcd-like & b1 is associative & b1 is commutative & b1 is well-unital & b1 is domRing-like & b1 is unital & b1 is distributive & not b1 is degenerated & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable ) proofend; end; definition mode gcdDomain is non degenerated commutative domRing-like gcd-like Ring; end; definition let R be non empty associative well-unital gcd-like multLoopStr ; let Amp be AmpleSet of R; let x, y be Element of R; func gcd (x,y,Amp) -> Element of R means :Def12: :: 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 ) ); existence ex b1 being Element of R st ( b1 in Amp & b1 divides x & b1 divides y & ( for z being Element of R st z divides x & z divides y holds z divides b1 ) ) proofend; uniqueness for b1, b2 being Element of R st b1 in Amp & b1 divides x & b1 divides y & ( for z being Element of R st z divides x & z divides y holds z divides b1 ) & b2 in Amp & b2 divides x & b2 divides y & ( for z being Element of R st z divides x & z divides y holds z divides b2 ) holds b1 = b2 proofend; end; :: 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 ) ) ); :: Lemmata about GCD theorem Th28: :: GCD_1:28 for R being gcdDomain for Amp being AmpleSet of R for a, b, c being Element of R st c divides gcd (a,b,Amp) holds ( c divides a & c divides b ) proofend; theorem Th29: :: GCD_1:29 for R being gcdDomain for Amp being AmpleSet of R for a, b being Element of R holds gcd (a,b,Amp) = gcd (b,a,Amp) proofend; theorem Th30: :: GCD_1:30 for R being gcdDomain 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) ) proofend; theorem Th31: :: GCD_1:31 for R being gcdDomain for Amp being AmpleSet of R holds gcd ((0. R),(0. R),Amp) = 0. R proofend; theorem Th32: :: GCD_1:32 for R being gcdDomain 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 ) proofend; theorem Th33: :: GCD_1:33 for R being gcdDomain 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 ) ) proofend; theorem Th34: :: GCD_1:34 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) ) proofend; :: Main Theorems theorem Th35: :: GCD_1:35 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) proofend; theorem Th36: :: GCD_1:36 for R being gcdDomain 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)) proofend; theorem Th37: :: GCD_1:37 for R being gcdDomain for Amp being AmpleSet of R for a, b, c being Element of R st gcd (a,b,Amp) = 1. R holds gcd (a,(b * c),Amp) = gcd (a,c,Amp) proofend; theorem Th38: :: GCD_1:38 for R being gcdDomain for Amp being AmpleSet of R for a, b, c being Element of R st c = gcd (a,b,Amp) & c <> 0. R holds gcd ((a / c),(b / c),Amp) = 1. R proofend; theorem Th39: :: GCD_1:39 for R being gcdDomain 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) proofend; begin :: Brown & Henrici :: [WP: ] Brown_Theorem theorem Th40: :: GCD_1:40 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) proofend; :: [WP: ] Henrici_Theorem theorem Th41: :: GCD_1:41 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 proofend; begin :: Properties of the Algorithms definition let R be non empty associative well-unital gcd-like multLoopStr ; let Amp be AmpleSet of R; let x, y be Element of R; predx,y are_canonical_wrt Amp means :Def13: :: GCD_1:def 13 gcd (x,y,Amp) = 1. R; end; :: 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 Th42: :: GCD_1:42 for R being gcdDomain 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 proofend; definition let R be non empty associative well-unital gcd-like multLoopStr ; let x, y be Element of R; predx,y are_co-prime means :Def14: :: GCD_1:def 14 ex Amp being AmpleSet of R st gcd (x,y,Amp) = 1. R; end; :: 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 ); definition let R be gcdDomain; let x, y be Element of R; :: original:are_co-prime redefine predx,y are_co-prime ; symmetry for x, y being Element of R st (R,b1,b2) holds (R,b2,b1) proofend; end; theorem Th43: :: GCD_1:43 for R being gcdDomain for Amp being AmpleSet of R for x, y being Element of R st x,y are_co-prime holds gcd (x,y,Amp) = 1. R proofend; definition let R be non empty associative well-unital gcd-like multLoopStr_0 ; let Amp be AmpleSet of R; let x, y be Element of R; predx,y are_normalized_wrt Amp means :Def15: :: GCD_1:def 15 ( gcd (x,y,Amp) = 1. R & y in Amp & y <> 0. R ); end; :: 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 ) ); :: Addition 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: :: 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)); 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 ) ) ) proofend; 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: :: 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)); 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 ) ) ) proofend; 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 :: GCD_1:44 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 proofend; theorem :: GCD_1:45 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)) proofend; :: 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 :Def18: :: 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))); 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)) ) ) ) proofend; 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: :: 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))); 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)) ) ) ) proofend; 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 :: GCD_1:46 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 proofend; theorem :: GCD_1:47 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) proofend; theorem :: GCD_1:48 for F being non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr for x, y being Element of F holds ( (- x) * y = - (x * y) & x * (- y) = - (x * y) ) by VECTSP_1:8, VECTSP_1:9; 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) " proofend;