:: by Christoph Schwarzweller

::

:: Received June 16, 1997

:: Copyright (c) 1997-2021 Association of Mizar Users

:: Theorems about Integral Domains

registration

coherence

for b_{1} being non empty multLoopStr st b_{1} is commutative & b_{1} is right_unital holds

b_{1} is left_unital

end;
for b

b

proof end;

registration

coherence

for b_{1} being non empty doubleLoopStr st b_{1} is commutative & b_{1} is right-distributive holds

b_{1} is distributive

for b_{1} being non empty doubleLoopStr st b_{1} is commutative & b_{1} is left-distributive holds

b_{1} is distributive

end;
for b

b

proof end;

coherence for b

b

proof end;

registration

for b_{1} being Ring holds b_{1} is well-unital
;

end;

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

coherence for b

registration

ex b_{1} being non empty doubleLoopStr st

( b_{1} is strict & b_{1} is Abelian & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is associative & b_{1} is commutative & b_{1} is domRing-like & b_{1} is distributive & b_{1} is well-unital & not b_{1} is degenerated & b_{1} is almost_left_invertible )
end;

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

( b

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

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

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

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_{1},b_{1})

end;
let x, y be Element of R;

:: original: divides

redefine pred x divides y;

reflexivity

for x being Element of R holds (R,b

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

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;

symmetry

for x, y being Element of R st x divides y & y divides x holds

( y divides x & x divides y ) ;

end;
let x, y be Element of R;

symmetry

for x, y being Element of R st x divides y & y divides x holds

( y divides x & x divides y ) ;

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

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;
let x, y be Element of R;

antonym x is_not_associated_to y for x is_associated_to y;

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_{1},b_{1})

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

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

existence

ex b_{1} being Element of R st b_{1} * y = x

for b_{1}, b_{2} being Element of R st b_{1} * y = x & b_{2} * y = x holds

b_{1} = b_{2}
by A2, Th1;

end;
let x, y be Element of R;

assume A1: y divides x ;

assume A2: y <> 0. R ;

existence

ex b

proof end;

uniqueness for b

b

:: 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_{4} being Element of R holds

( b_{4} = x / y iff b_{4} * y = x );

for R being commutative domRing-like Ring

for x, y being Element of R st y divides x & y <> 0. R holds

for b

( b

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

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

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;

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

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

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

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 )

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 Th10: :: GCD_1:10

for R being non degenerated commutative domRing-like Ring

for a being Element of R holds a / (1. R) = a

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

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

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 )

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)

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

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

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

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

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;

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;

ex b_{1} being Subset of R st

for b being Element of R holds

( b in b_{1} iff b is_associated_to a )

for b_{1}, b_{2} being Subset of R st ( for b being Element of R holds

( b in b_{1} iff b is_associated_to a ) ) & ( for b being Element of R holds

( b in b_{2} iff b is_associated_to a ) ) holds

b_{1} = b_{2}

end;
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 for b being Element of R holds

( b in it iff b is_associated_to a );

ex b

for b being Element of R holds

( b in b

proof end;

uniqueness for b

( b in b

( b in b

b

proof end;

:: deftheorem Def5 defines Class GCD_1:def 5 :

for R being non empty multLoopStr

for a being Element of R

for b_{3} being Subset of R holds

( b_{3} = Class a iff for b being Element of R holds

( b in b_{3} iff b is_associated_to a ) );

for R being non empty multLoopStr

for a being Element of R

for b

( b

( b in b

registration

let R be non empty well-unital multLoopStr ;

let a be Element of R;

coherence

not Class a is empty

end;
let a be Element of R;

coherence

not Class a is empty

proof 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

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 ;

ex b_{1} being Subset-Family of R st

for A being Subset of R holds

( A in b_{1} iff ex a being Element of R st A = Class a )

for b_{1}, b_{2} being Subset-Family of R st ( for A being Subset of R holds

( A in b_{1} iff ex a being Element of R st A = Class a ) ) & ( for A being Subset of R holds

( A in b_{2} iff ex a being Element of R st A = Class a ) ) holds

b_{1} = b_{2}

end;
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 for A being Subset of R holds

( A in it iff ex a being Element of R st A = Class a );

ex b

for A being Subset of R holds

( A in b

proof end;

uniqueness for b

( A in b

( A in b

b

proof end;

:: deftheorem Def6 defines Classes GCD_1:def 6 :

for R being non empty multLoopStr

for b_{2} being Subset-Family of R holds

( b_{2} = Classes R iff for A being Subset of R holds

( A in b_{2} iff ex a being Element of R st A = Class a ) );

for R being non empty multLoopStr

for b

( b

( A in b

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

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 ;

ex b_{1} being non empty Subset of R st

( ( for a being Element of R ex z being Element of b_{1} st z is_associated_to a ) & ( for x, y being Element of b_{1} st x <> y holds

x is_not_associated_to y ) )

end;
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 ( ( 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 ) );

ex b

( ( for a being Element of R ex z being Element of b

x is_not_associated_to y ) )

proof end;

:: deftheorem Def7 defines Am GCD_1:def 7 :

for R being non empty well-unital associative multLoopStr

for b_{2} being non empty Subset of R holds

( b_{2} is Am of R iff ( ( for a being Element of R ex z being Element of b_{2} st z is_associated_to a ) & ( for x, y being Element of b_{2} st x <> y holds

x is_not_associated_to y ) ) );

for R being non empty well-unital associative multLoopStr

for b

( b

x is_not_associated_to y ) ) );

definition

let R be non empty well-unital associative multLoopStr ;

ex b_{1} being non empty Subset of R st

( b_{1} is Am of R & 1. R in b_{1} )

end;
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 ( it is Am of R & 1. R in it );

ex b

( b

proof end;

:: deftheorem Def8 defines AmpleSet GCD_1:def 8 :

for R being non empty well-unital associative multLoopStr

for b_{2} being non empty Subset of R holds

( b_{2} is AmpleSet of R iff ( b_{2} is Am of R & 1. R in b_{2} ) );

for R being non empty well-unital associative multLoopStr

for b

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

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;

for Amp being AmpleSet of R

for x, y being Element of Amp st x is_associated_to y holds

x = y by Th22;

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

existence

ex b_{1} being Element of R st

( b_{1} in Amp & b_{1} is_associated_to x )

for b_{1}, b_{2} being Element of R st b_{1} in Amp & b_{1} is_associated_to x & b_{2} in Amp & b_{2} is_associated_to x holds

b_{1} = b_{2}
by Th4, Th22;

end;
let Amp be AmpleSet of R;

let x be Element of R;

existence

ex b

( b

proof end;

uniqueness for b

b

:: 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_{4} being Element of R holds

( b_{4} = NF (x,Amp) iff ( b_{4} in Amp & b_{4} is_associated_to x ) );

for R being non empty well-unital associative multLoopStr

for Amp being AmpleSet of R

for x, b

( b

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 )

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;

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

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

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

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

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

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

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

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

end;

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

( 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

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;
zz divides 1_ F

proof

y = (1_ F) * y
;
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

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

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

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

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

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

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

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

( 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

registration

ex b_{1} being domRing st b_{1} is gcd-like
end;

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

proof end;

registration

existence

ex b_{1} being non empty multLoopStr st

( b_{1} is gcd-like & b_{1} is associative & b_{1} is commutative & b_{1} is well-unital )

end;
ex b

( b

proof end;

registration

existence

ex b_{1} being non empty multLoopStr_0 st

( b_{1} is gcd-like & b_{1} is associative & b_{1} is commutative & b_{1} is well-unital )

end;
ex b

( b

proof end;

registration

for b_{1} being non empty right_complementable almost_left_invertible right-distributive left-distributive well-unital left_unital add-associative right_zeroed commutative doubleLoopStr holds b_{1} is gcd-like
end;

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

proof end;

registration

ex b_{1} being non empty doubleLoopStr st

( b_{1} is gcd-like & b_{1} is associative & b_{1} is commutative & b_{1} is well-unital & b_{1} is domRing-like & b_{1} is unital & b_{1} is distributive & not b_{1} is degenerated & b_{1} is Abelian & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable )
end;

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

( b

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

ex b_{1} being Element of R st

( b_{1} in Amp & b_{1} divides x & b_{1} divides y & ( for z being Element of R st z divides x & z divides y holds

z divides b_{1} ) )

for b_{1}, b_{2} being Element of R st b_{1} in Amp & b_{1} divides x & b_{1} divides y & ( for z being Element of R st z divides x & z divides y holds

z divides b_{1} ) & b_{2} in Amp & b_{2} divides x & b_{2} divides y & ( for z being Element of R st z divides x & z divides y holds

z divides b_{2} ) holds

b_{1} = b_{2}

end;
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 ( 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 ) );

ex b

( b

z divides b

proof end;

uniqueness for b

z divides b

z divides b

b

proof 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_{5} being Element of R holds

( b_{5} = gcd (x,y,Amp) iff ( b_{5} in Amp & b_{5} divides x & b_{5} divides y & ( for z being Element of R st z divides x & z divides y holds

z divides b_{5} ) ) );

for R being non empty well-unital associative gcd-like multLoopStr

for Amp being AmpleSet of R

for x, y, b

( b

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 )

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)

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

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

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

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

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)

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

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)

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

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)

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;

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)

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;

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

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;

end;
let Amp be AmpleSet of R;

let x, y be Element of R;

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

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

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

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_{1},b_{2}) holds

(R,b_{2},b_{1})

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

(R,b

proof 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

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;

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

( gcd (x,y,Amp) = 1. R & y in Amp & y <> 0. R );

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

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

( ( 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_{1} being Element of R holds

( ( r1 = 0. R & s1 = 0. R implies ( b_{1} = s1 iff b_{1} = r1 ) ) & ( r1 = 0. R & gcd (r2,s2,Amp) = 1. R implies ( b_{1} = s1 iff b_{1} = (r1 * s2) + (r2 * s1) ) ) & ( r1 = 0. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies ( b_{1} = s1 iff b_{1} = 0. R ) ) & ( s1 = 0. R & gcd (r2,s2,Amp) = 1. R implies ( b_{1} = r1 iff b_{1} = (r1 * s2) + (r2 * s1) ) ) & ( s1 = 0. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies ( b_{1} = r1 iff b_{1} = 0. R ) ) & ( gcd (r2,s2,Amp) = 1. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies ( b_{1} = (r1 * s2) + (r2 * s1) iff b_{1} = 0. R ) ) )

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

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

( ( r1 = 0. R & s1 = 0. R implies ( b

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

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

( ( 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_{1} being Element of R holds

( ( r1 = 0. R & s1 = 0. R implies ( b_{1} = s2 iff b_{1} = r2 ) ) & ( r1 = 0. R & gcd (r2,s2,Amp) = 1. R implies ( b_{1} = s2 iff b_{1} = r2 * s2 ) ) & ( r1 = 0. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies ( b_{1} = s2 iff b_{1} = 1. R ) ) & ( s1 = 0. R & gcd (r2,s2,Amp) = 1. R implies ( b_{1} = r2 iff b_{1} = r2 * s2 ) ) & ( s1 = 0. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies ( b_{1} = r2 iff b_{1} = 1. R ) ) & ( gcd (r2,s2,Amp) = 1. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies ( b_{1} = r2 * s2 iff b_{1} = 1. R ) ) )

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

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

( ( r1 = 0. R & s1 = 0. R implies ( b

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

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

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

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;

( ( ( 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_{1} being Element of R holds

( ( ( r1 = 0. R or s1 = 0. R ) & r2 = 1. R & s2 = 1. R implies ( b_{1} = 0. R iff b_{1} = r1 * s1 ) ) & ( ( r1 = 0. R or s1 = 0. R ) & s2 <> 0. R & r2 = 1. R implies ( b_{1} = 0. R iff b_{1} = (r1 * s1) / (gcd (r1,s2,Amp)) ) ) & ( ( r1 = 0. R or s1 = 0. R ) & r2 <> 0. R & s2 = 1. R implies ( b_{1} = 0. R iff b_{1} = (r1 * s1) / (gcd (s1,r2,Amp)) ) ) & ( r2 = 1. R & s2 = 1. R & s2 <> 0. R & r2 = 1. R implies ( b_{1} = r1 * s1 iff b_{1} = (r1 * s1) / (gcd (r1,s2,Amp)) ) ) & ( r2 = 1. R & s2 = 1. R & r2 <> 0. R & s2 = 1. R implies ( b_{1} = r1 * s1 iff b_{1} = (r1 * s1) / (gcd (s1,r2,Amp)) ) ) & ( s2 <> 0. R & r2 = 1. R & r2 <> 0. R & s2 = 1. R implies ( b_{1} = (r1 * s1) / (gcd (r1,s2,Amp)) iff b_{1} = (r1 * s1) / (gcd (s1,r2,Amp)) ) ) )

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

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

( ( ( r1 = 0. R or s1 = 0. R ) & r2 = 1. R & s2 = 1. R implies ( b

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

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

( ( ( 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_{1} being Element of R holds

( ( ( r1 = 0. R or s1 = 0. R ) & r2 = 1. R & s2 = 1. R implies ( b_{1} = 1. R iff b_{1} = 1. R ) ) & ( ( r1 = 0. R or s1 = 0. R ) & s2 <> 0. R & r2 = 1. R implies ( b_{1} = 1. R iff b_{1} = s2 / (gcd (r1,s2,Amp)) ) ) & ( ( r1 = 0. R or s1 = 0. R ) & r2 <> 0. R & s2 = 1. R implies ( b_{1} = 1. R iff b_{1} = r2 / (gcd (s1,r2,Amp)) ) ) & ( r2 = 1. R & s2 = 1. R & s2 <> 0. R & r2 = 1. R implies ( b_{1} = 1. R iff b_{1} = s2 / (gcd (r1,s2,Amp)) ) ) & ( r2 = 1. R & s2 = 1. R & r2 <> 0. R & s2 = 1. R implies ( b_{1} = 1. R iff b_{1} = r2 / (gcd (s1,r2,Amp)) ) ) & ( s2 <> 0. R & r2 = 1. R & r2 <> 0. R & s2 = 1. R implies ( b_{1} = s2 / (gcd (r1,s2,Amp)) iff b_{1} = r2 / (gcd (s1,r2,Amp)) ) ) )

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

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

( ( ( r1 = 0. R or s1 = 0. R ) & r2 = 1. R & s2 = 1. R implies ( b

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

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

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)

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;

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

for a, b being Element of F st a <> 0. F & b <> 0. F holds

(a ") * (b ") = (b * a) "

proof end;