:: 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-2021 Association of Mizar Users

:: Theorems about Integral Domains

registration

cluster non empty right_unital commutative -> non empty left_unital for multLoopStr ;

coherence
for b₁ being non empty multLoopStr st b₁ is commutative & b₁ is right_unital holds
b₁ is left_unital

proof end;

end;

registration

cluster non empty right-distributive commutative -> non empty distributive for doubleLoopStr ;

coherence
for b₁ being non empty doubleLoopStr st b₁ is commutative & b₁ is right-distributive holds
b₁ is distributive

proof end;

cluster non empty left-distributive commutative -> non empty distributive for doubleLoopStr ;

coherence
for b₁ being non empty doubleLoopStr st b₁ is commutative & b₁ is left-distributive holds
b₁ is distributive

proof end;

end;

registration

cluster non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative -> for doubleLoopStr ;

coherence
for b₁ being Ring holds b₁ is well-unital ;

end;

registration

cluster F_Real -> domRing-like ;

coherence
F_Real is domRing-like

proof end;

end;

registration

cluster non empty non degenerated right_complementable almost_left_invertible strict well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like for doubleLoopStr ;

existence
ex b₁ being non empty doubleLoopStr st
( b₁ is strict & b₁ is Abelian & b₁ is add-associative & b₁ is right_zeroed & b₁ is right_complementable & b₁ is associative & b₁ is commutative & b₁ is domRing-like & b₁ is distributive & b₁ is well-unital & not b₁ is degenerated & b₁ is almost_left_invertible )

proof end;

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 ) )

proof end;

:: 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;

:: deftheorem 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 pred x divides y;
reflexivity
for x being Element of R holds (R,b₁,b₁)

proof end;

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;

:: deftheorem 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;

pred x is_associated_to y means :: 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 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 pred x is_associated_to y;
reflexivity
for x being Element of R holds (R,b₁,b₁)

proof end;

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 ;

func x / y -> Element of R means :Def4: :: GCD_1:def 4
it * y = x;

existence
ex b₁ being Element of R st b₁ * y = x

proof end;

uniqueness
for b₁, b₂ being Element of R st b₁ * y = x & b₂ * y = x holds
b₁ = b₂ 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 b₄ being Element of R holds
( b₄ = x / y iff b₄ * 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

proof end;

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

proof end;

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 by Th2;

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

proof end;

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 ) )

proof end;

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

proof end;

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 )

proof end;

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

proof end;

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

proof end;

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) ) )

proof end;

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

proof end;

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 )

proof end;

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)

proof end;

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

proof end;

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

proof end;

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

proof end;

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 ) )

proof end;

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 by Th15;

:: 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 b₁ being Subset of R st
for b being Element of R holds
( b in b₁ iff b is_associated_to a )

proof end;

uniqueness
for b₁, b₂ being Subset of R st ( for b being Element of R holds
( b in b₁ iff b is_associated_to a ) ) & ( for b being Element of R holds
( b in b₂ iff b is_associated_to a ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines Class GCD_1:def 5 :
for R being non empty multLoopStr
for a being Element of R
for b₃ being Subset of R holds
( b₃ = Class a iff for b being Element of R holds
( b in b₃ 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

proof end;

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

proof end;

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 b₁ being Subset-Family of R st
for A being Subset of R holds
( A in b₁ iff ex a being Element of R st A = Class a )

proof end;

uniqueness
for b₁, b₂ being Subset-Family of R st ( for A being Subset of R holds
( A in b₁ iff ex a being Element of R st A = Class a ) ) & ( for A being Subset of R holds
( A in b₂ iff ex a being Element of R st A = Class a ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines Classes GCD_1:def 6 :
for R being non empty multLoopStr
for b₂ being Subset-Family of R holds
( b₂ = Classes R iff for A being Subset of R holds
( A in b₂ 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

proof end;

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

proof end;

definition

let R be non empty well-unital associative 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 b₁ being non empty Subset of R st
( ( for a being Element of R ex z being Element of b₁ st z is_associated_to a ) & ( for x, y being Element of b₁ st x <> y holds
x is_not_associated_to y ) )

proof end;

end;

:: deftheorem Def7 defines Am GCD_1:def 7 :
for R being non empty well-unital associative multLoopStr
for b₂ being non empty Subset of R holds
( b₂ is Am of R iff ( ( for a being Element of R ex z being Element of b₂ st z is_associated_to a ) & ( for x, y being Element of b₂ st x <> y holds
x is_not_associated_to y ) ) );

definition

let R be non empty well-unital associative 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 b₁ being non empty Subset of R st
( b₁ is Am of R & 1. R in b₁ )

proof end;

end;

:: deftheorem Def8 defines AmpleSet GCD_1:def 8 :
for R being non empty well-unital associative multLoopStr
for b₂ being non empty Subset of R holds
( b₂ is AmpleSet of R iff ( b₂ is Am of R & 1. R in b₂ ) );

theorem Th22: :: GCD_1:22

for R being non empty well-unital associative 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 ) )

proof end;

theorem :: GCD_1:23

for R being non empty well-unital associative 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

proof end;

:: Definition of Normalform

definition

let R be non empty well-unital associative 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 b₁ being Element of R st
( b₁ in Amp & b₁ is_associated_to x )

proof end;

uniqueness
for b₁, b₂ being Element of R st b₁ in Amp & b₁ is_associated_to x & b₂ in Amp & b₂ is_associated_to x holds
b₁ = b₂ by Th4, Th22;

end;

:: deftheorem Def9 defines NF GCD_1:def 9 :
for R being non empty well-unital associative multLoopStr
for Amp being AmpleSet of R
for x, b₄ being Element of R holds
( b₄ = NF (x,Amp) iff ( b₄ in Amp & b₄ 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 )

proof end;

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 well-unital associative 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;

:: deftheorem defines multiplicative GCD_1:def 10 :
for R being non empty well-unital associative 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

proof end;

:: Definition of GCD-Domain

definition

let R be non empty multLoopStr ;

attr R 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 ) ) ) )

per cases ( ( x <> 0. F & y <> 0. F ) or x = 0. F or y = 0. F ) ;

case A1: ( 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 ) ) )

per cases ( 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 ; :: thesis: verum

end;

case A4: 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 ;
hence zz divides 1_ F by A1, A4; :: thesis: verum

end;

end;

end;

hence zz divides 1_ F by A3; :: thesis: verum

end;

y = (1_ F) * y ;
then A5: 1_ F divides y ;
x = (1_ F) * x ;
then 1_ F 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 A5, A2; :: thesis: verum

end;

case A6: 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 ;
then A7: y divides 0. F ;
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;

case A8: 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 ;
then A9: x divides 0. F ;
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 V45() right_complementable right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed unital associative commutative domRing-like gcd-like for doubleLoopStr ;

existence
ex b₁ being domRing st b₁ is gcd-like

proof end;

end;

registration

cluster non empty well-unital associative commutative gcd-like for multLoopStr ;

existence
ex b₁ being non empty multLoopStr st
( b₁ is gcd-like & b₁ is associative & b₁ is commutative & b₁ is well-unital )

proof end;

end;

registration

cluster non empty well-unital associative commutative gcd-like for multLoopStr_0 ;

existence
ex b₁ being non empty multLoopStr_0 st
( b₁ is gcd-like & b₁ is associative & b₁ is commutative & b₁ is well-unital )

proof end;

end;

registration

cluster non empty right_complementable almost_left_invertible right-distributive left-distributive well-unital left_unital add-associative right_zeroed commutative -> non empty right_complementable almost_left_invertible right-distributive left-distributive well-unital left_unital add-associative right_zeroed commutative gcd-like for doubleLoopStr ;

coherence
for b₁ being non empty right_complementable almost_left_invertible right-distributive left-distributive well-unital left_unital add-associative right_zeroed commutative doubleLoopStr holds b₁ is gcd-like

proof end;

end;

registration

cluster non empty non degenerated right_complementable well-unital distributive Abelian add-associative right_zeroed unital associative commutative domRing-like gcd-like for doubleLoopStr ;

existence
ex b₁ being non empty doubleLoopStr st
( b₁ is gcd-like & b₁ is associative & b₁ is commutative & b₁ is well-unital & b₁ is domRing-like & b₁ is unital & b₁ is distributive & not b₁ is degenerated & b₁ is Abelian & b₁ is add-associative & b₁ is right_zeroed & b₁ is right_complementable )

proof end;

end;

definition

mode gcdDomain is non degenerated commutative domRing-like gcd-like Ring;

end;

definition

let R be non empty well-unital associative 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 b₁ being Element of R st
( b₁ in Amp & b₁ divides x & b₁ divides y & ( for z being Element of R st z divides x & z divides y holds
z divides b₁ ) )

proof end;

uniqueness
for b₁, b₂ being Element of R st b₁ in Amp & b₁ divides x & b₁ divides y & ( for z being Element of R st z divides x & z divides y holds
z divides b₁ ) & b₂ in Amp & b₂ divides x & b₂ divides y & ( for z being Element of R st z divides x & z divides y holds
z divides b₂ ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def12 defines gcd GCD_1:def 12 :
for R being non empty well-unital associative gcd-like multLoopStr
for Amp being AmpleSet of R
for x, y, b₅ being Element of R holds
( b₅ = gcd (x,y,Amp) iff ( b₅ in Amp & b₅ divides x & b₅ divides y & ( for z being Element of R st z divides x & z divides y holds
z divides b₅ ) ) );

:: 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 )

proof end;

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)

proof end;

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) )

proof end;

theorem Th31: :: GCD_1:31

for R being gcdDomain
for Amp being AmpleSet of R holds gcd ((0. R),(0. R),Amp) = 0. R

proof end;

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 )

proof end;

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 ) )

proof end;

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) )

proof end;

:: 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)

proof end;

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))

proof end;

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)

proof end;

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

proof end;

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)

proof end;

:: Brown & Henrici
:: 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)

proof end;

:: 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

proof end;

:: Properties of the Algorithms

definition

let R be non empty well-unital associative gcd-like 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;

:: deftheorem defines are_canonical_wrt GCD_1:def 13 :
for R being non empty well-unital associative 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

proof end;

definition

let R be non empty well-unital associative gcd-like 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;

:: deftheorem defines are_co-prime GCD_1:def 14 :
for R being non empty well-unital associative 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 pred x,y are_co-prime ;
symmetry
for x, y being Element of R st (R,b₁,b₂) holds
(R,b₂,b₁)

proof end;

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

proof end;

definition

let R be non empty well-unital associative gcd-like 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;

:: deftheorem defines are_normalized_wrt GCD_1:def 15 :
for R being non empty well-unital associative 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 b₁ being Element of R holds
( ( r1 = 0. R & s1 = 0. R implies ( b₁ = s1 iff b₁ = r1 ) ) & ( r1 = 0. R & gcd (r2,s2,Amp) = 1. R implies ( b₁ = s1 iff b₁ = (r1 * s2) + (r2 * s1) ) ) & ( r1 = 0. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies ( b₁ = s1 iff b₁ = 0. R ) ) & ( s1 = 0. R & gcd (r2,s2,Amp) = 1. R implies ( b₁ = r1 iff b₁ = (r1 * s2) + (r2 * s1) ) ) & ( s1 = 0. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies ( b₁ = r1 iff b₁ = 0. R ) ) & ( gcd (r2,s2,Amp) = 1. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies ( b₁ = (r1 * s2) + (r2 * s1) iff b₁ = 0. R ) ) )

proof end;

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 b₁ being Element of R holds
( ( r1 = 0. R & s1 = 0. R implies ( b₁ = s2 iff b₁ = r2 ) ) & ( r1 = 0. R & gcd (r2,s2,Amp) = 1. R implies ( b₁ = s2 iff b₁ = r2 * s2 ) ) & ( r1 = 0. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies ( b₁ = s2 iff b₁ = 1. R ) ) & ( s1 = 0. R & gcd (r2,s2,Amp) = 1. R implies ( b₁ = r2 iff b₁ = r2 * s2 ) ) & ( s1 = 0. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies ( b₁ = r2 iff b₁ = 1. R ) ) & ( gcd (r2,s2,Amp) = 1. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies ( b₁ = r2 * s2 iff b₁ = 1. R ) ) )

proof end;

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

proof end;

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))

proof end;

:: 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 b₁ being Element of R holds
( ( ( r1 = 0. R or s1 = 0. R ) & r2 = 1. R & s2 = 1. R implies ( b₁ = 0. R iff b₁ = r1 * s1 ) ) & ( ( r1 = 0. R or s1 = 0. R ) & s2 <> 0. R & r2 = 1. R implies ( b₁ = 0. R iff b₁ = (r1 * s1) / (gcd (r1,s2,Amp)) ) ) & ( ( r1 = 0. R or s1 = 0. R ) & r2 <> 0. R & s2 = 1. R implies ( b₁ = 0. R iff b₁ = (r1 * s1) / (gcd (s1,r2,Amp)) ) ) & ( r2 = 1. R & s2 = 1. R & s2 <> 0. R & r2 = 1. R implies ( b₁ = r1 * s1 iff b₁ = (r1 * s1) / (gcd (r1,s2,Amp)) ) ) & ( r2 = 1. R & s2 = 1. R & r2 <> 0. R & s2 = 1. R implies ( b₁ = r1 * s1 iff b₁ = (r1 * s1) / (gcd (s1,r2,Amp)) ) ) & ( s2 <> 0. R & r2 = 1. R & r2 <> 0. R & s2 = 1. R implies ( b₁ = (r1 * s1) / (gcd (r1,s2,Amp)) iff b₁ = (r1 * s1) / (gcd (s1,r2,Amp)) ) ) )

proof end;

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 b₁ being Element of R holds
( ( ( r1 = 0. R or s1 = 0. R ) & r2 = 1. R & s2 = 1. R implies ( b₁ = 1. R iff b₁ = 1. R ) ) & ( ( r1 = 0. R or s1 = 0. R ) & s2 <> 0. R & r2 = 1. R implies ( b₁ = 1. R iff b₁ = s2 / (gcd (r1,s2,Amp)) ) ) & ( ( r1 = 0. R or s1 = 0. R ) & r2 <> 0. R & s2 = 1. R implies ( b₁ = 1. R iff b₁ = r2 / (gcd (s1,r2,Amp)) ) ) & ( r2 = 1. R & s2 = 1. R & s2 <> 0. R & r2 = 1. R implies ( b₁ = 1. R iff b₁ = s2 / (gcd (r1,s2,Amp)) ) ) & ( r2 = 1. R & s2 = 1. R & r2 <> 0. R & s2 = 1. R implies ( b₁ = 1. R iff b₁ = r2 / (gcd (s1,r2,Amp)) ) ) & ( s2 <> 0. R & r2 = 1. R & r2 <> 0. R & s2 = 1. R implies ( b₁ = s2 / (gcd (r1,s2,Amp)) iff b₁ = r2 / (gcd (s1,r2,Amp)) ) ) )

proof end;

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

proof end;

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)

proof end;

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) "

proof end;