:: 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 b1 being non empty multLoopStr st b1 is commutative & b1 is right_unital holds
b1 is left_unital
proof end;
end;

registration
cluster non empty right-distributive commutative -> non empty distributive for doubleLoopStr ;
coherence
for b1 being non empty doubleLoopStr st b1 is commutative & b1 is right-distributive holds
b1 is distributive
proof end;
cluster non empty left-distributive commutative -> non empty distributive for doubleLoopStr ;
coherence
for b1 being non empty doubleLoopStr st b1 is commutative & b1 is left-distributive holds
b1 is distributive
proof end;
end;

registration
cluster non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative -> 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
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 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 )
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,b1,b1)
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,b1,b1)
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 b1 being Element of R st b1 * y = x
proof end;
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
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 b1 being Subset of R st
for b being Element of R holds
( b in b1 iff b is_associated_to a )
proof end;
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
proof end;
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
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 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 )
proof end;
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
proof end;
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
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 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 ) )
proof end;
end;

:: deftheorem Def7 defines Am GCD_1:def 7 :
for R being non empty well-unital associative 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 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 b1 being non empty Subset of R st
( b1 is Am of R & 1. R in b1 )
proof end;
end;

:: deftheorem Def8 defines AmpleSet GCD_1:def 8 :
for R being non empty well-unital associative 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 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 b1 being Element of R st
( b1 in Amp & b1 is_associated_to x )
proof end;
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 well-unital associative 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 )
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 b1 being domRing st b1 is gcd-like
proof end;
end;

registration
cluster non empty well-unital associative commutative 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 )
proof end;
end;

registration
cluster non empty well-unital associative commutative 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 )
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 b1 being non empty right_complementable almost_left_invertible right-distributive left-distributive well-unital left_unital add-associative right_zeroed commutative doubleLoopStr holds b1 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 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 )
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 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 ) )
proof end;
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
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, 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 )
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
:: 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)
proof end;

:: 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
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,b1,b2) holds
(R,b2,b1)
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 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 ) ) )
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 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 ) ) )
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 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)) ) ) )
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 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)) ) ) )
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;