:: GCD_1 semantic presentation

begin


registration
cluster non empty commutative right_unital  ->  non empty left_unital for multLoopStr ;
coherence
 for b1 being non empty multLoopStr st b1 is commutative & b1 is right_unital holds
b1 is left_unital
proof
let R be non empty multLoopStr ; ::_thesis: ( R is commutative & R is right_unital implies R is left_unital )
assume that
A1: R is commutative and
A2: R is right_unital ; ::_thesis: R is left_unital
let x be Element of R; :: according to VECTSP_1:def_8 ::_thesis: (1. R) * x = x
thus (1. R) * x = x * (1. R) by A1, GROUP_1:def_12
.= x by A2, VECTSP_1:def_4 ; ::_thesis: verum
end;
end;

registration
cluster non empty commutative right-distributive  ->  non empty distributive for doubleLoopStr ;
coherence
 for b1 being non empty doubleLoopStr st b1 is commutative & b1 is right-distributive holds
b1 is distributive
proof
let R be non empty doubleLoopStr ; ::_thesis: ( R is commutative & R is right-distributive implies R is distributive )
assume that
A1: R is commutative and
A2: R is right-distributive ; ::_thesis: R is distributive
let x, y, z be Element of R; :: according to VECTSP_1:def_7 ::_thesis: ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
thus  x * (y + z) = (x * y) + (x * z) by A2, VECTSP_1:def_2; ::_thesis: (y + z) * x = (y * x) + (z * x)
thus (y + z) * x = x * (y + z) by A1, GROUP_1:def_12
.= (x * y) + (x * z) by A2, VECTSP_1:def_2
.= (y * x) + (x * z) by A1, GROUP_1:def_12
.= (y * x) + (z * x) by A1, GROUP_1:def_12 ; ::_thesis: verum
end;
cluster non empty commutative left-distributive  ->  non empty distributive for doubleLoopStr ;
coherence
 for b1 being non empty doubleLoopStr st b1 is commutative & b1 is left-distributive holds
b1 is distributive
proof
let R be non empty doubleLoopStr ; ::_thesis: ( R is commutative & R is left-distributive implies R is distributive )
assume that
A3: R is commutative and
A4: R is left-distributive ; ::_thesis: R is distributive
let x, y, z be Element of R; :: according to VECTSP_1:def_7 ::_thesis: ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
thus x * (y + z) = (y + z) * x by A3, GROUP_1:def_12
.= (y * x) + (z * x) by A4, VECTSP_1:def_3
.= (x * y) + (z * x) by A3, GROUP_1:def_12
.= (x * y) + (x * z) by A3, GROUP_1:def_12 ; ::_thesis: (y + z) * x = (y * x) + (z * x)
thus  (y + z) * x = (y * x) + (z * x) by A4, VECTSP_1:def_3; ::_thesis: verum
end;
end;

registration
cluster non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed  ->  for doubleLoopStr ;
coherence
 for b1 being Ring holds b1 is well-unital ;
end;

registration
cluster F_Real  ->  domRing-like ;
coherence
 F_Real is domRing-like
proof
set D = F_Real ;
hereby  :: according to VECTSP_2:def_1 ::_thesis: verum
let x, y be Element of F_Real; ::_thesis: ( x * y = 0. F_Real & x <> 0. F_Real implies y = 0. F_Real )
A1: 0. F_Real = 0 by STRUCT_0:def_6;
assume  ( x * y = 0. F_Real & x <> 0. F_Real ) ; ::_thesis: y = 0. F_Real
hence  y = 0. F_Real by A1, XCMPLX_1:6; ::_thesis: verum
end;
end;
end;

registration
cluster non empty non degenerated right_complementable almost_left_invertible strict associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like for doubleLoopStr ;
existence
 ex b1 being non empty doubleLoopStr st
( b1 is strict & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is associative & b1 is commutative & b1 is domRing-like & b1 is distributive & b1 is well-unital & not b1 is degenerated & b1 is almost_left_invertible )
proof
take  F_Real ; ::_thesis: ( F_Real is strict & F_Real is Abelian & F_Real is add-associative & F_Real is right_zeroed & F_Real is right_complementable & F_Real is associative & F_Real is commutative & F_Real is domRing-like & F_Real is distributive & F_Real is well-unital & not F_Real is degenerated & F_Real is almost_left_invertible )
thus  ( F_Real is strict & F_Real is Abelian & F_Real is add-associative & F_Real is right_zeroed & F_Real is right_complementable & F_Real is associative & F_Real is commutative & F_Real is domRing-like & F_Real is distributive & F_Real is well-unital & not F_Real is degenerated & F_Real is almost_left_invertible ) ; ::_thesis: verum
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
let R be commutative domRing-like Ring; ::_thesis: 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 ) )
let a, b, c be Element of R; ::_thesis: ( a <> 0. R implies ( ( a * b = a * c implies b = c ) & ( b * a = c * a implies b = c ) ) )
assume A1: a <> 0. R ; ::_thesis: ( ( a * b = a * c implies b = c ) & ( b * a = c * a implies b = c ) )
now__::_thesis:_(_a_*_b_=_a_*_c_implies_b_=_c_)
assume  a * b = a * c ; ::_thesis: b = c
then  0. R = (a * b) + (- (a * c)) by RLVECT_1:def_10
.= (a * b) + (a * (- c)) by VECTSP_1:8
.= a * (b + (- c)) by VECTSP_1:def_2
.= a * (b - c) by RLVECT_1:def_11 ;
then  b - c = 0. R by A1, VECTSP_2:def_1;
then c = (b - c) + c by RLVECT_1:4
.= (b + (- c)) + c by RLVECT_1:def_11
.= b + (c + (- c)) by RLVECT_1:def_3
.= b + (0. R) by RLVECT_1:def_10
.= b by RLVECT_1:4 ;
hence  b = c ; ::_thesis: verum
end;
hence  ( ( a * b = a * c implies b = c ) & ( b * a = c * a implies b = c ) ) ; ::_thesis: verum
end;

definition
let R be non empty multMagma ;
let x, y be Element of R;
predx divides y means :Def1: :: GCD_1:def 1
 ex z being Element of R st y = x * z;
end;

:: deftheorem Def1 defines divides GCD_1:def_1_:_
 for R being non empty multMagma
for x, y being Element of R holds
( x divides y iff ex z being Element of R st y = x * z );

definition
let R be non empty right_unital multLoopStr ;
let x, y be Element of R;
:: original: divides
redefine predx divides y;
reflexivity
 for x being Element of R holds (R,b1,b1)
proof
let A be Element of R; ::_thesis: (R,A,A)
 A * (1. R) = A by VECTSP_1:def_4;
hence  (R,A,A) by Def1; ::_thesis: verum
end;
end;

definition
let R be non empty multLoopStr ;
let x be Element of R;
attrx is unital  means :Def2: :: GCD_1:def 2
x divides 1. R;
end;

:: deftheorem Def2 defines unital GCD_1:def_2_:_
 for R being non empty multLoopStr
for x being Element of R holds
( x is unital iff x divides 1. R );

definition
let R be non empty multLoopStr ;
let x, y be Element of R;
predx is_associated_to y means :Def3: :: GCD_1:def 3
( x divides y & y divides x );
symmetry
 for x, y being Element of R st x divides y & y divides x holds
( y divides x & x divides y ) ;
end;

:: deftheorem Def3 defines is_associated_to GCD_1:def_3_:_
 for R being non empty multLoopStr
for x, y being Element of R holds
( x is_associated_to y iff ( x divides y & y divides x ) );

notation
let R be non empty multLoopStr ;
let x, y be Element of R;
antonym x is_not_associated_to y for x is_associated_to y;
end;

definition
let R be non empty well-unital multLoopStr ;
let x, y be Element of R;
:: original: is_associated_to
redefine predx is_associated_to y;
reflexivity
 for x being Element of R holds (R,b1,b1)
proof
let a be Element of R; ::_thesis: (R,a,a)
thus  ( a divides a & a divides a ) ; :: according to GCD_1:def_3 ::_thesis: verum
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 ;
funcx / y ->  Element of R means :Def4: :: GCD_1:def 4
it * y = x;
existence
 ex b1 being Element of R st b1 * y = x
proof
 ex z being Element of R st x = y * z by A1, Def1;
hence  ex b1 being Element of R st b1 * y = x ; ::_thesis: verum
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 );

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
let R be non empty associative multLoopStr ; ::_thesis: for a, b, c being Element of R st a divides b & b divides c holds
a divides c
let A, B, C be Element of R; ::_thesis: ( A divides B & B divides C implies A divides C )
now__::_thesis:_(_A_divides_B_&_B_divides_C_&_A_divides_B_&_B_divides_C_implies_A_divides_C_)
assume that
A1: A divides B and
A2: B divides C ; ::_thesis: ( A divides B & B divides C implies A divides C )
consider D being Element of R such that
A3: A * D = B by A1, Def1;
consider E being Element of R such that
A4: B * E = C by A2, Def1;
 A * (D * E) = C by A3, A4, GROUP_1:def_3;
hence  ( A divides B & B divides C implies A divides C ) by Def1; ::_thesis: verum
end;
hence  ( A divides B & B divides C implies A divides C ) ; ::_thesis: verum
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
let R be non empty associative commutative multLoopStr ; ::_thesis: for a, b, c, d being Element of R st b divides a & d divides c holds
b * d divides a * c
let a, b, c, d be Element of R; ::_thesis: ( b divides a & d divides c implies b * d divides a * c )
assume that
A1: b divides a and
A2: d divides c ; ::_thesis: b * d divides a * c
consider x being Element of R such that
A3: b * x = a by A1, Def1;
consider y being Element of R such that
A4: d * y = c by A2, Def1;
(b * d) * (y * x) = ((b * d) * y) * x by GROUP_1:def_3
.= (b * c) * x by A4, GROUP_1:def_3
.= a * c by A3, GROUP_1:def_3 ;
hence  b * d divides a * c by Def1; ::_thesis: verum
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
proof
let R be non empty associative multLoopStr ; ::_thesis: 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
let A, B, C be Element of R; ::_thesis: ( A is_associated_to B & B is_associated_to C implies A is_associated_to C )
now__::_thesis:_(_A_is_associated_to_B_&_B_is_associated_to_C_&_A_is_associated_to_B_&_B_is_associated_to_C_implies_A_is_associated_to_C_)
assume A1: ( A is_associated_to B & B is_associated_to C ) ; ::_thesis: ( A is_associated_to B & B is_associated_to C implies A is_associated_to C )
then  ( B divides A & C divides B ) by Def3;
then A2: C divides A by Th2;
 ( A divides B & B divides C ) by A1, Def3;
then  A divides C by Th2;
hence  ( A is_associated_to B & B is_associated_to C implies A is_associated_to C ) by A2, Def3; ::_thesis: verum
end;
hence  ( A is_associated_to B & B is_associated_to C implies A is_associated_to C ) ; ::_thesis: verum
end;

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
let R be non empty associative multLoopStr ; ::_thesis: for a, b, c being Element of R st a divides b holds
c * a divides c * b
let A, B, C be Element of R; ::_thesis: ( A divides B implies C * A divides C * B )
assume  A divides B ; ::_thesis: C * A divides C * B
then consider D being Element of R such that
A1: A * D = B by Def1;
 (C * A) * D = C * B by A1, GROUP_1:def_3;
hence  C * A divides C * B by Def1; ::_thesis: verum
end;

theorem Th6: :: GCD_1:6
for R being non empty multLoopStr
for a, b being Element of R holds
( a divides a * b & ( R is commutative implies b divides a * b ) )
proof
let R be non empty multLoopStr ; ::_thesis: for a, b being Element of R holds
( a divides a * b & ( R is commutative implies b divides a * b ) )
let a, b be Element of R; ::_thesis: ( a divides a * b & ( R is commutative implies b divides a * b ) )
thus  a divides a * b ::_thesis: ( R is commutative implies b divides a * b )
proof
take  b ; :: according to GCD_1:def_1 ::_thesis: a * b = a * b
thus  a * b = a * b ; ::_thesis: verum
end;
assume A1: R is commutative ; ::_thesis: b divides a * b
take  a ; :: according to GCD_1:def_1 ::_thesis: a * b = b * a
thus  a * b = b * a by A1, GROUP_1:def_12; ::_thesis: verum
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
let R be non empty associative multLoopStr ; ::_thesis: for a, b, c being Element of R st a divides b holds
a divides b * c
let a, b, c be Element of R; ::_thesis: ( a divides b implies a divides b * c )
assume  a divides b ; ::_thesis: a divides b * c
then consider d being Element of R such that
A1: a * d = b by Def1;
 a * (d * c) = b * c by A1, GROUP_1:def_3;
hence  a divides b * c by Def1; ::_thesis: verum
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
let R be commutative domRing-like Ring; ::_thesis: for a, b being Element of R st b divides a & b <> 0. R holds
( a / b = 0. R iff a = 0. R )
let a, b be Element of R; ::_thesis: ( b divides a & b <> 0. R implies ( a / b = 0. R iff a = 0. R ) )
assume that
A1: b divides a and
A2: b <> 0. R ; ::_thesis: ( a / b = 0. R iff a = 0. R )
hereby  ::_thesis: ( a = 0. R implies a / b = 0. R )
assume  a / b = 0. R ; ::_thesis: a = 0. R
then a = (0. R) * b by A1, A2, Def4
.= 0. R by VECTSP_1:7 ;
hence  a = 0. R ; ::_thesis: verum
end;
assume  a = 0. R ; ::_thesis: a / b = 0. R
then  0. R = (a / b) * b by A1, A2, Def4;
hence  a / b = 0. R by A2, VECTSP_2:def_1; ::_thesis: verum
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
let R be commutative domRing-like Ring; ::_thesis: for a being Element of R st a <> 0. R holds
a / a = 1. R
let A be Element of R; ::_thesis: ( A <> 0. R implies A / A = 1. R )
assume A1: A <> 0. R ; ::_thesis: A / A = 1. R
then (A / A) * A = A by Def4
.= (1. R) * A by VECTSP_1:def_8 ;
hence  A / A = 1. R by A1, Th1; ::_thesis: verum
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
let R be non degenerated commutative domRing-like Ring; ::_thesis: for a being Element of R holds a / (1. R) = a
let a be Element of R; ::_thesis: a / (1. R) = a
set A = a / (1. R);
 (1. R) * a = a by VECTSP_1:def_8;
then A1: ( 1. R <> 0. R & 1. R divides a ) by Def1;
a / (1. R) = (a / (1. R)) * (1. R) by VECTSP_1:def_4
.= a by A1, Def4 ;
hence  a / (1. R) = a ; ::_thesis: verum
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
let R be commutative domRing-like Ring; ::_thesis: 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) ) )
let A, B, C be Element of R; ::_thesis: ( C <> 0. R implies ( ( C divides A * B & C divides A implies (A * B) / C = (A / C) * B ) & ( C divides A * B & C divides B implies (A * B) / C = A * (B / C) ) ) )
assume A1: C <> 0. R ; ::_thesis: ( ( 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) ) )
A2: now__::_thesis:_(_C_divides_A_*_B_&_C_divides_B_&_C_divides_A_*_B_&_C_divides_B_implies_(A_*_B)_/_C_=_A_*_(B_/_C)_)
set A2 = B / C;
set A1 = (A * B) / C;
assume  ( C divides A * B & C divides B ) ; ::_thesis: ( C divides A * B & C divides B implies (A * B) / C = A * (B / C) )
then  ( ((A * B) / C) * C = A * B & (B / C) * C = B ) by A1, Def4;
then  ((A * B) / C) * C = (A * (B / C)) * C by GROUP_1:def_3;
hence  ( C divides A * B & C divides B implies (A * B) / C = A * (B / C) ) by A1, Th1; ::_thesis: verum
end;
now__::_thesis:_(_C_divides_A_*_B_&_C_divides_A_&_C_divides_A_*_B_&_C_divides_A_implies_(A_*_B)_/_C_=_(A_/_C)_*_B_)
set A2 = A / C;
set A1 = (A * B) / C;
assume  ( C divides A * B & C divides A ) ; ::_thesis: ( C divides A * B & C divides A implies (A * B) / C = (A / C) * B )
then  ( ((A * B) / C) * C = A * B & (A / C) * C = A ) by A1, Def4;
then  ((A * B) / C) * C = ((A / C) * B) * C by GROUP_1:def_3;
hence  ( C divides A * B & C divides A implies (A * B) / C = (A / C) * B ) by A1, Th1; ::_thesis: verum
end;
hence  ( ( 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) ) ) by A2; ::_thesis: verum
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
let R be commutative domRing-like Ring; ::_thesis: 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
let a, b, c be Element of R; ::_thesis: ( c <> 0. R & c divides a & c divides b & c divides a + b implies (a / c) + (b / c) = (a + b) / c )
assume A1: c <> 0. R ; ::_thesis: ( not c divides a or not c divides b or not c divides a + b or (a / c) + (b / c) = (a + b) / c )
set e = b / c;
set d = a / c;
assume that
A2: ( c divides a & c divides b ) and
A3: c divides a + b ; ::_thesis: (a / c) + (b / c) = (a + b) / c
 ( (a / c) * c = a & (b / c) * c = b ) by A1, A2, Def4;
then  a + b = ((a / c) + (b / c)) * c by VECTSP_1:def_3;
then (a + b) / c = ((a / c) + (b / c)) * (c / c) by A1, A3, Th11
.= ((a / c) + (b / c)) * (1. R) by A1, Th9
.= (a / c) + (b / c) by VECTSP_1:def_4 ;
hence  (a / c) + (b / c) = (a + b) / c ; ::_thesis: verum
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
let R be commutative domRing-like Ring; ::_thesis: 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 )
let a, b, c be Element of R; ::_thesis: ( c <> 0. R & c divides a & c divides b implies ( a / c = b / c iff a = b ) )
assume A1: c <> 0. R ; ::_thesis: ( not c divides a or not c divides b or ( a / c = b / c iff a = b ) )
assume that
A2: c divides a and
A3: c divides b ; ::_thesis: ( a / c = b / c iff a = b )
now__::_thesis:_(_a_/_c_=_b_/_c_&_a_/_c_=_b_/_c_implies_a_=_b_)
assume  a / c = b / c ; ::_thesis: ( a / c = b / c implies a = b )
consider e being Element of R such that
A4: e = b / c ;
 e * c = b by A1, A3, A4, Def4;
hence  ( a / c = b / c implies a = b ) by A1, A2, A4, Def4; ::_thesis: verum
end;
hence  ( a / c = b / c iff a = b ) ; ::_thesis: verum
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
let R be commutative domRing-like Ring; ::_thesis: 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)
let a, b, c, d be Element of R; ::_thesis: ( b <> 0. R & d <> 0. R & b divides a & d divides c implies (a / b) * (c / d) = (a * c) / (b * d) )
assume that
A1: ( b <> 0. R & d <> 0. R ) and
A2: ( b divides a & d divides c ) ; ::_thesis: (a / b) * (c / d) = (a * c) / (b * d)
A3: b * d divides a * c by A2, Th3;
set z = (a * c) / (b * d);
set y = c / d;
set x = a / b;
A4: b * d <> 0. R by A1, VECTSP_2:def_1;
 ( (a / b) * b = a & (c / d) * d = c ) by A1, A2, Def4;
then ((a * c) / (b * d)) * (b * d) = ((a / b) * b) * ((c / d) * d) by A3, A4, Def4
.= (a / b) * (b * ((c / d) * d)) by GROUP_1:def_3
.= (a / b) * ((c / d) * (b * d)) by GROUP_1:def_3
.= ((a / b) * (c / d)) * (b * d) by GROUP_1:def_3 ;
hence  (a / b) * (c / d) = (a * c) / (b * d) by A4, Th1; ::_thesis: verum
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
let R be commutative domRing-like Ring; ::_thesis: for a, b, c being Element of R st a <> 0. R & a * b divides a * c holds
b divides c
let A, B, C be Element of R; ::_thesis: ( A <> 0. R & A * B divides A * C implies B divides C )
assume that
A1: A <> 0. R and
A2: A * B divides A * C ; ::_thesis: B divides C
consider D being Element of R such that
A3: (A * B) * D = A * C by A2, Def1;
 A divides A * C by Th6;
then A4: (A * C) / A = (A / A) * C by A1, Th11;
 A divides A * (B * D) by Th6;
then A5: (A * (B * D)) / A = (A / A) * (B * D) by A1, Th11;
A6: A * (B * D) = A * C by A3, GROUP_1:def_3;
B * D = (1. R) * (B * D) by VECTSP_1:def_8
.= (A / A) * C by A1, A6, A5, A4, Th9
.= (1. R) * C by A1, Th9
.= C by VECTSP_1:def_8 ;
hence  B divides C by Def1; ::_thesis: verum
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
let R be commutative domRing-like Ring; ::_thesis: for a being Element of R st a is_associated_to 0. R holds
a = 0. R
let A be Element of R; ::_thesis: ( A is_associated_to 0. R implies A = 0. R )
assume  A is_associated_to 0. R ; ::_thesis: A = 0. R
then  0. R divides A by Def3;
then  ex D being Element of R st (0. R) * D = A by Def1;
hence  A = 0. R by VECTSP_1:7; ::_thesis: verum
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
let R be commutative domRing-like Ring; ::_thesis: for a, b being Element of R st a <> 0. R & a * b = a holds
b = 1. R
let A, B be Element of R; ::_thesis: ( A <> 0. R & A * B = A implies B = 1. R )
assume that
A1: A <> 0. R and
A2: A * B = A ; ::_thesis: B = 1. R
set A1 = A / A;
 ( A / A = 1. R & (A * B) / A = (A / A) * B ) by A1, A2, Th9, Th11;
hence  B = 1. R by A2, VECTSP_1:def_8; ::_thesis: verum
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
let R be commutative domRing-like Ring; ::_thesis: 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 ) )
A1: for a, b being Element of R st a is_associated_to b holds
ex c being Element of R st
( c is unital & a * c = b )
proof
let A, B be Element of R; ::_thesis: ( A is_associated_to B implies ex c being Element of R st
( c is unital & A * c = B ) )
assume A2: A is_associated_to B ; ::_thesis: ex c being Element of R st
( c is unital & A * c = B )
then  A divides B by Def3;
then consider C being Element of R such that
A3: B = A * C by Def1;
 B divides A by A2, Def3;
then consider D being Element of R such that
A4: A = B * D by Def1;
now__::_thesis:_(_(_A_<>_0._R_&_ex_c_being_Element_of_R_st_
(_c_is_unital_&_A_*_c_=_B_)_)_or_(_A_=_0._R_&_ex_c_being_Element_of_R_st_
(_c_is_unital_&_A_*_c_=_B_)_)_)
percases ( A <> 0. R or A = 0. R ) ;
caseA5: A <> 0. R ; ::_thesis: ex c being Element of R st
( c is unital & A * c = B )
 A = A * (C * D) by A3, A4, GROUP_1:def_3;
then  C * D = 1. R by A5, Th17;
then  C divides 1. R by Def1;
then  C is unital by Def2;
hence  ex c being Element of R st
( c is unital & A * c = B ) by A3; ::_thesis: verum
end;
caseA6: A = 0. R ; ::_thesis: ex c being Element of R st
( c is unital & A * c = B )
 1. R divides 1. R ;
then A7: 1. R is unital by Def2;
 B = 0. R by A3, A6, VECTSP_1:7;
then  B = A * (1. R) by A6, VECTSP_1:def_4;
hence  ex c being Element of R st
( c is unital & A * c = B ) by A7; ::_thesis: verum
end;
end;
end;
hence  ex c being Element of R st
( c is unital & A * c = B ) ; ::_thesis: verum
end;
 for a, b being Element of R st ex c being Element of R st
( c is unital & a * c = b ) holds
a is_associated_to b
proof
let A, B be Element of R; ::_thesis: ( ex c being Element of R st
( c is unital & A * c = B ) implies A is_associated_to B )
 ( ex c being Element of R st
( c is unital & A * c = B ) implies A is_associated_to B )
proof
now__::_thesis:_(_ex_c_being_Element_of_R_st_
(_c_is_unital_&_A_*_c_=_B_)_&_ex_c_being_Element_of_R_st_
(_c_is_unital_&_A_*_c_=_B_)_implies_A_is_associated_to_B_)
assume  ex c being Element of R st
( c is unital & A * c = B ) ; ::_thesis: ( ex c being Element of R st
( c is unital & A * c = B ) implies A is_associated_to B )
then consider C being Element of R such that
A8: C is unital and
A9: A * C = B ;
 C divides 1. R by A8, Def2;
then consider D being Element of R such that
A10: C * D = 1. R by Def1;
A = A * (C * D) by A10, VECTSP_1:def_4
.= B * D by A9, GROUP_1:def_3 ;
then A11: B divides A by Def1;
 A divides B by A9, Def1;
hence  ( ex c being Element of R st
( c is unital & A * c = B ) implies A is_associated_to B ) by A11, Def3; ::_thesis: verum
end;
hence  ( ex c being Element of R st
( c is unital & A * c = B ) implies A is_associated_to B ) ; ::_thesis: verum
end;
hence  ( ex c being Element of R st
( c is unital & A * c = B ) implies A is_associated_to B ) ; ::_thesis: verum
end;
hence  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 ) ) by A1; ::_thesis: verum
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
proof
let R be commutative domRing-like Ring; ::_thesis: 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
let A, B, C be Element of R; ::_thesis: ( C <> 0. R & C * A is_associated_to C * B implies A is_associated_to B )
assume that
A1: C <> 0. R and
A2: C * A is_associated_to C * B ; ::_thesis: A is_associated_to B
 C * B divides C * A by A2, Def3;
then A3: B divides A by A1, Th15;
 C * A divides C * B by A2, Def3;
then  A divides B by A1, Th15;
hence  A is_associated_to B by A3, Def3; ::_thesis: verum
end;

begin

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
set M =  {  b where b is Element of R : b is_associated_to a  }  ;
now__::_thesis:_for_B_being_set_st_B_in__{__b_where_b_is_Element_of_R_:_b_is_associated_to_a__}__holds_
B_in_the_carrier_of_R
let B be set ; ::_thesis: ( B in  {  b where b is Element of R : b is_associated_to a  }  implies B in the carrier of R )
now__::_thesis:_(_B_in__{__b_where_b_is_Element_of_R_:_b_is_associated_to_a__}__&_B_in__{__b_where_b_is_Element_of_R_:_b_is_associated_to_a__}__implies_B_in_the_carrier_of_R_)
assume  B in  {  b where b is Element of R : b is_associated_to a  }  ; ::_thesis: ( B in  {  b where b is Element of R : b is_associated_to a  }  implies B in the carrier of R )
then  ex B9 being Element of R st
( B = B9 & B9 is_associated_to a ) ;
hence  ( B in  {  b where b is Element of R : b is_associated_to a  }  implies B in the carrier of R ) ; ::_thesis: verum
end;
hence  ( B in  {  b where b is Element of R : b is_associated_to a  }  implies B in the carrier of R ) ; ::_thesis: verum
end;
then A1:  {  b where b is Element of R : b is_associated_to a  }  c= the carrier of R by TARSKI:def_3;
now__::_thesis:_for_A_being_Element_of_R_holds_
(_A_in__{__b_where_b_is_Element_of_R_:_b_is_associated_to_a__}__iff_A_is_associated_to_a_)
let A be Element of R; ::_thesis: ( A in  {  b where b is Element of R : b is_associated_to a  }  iff A is_associated_to a )
 ( A in  {  b where b is Element of R : b is_associated_to a  }  implies A is_associated_to a )
proof
assume  A in  {  b where b is Element of R : b is_associated_to a  }  ; ::_thesis: A is_associated_to a
then  ex A9 being Element of R st
( A = A9 & A9 is_associated_to a ) ;
hence  A is_associated_to a ; ::_thesis: verum
end;
hence  ( A in  {  b where b is Element of R : b is_associated_to a  }  iff A is_associated_to a ) ; ::_thesis: verum
end;
hence  ex b1 being Subset of R st
for b being Element of R holds
( b in b1 iff b is_associated_to a ) by A1; ::_thesis: verum
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
defpred S1[ Element of R] means $1 is_associated_to a;
let X1, X2 be Subset of R; ::_thesis: ( ( for b being Element of R holds
( b in X1 iff b is_associated_to a ) ) & ( for b being Element of R holds
( b in X2 iff b is_associated_to a ) ) implies X1 = X2 )
assume that
A2: for y being Element of R holds
( y in X1 iff S1[y] ) and
A3: for y being Element of R holds
( y in X2 iff S1[y] ) ; ::_thesis: X1 = X2
thus  X1 = X2 from SUBSET_1:sch_2(A2, A3); ::_thesis: verum
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
 a is_associated_to a ;
hence  not Class a is empty by Def5; ::_thesis: verum
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
let R be non empty associative multLoopStr ; ::_thesis: for a, b being Element of R st Class a meets Class b holds
Class a = Class b
let a, b be Element of R; ::_thesis: ( Class a meets Class b implies Class a = Class b )
assume  (Class a) /\ (Class b) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: Class a = Class b
then  Class a meets Class b by XBOOLE_0:def_7;
then consider Z being set  such that
A1: Z in Class a and
A2: Z in Class b by XBOOLE_0:3;
reconsider Z = Z as Element of R by A1;
A3: Z is_associated_to b by A2, Def5;
A4: Z is_associated_to a by A1, Def5;
A5: for c being Element of R st c in Class b holds
c in Class a
proof
let c be Element of R; ::_thesis: ( c in Class b implies c in Class a )
assume  c in Class b ; ::_thesis: c in Class a
then  c is_associated_to b by Def5;
then  Z is_associated_to c by A3, Th4;
then  a is_associated_to c by A4, Th4;
hence  c in Class a by Def5; ::_thesis: verum
end;
 for c being Element of R st c in Class a holds
c in Class b
proof
let c be Element of R; ::_thesis: ( c in Class a implies c in Class b )
assume  c in Class a ; ::_thesis: c in Class b
then  c is_associated_to a by Def5;
then  Z is_associated_to c by A4, Th4;
then  b is_associated_to c by A3, Th4;
hence  c in Class b by Def5; ::_thesis: verum
end;
hence  Class a = Class b by A5, SUBSET_1:3; ::_thesis: verum
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
defpred S1[ set ] means  ex a being Element of R st $1 = Class a;
 ex F being Subset-Family of R st
for A being Subset of R holds
( A in F iff S1[A] ) from SUBSET_1:sch_3();
hence  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 ) ; ::_thesis: verum
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
defpred S1[ set ] means  ex a being Element of R st $1 = Class a;
let F1, F2 be Subset-Family of R; ::_thesis: ( ( for A being Subset of R holds
( A in F1 iff ex a being Element of R st A = Class a ) ) & ( for A being Subset of R holds
( A in F2 iff ex a being Element of R st A = Class a ) ) implies F1 = F2 )
assume A1: for A being Subset of R holds
( A in F1 iff S1[A] ) ; ::_thesis: ( ex A being Subset of R st
( ( A in F2 implies ex a being Element of R st A = Class a ) implies ( ex a being Element of R st A = Class a & not A in F2 ) ) or F1 = F2 )
assume A2: for A being Subset of R holds
( A in F2 iff S1[A] ) ; ::_thesis: F1 = F2
thus  F1 = F2 from SUBSET_1:sch_4(A1, A2); ::_thesis: verum
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
 Class (1. R) in Classes R by Def6;
hence  not Classes R is empty ; ::_thesis: verum
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
let R be non empty well-unital multLoopStr ; ::_thesis: for X being Subset of R st X in Classes R holds
not X is empty
let X be Subset of R; ::_thesis: ( X in Classes R implies not X is empty )
assume  X in Classes R ; ::_thesis: not X is empty
then  ex a being Element of R st X = Class a by Def6;
hence  not X is empty ; ::_thesis: verum
end;

definition
let R be non empty associative well-unital multLoopStr ;
mode Am of R ->  non empty Subset of R means :Def7: :: GCD_1:def 7
( ( for a being Element of R ex z being Element of it st z is_associated_to a ) & ( for x, y being Element of it st x <> y holds
x is_not_associated_to y ) );
existence
 ex b1 being non empty Subset of R st
( ( for a being Element of R ex z being Element of b1 st z is_associated_to a ) & ( for x, y being Element of b1 st x <> y holds
x is_not_associated_to y ) )
proof
now__::_thesis:_for_R_being_non_empty_associative_well-unital_multLoopStr_ex_s_being_non_empty_Subset_of_R_st_
(_(_for_a_being_Element_of_R_ex_z_being_Element_of_s_st_z_is_associated_to_a_)_&_(_for_x,_y_being_Element_of_s_st_x_<>_y_holds_
x_is_not_associated_to_y_)_)
let R be non empty associative well-unital multLoopStr ; ::_thesis: ex s being non empty Subset of R st
( ( for a being Element of R ex z being Element of s st z is_associated_to a ) & ( for x, y being Element of s st x <> y holds
x is_not_associated_to y ) )
reconsider M = Classes R as non empty set ;
A1: for X being set st X in M holds
X <> {}
proof
let X be set ; ::_thesis: ( X in M implies X <> {} )
assume  X in M ; ::_thesis: X <> {}
then  ex A being Element of R st X = Class A by Def6;
hence  X <> {} ; ::_thesis: verum
end;
 for X, Y being set st X in M & Y in M & X <> Y holds
X misses Y
proof
let X, Y be set ; ::_thesis: ( X in M & Y in M & X <> Y implies X misses Y )
assume that
A2: ( X in M & Y in M ) and
A3: X <> Y ; ::_thesis: X misses Y
assume A4: X meets Y ; ::_thesis: contradiction
 ( ex A being Element of R st X = Class A & ex B being Element of R st Y = Class B ) by A2, Def6;
hence  contradiction by A3, A4, Th20; ::_thesis: verum
end;
then consider AmpS9 being set  such that
A5: for X being set st X in M holds
ex x being set st AmpS9 /\ X = {x} by A1, WELLORD2:18;
 not AmpS9 is empty
proof
 Class (1. R) in M by Def6;
then  ex x being set st AmpS9 /\ (Class (1. R)) = {x} by A5;
hence  not AmpS9 is empty ; ::_thesis: verum
end;
then reconsider AmpS9 = AmpS9 as non empty set ;
set AmpS =  {  x where x is Element of AmpS9 : ex X being non empty Subset of R st
( X in M & AmpS9 /\ X = {x} )  }  ;
A6:  {  x where x is Element of AmpS9 : ex X being non empty Subset of R st
( X in M & AmpS9 /\ X = {x} )  }  is non empty Subset of R
proof
 not  {  x where x is Element of AmpS9 : ex X being non empty Subset of R st
( X in M & AmpS9 /\ X = {x} )  }  is empty
proof
A7: Class (1. R) in M by Def6;
then consider x being set  such that
A8: AmpS9 /\ (Class (1. R)) = {x} by A5;
 x in {x} by TARSKI:def_1;
then  x in AmpS9 by A8, XBOOLE_0:def_4;
then  x in  {  x where x is Element of AmpS9 : ex X being non empty Subset of R st
( X in M & AmpS9 /\ X = {x} )  }  by A7, A8;
hence  not  {  x where x is Element of AmpS9 : ex X being non empty Subset of R st
( X in M & AmpS9 /\ X = {x} )  }  is empty ; ::_thesis: verum
end;
then reconsider AmpS =  {  x where x is Element of AmpS9 : ex X being non empty Subset of R st
( X in M & AmpS9 /\ X = {x} )  }  as non empty set ;
now__::_thesis:_for_A_being_set_st_A_in_AmpS_holds_
A_in_the_carrier_of_R
let A be set ; ::_thesis: ( A in AmpS implies A in the carrier of R )
now__::_thesis:_(_A_in_AmpS_&_A_in_AmpS_implies_A_in_the_carrier_of_R_)
assume  A in AmpS ; ::_thesis: ( A in AmpS implies A in the carrier of R )
then consider x being Element of AmpS9 such that
A9: ( A = x & ex X being non empty Subset of R st
( X in M & AmpS9 /\ X = {x} ) ) ;
 x in {x} by TARSKI:def_1;
hence  ( A in AmpS implies A in the carrier of R ) by A9; ::_thesis: verum
end;
hence  ( A in AmpS implies A in the carrier of R ) ; ::_thesis: verum
end;
hence   {  x where x is Element of AmpS9 : ex X being non empty Subset of R st
( X in M & AmpS9 /\ X = {x} )  }  is non empty Subset of R by TARSKI:def_3; ::_thesis: verum
end;
A10: for X being Element of M ex z being Element of  {  x where x is Element of AmpS9 : ex X being non empty Subset of R st
( X in M & AmpS9 /\ X = {x} )  }  st  {  x where x is Element of AmpS9 : ex X being non empty Subset of R st
( X in M & AmpS9 /\ X = {x} )  }  /\ X = {z}
proof
let X be Element of M; ::_thesis: ex z being Element of  {  x where x is Element of AmpS9 : ex X being non empty Subset of R st
( X in M & AmpS9 /\ X = {x} )  }  st  {  x where x is Element of AmpS9 : ex X being non empty Subset of R st
( X in M & AmpS9 /\ X = {x} )  }  /\ X = {z}
consider x being set  such that
A11: AmpS9 /\ X = {x} by A5;
 X in Classes R ;
then A12: X is non empty Subset of R by Th21;
A13: x in {x} by TARSKI:def_1;
then  x in AmpS9 by A11, XBOOLE_0:def_4;
then A14: x in  {  x where x is Element of AmpS9 : ex X being non empty Subset of R st
( X in M & AmpS9 /\ X = {x} )  }  by A11, A12;
A15: x in X by A11, A13, XBOOLE_0:def_4;
now__::_thesis:_for_y_being_set_holds_
(_y_in_{x}_iff_y_in__{__x_where_x_is_Element_of_AmpS9_:_ex_X_being_non_empty_Subset_of_R_st_
(_X_in_M_&_AmpS9_/\_X_=_{x}_)__}__/\_X_)
let y be set ; ::_thesis: ( y in {x} iff y in  {  x where x is Element of AmpS9 : ex X being non empty Subset of R st
( X in M & AmpS9 /\ X = {x} )  }  /\ X )
A16: now__::_thesis:_(_y_in__{__x_where_x_is_Element_of_AmpS9_:_ex_X_being_non_empty_Subset_of_R_st_
(_X_in_M_&_AmpS9_/\_X_=_{x}_)__}__/\_X_&_y_in__{__x_where_x_is_Element_of_AmpS9_:_ex_X_being_non_empty_Subset_of_R_st_
(_X_in_M_&_AmpS9_/\_X_=_{x}_)__}__/\_X_implies_y_in_{x}_)
assume A17: y in  {  x where x is Element of AmpS9 : ex X being non empty Subset of R st
( X in M & AmpS9 /\ X = {x} )  }  /\ X ; ::_thesis: ( y in  {  x where x is Element of AmpS9 : ex X being non empty Subset of R st
( X in M & AmpS9 /\ X = {x} )  }  /\ X implies y in {x} )
then  y in  {  x where x is Element of AmpS9 : ex X being non empty Subset of R st
( X in M & AmpS9 /\ X = {x} )  }  by XBOOLE_0:def_4;
then A18: ex zz being Element of AmpS9 st
( y = zz & ex X being non empty Subset of R st
( X in M & AmpS9 /\ X = {zz} ) ) ;
 y in X by A17, XBOOLE_0:def_4;
hence  ( y in  {  x where x is Element of AmpS9 : ex X being non empty Subset of R st
( X in M & AmpS9 /\ X = {x} )  }  /\ X implies y in {x} ) by A11, A18, XBOOLE_0:def_4; ::_thesis: verum
end;
now__::_thesis:_(_y_in_{x}_&_y_in_{x}_implies_y_in__{__x_where_x_is_Element_of_AmpS9_:_ex_X_being_non_empty_Subset_of_R_st_
(_X_in_M_&_AmpS9_/\_X_=_{x}_)__}__/\_X_)
assume  y in {x} ; ::_thesis: ( y in {x} implies y in  {  x where x is Element of AmpS9 : ex X being non empty Subset of R st
( X in M & AmpS9 /\ X = {x} )  }  /\ X )
then  y = x by TARSKI:def_1;
hence  ( y in {x} implies y in  {  x where x is Element of AmpS9 : ex X being non empty Subset of R st
( X in M & AmpS9 /\ X = {x} )  }  /\ X ) by A15, A14, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  ( y in {x} iff y in  {  x where x is Element of AmpS9 : ex X being non empty Subset of R st
( X in M & AmpS9 /\ X = {x} )  }  /\ X ) by A16; ::_thesis: verum
end;
then   {  x where x is Element of AmpS9 : ex X being non empty Subset of R st
( X in M & AmpS9 /\ X = {x} )  }  /\ X = {x} by TARSKI:1;
hence  ex z being Element of  {  x where x is Element of AmpS9 : ex X being non empty Subset of R st
( X in M & AmpS9 /\ X = {x} )  }  st  {  x where x is Element of AmpS9 : ex X being non empty Subset of R st
( X in M & AmpS9 /\ X = {x} )  }  /\ X = {z} by A14; ::_thesis: verum
end;
reconsider AmpS =  {  x where x is Element of AmpS9 : ex X being non empty Subset of R st
( X in M & AmpS9 /\ X = {x} )  }  as non empty Subset of R by A6;
A19: for x, y being Element of AmpS st x <> y holds
x is_not_associated_to y
proof
let x, y be Element of AmpS; ::_thesis: ( x <> y implies x is_not_associated_to y )
assume A20: x <> y ; ::_thesis: x is_not_associated_to y
 x is_associated_to x ;
then  x in Class x by Def5;
then A21: x in AmpS /\ (Class x) by XBOOLE_0:def_4;
 Class x in M by Def6;
then consider z being Element of AmpS such that
A22: AmpS /\ (Class x) = {z} by A10;
assume  x is_associated_to y ; ::_thesis: contradiction
then  y in Class x by Def5;
then  y in AmpS /\ (Class x) by XBOOLE_0:def_4;
then  y = z by A22, TARSKI:def_1;
hence  contradiction by A20, A21, A22, TARSKI:def_1; ::_thesis: verum
end;
 for a being Element of R ex z being Element of AmpS st z is_associated_to a
proof
let a be Element of R; ::_thesis: ex z being Element of AmpS st z is_associated_to a
reconsider N = Class a as Element of M by Def6;
consider z being Element of AmpS such that
A23: AmpS /\ N = {z} by A10;
 z in {z} by TARSKI:def_1;
then  z in Class a by A23, XBOOLE_0:def_4;
then  z is_associated_to a by Def5;
hence  ex z being Element of AmpS st z is_associated_to a ; ::_thesis: verum
end;
hence  ex s being non empty Subset of R st
( ( for a being Element of R ex z being Element of s st z is_associated_to a ) & ( for x, y being Element of s st x <> y holds
x is_not_associated_to y ) ) by A19; ::_thesis: verum
end;
hence  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 ) ) ; ::_thesis: verum
end;
end;

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

definition
let R be non empty associative well-unital multLoopStr ;
mode AmpleSet of R ->  non empty Subset of R means :Def8: :: GCD_1:def 8
( it is Am of R & 1. R in it );
existence
 ex b1 being non empty Subset of R st
( b1 is Am of R & 1. R in b1 )
proof
now__::_thesis:_for_A_being_Am_of_R_ex_b2_being_non_empty_Subset_of_R_st_
(_b2_is_Am_of_R_&_1._R_in_b2_)
let A be Am of R; ::_thesis: ex b1 being non empty Subset of R st
( b1 is Am of R & 1. R in b1 )
consider x being Element of A such that
A1: x is_associated_to 1. R by Def7;
set A9 =  {  z where z is Element of A : z <> x  }  \/ {(1. R)};
 1. R in {(1. R)} by TARSKI:def_1;
then A2: 1. R in  {  z where z is Element of A : z <> x  }  \/ {(1. R)} by XBOOLE_0:def_3;
reconsider A9 =  {  z where z is Element of A : z <> x  }  \/ {(1. R)} as non empty set ;
A3: for x being Element of A9 holds
( x = 1. R or x in A )
proof
let y be Element of A9; ::_thesis: ( y = 1. R or y in A )
now__::_thesis:_(_(_y_in__{__z_where_z_is_Element_of_A_:_z_<>_x__}__&_(_y_=_1._R_or_y_in_A_)_)_or_(_y_in_{(1._R)}_&_(_y_=_1._R_or_y_in_A_)_)_)
percases ( y in  {  z where z is Element of A : z <> x  }  or y in {(1. R)} ) by XBOOLE_0:def_3;
case y in  {  z where z is Element of A : z <> x  }  ; ::_thesis: ( y = 1. R or y in A )
then  ex zz being Element of A st
( y = zz & zz <> x ) ;
hence  ( y = 1. R or y in A ) ; ::_thesis: verum
end;
case y in {(1. R)} ; ::_thesis: ( y = 1. R or y in A )
hence  ( y = 1. R or y in A ) by TARSKI:def_1; ::_thesis: verum
end;
end;
end;
hence  ( y = 1. R or y in A ) ; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_A9_holds_
x_in_the_carrier_of_R
let x be set ; ::_thesis: ( x in A9 implies x in the carrier of R )
now__::_thesis:_(_x_in_A9_&_x_in_A9_implies_x_in_the_carrier_of_R_)
assume A4: x in A9 ; ::_thesis: ( x in A9 implies x in the carrier of R )
 x in the carrier of R
proof
now__::_thesis:_(_(_x_=_1._R_&_x_in_the_carrier_of_R_)_or_(_x_in_A_&_x_in_the_carrier_of_R_)_)
percases ( x = 1. R or x in A ) by A3, A4;
case x = 1. R ; ::_thesis: x in the carrier of R
hence  x in the carrier of R ; ::_thesis: verum
end;
case x in A ; ::_thesis: x in the carrier of R
hence  x in the carrier of R ; ::_thesis: verum
end;
end;
end;
hence  x in the carrier of R ; ::_thesis: verum
end;
hence  ( x in A9 implies x in the carrier of R ) ; ::_thesis: verum
end;
hence  ( x in A9 implies x in the carrier of R ) ; ::_thesis: verum
end;
then reconsider A9 = A9 as non empty Subset of R by TARSKI:def_3;
A5: for z, y being Element of A9 st z <> y holds
z is_not_associated_to y
proof
let z, y be Element of A9; ::_thesis: ( z <> y implies z is_not_associated_to y )
assume A6: z <> y ; ::_thesis: z is_not_associated_to y
now__::_thesis:_(_(_z_=_1._R_&_y_=_1._R_&_z_is_not_associated_to_y_)_or_(_z_=_1._R_&_y_<>_1._R_&_(_z_is_associated_to_y_implies_z_is_not_associated_to_y_)_)_or_(_z_<>_1._R_&_y_=_1._R_&_(_z_is_associated_to_y_implies_z_is_not_associated_to_y_)_)_or_(_z_<>_1._R_&_y_<>_1._R_&_z_is_not_associated_to_y_)_)
percases ( ( z = 1. R & y = 1. R ) or ( z = 1. R & y <> 1. R ) or ( z <> 1. R & y = 1. R ) or ( z <> 1. R & y <> 1. R ) ) ;
case ( z = 1. R & y = 1. R ) ; ::_thesis: z is_not_associated_to y
hence  z is_not_associated_to y by A6; ::_thesis: verum
end;
caseA7: ( z = 1. R & y <> 1. R ) ; ::_thesis: ( z is_associated_to y implies z is_not_associated_to y )
assume  z is_associated_to y ; ::_thesis: z is_not_associated_to y
 not y in {(1. R)} by A7, TARSKI:def_1;
then  y in  {  zz where zz is Element of A : zz <> x  }  by XBOOLE_0:def_3;
then  ex zz being Element of A st
( y = zz & zz <> x ) ;
hence  z is_not_associated_to y by A1, A7, Def7, Th4; ::_thesis: verum
end;
caseA8: ( z <> 1. R & y = 1. R ) ; ::_thesis: ( z is_associated_to y implies z is_not_associated_to y )
assume  z is_associated_to y ; ::_thesis: z is_not_associated_to y
 not z in {(1. R)} by A8, TARSKI:def_1;
then  z in  {  zz where zz is Element of A : zz <> x  }  by XBOOLE_0:def_3;
then  ex zz being Element of A st
( z = zz & zz <> x ) ;
hence  z is_not_associated_to y by A1, A8, Def7, Th4; ::_thesis: verum
end;
case ( z <> 1. R & y <> 1. R ) ; ::_thesis: z is_not_associated_to y
then  ( z in A & y in A ) by A3;
hence  z is_not_associated_to y by A6, Def7; ::_thesis: verum
end;
end;
end;
hence  z is_not_associated_to y ; ::_thesis: verum
end;
 for a being Element of R ex z being Element of A9 st z is_associated_to a
proof
let a be Element of R; ::_thesis: ex z being Element of A9 st z is_associated_to a
now__::_thesis:_(_(_a_is_associated_to_1._R_&_ex_z_being_Element_of_A9_st_z_is_associated_to_a_)_or_(_a_is_not_associated_to_1._R_&_ex_z_being_Element_of_A9_st_z_is_associated_to_a_)_)
percases ( a is_associated_to 1. R or a is_not_associated_to 1. R ) ;
case a is_associated_to 1. R ; ::_thesis: ex z being Element of A9 st z is_associated_to a
hence  ex z being Element of A9 st z is_associated_to a by A2; ::_thesis: verum
end;
caseA9: a is_not_associated_to 1. R ; ::_thesis: ex z being Element of A9 st z is_associated_to a
consider z being Element of A such that
A10: z is_associated_to a by Def7;
 z <> x by A1, A9, A10, Th4;
then  z in  {  zz where zz is Element of A : zz <> x  }  ;
then  z in A9 by XBOOLE_0:def_3;
hence  ex z being Element of A9 st z is_associated_to a by A10; ::_thesis: verum
end;
end;
end;
hence  ex z being Element of A9 st z is_associated_to a ; ::_thesis: verum
end;
then  A9 is Am of R by A5, Def7;
hence  ex b1 being non empty Subset of R st
( b1 is Am of R & 1. R in b1 ) by A2; ::_thesis: verum
end;
hence  ex b1 being non empty Subset of R st
( b1 is Am of R & 1. R in b1 ) ; ::_thesis: verum
end;
end;

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

theorem Th22: :: GCD_1:22
for R being non empty associative well-unital multLoopStr
for Amp being AmpleSet of R holds
( 1. R in Amp & ( for a being Element of R ex z being Element of Amp st z is_associated_to a ) & ( for x, y being Element of Amp st x <> y holds
x is_not_associated_to y ) )
proof
let R be non empty associative well-unital multLoopStr ; ::_thesis: 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 ) )
let Amp be AmpleSet of R; ::_thesis: ( 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 ) )
 Amp is Am of R by Def8;
hence  ( 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 ) ) by Def7, Def8; ::_thesis: verum
end;

theorem :: GCD_1:23
for R being non empty associative well-unital multLoopStr
for Amp being AmpleSet of R
for x, y being Element of Amp st x is_associated_to y holds
x = y by Th22;

theorem Th24: :: GCD_1:24
for R being commutative domRing-like Ring
for Amp being AmpleSet of R holds 0. R is Element of Amp
proof
let R be commutative domRing-like Ring; ::_thesis: for Amp being AmpleSet of R holds 0. R is Element of Amp
let Amp be AmpleSet of R; ::_thesis: 0. R is Element of Amp
consider A being Element of Amp such that
A1: A is_associated_to 0. R by Th22;
 0. R divides A by A1, Def3;
then  ex D being Element of R st (0. R) * D = A by Def1;
hence  0. R is Element of Amp by VECTSP_1:7; ::_thesis: verum
end;

definition
let R be non empty associative well-unital multLoopStr ;
let Amp be AmpleSet of R;
let x be Element of R;
func NF (x,Amp) ->  Element of R means :Def9: :: GCD_1:def 9
( it in Amp & it is_associated_to x );
existence
 ex b1 being Element of R st
( b1 in Amp & b1 is_associated_to x )
proof
now__::_thesis:_for_Amp_being_AmpleSet_of_R
for_x_being_Element_of_R_ex_zz_being_Element_of_R_st_
(_zz_in_Amp_&_zz_is_associated_to_x_)
let Amp be AmpleSet of R; ::_thesis: for x being Element of R ex zz being Element of R st
( zz in Amp & zz is_associated_to x )
let x be Element of R; ::_thesis: ex zz being Element of R st
( zz in Amp & zz is_associated_to x )
 ex z being Element of Amp st z is_associated_to x by Th22;
hence  ex zz being Element of R st
( zz in Amp & zz is_associated_to x ) ; ::_thesis: verum
end;
hence  ex b1 being Element of R st
( b1 in Amp & b1 is_associated_to x ) ; ::_thesis: verum
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 associative well-unital multLoopStr
for Amp being AmpleSet of R
for x, b4 being Element of R holds
( b4 = NF (x,Amp) iff ( b4 in Amp & b4 is_associated_to x ) );

theorem Th25: :: GCD_1:25
for R being commutative domRing-like Ring
for Amp being AmpleSet of R holds
( NF ((0. R),Amp) = 0. R & NF ((1. R),Amp) = 1. R )
proof
let R be commutative domRing-like Ring; ::_thesis: for Amp being AmpleSet of R holds
( NF ((0. R),Amp) = 0. R & NF ((1. R),Amp) = 1. R )
let Amp be AmpleSet of R; ::_thesis: ( NF ((0. R),Amp) = 0. R & NF ((1. R),Amp) = 1. R )
 ( 1. R in Amp & 0. R is Element of Amp ) by Def8, Th24;
hence  ( NF ((0. R),Amp) = 0. R & NF ((1. R),Amp) = 1. R ) by Def9; ::_thesis: verum
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
let R be non empty associative well-unital multLoopStr ;
let Amp be AmpleSet of R;
attrAmp is multiplicative  means :Def10: :: GCD_1:def 10
 for x, y being Element of Amp holds x * y in Amp;
end;

:: deftheorem Def10 defines multiplicative GCD_1:def_10_:_
 for R being non empty associative well-unital multLoopStr
for Amp being AmpleSet of R holds
( Amp is multiplicative iff for x, y being Element of Amp holds x * y in Amp );

theorem Th27: :: GCD_1:27
for R being commutative domRing-like Ring
for Amp being AmpleSet of R st Amp is multiplicative holds
for x, y being Element of Amp st y divides x & y <> 0. R holds
x / y in Amp
proof
let R be commutative domRing-like Ring; ::_thesis: 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
let Amp be AmpleSet of R; ::_thesis: ( Amp is multiplicative implies for x, y being Element of Amp st y divides x & y <> 0. R holds
x / y in Amp )
assume A1: Amp is multiplicative ; ::_thesis: for x, y being Element of Amp st y divides x & y <> 0. R holds
x / y in Amp
let x, y be Element of Amp; ::_thesis: ( y divides x & y <> 0. R implies x / y in Amp )
assume that
A2: y divides x and
A3: y <> 0. R ; ::_thesis: x / y in Amp
now__::_thesis:_(_(_x_<>_0._R_&_x_/_y_in_Amp_)_or_(_x_=_0._R_&_x_/_y_in_Amp_)_)
percases ( x <> 0. R or x = 0. R ) ;
caseA4: x <> 0. R ; ::_thesis: x / y in Amp
set d = x / y;
consider d9 being Element of Amp such that
A5: d9 is_associated_to x / y by Th22;
consider u being Element of R such that
A6: u is unital and
A7: (x / y) * u = d9 by A5, Th18;
 x = y * (x / y) by A2, A3, Def4;
then A8: u * x = y * d9 by A7, GROUP_1:def_3;
A9: x is_associated_to u * x
proof
 u divides 1. R by A6, Def2;
then consider e being Element of R such that
A10: u * e = 1. R by Def1;
 x divides x ;
then A11: x divides u * x by Th7;
(u * x) * e = (e * u) * x by GROUP_1:def_3
.= x by A10, VECTSP_1:def_8 ;
then  u * x divides x by Def1;
hence  x is_associated_to u * x by A11, Def3; ::_thesis: verum
end;
A12: y * d9 in Amp by A1, Def10;
(1. R) * x = x by VECTSP_1:def_8
.= u * x by A8, A12, A9, Th22 ;
then  u = 1. R by A4, Th1;
then  d9 = x / y by A7, VECTSP_1:def_4;
hence  x / y in Amp ; ::_thesis: verum
end;
caseA13: x = 0. R ; ::_thesis: x / y in Amp
set d = x / y;
 x = y * (x / y) by A2, A3, Def4;
then A14: x / y = 0. R by A3, A13, VECTSP_2:def_1;
 0. R is Element of Amp by Th24;
hence  x / y in Amp by A14; ::_thesis: verum
end;
end;
end;
hence  x / y in Amp ; ::_thesis: verum
end;

begin

definition
let R be non empty multLoopStr ;
attrR is gcd-like  means :Def11: :: GCD_1:def 11
 for x, y being Element of R ex z being Element of R st
( z divides x & z divides y & ( for zz being Element of R st zz divides x & zz divides y holds
zz divides z ) );
end;

:: deftheorem Def11 defines gcd-like GCD_1:def_11_:_
 for R being non empty multLoopStr holds
( R is gcd-like iff for x, y being Element of R ex z being Element of R st
( z divides x & z divides y & ( for zz being Element of R st zz divides x & zz divides y holds
zz divides z ) ) );

Lm1: now__::_thesis:_for_F_being_Field
for_x,_y_being_Element_of_F_ex_z_being_Element_of_F_st_
(_z_divides_x_&_z_divides_y_&_(_for_zz_being_Element_of_F_st_zz_divides_x_&_zz_divides_y_holds_
zz_divides_z_)_)
let F be Field; ::_thesis: for x, y being Element of F ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) )
let x, y be Element of F; ::_thesis: ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) )
now__::_thesis:_(_(_x_<>_0._F_&_y_<>_0._F_&_ex_z_being_Element_of_F_st_
(_z_divides_x_&_z_divides_y_&_(_for_zz_being_Element_of_F_st_zz_divides_x_&_zz_divides_y_holds_
zz_divides_z_)_)_)_or_(_x_=_0._F_&_ex_z_being_Element_of_F_st_
(_z_divides_x_&_z_divides_y_&_(_for_zz_being_Element_of_F_st_zz_divides_x_&_zz_divides_y_holds_
zz_divides_z_)_)_)_or_(_y_=_0._F_&_ex_z_being_Element_of_F_st_
(_z_divides_x_&_z_divides_y_&_(_for_zz_being_Element_of_F_st_zz_divides_x_&_zz_divides_y_holds_
zz_divides_z_)_)_)_)
percases ( ( x <> 0. F & y <> 0. F ) or x = 0. F or y = 0. F ) ;
caseA1: ( x <> 0. F & y <> 0. F ) ; ::_thesis: ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) )
A2: for zz being Element of F st zz divides x & zz divides y holds
zz divides 1_ F
proof
let zz be Element of F; ::_thesis: ( zz divides x & zz divides y implies zz divides 1_ F )
assume that
A3: zz divides x and
 zz divides y ; ::_thesis: zz divides 1_ F
now__::_thesis:_(_(_zz_<>_0._F_&_zz_divides_1__F_)_or_(_zz_=_0._F_&_(_zz_divides_x_implies_zz_divides_1__F_)_)_)
percases ( zz <> 0. F or zz = 0. F ) ;
case zz <> 0. F ; ::_thesis: zz divides 1_ F
then  ex zz9 being Element of F st zz9 * zz = 1_ F by VECTSP_1:def_9;
hence  zz divides 1_ F by Def1; ::_thesis: verum
end;
caseA4: zz = 0. F ; ::_thesis: ( zz divides x implies zz divides 1_ F )
assume  zz divides x ; ::_thesis: zz divides 1_ F
then  ex d being Element of F st zz * d = x by Def1;
hence  zz divides 1_ F by A1, A4, VECTSP_1:7; ::_thesis: verum
end;
end;
end;
hence  zz divides 1_ F by A3; ::_thesis: verum
end;
 y = (1_ F) * y by VECTSP_1:def_6;
then A5: 1_ F divides y by Def1;
 x = (1_ F) * x by VECTSP_1:def_6;
then  1_ F divides x by Def1;
hence  ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) ) by A5, A2; ::_thesis: verum
end;
caseA6: x = 0. F ; ::_thesis: ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) )
 y * (0. F) = 0. F by VECTSP_1:7;
then A7: y divides 0. F by Def1;
 for z being Element of F st z divides 0. F & z divides y holds
z divides y ;
hence  ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) ) by A6, A7; ::_thesis: verum
end;
caseA8: y = 0. F ; ::_thesis: ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) )
 x * (0. F) = 0. F by VECTSP_1:7;
then A9: x divides 0. F by Def1;
 for z being Element of F st z divides x & z divides 0. F holds
z divides x ;
hence  ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) ) by A8, A9; ::_thesis: verum
end;
end;
end;
hence  ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) ) ; ::_thesis: verum
end;

registration
cluster non empty non degenerated V46() right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like gcd-like for doubleLoopStr ;
existence
 ex b1 being domRing st b1 is gcd-like
proof
set F = the strict Field;
reconsider F = the strict Field as comRing ;
reconsider F = F as domRing by VECTSP_2:1;
 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 ) ) by Lm1;
then  F is gcd-like by Def11;
hence  ex b1 being domRing st b1 is gcd-like ; ::_thesis: verum
end;
end;

registration
cluster non empty associative commutative well-unital gcd-like for multLoopStr ;
existence
 ex b1 being non empty multLoopStr st
( b1 is gcd-like & b1 is associative & b1 is commutative & b1 is well-unital )
proof
set F = the strict Field;
 for x, y being Element of the strict Field ex z being Element of the strict Field st
( z divides x & z divides y & ( for zz being Element of the strict Field st zz divides x & zz divides y holds
zz divides z ) ) by Lm1;
then  the strict Field is gcd-like by Def11;
hence  ex b1 being non empty multLoopStr st
( b1 is gcd-like & b1 is associative & b1 is commutative & b1 is well-unital ) ; ::_thesis: verum
end;
end;

registration
cluster non empty associative commutative well-unital gcd-like for multLoopStr_0 ;
existence
 ex b1 being non empty multLoopStr_0 st
( b1 is gcd-like & b1 is associative & b1 is commutative & b1 is well-unital )
proof
set F = the strict Field;
 for x, y being Element of the strict Field ex z being Element of the strict Field st
( z divides x & z divides y & ( for zz being Element of the strict Field st zz divides x & zz divides y holds
zz divides z ) ) by Lm1;
then  the strict Field is gcd-like by Def11;
hence  ex b1 being non empty multLoopStr_0 st
( b1 is gcd-like & b1 is associative & b1 is commutative & b1 is well-unital ) ; ::_thesis: verum
end;
end;

registration
cluster non empty right_complementable almost_left_invertible commutative right-distributive left-distributive well-unital left_unital add-associative right_zeroed  ->  non empty right_complementable almost_left_invertible commutative right-distributive left-distributive well-unital left_unital add-associative right_zeroed gcd-like for doubleLoopStr ;
coherence
 for b1 being non empty right_complementable almost_left_invertible commutative right-distributive left-distributive well-unital left_unital add-associative right_zeroed doubleLoopStr holds b1 is gcd-like
proof
let F be non empty right_complementable almost_left_invertible commutative right-distributive left-distributive well-unital left_unital add-associative right_zeroed doubleLoopStr ; ::_thesis: F is gcd-like
let x, y be Element of F; :: according to GCD_1:def_11 ::_thesis: ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) )
now__::_thesis:_(_(_x_<>_0._F_&_y_<>_0._F_&_ex_z_being_Element_of_F_st_
(_z_divides_x_&_z_divides_y_&_(_for_zz_being_Element_of_F_st_zz_divides_x_&_zz_divides_y_holds_
zz_divides_z_)_)_)_or_(_x_=_0._F_&_ex_z_being_Element_of_F_st_
(_z_divides_x_&_z_divides_y_&_(_for_zz_being_Element_of_F_st_zz_divides_x_&_zz_divides_y_holds_
zz_divides_z_)_)_)_or_(_y_=_0._F_&_ex_z_being_Element_of_F_st_
(_z_divides_x_&_z_divides_y_&_(_for_zz_being_Element_of_F_st_zz_divides_x_&_zz_divides_y_holds_
zz_divides_z_)_)_)_)
percases ( ( x <> 0. F & y <> 0. F ) or x = 0. F or y = 0. F ) ;
caseA1: ( x <> 0. F & y <> 0. F ) ; ::_thesis: ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) )
A2: for zz being Element of F st zz divides x & zz divides y holds
zz divides 1_ F
proof
let zz be Element of F; ::_thesis: ( zz divides x & zz divides y implies zz divides 1_ F )
assume that
A3: zz divides x and
 zz divides y ; ::_thesis: zz divides 1_ F
now__::_thesis:_(_(_zz_<>_0._F_&_zz_divides_1__F_)_or_(_zz_=_0._F_&_(_zz_divides_x_implies_zz_divides_1__F_)_)_)
percases ( zz <> 0. F or zz = 0. F ) ;
case zz <> 0. F ; ::_thesis: zz divides 1_ F
then  ex zz9 being Element of F st zz9 * zz = 1_ F by VECTSP_1:def_9;
hence  zz divides 1_ F by Def1; ::_thesis: verum
end;
caseA4: zz = 0. F ; ::_thesis: ( zz divides x implies zz divides 1_ F )
assume  zz divides x ; ::_thesis: zz divides 1_ F
then  ex d being Element of F st zz * d = x by Def1;
hence  zz divides 1_ F by A1, A4, VECTSP_1:7; ::_thesis: verum
end;
end;
end;
hence  zz divides 1_ F by A3; ::_thesis: verum
end;
 y = (1_ F) * y by VECTSP_1:def_8;
then A5: 1_ F divides y by Def1;
 x = (1_ F) * x by VECTSP_1:def_8;
then  1_ F divides x by Def1;
hence  ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) ) by A5, A2; ::_thesis: verum
end;
caseA6: x = 0. F ; ::_thesis: ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) )
 y * (0. F) = 0. F by VECTSP_1:6;
then A7: y divides 0. F by Def1;
 for z being Element of F st z divides 0. F & z divides y holds
z divides y ;
hence  ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) ) by A6, A7; ::_thesis: verum
end;
caseA8: y = 0. F ; ::_thesis: ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) )
 x * (0. F) = 0. F by VECTSP_1:6;
then A9: x divides 0. F by Def1;
 for z being Element of F st z divides x & z divides 0. F holds
z divides x ;
hence  ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) ) by A8, A9; ::_thesis: verum
end;
end;
end;
hence  ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) ) ; ::_thesis: verum
end;
end;

registration
cluster non empty non degenerated right_complementable unital associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like gcd-like for doubleLoopStr ;
existence
 ex b1 being non empty doubleLoopStr st
( b1 is gcd-like & b1 is associative & b1 is commutative & b1 is well-unital & b1 is domRing-like & b1 is unital & b1 is distributive & not b1 is degenerated & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable )
proof
take  F_Real ; ::_thesis: ( F_Real is gcd-like & F_Real is associative & F_Real is commutative & F_Real is well-unital & F_Real is domRing-like & F_Real is unital & F_Real is distributive & not F_Real is degenerated & F_Real is Abelian & F_Real is add-associative & F_Real is right_zeroed & F_Real is right_complementable )
thus  ( F_Real is gcd-like & F_Real is associative & F_Real is commutative & F_Real is well-unital & F_Real is domRing-like & F_Real is unital & F_Real is distributive & not F_Real is degenerated & F_Real is Abelian & F_Real is add-associative & F_Real is right_zeroed & F_Real is right_complementable ) ; ::_thesis: verum
end;
end;

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

definition
let R be non empty associative well-unital gcd-like multLoopStr ;
let Amp be AmpleSet of R;
let x, y be Element of R;
func gcd (x,y,Amp) ->  Element of R means :Def12: :: GCD_1:def 12
( it in Amp & it divides x & it divides y & ( for z being Element of R st z divides x & z divides y holds
z divides it ) );
existence
 ex b1 being Element of R st
( b1 in Amp & b1 divides x & b1 divides y & ( for z being Element of R st z divides x & z divides y holds
z divides b1 ) )
proof
consider u being Element of R such that
A1: ( u divides x & u divides y ) and
A2: for zz being Element of R st zz divides x & zz divides y holds
zz divides u by Def11;
consider z being Element of Amp such that
A3: z is_associated_to u by Th22;
A4: for zz being Element of R st zz divides x & zz divides y holds
zz divides z
proof
let zz be Element of R; ::_thesis: ( zz divides x & zz divides y implies zz divides z )
assume  ( zz divides x & zz divides y ) ; ::_thesis: zz divides z
then A5: zz divides u by A2;
 u divides z by A3, Def3;
hence  zz divides z by A5, Th2; ::_thesis: verum
end;
 z divides u by A3, Def3;
then  ( z divides x & z divides y ) by A1, Th2;
hence  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 ) ) by A4; ::_thesis: verum
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
now__::_thesis:_for_z1_being_Element_of_R_st_z1_in_Amp_&_z1_divides_x_&_z1_divides_y_&_(_for_z_being_Element_of_R_st_z_divides_x_&_z_divides_y_holds_
z_divides_z1_)_holds_
for_z2_being_Element_of_R_st_z2_in_Amp_&_z2_divides_x_&_z2_divides_y_&_(_for_z_being_Element_of_R_st_z_divides_x_&_z_divides_y_holds_
z_divides_z2_)_holds_
z1_=_z2
let z1 be Element of R; ::_thesis: ( z1 in Amp & z1 divides x & z1 divides y & ( for z being Element of R st z divides x & z divides y holds
z divides z1 ) implies for z2 being Element of R st z2 in Amp & z2 divides x & z2 divides y & ( for z being Element of R st z divides x & z divides y holds
z divides z2 ) holds
z1 = z2 )
assume that
A6: z1 in Amp and
A7: ( z1 divides x & z1 divides y & ( for z being Element of R st z divides x & z divides y holds
z divides z1 ) ) ; ::_thesis: for z2 being Element of R st z2 in Amp & z2 divides x & z2 divides y & ( for z being Element of R st z divides x & z divides y holds
z divides z2 ) holds
z1 = z2
let z2 be Element of R; ::_thesis: ( z2 in Amp & z2 divides x & z2 divides y & ( for z being Element of R st z divides x & z divides y holds
z divides z2 ) implies z1 = z2 )
assume that
A8: z2 in Amp and
A9: ( z2 divides x & z2 divides y & ( for z being Element of R st z divides x & z divides y holds
z divides z2 ) ) ; ::_thesis: z1 = z2
 ( z1 divides z2 & z2 divides z1 ) by A7, A9;
then  z1 is_associated_to z2 by Def3;
hence  z1 = z2 by A6, A8, Th22; ::_thesis: verum
end;
hence  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 ; ::_thesis: verum
end;
end;

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

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
let R be gcdDomain; ::_thesis: 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 )
let Amp be AmpleSet of R; ::_thesis: for a, b, c being Element of R st c divides gcd (a,b,Amp) holds
( c divides a & c divides b )
let A, B, C be Element of R; ::_thesis: ( C divides gcd (A,B,Amp) implies ( C divides A & C divides B ) )
assume  C divides gcd (A,B,Amp) ; ::_thesis: ( C divides A & C divides B )
then consider D being Element of R such that
A1: C * D = gcd (A,B,Amp) by Def1;
 gcd (A,B,Amp) divides A by Def12;
then consider E being Element of R such that
A2: (gcd (A,B,Amp)) * E = A by Def1;
A3: C * (D * E) = A by A1, A2, GROUP_1:def_3;
 gcd (A,B,Amp) divides B by Def12;
then consider E being Element of R such that
A4: (gcd (A,B,Amp)) * E = B by Def1;
 C * (D * E) = B by A1, A4, GROUP_1:def_3;
hence  ( C divides A & C divides B ) by A3, Def1; ::_thesis: verum
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
let R be gcdDomain; ::_thesis: for Amp being AmpleSet of R
for a, b being Element of R holds gcd (a,b,Amp) = gcd (b,a,Amp)
let Amp be AmpleSet of R; ::_thesis: for a, b being Element of R holds gcd (a,b,Amp) = gcd (b,a,Amp)
let A, B be Element of R; ::_thesis: gcd (A,B,Amp) = gcd (B,A,Amp)
set D = gcd (A,B,Amp);
A1: ( gcd (A,B,Amp) divides A & ( for z being Element of R st z divides B & z divides A holds
z divides gcd (A,B,Amp) ) ) by Def12;
 ( gcd (A,B,Amp) in Amp & gcd (A,B,Amp) divides B ) by Def12;
hence  gcd (A,B,Amp) = gcd (B,A,Amp) by A1, Def12; ::_thesis: verum
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
let R be gcdDomain; ::_thesis: 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) )
let Amp be AmpleSet of R; ::_thesis: for a being Element of R holds
( gcd (a,(0. R),Amp) = NF (a,Amp) & gcd ((0. R),a,Amp) = NF (a,Amp) )
let A be Element of R; ::_thesis: ( gcd (A,(0. R),Amp) = NF (A,Amp) & gcd ((0. R),A,Amp) = NF (A,Amp) )
A1: NF (A,Amp) in Amp by Def9;
 (NF (A,Amp)) * (0. R) = 0. R by VECTSP_1:6;
then A2: NF (A,Amp) divides 0. R by Def1;
A3: NF (A,Amp) is_associated_to A by Def9;
A4: for z being Element of R st z divides A & z divides 0. R holds
z divides NF (A,Amp)
proof
let z be Element of R; ::_thesis: ( z divides A & z divides 0. R implies z divides NF (A,Amp) )
assume that
A5: z divides A and
 z divides 0. R ; ::_thesis: z divides NF (A,Amp)
 A divides NF (A,Amp) by A3, Def3;
hence  z divides NF (A,Amp) by A5, Th2; ::_thesis: verum
end;
 NF (A,Amp) divides A by A3, Def3;
then  gcd (A,(0. R),Amp) = NF (A,Amp) by A2, A4, A1, Def12;
hence  ( gcd (A,(0. R),Amp) = NF (A,Amp) & gcd ((0. R),A,Amp) = NF (A,Amp) ) by Th29; ::_thesis: verum
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
let R be gcdDomain; ::_thesis: for Amp being AmpleSet of R holds gcd ((0. R),(0. R),Amp) = 0. R
let Amp be AmpleSet of R; ::_thesis: gcd ((0. R),(0. R),Amp) = 0. R
 gcd ((0. R),(0. R),Amp) = NF ((0. R),Amp) by Th30;
hence  gcd ((0. R),(0. R),Amp) = 0. R by Th25; ::_thesis: verum
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
let R be gcdDomain; ::_thesis: 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 )
let Amp be AmpleSet of R; ::_thesis: for a being Element of R holds
( gcd (a,(1. R),Amp) = 1. R & gcd ((1. R),a,Amp) = 1. R )
let A be Element of R; ::_thesis: ( gcd (A,(1. R),Amp) = 1. R & gcd ((1. R),A,Amp) = 1. R )
 (1. R) * A = A by VECTSP_1:def_8;
then A1: 1. R divides A by Def1;
 ( 1. R in Amp & ( for z being Element of R st z divides A & z divides 1. R holds
z divides 1. R ) ) by Def8;
then  gcd (A,(1. R),Amp) = 1. R by A1, Def12;
hence  ( gcd (A,(1. R),Amp) = 1. R & gcd ((1. R),A,Amp) = 1. R ) by Th29; ::_thesis: verum
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
let R be gcdDomain; ::_thesis: 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 ) )
let Amp be AmpleSet of R; ::_thesis: for a, b being Element of R holds
( gcd (a,b,Amp) = 0. R iff ( a = 0. R & b = 0. R ) )
let A, B be Element of R; ::_thesis: ( gcd (A,B,Amp) = 0. R iff ( A = 0. R & B = 0. R ) )
A1: now__::_thesis:_(_gcd_(A,B,Amp)_=_0._R_&_gcd_(A,B,Amp)_=_0._R_implies_(_A_=_0._R_&_B_=_0._R_)_)
assume A2: gcd (A,B,Amp) = 0. R ; ::_thesis: ( gcd (A,B,Amp) = 0. R implies ( A = 0. R & B = 0. R ) )
then  0. R divides B by Def12;
then A3: ex E being Element of R st (0. R) * E = B by Def1;
 0. R divides A by A2, Def12;
then  ex D being Element of R st (0. R) * D = A by Def1;
hence  ( gcd (A,B,Amp) = 0. R implies ( A = 0. R & B = 0. R ) ) by A3, VECTSP_1:7; ::_thesis: verum
end;
 ( A = 0. R & B = 0. R implies gcd (A,B,Amp) = 0. R )
proof
assume that
A4: A = 0. R and
A5: B = 0. R ; ::_thesis: gcd (A,B,Amp) = 0. R
 gcd (A,B,Amp) = NF (A,Amp) by A5, Th30;
hence  gcd (A,B,Amp) = 0. R by A4, Th25; ::_thesis: verum
end;
hence  ( gcd (A,B,Amp) = 0. R iff ( A = 0. R & B = 0. R ) ) by A1; ::_thesis: verum
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
let R be gcdDomain; ::_thesis: 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) )
let Amp be AmpleSet of R; ::_thesis: 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) )
let A, B, C be Element of R; ::_thesis: ( B is_associated_to C implies ( gcd (A,B,Amp) is_associated_to gcd (A,C,Amp) & gcd (B,A,Amp) is_associated_to gcd (C,A,Amp) ) )
A1: gcd (A,B,Amp) divides B by Def12;
A2: gcd (A,B,Amp) divides A by Def12;
A3: gcd (A,C,Amp) divides A by Def12;
A4: gcd (A,C,Amp) divides C by Def12;
A5: gcd (A,B,Amp) = gcd (B,A,Amp) by Th29;
assume A6: B is_associated_to C ; ::_thesis: ( gcd (A,B,Amp) is_associated_to gcd (A,C,Amp) & gcd (B,A,Amp) is_associated_to gcd (C,A,Amp) )
then  C divides B by Def3;
then  gcd (A,C,Amp) divides B by A4, Th2;
then A7: gcd (A,C,Amp) divides gcd (A,B,Amp) by A3, Def12;
 B divides C by A6, Def3;
then  gcd (A,B,Amp) divides C by A1, Th2;
then  gcd (A,B,Amp) divides gcd (A,C,Amp) by A2, Def12;
then  gcd (A,B,Amp) is_associated_to gcd (A,C,Amp) by A7, Def3;
hence  ( gcd (A,B,Amp) is_associated_to gcd (A,C,Amp) & gcd (B,A,Amp) is_associated_to gcd (C,A,Amp) ) by A5, Th29; ::_thesis: verum
end;

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
let R be gcdDomain; ::_thesis: 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)
let Amp be AmpleSet of R; ::_thesis: for a, b, c being Element of R holds gcd ((gcd (a,b,Amp)),c,Amp) = gcd (a,(gcd (b,c,Amp)),Amp)
let A, B, C be Element of R; ::_thesis: gcd ((gcd (A,B,Amp)),C,Amp) = gcd (A,(gcd (B,C,Amp)),Amp)
set D = gcd ((gcd (A,B,Amp)),C,Amp);
set E = gcd (A,(gcd (B,C,Amp)),Amp);
A1: gcd ((gcd (A,B,Amp)),C,Amp) divides C by Def12;
A2: gcd (A,(gcd (B,C,Amp)),Amp) divides A by Def12;
A3: gcd (A,(gcd (B,C,Amp)),Amp) divides gcd (B,C,Amp) by Def12;
then A4: gcd (A,(gcd (B,C,Amp)),Amp) divides C by Th28;
 gcd (A,(gcd (B,C,Amp)),Amp) divides B by A3, Th28;
then  gcd (A,(gcd (B,C,Amp)),Amp) divides gcd (A,B,Amp) by A2, Def12;
then A5: gcd (A,(gcd (B,C,Amp)),Amp) divides gcd ((gcd (A,B,Amp)),C,Amp) by A4, Def12;
A6: ( gcd ((gcd (A,B,Amp)),C,Amp) is Element of Amp & gcd (A,(gcd (B,C,Amp)),Amp) is Element of Amp ) by Def12;
A7: gcd ((gcd (A,B,Amp)),C,Amp) divides gcd (A,B,Amp) by Def12;
then A8: gcd ((gcd (A,B,Amp)),C,Amp) divides A by Th28;
 gcd ((gcd (A,B,Amp)),C,Amp) divides B by A7, Th28;
then  gcd ((gcd (A,B,Amp)),C,Amp) divides gcd (B,C,Amp) by A1, Def12;
then  gcd ((gcd (A,B,Amp)),C,Amp) divides gcd (A,(gcd (B,C,Amp)),Amp) by A8, Def12;
then  gcd ((gcd (A,B,Amp)),C,Amp) is_associated_to gcd (A,(gcd (B,C,Amp)),Amp) by A5, Def3;
hence  gcd ((gcd (A,B,Amp)),C,Amp) = gcd (A,(gcd (B,C,Amp)),Amp) by A6, Th22; ::_thesis: verum
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
let R be gcdDomain; ::_thesis: 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))
let Amp be AmpleSet of R; ::_thesis: for a, b, c being Element of R holds gcd ((a * c),(b * c),Amp) is_associated_to c * (gcd (a,b,Amp))
let A, B, C be Element of R; ::_thesis: gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp))
now__::_thesis:_(_(_C_<>_0._R_&_gcd_((A_*_C),(B_*_C),Amp)_is_associated_to_C_*_(gcd_(A,B,Amp))_)_or_(_C_=_0._R_&_gcd_((A_*_C),(B_*_C),Amp)_is_associated_to_C_*_(gcd_(A,B,Amp))_)_)
percases ( C <> 0. R or C = 0. R ) ;
caseA1: C <> 0. R ; ::_thesis: gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp))
set D = gcd (A,B,Amp);
now__::_thesis:_(_(_gcd_(A,B,Amp)_<>_0._R_&_gcd_((A_*_C),(B_*_C),Amp)_is_associated_to_C_*_(gcd_(A,B,Amp))_)_or_(_gcd_(A,B,Amp)_=_0._R_&_gcd_((A_*_C),(B_*_C),Amp)_is_associated_to_C_*_(gcd_(A,B,Amp))_)_)
percases ( gcd (A,B,Amp) <> 0. R or gcd (A,B,Amp) = 0. R ) ;
caseA2: gcd (A,B,Amp) <> 0. R ; ::_thesis: gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp))
set E = gcd ((A * C),(B * C),Amp);
A3: gcd ((A * C),(B * C),Amp) divides B * C by Def12;
 gcd (A,B,Amp) divides B by Def12;
then A4: C * (gcd (A,B,Amp)) divides B * C by Th5;
 gcd (A,B,Amp) divides A by Def12;
then  C * (gcd (A,B,Amp)) divides A * C by Th5;
then  C * (gcd (A,B,Amp)) divides gcd ((A * C),(B * C),Amp) by A4, Def12;
then consider F being Element of R such that
A5: gcd ((A * C),(B * C),Amp) = (C * (gcd (A,B,Amp))) * F by Def1;
A6: gcd ((A * C),(B * C),Amp) divides A * C by Def12;
 ( (gcd (A,B,Amp)) * F divides A & (gcd (A,B,Amp)) * F divides B )
proof
consider G being Element of R such that
A7: ((C * (gcd (A,B,Amp))) * F) * G = A * C by A5, A6, Def1;
 (C * ((gcd (A,B,Amp)) * F)) * G = C * A by A7, GROUP_1:def_3;
then A8: C * ((gcd (A,B,Amp)) * F) divides C * A by Def1;
consider G being Element of R such that
A9: ((C * (gcd (A,B,Amp))) * F) * G = B * C by A5, A3, Def1;
 (C * ((gcd (A,B,Amp)) * F)) * G = C * B by A9, GROUP_1:def_3;
then  C * ((gcd (A,B,Amp)) * F) divides C * B by Def1;
hence  ( (gcd (A,B,Amp)) * F divides A & (gcd (A,B,Amp)) * F divides B ) by A1, A8, Th15; ::_thesis: verum
end;
then A10: (gcd (A,B,Amp)) * F divides gcd (A,B,Amp) by Def12;
 gcd (A,B,Amp) = (gcd (A,B,Amp)) * (1. R) by VECTSP_1:def_4;
then  F divides 1. R by A2, A10, Th15;
then  F is unital by Def2;
hence  gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp)) by A5, Th18; ::_thesis: verum
end;
caseA11: gcd (A,B,Amp) = 0. R ; ::_thesis: gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp))
then A12: C * (gcd (A,B,Amp)) = 0. R by VECTSP_1:7;
 ( A = 0. R & B = 0. R ) by A11, Th33;
then  gcd ((A * C),(B * C),Amp) = gcd ((0. R),((0. R) * C),Amp) by VECTSP_1:7
.= gcd ((0. R),(0. R),Amp) by VECTSP_1:7
.= C * (gcd (A,B,Amp)) by A12, Th31 ;
hence  gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp)) ; ::_thesis: verum
end;
end;
end;
hence  gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp)) ; ::_thesis: verum
end;
caseA13: C = 0. R ; ::_thesis: gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp))
then  ( A * C = 0. R & B * C = 0. R ) by VECTSP_1:7;
then  gcd ((A * C),(B * C),Amp) = 0. R by Th31
.= C * (gcd (A,B,Amp)) by A13, VECTSP_1:7 ;
hence  gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp)) ; ::_thesis: verum
end;
end;
end;
hence  gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp)) ; ::_thesis: verum
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
let R be gcdDomain; ::_thesis: 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)
let Amp be AmpleSet of R; ::_thesis: 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)
let A, B, C be Element of R; ::_thesis: ( gcd (A,B,Amp) = 1. R implies gcd (A,(B * C),Amp) = gcd (A,C,Amp) )
assume  gcd (A,B,Amp) = 1. R ; ::_thesis: gcd (A,(B * C),Amp) = gcd (A,C,Amp)
then A1: C * (gcd (A,B,Amp)) = C by VECTSP_1:def_4;
 gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp)) by Th36;
then  gcd (A,C,Amp) is_associated_to gcd (A,(gcd ((A * C),(B * C),Amp)),Amp) by A1, Th34;
then A2: gcd (A,C,Amp) is_associated_to gcd ((gcd (A,(A * C),Amp)),(B * C),Amp) by Th35;
A3: A * (gcd ((1. R),C,Amp)) = A * (1. R) by Th32
.= A by VECTSP_1:def_4 ;
 gcd ((A * (1. R)),(A * C),Amp) is_associated_to A * (gcd ((1. R),C,Amp)) by Th36;
then  gcd (A,(A * C),Amp) is_associated_to A by A3, VECTSP_1:def_4;
then A4: gcd ((gcd (A,(A * C),Amp)),(B * C),Amp) is_associated_to gcd (A,(B * C),Amp) by Th34;
 ( gcd (A,(B * C),Amp) is Element of Amp & gcd (A,C,Amp) is Element of Amp ) by Def12;
hence  gcd (A,(B * C),Amp) = gcd (A,C,Amp) by A2, A4, Th4, Th22; ::_thesis: verum
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
let R be gcdDomain; ::_thesis: 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
let Amp be AmpleSet of R; ::_thesis: 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
let A, B, C be Element of R; ::_thesis: ( C = gcd (A,B,Amp) & C <> 0. R implies gcd ((A / C),(B / C),Amp) = 1. R )
assume that
A1: C = gcd (A,B,Amp) and
A2: C <> 0. R ; ::_thesis: gcd ((A / C),(B / C),Amp) = 1. R
set A1 = A / C;
 C divides A by A1, Def12;
then A3: (A / C) * C = A by A2, Def4;
set B1 = B / C;
A4: gcd (((A / C) * C),((B / C) * C),Amp) is_associated_to C * (gcd ((A / C),(B / C),Amp)) by Th36;
A5: ( gcd ((A / C),(B / C),Amp) is Element of Amp & 1. R is Element of Amp ) by Def8, Def12;
 C divides B by A1, Def12;
then  gcd (A,B,Amp) = gcd (((A / C) * C),((B / C) * C),Amp) by A2, A3, Def4;
then  C * (1. R) is_associated_to C * (gcd ((A / C),(B / C),Amp)) by A1, A4, VECTSP_1:def_4;
hence  gcd ((A / C),(B / C),Amp) = 1. R by A2, A5, Th19, Th22; ::_thesis: verum
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
let R be gcdDomain; ::_thesis: 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)
let Amp be AmpleSet of R; ::_thesis: for a, b, c being Element of R holds gcd ((a + (b * c)),c,Amp) = gcd (a,c,Amp)
let A, B, C be Element of R; ::_thesis: gcd ((A + (B * C)),C,Amp) = gcd (A,C,Amp)
set D = gcd (A,C,Amp);
 gcd (A,C,Amp) divides A by Def12;
then consider E being Element of R such that
A1: (gcd (A,C,Amp)) * E = A by Def1;
A2: gcd (A,C,Amp) divides C by Def12;
then consider F being Element of R such that
A3: (gcd (A,C,Amp)) * F = C by Def1;
A4: for z being Element of R st z divides A + (B * C) & z divides C holds
z divides gcd (A,C,Amp)
proof
let Z be Element of R; ::_thesis: ( Z divides A + (B * C) & Z divides C implies Z divides gcd (A,C,Amp) )
assume that
A5: Z divides A + (B * C) and
A6: Z divides C ; ::_thesis: Z divides gcd (A,C,Amp)
consider X being Element of R such that
A7: Z * X = C by A6, Def1;
consider Y being Element of R such that
A8: Z * Y = A + (B * C) by A5, Def1;
Z * (Y + (- (B * X))) = (Z * Y) + (Z * (- (B * X))) by VECTSP_1:def_2
.= (Z * Y) + (- (Z * (X * B))) by VECTSP_1:8
.= (A + (B * C)) + (- (C * B)) by A7, A8, GROUP_1:def_3
.= A + ((B * C) + (- (C * B))) by RLVECT_1:def_3
.= A + (0. R) by RLVECT_1:def_10
.= A by RLVECT_1:4 ;
then  Z divides A by Def1;
hence  Z divides gcd (A,C,Amp) by A6, Def12; ::_thesis: verum
end;
(gcd (A,C,Amp)) * (E + (F * B)) = ((gcd (A,C,Amp)) * E) + ((gcd (A,C,Amp)) * (F * B)) by VECTSP_1:def_2
.= A + (B * C) by A1, A3, GROUP_1:def_3 ;
then A9: gcd (A,C,Amp) divides A + (B * C) by Def1;
 gcd (A,C,Amp) is Element of Amp by Def12;
hence  gcd ((A + (B * C)),C,Amp) = gcd (A,C,Amp) by A2, A9, A4, Def12; ::_thesis: verum
end;

begin

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
let R be gcdDomain; ::_thesis: 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)
let Amp be AmpleSet of R; ::_thesis: 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)
let r1, r2, s1, s2 be Element of R; ::_thesis: ( gcd (r1,r2,Amp) = 1. R & gcd (s1,s2,Amp) = 1. R & r2 <> 0. R implies gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(r2 * (s2 / (gcd (r2,s2,Amp)))),Amp) = gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp) )
assume that
A1: gcd (r1,r2,Amp) = 1. R and
A2: gcd (s1,s2,Amp) = 1. R and
A3: r2 <> 0. R ; ::_thesis: 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)
set d = gcd (r2,s2,Amp);
set r = r2 / (gcd (r2,s2,Amp));
set s = s2 / (gcd (r2,s2,Amp));
A4: gcd (r2,s2,Amp) <> 0. R by A3, Th33;
then A5: gcd ((r2 / (gcd (r2,s2,Amp))),(s2 / (gcd (r2,s2,Amp))),Amp) = 1. R by Th38;
A6: gcd (r2,s2,Amp) divides s2 by Def12;
 gcd ((s2 / (gcd (r2,s2,Amp))),s1,Amp) = 1. R
proof
 gcd ((s2 / (gcd (r2,s2,Amp))),s1,Amp) divides s2 / (gcd (r2,s2,Amp)) by Def12;
then consider e being Element of R such that
A7: (gcd ((s2 / (gcd (r2,s2,Amp))),s1,Amp)) * e = s2 / (gcd (r2,s2,Amp)) by Def1;
(gcd ((s2 / (gcd (r2,s2,Amp))),s1,Amp)) * (e * (gcd (r2,s2,Amp))) = (s2 / (gcd (r2,s2,Amp))) * (gcd (r2,s2,Amp)) by A7, GROUP_1:def_3
.= s2 by A6, A4, Def4 ;
then A8: gcd ((s2 / (gcd (r2,s2,Amp))),s1,Amp) divides s2 by Def1;
A9: ( gcd ((s2 / (gcd (r2,s2,Amp))),s1,Amp) is Element of Amp & 1. R is Element of Amp ) by Def8, Def12;
 (1. R) * (gcd ((s2 / (gcd (r2,s2,Amp))),s1,Amp)) = gcd ((s2 / (gcd (r2,s2,Amp))),s1,Amp) by VECTSP_1:def_8;
then A10: 1. R divides gcd ((s2 / (gcd (r2,s2,Amp))),s1,Amp) by Def1;
 gcd ((s2 / (gcd (r2,s2,Amp))),s1,Amp) divides s1 by Def12;
then  gcd ((s2 / (gcd (r2,s2,Amp))),s1,Amp) divides gcd (s1,s2,Amp) by A8, Def12;
then  gcd ((s2 / (gcd (r2,s2,Amp))),s1,Amp) is_associated_to 1. R by A2, A10, Def3;
hence  gcd ((s2 / (gcd (r2,s2,Amp))),s1,Amp) = 1. R by A9, Th22; ::_thesis: verum
end;
then A11: gcd ((s2 / (gcd (r2,s2,Amp))),(s1 * (r2 / (gcd (r2,s2,Amp)))),Amp) = gcd ((s2 / (gcd (r2,s2,Amp))),(r2 / (gcd (r2,s2,Amp))),Amp) by Th37;
 gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(s2 / (gcd (r2,s2,Amp))),Amp) = gcd ((s1 * (r2 / (gcd (r2,s2,Amp)))),(s2 / (gcd (r2,s2,Amp))),Amp) by Th39;
then A12: gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(s2 / (gcd (r2,s2,Amp))),Amp) = gcd ((s2 / (gcd (r2,s2,Amp))),(s1 * (r2 / (gcd (r2,s2,Amp)))),Amp) by Th29
.= 1. R by A11, A5, Th29 ;
A13: gcd (r2,s2,Amp) divides (gcd (r2,s2,Amp)) * r2 by Th6;
A14: gcd (r2,s2,Amp) divides r2 by Def12;
 gcd ((r2 / (gcd (r2,s2,Amp))),r1,Amp) = 1. R
proof
 gcd ((r2 / (gcd (r2,s2,Amp))),r1,Amp) divides r2 / (gcd (r2,s2,Amp)) by Def12;
then consider e being Element of R such that
A15: (gcd ((r2 / (gcd (r2,s2,Amp))),r1,Amp)) * e = r2 / (gcd (r2,s2,Amp)) by Def1;
(gcd ((r2 / (gcd (r2,s2,Amp))),r1,Amp)) * (e * (gcd (r2,s2,Amp))) = (r2 / (gcd (r2,s2,Amp))) * (gcd (r2,s2,Amp)) by A15, GROUP_1:def_3
.= r2 by A14, A4, Def4 ;
then A16: gcd ((r2 / (gcd (r2,s2,Amp))),r1,Amp) divides r2 by Def1;
A17: ( gcd ((r2 / (gcd (r2,s2,Amp))),r1,Amp) is Element of Amp & 1. R is Element of Amp ) by Def8, Def12;
 (1. R) * (gcd ((r2 / (gcd (r2,s2,Amp))),r1,Amp)) = gcd ((r2 / (gcd (r2,s2,Amp))),r1,Amp) by VECTSP_1:def_8;
then A18: 1. R divides gcd ((r2 / (gcd (r2,s2,Amp))),r1,Amp) by Def1;
 gcd ((r2 / (gcd (r2,s2,Amp))),r1,Amp) divides r1 by Def12;
then  gcd ((r2 / (gcd (r2,s2,Amp))),r1,Amp) divides gcd (r1,r2,Amp) by A16, Def12;
then  gcd ((r2 / (gcd (r2,s2,Amp))),r1,Amp) is_associated_to 1. R by A1, A18, Def3;
hence  gcd ((r2 / (gcd (r2,s2,Amp))),r1,Amp) = 1. R by A17, Th22; ::_thesis: verum
end;
then A19: gcd ((r2 / (gcd (r2,s2,Amp))),(r1 * (s2 / (gcd (r2,s2,Amp)))),Amp) = gcd ((r2 / (gcd (r2,s2,Amp))),(s2 / (gcd (r2,s2,Amp))),Amp) by Th37;
A20: gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(r2 / (gcd (r2,s2,Amp))),Amp) = gcd ((r1 * (s2 / (gcd (r2,s2,Amp)))),(r2 / (gcd (r2,s2,Amp))),Amp) by Th39;
 gcd ((r2 / (gcd (r2,s2,Amp))),(s2 / (gcd (r2,s2,Amp))),Amp) = 1. R by A4, Th38;
then A21: gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),((gcd (r2,s2,Amp)) * (r2 / (gcd (r2,s2,Amp)))),Amp) = gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp) by A20, A19, Th29, Th37;
r2 * (s2 / (gcd (r2,s2,Amp))) = ((1. R) * r2) * (s2 / (gcd (r2,s2,Amp))) by VECTSP_1:def_8
.= (((gcd (r2,s2,Amp)) / (gcd (r2,s2,Amp))) * r2) * (s2 / (gcd (r2,s2,Amp))) by A4, Th9
.= (((gcd (r2,s2,Amp)) * r2) / (gcd (r2,s2,Amp))) * (s2 / (gcd (r2,s2,Amp))) by A4, A13, Th11
.= (s2 / (gcd (r2,s2,Amp))) * ((gcd (r2,s2,Amp)) * (r2 / (gcd (r2,s2,Amp)))) by A14, A4, A13, Th11 ;
hence  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) by A12, A21, Th37; ::_thesis: verum
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
proof
let R be gcdDomain; ::_thesis: 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
let Amp be AmpleSet of R; ::_thesis: 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
let r1, r2, s1, s2 be Element of R; ::_thesis: ( gcd (r1,r2,Amp) = 1. R & gcd (s1,s2,Amp) = 1. R & r2 <> 0. R & s2 <> 0. R implies gcd (((r1 / (gcd (r1,s2,Amp))) * (s1 / (gcd (s1,r2,Amp)))),((r2 / (gcd (s1,r2,Amp))) * (s2 / (gcd (r1,s2,Amp)))),Amp) = 1. R )
assume that
A1: gcd (r1,r2,Amp) = 1. R and
A2: gcd (s1,s2,Amp) = 1. R and
A3: r2 <> 0. R and
A4: s2 <> 0. R ; ::_thesis: gcd (((r1 / (gcd (r1,s2,Amp))) * (s1 / (gcd (s1,r2,Amp)))),((r2 / (gcd (s1,r2,Amp))) * (s2 / (gcd (r1,s2,Amp)))),Amp) = 1. R
set d1 = gcd (r1,s2,Amp);
A5: gcd (r1,s2,Amp) <> 0. R by A4, Th33;
set d2 = gcd (s1,r2,Amp);
set s19 = s1 / (gcd (s1,r2,Amp));
set r29 = r2 / (gcd (s1,r2,Amp));
A6: gcd (s1,r2,Amp) <> 0. R by A3, Th33;
then A7: gcd ((s1 / (gcd (s1,r2,Amp))),(r2 / (gcd (s1,r2,Amp))),Amp) = 1. R by Th38;
set r19 = r1 / (gcd (r1,s2,Amp));
A8: gcd ((r1 / (gcd (r1,s2,Amp))),(r2 / (gcd (s1,r2,Amp))),Amp) divides r2 / (gcd (s1,r2,Amp)) by Def12;
 gcd (s1,r2,Amp) divides r2 by Def12;
then  (r2 / (gcd (s1,r2,Amp))) * (gcd (s1,r2,Amp)) = r2 by A6, Def4;
then  r2 / (gcd (s1,r2,Amp)) divides r2 by Def1;
then A9: gcd ((r1 / (gcd (r1,s2,Amp))),(r2 / (gcd (s1,r2,Amp))),Amp) divides r2 by A8, Th2;
A10: ( gcd ((r1 / (gcd (r1,s2,Amp))),(r2 / (gcd (s1,r2,Amp))),Amp) is Element of Amp & 1. R is Element of Amp ) by Def8, Def12;
 gcd (r1,s2,Amp) divides r1 by Def12;
then  (r1 / (gcd (r1,s2,Amp))) * (gcd (r1,s2,Amp)) = r1 by A5, Def4;
then A11: r1 / (gcd (r1,s2,Amp)) divides r1 by Def1;
 (1. R) * (gcd ((r1 / (gcd (r1,s2,Amp))),(r2 / (gcd (s1,r2,Amp))),Amp)) = gcd ((r1 / (gcd (r1,s2,Amp))),(r2 / (gcd (s1,r2,Amp))),Amp) by VECTSP_1:def_8;
then A12: 1. R divides gcd ((r1 / (gcd (r1,s2,Amp))),(r2 / (gcd (s1,r2,Amp))),Amp) by Def1;
 gcd ((r1 / (gcd (r1,s2,Amp))),(r2 / (gcd (s1,r2,Amp))),Amp) divides r1 / (gcd (r1,s2,Amp)) by Def12;
then  gcd ((r1 / (gcd (r1,s2,Amp))),(r2 / (gcd (s1,r2,Amp))),Amp) divides r1 by A11, Th2;
then  gcd ((r1 / (gcd (r1,s2,Amp))),(r2 / (gcd (s1,r2,Amp))),Amp) divides gcd (r1,r2,Amp) by A9, Def12;
then  gcd ((r1 / (gcd (r1,s2,Amp))),(r2 / (gcd (s1,r2,Amp))),Amp) is_associated_to 1. R by A1, A12, Def3;
then  gcd ((r1 / (gcd (r1,s2,Amp))),(r2 / (gcd (s1,r2,Amp))),Amp) = 1. R by A10, Th22;
then A13: gcd ((r2 / (gcd (s1,r2,Amp))),(r1 / (gcd (r1,s2,Amp))),Amp) = 1. R by Th29;
set s29 = s2 / (gcd (r1,s2,Amp));
A14: gcd ((s1 / (gcd (s1,r2,Amp))),(s2 / (gcd (r1,s2,Amp))),Amp) divides s2 / (gcd (r1,s2,Amp)) by Def12;
 gcd (r1,s2,Amp) divides s2 by Def12;
then  (s2 / (gcd (r1,s2,Amp))) * (gcd (r1,s2,Amp)) = s2 by A5, Def4;
then  s2 / (gcd (r1,s2,Amp)) divides s2 by Def1;
then A15: gcd ((s1 / (gcd (s1,r2,Amp))),(s2 / (gcd (r1,s2,Amp))),Amp) divides s2 by A14, Th2;
A16: ( gcd ((s1 / (gcd (s1,r2,Amp))),(s2 / (gcd (r1,s2,Amp))),Amp) is Element of Amp & 1. R is Element of Amp ) by Def8, Def12;
 gcd (s1,r2,Amp) divides s1 by Def12;
then  (s1 / (gcd (s1,r2,Amp))) * (gcd (s1,r2,Amp)) = s1 by A6, Def4;
then A17: s1 / (gcd (s1,r2,Amp)) divides s1 by Def1;
 (1. R) * (gcd ((s1 / (gcd (s1,r2,Amp))),(s2 / (gcd (r1,s2,Amp))),Amp)) = gcd ((s1 / (gcd (s1,r2,Amp))),(s2 / (gcd (r1,s2,Amp))),Amp) by VECTSP_1:def_8;
then A18: 1. R divides gcd ((s1 / (gcd (s1,r2,Amp))),(s2 / (gcd (r1,s2,Amp))),Amp) by Def1;
 gcd ((s1 / (gcd (s1,r2,Amp))),(s2 / (gcd (r1,s2,Amp))),Amp) divides s1 / (gcd (s1,r2,Amp)) by Def12;
then  gcd ((s1 / (gcd (s1,r2,Amp))),(s2 / (gcd (r1,s2,Amp))),Amp) divides s1 by A17, Th2;
then  gcd ((s1 / (gcd (s1,r2,Amp))),(s2 / (gcd (r1,s2,Amp))),Amp) divides gcd (s1,s2,Amp) by A15, Def12;
then  gcd ((s1 / (gcd (s1,r2,Amp))),(s2 / (gcd (r1,s2,Amp))),Amp) is_associated_to 1. R by A2, A18, Def3;
then A19: gcd ((s1 / (gcd (s1,r2,Amp))),(s2 / (gcd (r1,s2,Amp))),Amp) = 1. R by A16, Th22;
A20: gcd ((s2 / (gcd (r1,s2,Amp))),(r1 / (gcd (r1,s2,Amp))),Amp) = gcd ((r1 / (gcd (r1,s2,Amp))),(s2 / (gcd (r1,s2,Amp))),Amp) by Th29
.= 1. R by A5, Th38 ;
gcd (((r1 / (gcd (r1,s2,Amp))) * (s1 / (gcd (s1,r2,Amp)))),(r2 / (gcd (s1,r2,Amp))),Amp) = gcd ((r2 / (gcd (s1,r2,Amp))),((r1 / (gcd (r1,s2,Amp))) * (s1 / (gcd (s1,r2,Amp)))),Amp) by Th29
.= gcd ((r2 / (gcd (s1,r2,Amp))),(s1 / (gcd (s1,r2,Amp))),Amp) by A13, Th37
.= 1. R by A7, Th29 ;
then  gcd (((r1 / (gcd (r1,s2,Amp))) * (s1 / (gcd (s1,r2,Amp)))),((r2 / (gcd (s1,r2,Amp))) * (s2 / (gcd (r1,s2,Amp)))),Amp) = gcd (((r1 / (gcd (r1,s2,Amp))) * (s1 / (gcd (s1,r2,Amp)))),(s2 / (gcd (r1,s2,Amp))),Amp) by Th37
.= gcd ((s2 / (gcd (r1,s2,Amp))),((r1 / (gcd (r1,s2,Amp))) * (s1 / (gcd (s1,r2,Amp)))),Amp) by Th29
.= gcd ((s2 / (gcd (r1,s2,Amp))),(s1 / (gcd (s1,r2,Amp))),Amp) by A20, Th37
.= 1. R by A19, Th29 ;
hence  gcd (((r1 / (gcd (r1,s2,Amp))) * (s1 / (gcd (s1,r2,Amp)))),((r2 / (gcd (s1,r2,Amp))) * (s2 / (gcd (r1,s2,Amp)))),Amp) = 1. R ; ::_thesis: verum
end;

begin

definition
let R be non empty associative well-unital gcd-like multLoopStr ;
let Amp be AmpleSet of R;
let x, y be Element of R;
predx,y are_canonical_wrt Amp means :Def13: :: GCD_1:def 13
 gcd (x,y,Amp) = 1. R;
end;

:: deftheorem Def13 defines are_canonical_wrt GCD_1:def_13_:_
 for R being non empty associative well-unital gcd-like multLoopStr
for Amp being AmpleSet of R
for x, y being Element of R holds
( x,y are_canonical_wrt Amp iff gcd (x,y,Amp) = 1. R );

theorem Th42: :: GCD_1:42
for R being gcdDomain
for Amp, Amp9 being AmpleSet of R
for x, y being Element of R st x,y are_canonical_wrt Amp holds
x,y are_canonical_wrt Amp9
proof
let R be gcdDomain; ::_thesis: 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
let Amp, Amp9 be AmpleSet of R; ::_thesis: for x, y being Element of R st x,y are_canonical_wrt Amp holds
x,y are_canonical_wrt Amp9
let x, y be Element of R; ::_thesis: ( x,y are_canonical_wrt Amp implies x,y are_canonical_wrt Amp9 )
 (1. R) * x = x by VECTSP_1:def_8;
then A1: 1. R divides x by Def1;
 (1. R) * y = y by VECTSP_1:def_8;
then A2: 1. R divides y by Def1;
assume  x,y are_canonical_wrt Amp ; ::_thesis: x,y are_canonical_wrt Amp9
then  gcd (x,y,Amp) = 1. R by Def13;
then A3: for z being Element of R st z divides x & z divides y holds
z divides 1. R by Def12;
 1. R in Amp9 by Def8;
then  gcd (x,y,Amp9) = 1. R by A3, A1, A2, Def12;
hence  x,y are_canonical_wrt Amp9 by Def13; ::_thesis: verum
end;

definition
let R be non empty associative well-unital gcd-like multLoopStr ;
let x, y be Element of R;
predx,y are_co-prime  means :Def14: :: GCD_1:def 14
 ex Amp being AmpleSet of R st gcd (x,y,Amp) = 1. R;
end;

:: deftheorem Def14 defines are_co-prime GCD_1:def_14_:_
 for R being non empty associative well-unital gcd-like multLoopStr
for x, y being Element of R holds
( x,y are_co-prime iff ex Amp being AmpleSet of R st gcd (x,y,Amp) = 1. R );

definition
let R be gcdDomain;
let x, y be Element of R;
:: original: are_co-prime
redefine predx,y are_co-prime ;
symmetry
 for x, y being Element of R st (R,b1,b2) holds
(R,b2,b1)
proof
let x, y be Element of R; ::_thesis: ( (R,x,y) implies (R,y,x) )
given Amp being AmpleSet of R such that A1: gcd (x,y,Amp) = 1. R ; :: according to GCD_1:def_14 ::_thesis: (R,y,x)
 gcd (y,x,Amp) = 1. R by A1, Th29;
hence  (R,y,x) by Def14; ::_thesis: verum
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
let R be gcdDomain; ::_thesis: 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
let Amp be AmpleSet of R; ::_thesis: for x, y being Element of R st x,y are_co-prime holds
gcd (x,y,Amp) = 1. R
let x, y be Element of R; ::_thesis: ( x,y are_co-prime implies gcd (x,y,Amp) = 1. R )
assume  x,y are_co-prime ; ::_thesis: gcd (x,y,Amp) = 1. R
then consider Amp9 being AmpleSet of R such that
A1: gcd (x,y,Amp9) = 1. R by Def14;
 x,y are_canonical_wrt Amp9 by A1, Def13;
then  x,y are_canonical_wrt Amp by Th42;
hence  gcd (x,y,Amp) = 1. R by Def13; ::_thesis: verum
end;

definition
let R be non empty associative well-unital gcd-like multLoopStr_0 ;
let Amp be AmpleSet of R;
let x, y be Element of R;
predx,y are_normalized_wrt Amp means :Def15: :: GCD_1:def 15
( gcd (x,y,Amp) = 1. R & y in Amp & y <> 0. R );
end;

:: deftheorem Def15 defines are_normalized_wrt GCD_1:def_15_:_
 for R being non empty associative well-unital gcd-like multLoopStr_0
for Amp being AmpleSet of R
for x, y being Element of R holds
( x,y are_normalized_wrt Amp iff ( gcd (x,y,Amp) = 1. R & y in Amp & y <> 0. R ) );

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
A5: gcd (s1,s2,Amp) = 1. R by A2, Th43;
A6: ( s1 = 0. R & gcd (r2,s2,Amp) = 1. R implies for z being Element of R holds
( z = r1 iff z = (r1 * s2) + (r2 * s1) ) )
proof
assume that
A7: s1 = 0. R and
 gcd (r2,s2,Amp) = 1. R ; ::_thesis: for z being Element of R holds
( z = r1 iff z = (r1 * s2) + (r2 * s1) )
A8: s2 = 1. R by A4, A5, A7, Th30;
let z be Element of R; ::_thesis: ( z = r1 iff z = (r1 * s2) + (r2 * s1) )
(r1 * s2) + (r2 * s1) = (r1 * s2) + (0. R) by A7, VECTSP_1:7
.= r1 * (1. R) by A8, RLVECT_1:4
.= r1 by VECTSP_1:def_4 ;
hence  ( z = r1 iff z = (r1 * s2) + (r2 * s1) ) ; ::_thesis: verum
end;
A9: ( s1 = 0. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies for z being Element of R holds
( z = r1 iff z = 0. R ) )
proof
A10: 1. R <> 0. R ;
assume that
A11: s1 = 0. R and
A12: (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R ; ::_thesis: for z being Element of R holds
( z = r1 iff z = 0. R )
let z be Element of R; ::_thesis: ( z = r1 iff z = 0. R )
A13: s2 = 1. R by A4, A5, A11, Th30;
then A14: gcd (r2,s2,Amp) = 1. R by Th32;
0. R = (r1 * (s2 / (gcd (r2,s2,Amp)))) + (0. R) by A11, A12, VECTSP_1:7
.= r1 * ((1. R) / (gcd (r2,s2,Amp))) by A13, RLVECT_1:4
.= r1 * (1. R) by A14, A10, Th9
.= r1 by VECTSP_1:def_4 ;
hence  ( z = r1 iff z = 0. R ) ; ::_thesis: verum
end;
A15: gcd (r1,r2,Amp) = 1. R by A1, Th43;
A16: ( r1 = 0. R & gcd (r2,s2,Amp) = 1. R implies for z being Element of R holds
( z = s1 iff z = (r1 * s2) + (r2 * s1) ) )
proof
assume that
A17: r1 = 0. R and
 gcd (r2,s2,Amp) = 1. R ; ::_thesis: for z being Element of R holds
( z = s1 iff z = (r1 * s2) + (r2 * s1) )
A18: r2 = 1. R by A3, A15, A17, Th30;
let z be Element of R; ::_thesis: ( z = s1 iff z = (r1 * s2) + (r2 * s1) )
(r1 * s2) + (r2 * s1) = (0. R) + (r2 * s1) by A17, VECTSP_1:7
.= (1. R) * s1 by A18, RLVECT_1:4
.= s1 by VECTSP_1:def_8 ;
hence  ( z = s1 iff z = (r1 * s2) + (r2 * s1) ) ; ::_thesis: verum
end;
A19: ( r1 = 0. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies for z being Element of R holds
( z = s1 iff z = 0. R ) )
proof
A20: 1. R <> 0. R ;
assume that
A21: r1 = 0. R and
A22: (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R ; ::_thesis: for z being Element of R holds
( z = s1 iff z = 0. R )
let z be Element of R; ::_thesis: ( z = s1 iff z = 0. R )
A23: r2 = 1. R by A3, A15, A21, Th30;
then A24: gcd (r2,s2,Amp) = 1. R by Th32;
0. R = (0. R) + (s1 * (r2 / (gcd (r2,s2,Amp)))) by A21, A22, VECTSP_1:7
.= s1 * ((1. R) / (gcd (r2,s2,Amp))) by A23, RLVECT_1:4
.= s1 * (1. R) by A24, A20, Th9
.= s1 by VECTSP_1:def_4 ;
hence  ( z = s1 iff z = 0. R ) ; ::_thesis: verum
end;
 ( gcd (r2,s2,Amp) = 1. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies for z being Element of R holds
( z = (r1 * s2) + (r2 * s1) iff z = 0. R ) )
proof
assume A25: ( gcd (r2,s2,Amp) = 1. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R ) ; ::_thesis: for z being Element of R holds
( z = (r1 * s2) + (r2 * s1) iff z = 0. R )
let z be Element of R; ::_thesis: ( z = (r1 * s2) + (r2 * s1) iff z = 0. R )
0. R = (r1 * s2) + (s1 * (r2 / (1. R))) by A25, Th10
.= (r1 * s2) + (s1 * r2) by Th10 ;
hence  ( z = (r1 * s2) + (r2 * s1) iff z = 0. R ) ; ::_thesis: verum
end;
hence  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 ) ) ) by A16, A19, A6, A9; ::_thesis: verum
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
A5: ( gcd (r2,s2,Amp) = 1. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies for z being Element of R holds
( z = r2 * s2 iff z = 1. R ) )
proof
assume that
A6: gcd (r2,s2,Amp) = 1. R and
A7: (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R ; ::_thesis: for z being Element of R holds
( z = r2 * s2 iff z = 1. R )
A8: 0. R = (r1 * s2) + (s1 * (r2 / (1. R))) by A6, A7, Th10
.= (r1 * s2) + (s1 * r2) by Th10 ;
then A9: r1 * s2 = - (s1 * r2) by RLVECT_1:6;
A10: s1 * r2 = - (r1 * s2) by A8, RLVECT_1:6;
 gcd (s2,s1,Amp) = 1. R by A2, Th43;
then  gcd (s2,(s1 * r2),Amp) = gcd (s2,r2,Amp) by Th37
.= 1. R by A6, Th29 ;
then  1. R = gcd (((1. R) * s2),(- (r1 * s2)),Amp) by A10, VECTSP_1:def_8
.= gcd (((1. R) * s2),((- r1) * s2),Amp) by VECTSP_1:8 ;
then A11: 1. R is_associated_to s2 * (gcd ((1. R),(- r1),Amp)) by Th36;
let z be Element of R; ::_thesis: ( z = r2 * s2 iff z = 1. R )
A12: 1. R in Amp by Th22;
 gcd (r2,r1,Amp) = 1. R by A1, Th43;
then  gcd (r2,(r1 * s2),Amp) = 1. R by A6, Th37;
then  1. R = gcd (((1. R) * r2),(- (s1 * r2)),Amp) by A9, VECTSP_1:def_8
.= gcd (((1. R) * r2),((- s1) * r2),Amp) by VECTSP_1:8 ;
then A13: 1. R is_associated_to r2 * (gcd ((1. R),(- s1),Amp)) by Th36;
s2 * (gcd ((1. R),(- r1),Amp)) = s2 * (1. R) by Th32
.= s2 by VECTSP_1:def_4 ;
then A14: s2 = 1. R by A4, A12, A11, Def9;
r2 * (gcd ((1. R),(- s1),Amp)) = r2 * (1. R) by Th32
.= r2 by VECTSP_1:def_4 ;
then  r2 = 1. R by A3, A13, A12, Def9;
hence  ( z = r2 * s2 iff z = 1. R ) by A14, VECTSP_1:def_4; ::_thesis: verum
end;
A15: gcd (r1,r2,Amp) = 1. R by A1, Th43;
A16: ( r1 = 0. R & gcd (r2,s2,Amp) = 1. R implies for z being Element of R holds
( z = s2 iff z = r2 * s2 ) )
proof
assume that
A17: r1 = 0. R and
 gcd (r2,s2,Amp) = 1. R ; ::_thesis: for z being Element of R holds
( z = s2 iff z = r2 * s2 )
let z be Element of R; ::_thesis: ( z = s2 iff z = r2 * s2 )
 r2 = 1. R by A3, A15, A17, Th30;
hence  ( z = s2 iff z = r2 * s2 ) by VECTSP_1:def_8; ::_thesis: verum
end;
A18: gcd (s1,s2,Amp) = 1. R by A2, Th43;
A19: ( s1 = 0. R & gcd (r2,s2,Amp) = 1. R implies for z being Element of R holds
( z = r2 iff z = r2 * s2 ) )
proof
assume that
A20: s1 = 0. R and
 gcd (r2,s2,Amp) = 1. R ; ::_thesis: for z being Element of R holds
( z = r2 iff z = r2 * s2 )
let z be Element of R; ::_thesis: ( z = r2 iff z = r2 * s2 )
 s2 = 1. R by A4, A18, A20, Th30;
hence  ( z = r2 iff z = r2 * s2 ) by VECTSP_1:def_4; ::_thesis: verum
end;
A21: ( s1 = 0. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies for z being Element of R holds
( z = r2 iff z = 1. R ) )
proof
A22: 1. R <> 0. R ;
assume that
A23: s1 = 0. R and
A24: (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R ; ::_thesis: for z being Element of R holds
( z = r2 iff z = 1. R )
let z be Element of R; ::_thesis: ( z = r2 iff z = 1. R )
A25: s2 = 1. R by A4, A18, A23, Th30;
then A26: gcd (r2,s2,Amp) = 1. R by Th32;
0. R = (r1 * (s2 / (gcd (r2,s2,Amp)))) + (0. R) by A23, A24, VECTSP_1:7
.= r1 * ((1. R) / (gcd (r2,s2,Amp))) by A25, RLVECT_1:4
.= r1 * (1. R) by A26, A22, Th9
.= r1 by VECTSP_1:def_4 ;
hence  ( z = r2 iff z = 1. R ) by A3, A15, Th30; ::_thesis: verum
end;
A27: ( r1 = 0. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R implies for z being Element of R holds
( z = s2 iff z = 1. R ) )
proof
A28: 1. R <> 0. R ;
assume that
A29: r1 = 0. R and
A30: (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R ; ::_thesis: for z being Element of R holds
( z = s2 iff z = 1. R )
let z be Element of R; ::_thesis: ( z = s2 iff z = 1. R )
A31: r2 = 1. R by A3, A15, A29, Th30;
then A32: gcd (r2,s2,Amp) = 1. R by Th32;
0. R = (0. R) + (s1 * (r2 / (gcd (r2,s2,Amp)))) by A29, A30, VECTSP_1:7
.= s1 * ((1. R) / (gcd (r2,s2,Amp))) by A31, RLVECT_1:4
.= s1 * (1. R) by A32, A28, Th9
.= s1 by VECTSP_1:def_4 ;
hence  ( z = s2 iff z = 1. R ) by A4, A18, Th30; ::_thesis: verum
end;
 ( r1 = 0. R & s1 = 0. R implies for z being Element of R holds
( z = s2 iff z = r2 ) )
proof
assume that
A33: r1 = 0. R and
A34: s1 = 0. R ; ::_thesis: for z being Element of R holds
( z = s2 iff z = r2 )
let z be Element of R; ::_thesis: ( z = s2 iff z = r2 )
 r2 = 1. R by A3, A15, A33, Th30;
hence  ( z = s2 iff z = r2 ) by A4, A18, A34, Th30; ::_thesis: verum
end;
hence  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 ) ) ) by A16, A27, A19, A21, A5; ::_thesis: verum
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
let R be gcdDomain; ::_thesis: 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
let Amp be AmpleSet of R; ::_thesis: 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
let r1, r2, s1, s2 be Element of R; ::_thesis: ( Amp is multiplicative & r1,r2 are_normalized_wrt Amp & s1,s2 are_normalized_wrt Amp implies add1 (r1,r2,s1,s2,Amp), add2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp )
assume that
A1: Amp is multiplicative and
A2: r1,r2 are_normalized_wrt Amp and
A3: s1,s2 are_normalized_wrt Amp ; ::_thesis: add1 (r1,r2,s1,s2,Amp), add2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp
A4: r2 <> 0. R by A2, Def15;
 r2 in Amp by A2, Def15;
then A5: r2 = NF (r2,Amp) by Def9;
 s2 in Amp by A3, Def15;
then A6: s2 = NF (s2,Amp) by Def9;
A7: gcd (r1,r2,Amp) = 1. R by A2, Def15;
then A8: r1,r2 are_co-prime by Def14;
A9: gcd (s1,s2,Amp) = 1. R by A3, Def15;
then A10: s1,s2 are_co-prime by Def14;
A11: s2 <> 0. R by A3, Def15;
now__::_thesis:_(_(_r1_=_0._R_&_add1_(r1,r2,s1,s2,Amp),_add2_(r1,r2,s1,s2,Amp)_are_normalized_wrt_Amp_)_or_(_s1_=_0._R_&_add1_(r1,r2,s1,s2,Amp),_add2_(r1,r2,s1,s2,Amp)_are_normalized_wrt_Amp_)_or_(_gcd_(r2,s2,Amp)_=_1._R_&_add1_(r1,r2,s1,s2,Amp),_add2_(r1,r2,s1,s2,Amp)_are_normalized_wrt_Amp_)_or_(_(r1_*_(s2_/_(gcd_(r2,s2,Amp))))_+_(s1_*_(r2_/_(gcd_(r2,s2,Amp))))_=_0._R_&_add1_(r1,r2,s1,s2,Amp),_add2_(r1,r2,s1,s2,Amp)_are_normalized_wrt_Amp_)_or_(_r1_<>_0._R_&_s1_<>_0._R_&_gcd_(r2,s2,Amp)_<>_1._R_&_(r1_*_(s2_/_(gcd_(r2,s2,Amp))))_+_(s1_*_(r2_/_(gcd_(r2,s2,Amp))))_<>_0._R_&_add1_(r1,r2,s1,s2,Amp),_add2_(r1,r2,s1,s2,Amp)_are_normalized_wrt_Amp_)_)
percases ( r1 = 0. R or s1 = 0. R or gcd (r2,s2,Amp) = 1. R or (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R or ( r1 <> 0. R & s1 <> 0. R & gcd (r2,s2,Amp) <> 1. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) <> 0. R ) ) ;
caseA12: r1 = 0. R ; ::_thesis: add1 (r1,r2,s1,s2,Amp), add2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp
then  add2 (r1,r2,s1,s2,Amp) = s2 by A5, A6, A8, A10, Def17;
hence  add1 (r1,r2,s1,s2,Amp), add2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp by A3, A5, A6, A8, A10, A12, Def16; ::_thesis: verum
end;
caseA13: s1 = 0. R ; ::_thesis: add1 (r1,r2,s1,s2,Amp), add2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp
then  add2 (r1,r2,s1,s2,Amp) = r2 by A5, A6, A8, A10, Def17;
hence  add1 (r1,r2,s1,s2,Amp), add2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp by A2, A5, A6, A8, A10, A13, Def16; ::_thesis: verum
end;
caseA14: gcd (r2,s2,Amp) = 1. R ; ::_thesis: add1 (r1,r2,s1,s2,Amp), add2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp
then A15: add2 (r1,r2,s1,s2,Amp) = r2 * s2 by A5, A6, A8, A10, Def17;
 add1 (r1,r2,s1,s2,Amp) = (r1 * s2) + (r2 * s1) by A5, A6, A8, A10, A14, Def16;
then A16: gcd ((add1 (r1,r2,s1,s2,Amp)),(add2 (r1,r2,s1,s2,Amp)),Amp) = gcd (((r1 * (s2 / (1. R))) + (s1 * r2)),(r2 * s2),Amp) by A15, Th10
.= gcd (((r1 * (s2 / (1. R))) + (s1 * (r2 / (1. R)))),(r2 * s2),Amp) by Th10
.= gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(r2 * (s2 / (gcd (r2,s2,Amp)))),Amp) by A14, Th10
.= gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp) by A4, A7, A9, Th40
.= 1. R by A14, Th32 ;
reconsider r2 = r2, s2 = s2 as Element of Amp by A2, A3, Def15;
 ( r2 * s2 in Amp & r2 * s2 <> 0. R ) by A1, A4, A11, Def10, VECTSP_2:def_1;
hence  add1 (r1,r2,s1,s2,Amp), add2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp by A15, A16, Def15; ::_thesis: verum
end;
caseA17: (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R ; ::_thesis: add1 (r1,r2,s1,s2,Amp), add2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp
A18: ( 1. R in Amp & 1. R <> 0. R ) by Th22;
A19: add2 (r1,r2,s1,s2,Amp) = 1. R by A5, A6, A8, A10, A17, Def17;
then  gcd ((add1 (r1,r2,s1,s2,Amp)),(add2 (r1,r2,s1,s2,Amp)),Amp) = 1. R by Th32;
hence  add1 (r1,r2,s1,s2,Amp), add2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp by A19, A18, Def15; ::_thesis: verum
end;
case ( r1 <> 0. R & s1 <> 0. R & gcd (r2,s2,Amp) <> 1. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) <> 0. R ) ; ::_thesis: add1 (r1,r2,s1,s2,Amp), add2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp
then A20: ( 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)) & 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)) ) by A5, A6, A8, A10, Def16, Def17;
 gcd (r2,s2,Amp) <> 0. R by A4, Th33;
then A21: gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp) <> 0. R by Th33;
 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) by A4, A7, A9, Th40;
then A22: gcd ((((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))),((r2 * (s2 / (gcd (r2,s2,Amp)))) / (gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp))),Amp) = 1. R by A21, Th38;
reconsider r2 = r2, s2 = s2 as Element of Amp by A2, A3, Def15;
A23: gcd (r2,s2,Amp) divides s2 by Def12;
reconsider z2 = gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp) as Element of Amp by Def12;
A24: gcd (r2,s2,Amp) <> 0. R by A4, Th33;
then A25: z2 <> 0. R by Th33;
 gcd (r2,s2,Amp) in Amp by Def12;
then reconsider z3 = s2 / (gcd (r2,s2,Amp)) as Element of Amp by A1, A23, A24, Th27;
 r2 * z3 in Amp by A1, Def10;
then reconsider z1 = r2 * (s2 / (gcd (r2,s2,Amp))) as Element of Amp ;
A26: r2 * s2 <> 0. R by A4, A11, VECTSP_2:def_1;
A27: gcd (r2,s2,Amp) divides r2 * s2 by A23, Th7;
then  z1 = (r2 * s2) / (gcd (r2,s2,Amp)) by A23, A24, Th11;
then A28: z1 <> 0. R by A24, A26, A27, Th8;
 ( z2 divides gcd (r2,s2,Amp) & gcd (r2,s2,Amp) divides r2 ) by Def12;
then A29: z2 divides r2 by Th2;
then  z2 divides z1 by Th7;
then A30: z1 / z2 <> 0. R by A25, A28, Th8;
 z1 / z2 in Amp by A1, A29, A25, Th7, Th27;
hence  add1 (r1,r2,s1,s2,Amp), add2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp by A20, A22, A30, Def15; ::_thesis: verum
end;
end;
end;
hence  add1 (r1,r2,s1,s2,Amp), add2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp ; ::_thesis: verum
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
let R be gcdDomain; ::_thesis: 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))
let Amp be AmpleSet of R; ::_thesis: 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))
let r1, r2, s1, s2 be Element of R; ::_thesis: ( r1,r2 are_normalized_wrt Amp & s1,s2 are_normalized_wrt Amp implies (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2)) )
assume that
A1: r1,r2 are_normalized_wrt Amp and
A2: s1,s2 are_normalized_wrt Amp ; ::_thesis: (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2))
 gcd (r1,r2,Amp) = 1. R by A1, Def15;
then A3: r1,r2 are_co-prime by Def14;
 s2 in Amp by A2, Def15;
then A4: s2 = NF (s2,Amp) by Def9;
 gcd (s1,s2,Amp) = 1. R by A2, Def15;
then A5: s1,s2 are_co-prime by Def14;
 r2 in Amp by A1, Def15;
then A6: r2 = NF (r2,Amp) by Def9;
A7: r2 <> 0. R by A1, Def15;
now__::_thesis:_(_(_r1_=_0._R_&_(add1_(r1,r2,s1,s2,Amp))_*_(r2_*_s2)_=_(add2_(r1,r2,s1,s2,Amp))_*_((r1_*_s2)_+_(s1_*_r2))_)_or_(_s1_=_0._R_&_(add1_(r1,r2,s1,s2,Amp))_*_(r2_*_s2)_=_(add2_(r1,r2,s1,s2,Amp))_*_((r1_*_s2)_+_(s1_*_r2))_)_or_(_gcd_(r2,s2,Amp)_=_1._R_&_(add1_(r1,r2,s1,s2,Amp))_*_(r2_*_s2)_=_(add2_(r1,r2,s1,s2,Amp))_*_((r1_*_s2)_+_(s1_*_r2))_)_or_(_(r1_*_(s2_/_(gcd_(r2,s2,Amp))))_+_(s1_*_(r2_/_(gcd_(r2,s2,Amp))))_=_0._R_&_(add1_(r1,r2,s1,s2,Amp))_*_(r2_*_s2)_=_(add2_(r1,r2,s1,s2,Amp))_*_((r1_*_s2)_+_(s1_*_r2))_)_or_(_r1_<>_0._R_&_s1_<>_0._R_&_gcd_(r2,s2,Amp)_<>_1._R_&_(r1_*_(s2_/_(gcd_(r2,s2,Amp))))_+_(s1_*_(r2_/_(gcd_(r2,s2,Amp))))_<>_0._R_&_(add1_(r1,r2,s1,s2,Amp))_*_(r2_*_s2)_=_(add2_(r1,r2,s1,s2,Amp))_*_((r1_*_s2)_+_(s1_*_r2))_)_)
percases ( r1 = 0. R or s1 = 0. R or gcd (r2,s2,Amp) = 1. R or (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R or ( r1 <> 0. R & s1 <> 0. R & gcd (r2,s2,Amp) <> 1. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) <> 0. R ) ) ;
caseA8: r1 = 0. R ; ::_thesis: (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2))
then A9: add1 (r1,r2,s1,s2,Amp) = s1 by A3, A5, A6, A4, Def16;
 add2 (r1,r2,s1,s2,Amp) = s2 by A3, A5, A6, A4, A8, Def17;
then (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2)) = s2 * ((0. R) + (s1 * r2)) by A8, VECTSP_1:7
.= s2 * (s1 * r2) by RLVECT_1:4
.= (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) by A9, GROUP_1:def_3 ;
hence  (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2)) ; ::_thesis: verum
end;
caseA10: s1 = 0. R ; ::_thesis: (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2))
then A11: add1 (r1,r2,s1,s2,Amp) = r1 by A3, A5, A6, A4, Def16;
 add2 (r1,r2,s1,s2,Amp) = r2 by A3, A5, A6, A4, A10, Def17;
then (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2)) = r2 * ((r1 * s2) + (0. R)) by A10, VECTSP_1:7
.= r2 * (r1 * s2) by RLVECT_1:4
.= (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) by A11, GROUP_1:def_3 ;
hence  (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2)) ; ::_thesis: verum
end;
caseA12: gcd (r2,s2,Amp) = 1. R ; ::_thesis: (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2))
then  add2 (r1,r2,s1,s2,Amp) = r2 * s2 by A3, A5, A6, A4, Def17;
hence  (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2)) by A3, A5, A6, A4, A12, Def16; ::_thesis: verum
end;
caseA13: (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) = 0. R ; ::_thesis: (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2))
A14: (r1 * s2) + (s1 * r2) = 0. R
proof
A15: gcd (r2,s2,Amp) divides r2 by Def12;
then A16: gcd (r2,s2,Amp) divides s1 * r2 by Th7;
A17: gcd (r2,s2,Amp) divides s2 by Def12;
then consider f being Element of R such that
A18: (gcd (r2,s2,Amp)) * f = s2 by Def1;
A19: gcd (r2,s2,Amp) <> 0. R by A7, Th33;
consider e being Element of R such that
A20: (gcd (r2,s2,Amp)) * e = r2 by A15, Def1;
(gcd (r2,s2,Amp)) * ((e * s1) + (f * r1)) = ((gcd (r2,s2,Amp)) * (e * s1)) + ((gcd (r2,s2,Amp)) * (f * r1)) by VECTSP_1:def_2
.= (((gcd (r2,s2,Amp)) * e) * s1) + ((gcd (r2,s2,Amp)) * (f * r1)) by GROUP_1:def_3
.= (r1 * s2) + (s1 * r2) by A20, A18, GROUP_1:def_3 ;
then A21: gcd (r2,s2,Amp) divides (r1 * s2) + (s1 * r2) by Def1;
A22: gcd (r2,s2,Amp) divides r1 * s2 by A17, Th7;
then  0. R = ((r1 * s2) / (gcd (r2,s2,Amp))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) by A13, A19, A17, Th11
.= ((r1 * s2) / (gcd (r2,s2,Amp))) + ((s1 * r2) / (gcd (r2,s2,Amp))) by A19, A15, A16, Th11 ;
then A23: 0. R = ((r1 * s2) + (s1 * r2)) / (gcd (r2,s2,Amp)) by A19, A22, A16, A21, Th12;
0. R = (0. R) * (gcd (r2,s2,Amp)) by VECTSP_1:7
.= (r1 * s2) + (s1 * r2) by A19, A21, A23, Def4 ;
hence  (r1 * s2) + (s1 * r2) = 0. R ; ::_thesis: verum
end;
 add1 (r1,r2,s1,s2,Amp) = 0. R by A3, A5, A6, A4, A13, Def16;
then (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = 0. R by VECTSP_1:7
.= (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2)) by A14, VECTSP_1:7 ;
hence  (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2)) ; ::_thesis: verum
end;
caseA24: ( r1 <> 0. R & s1 <> 0. R & gcd (r2,s2,Amp) <> 1. R & (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) <> 0. R ) ; ::_thesis: (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2))
A25: gcd (r2,s2,Amp) divides s2 by Def12;
then A26: gcd (r2,s2,Amp) divides r1 * s2 by Th7;
then A27: gcd (r2,s2,Amp) divides (r1 * s2) * r2 by Th7;
then A28: gcd (r2,s2,Amp) divides ((r1 * s2) * r2) * s2 by Th7;
A29: 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)) by A3, A5, A6, A4, A24, Def16;
A30: gcd (r2,s2,Amp) divides r2 by Def12;
then A31: gcd (r2,s2,Amp) divides s1 * r2 by Th7;
 gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp) divides gcd (r2,s2,Amp) by Def12;
then  gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp) divides r2 by A30, Th2;
then A32: gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp) divides r2 * (s2 / (gcd (r2,s2,Amp))) by Th7;
then A33: gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp) divides (r2 * (s2 / (gcd (r2,s2,Amp)))) * ((r1 * s2) + (s1 * r2)) by Th7;
A34: gcd (r2,s2,Amp) divides (s1 * r2) * r2 by A30, Th7;
then A35: gcd (r2,s2,Amp) divides ((s1 * r2) * r2) * s2 by Th7;
A36: gcd (r2,s2,Amp) divides r2 * s2 by A30, Th7;
then A37: gcd (r2,s2,Amp) divides (r2 * s2) * r1 by Th7;
then A38: gcd (r2,s2,Amp) divides ((r2 * s2) * r1) * s2 by Th7;
A39: gcd (r2,s2,Amp) divides (r2 * s2) * s1 by A36, Th7;
then A40: gcd (r2,s2,Amp) divides ((r2 * s2) * s1) * r2 by Th7;
A41: 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)) by A3, A5, A6, A4, A24, Def17;
A42: gcd (r2,s2,Amp) <> 0. R by A7, Th33;
then A43: gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp) <> 0. R by Th33;
A44: (r2 * (s2 / (gcd (r2,s2,Amp)))) * ((r1 * s2) + (s1 * r2)) = ((r2 * (s2 / (gcd (r2,s2,Amp)))) * (r1 * s2)) + ((r2 * (s2 / (gcd (r2,s2,Amp)))) * (s1 * r2)) by VECTSP_1:def_2
.= (((r2 * (s2 / (gcd (r2,s2,Amp)))) * r1) * s2) + ((r2 * (s2 / (gcd (r2,s2,Amp)))) * (s1 * r2)) by GROUP_1:def_3
.= (((r2 * (s2 / (gcd (r2,s2,Amp)))) * r1) * s2) + (((r2 * (s2 / (gcd (r2,s2,Amp)))) * s1) * r2) by GROUP_1:def_3
.= ((((r2 * s2) / (gcd (r2,s2,Amp))) * r1) * s2) + (((r2 * (s2 / (gcd (r2,s2,Amp)))) * s1) * r2) by A42, A25, A36, Th11
.= ((((r2 * s2) / (gcd (r2,s2,Amp))) * r1) * s2) + ((((r2 * s2) / (gcd (r2,s2,Amp))) * s1) * r2) by A42, A25, A36, Th11
.= ((((r2 * s2) * r1) / (gcd (r2,s2,Amp))) * s2) + ((((r2 * s2) / (gcd (r2,s2,Amp))) * s1) * r2) by A42, A36, A37, Th11
.= ((((r2 * s2) * r1) / (gcd (r2,s2,Amp))) * s2) + ((((r2 * s2) * s1) / (gcd (r2,s2,Amp))) * r2) by A42, A36, A39, Th11
.= ((((r2 * s2) * r1) * s2) / (gcd (r2,s2,Amp))) + ((((r2 * s2) * s1) / (gcd (r2,s2,Amp))) * r2) by A42, A37, A38, Th11
.= (((r1 * (s2 * r2)) * s2) / (gcd (r2,s2,Amp))) + ((((r2 * s2) * s1) * r2) / (gcd (r2,s2,Amp))) by A42, A39, A40, Th11
.= ((((r1 * s2) * r2) * s2) / (gcd (r2,s2,Amp))) + ((((r2 * s2) * s1) * r2) / (gcd (r2,s2,Amp))) by GROUP_1:def_3
.= ((((r1 * s2) * r2) * s2) / (gcd (r2,s2,Amp))) + ((s1 * ((r2 * s2) * r2)) / (gcd (r2,s2,Amp))) by GROUP_1:def_3
.= ((((r1 * s2) * r2) * s2) / (gcd (r2,s2,Amp))) + ((s1 * ((r2 * r2) * s2)) / (gcd (r2,s2,Amp))) by GROUP_1:def_3
.= ((((r1 * s2) * r2) * s2) / (gcd (r2,s2,Amp))) + (((s1 * (r2 * r2)) * s2) / (gcd (r2,s2,Amp))) by GROUP_1:def_3
.= ((((r1 * s2) * r2) * s2) / (gcd (r2,s2,Amp))) + ((((s1 * r2) * r2) * s2) / (gcd (r2,s2,Amp))) by GROUP_1:def_3 ;
A45: ((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))) * (r2 * s2) = ((r1 * (s2 / (gcd (r2,s2,Amp)))) * (r2 * s2)) + ((s1 * (r2 / (gcd (r2,s2,Amp)))) * (r2 * s2)) by VECTSP_1:def_7
.= (((r1 * s2) / (gcd (r2,s2,Amp))) * (r2 * s2)) + ((s1 * (r2 / (gcd (r2,s2,Amp)))) * (r2 * s2)) by A42, A25, A26, Th11
.= (((r1 * s2) / (gcd (r2,s2,Amp))) * (r2 * s2)) + (((s1 * r2) / (gcd (r2,s2,Amp))) * (r2 * s2)) by A42, A30, A31, Th11
.= ((((r1 * s2) / (gcd (r2,s2,Amp))) * r2) * s2) + (((s1 * r2) / (gcd (r2,s2,Amp))) * (r2 * s2)) by GROUP_1:def_3
.= ((((r1 * s2) / (gcd (r2,s2,Amp))) * r2) * s2) + ((((s1 * r2) / (gcd (r2,s2,Amp))) * r2) * s2) by GROUP_1:def_3
.= ((((r1 * s2) * r2) / (gcd (r2,s2,Amp))) * s2) + ((((s1 * r2) / (gcd (r2,s2,Amp))) * r2) * s2) by A42, A26, A27, Th11
.= ((((r1 * s2) * r2) / (gcd (r2,s2,Amp))) * s2) + ((((s1 * r2) * r2) / (gcd (r2,s2,Amp))) * s2) by A42, A31, A34, Th11
.= ((((r1 * s2) * r2) * s2) / (gcd (r2,s2,Amp))) + ((((s1 * r2) * r2) / (gcd (r2,s2,Amp))) * s2) by A42, A27, A28, Th11
.= ((((r1 * s2) * r2) * s2) / (gcd (r2,s2,Amp))) + ((((s1 * r2) * r2) * s2) / (gcd (r2,s2,Amp))) by A42, A34, A35, Th11 ;
A46: gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp) divides (r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp)))) by Def12;
then  gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp) divides ((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))) * (r2 * s2) by Th7;
then (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))) * (r2 * s2)) / (gcd (((r1 * (s2 / (gcd (r2,s2,Amp)))) + (s1 * (r2 / (gcd (r2,s2,Amp))))),(gcd (r2,s2,Amp)),Amp)) by A29, A43, A46, Th11
.= (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2)) by A41, A45, A44, A43, A32, A33, Th11 ;
hence  (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2)) ; ::_thesis: verum
end;
end;
end;
hence  (add1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (add2 (r1,r2,s1,s2,Amp)) * ((r1 * s2) + (s1 * r2)) ; ::_thesis: verum
end;

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
A1: ( ( r1 = 0. R or s1 = 0. R ) & r2 <> 0. R & s2 = 1. R implies for z being Element of R holds
( z = 0. R iff z = (r1 * s1) / (gcd (s1,r2,Amp)) ) )
proof
set d = (r1 * s1) / (gcd (s1,r2,Amp));
assume that
A2: ( r1 = 0. R or s1 = 0. R ) and
A3: r2 <> 0. R and
 s2 = 1. R ; ::_thesis: for z being Element of R holds
( z = 0. R iff z = (r1 * s1) / (gcd (s1,r2,Amp)) )
A4: gcd (s1,r2,Amp) <> 0. R by A3, Th33;
let z be Element of R; ::_thesis: ( z = 0. R iff z = (r1 * s1) / (gcd (s1,r2,Amp)) )
A5: r1 * s1 = 0. R
proof
now__::_thesis:_(_(_r1_=_0._R_&_r1_*_s1_=_0._R_)_or_(_s1_=_0._R_&_r1_*_s1_=_0._R_)_)
percases ( r1 = 0. R or s1 = 0. R ) by A2;
case r1 = 0. R ; ::_thesis: r1 * s1 = 0. R
hence  r1 * s1 = 0. R by VECTSP_1:7; ::_thesis: verum
end;
case s1 = 0. R ; ::_thesis: r1 * s1 = 0. R
hence  r1 * s1 = 0. R by VECTSP_1:7; ::_thesis: verum
end;
end;
end;
hence  r1 * s1 = 0. R ; ::_thesis: verum
end;
 gcd (s1,r2,Amp) divides s1 by Def12;
then  gcd (s1,r2,Amp) divides r1 * s1 by Th7;
then  ((r1 * s1) / (gcd (s1,r2,Amp))) * (gcd (s1,r2,Amp)) = 0. R by A5, A4, Def4;
hence  ( z = 0. R iff z = (r1 * s1) / (gcd (s1,r2,Amp)) ) by A4, VECTSP_2:def_1; ::_thesis: verum
end;
A6: ( ( r1 = 0. R or s1 = 0. R ) & s2 <> 0. R & r2 = 1. R implies for z being Element of R holds
( z = 0. R iff z = (r1 * s1) / (gcd (r1,s2,Amp)) ) )
proof
set d = (r1 * s1) / (gcd (r1,s2,Amp));
assume that
A7: ( r1 = 0. R or s1 = 0. R ) and
A8: s2 <> 0. R and
 r2 = 1. R ; ::_thesis: for z being Element of R holds
( z = 0. R iff z = (r1 * s1) / (gcd (r1,s2,Amp)) )
A9: gcd (r1,s2,Amp) <> 0. R by A8, Th33;
let z be Element of R; ::_thesis: ( z = 0. R iff z = (r1 * s1) / (gcd (r1,s2,Amp)) )
A10: r1 * s1 = 0. R
proof
now__::_thesis:_(_(_r1_=_0._R_&_r1_*_s1_=_0._R_)_or_(_s1_=_0._R_&_r1_*_s1_=_0._R_)_)
percases ( r1 = 0. R or s1 = 0. R ) by A7;
case r1 = 0. R ; ::_thesis: r1 * s1 = 0. R
hence  r1 * s1 = 0. R by VECTSP_1:7; ::_thesis: verum
end;
case s1 = 0. R ; ::_thesis: r1 * s1 = 0. R
hence  r1 * s1 = 0. R by VECTSP_1:7; ::_thesis: verum
end;
end;
end;
hence  r1 * s1 = 0. R ; ::_thesis: verum
end;
 gcd (r1,s2,Amp) divides r1 by Def12;
then  gcd (r1,s2,Amp) divides r1 * s1 by Th7;
then  ((r1 * s1) / (gcd (r1,s2,Amp))) * (gcd (r1,s2,Amp)) = 0. R by A10, A9, Def4;
hence  ( z = 0. R iff z = (r1 * s1) / (gcd (r1,s2,Amp)) ) by A9, VECTSP_2:def_1; ::_thesis: verum
end;
A11: ( r2 = 1. R & s2 = 1. R & r2 <> 0. R & s2 = 1. R implies for z being Element of R holds
( z = r1 * s1 iff z = (r1 * s1) / (gcd (s1,r2,Amp)) ) )
proof
assume that
A12: r2 = 1. R and
 s2 = 1. R and
 r2 <> 0. R and
 s2 = 1. R ; ::_thesis: for z being Element of R holds
( z = r1 * s1 iff z = (r1 * s1) / (gcd (s1,r2,Amp)) )
 gcd (s1,r2,Amp) = 1. R by A12, Th32;
hence  for z being Element of R holds
( z = r1 * s1 iff z = (r1 * s1) / (gcd (s1,r2,Amp)) ) by Th10; ::_thesis: verum
end;
 ( r2 = 1. R & s2 = 1. R & s2 <> 0. R & r2 = 1. R implies for z being Element of R holds
( z = r1 * s1 iff z = (r1 * s1) / (gcd (r1,s2,Amp)) ) )
proof
assume that
 r2 = 1. R and
A13: s2 = 1. R and
 s2 <> 0. R and
 r2 = 1. R ; ::_thesis: for z being Element of R holds
( z = r1 * s1 iff z = (r1 * s1) / (gcd (r1,s2,Amp)) )
 gcd (r1,s2,Amp) = 1. R by A13, Th32;
hence  for z being Element of R holds
( z = r1 * s1 iff z = (r1 * s1) / (gcd (r1,s2,Amp)) ) by Th10; ::_thesis: verum
end;
hence  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)) ) ) ) by A6, A1, A11; ::_thesis: verum
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
A5: gcd (s1,s2,Amp) = 1. R by A2, Th43;
A6: ( ( r1 = 0. R or s1 = 0. R ) & s2 <> 0. R & r2 = 1. R implies for z being Element of R holds
( z = 1. R iff z = s2 / (gcd (r1,s2,Amp)) ) )
proof
assume that
A7: ( r1 = 0. R or s1 = 0. R ) and
A8: s2 <> 0. R and
 r2 = 1. R ; ::_thesis: for z being Element of R holds
( z = 1. R iff z = s2 / (gcd (r1,s2,Amp)) )
now__::_thesis:_(_(_r1_=_0._R_&_(_for_z_being_Element_of_R_holds_
(_z_=_1._R_iff_z_=_s2_/_(gcd_(r1,s2,Amp))_)_)_)_or_(_s1_=_0._R_&_(_for_z_being_Element_of_R_holds_
(_z_=_1._R_iff_z_=_s2_/_(gcd_(r1,s2,Amp))_)_)_)_)
percases ( r1 = 0. R or s1 = 0. R ) by A7;
case r1 = 0. R ; ::_thesis: for z being Element of R holds
( z = 1. R iff z = s2 / (gcd (r1,s2,Amp)) )
then  gcd (r1,s2,Amp) = s2 by A4, Th30;
hence  for z being Element of R holds
( z = 1. R iff z = s2 / (gcd (r1,s2,Amp)) ) by A8, Th9; ::_thesis: verum
end;
caseA9: s1 = 0. R ; ::_thesis: for z being Element of R holds
( z = 1. R iff z = s2 / (gcd (r1,s2,Amp)) )
A10: 1. R <> 0. R ;
A11: 1. R = s2 by A4, A5, A9, Th30;
then  gcd (r1,s2,Amp) = 1. R by Th32;
hence  for z being Element of R holds
( z = 1. R iff z = s2 / (gcd (r1,s2,Amp)) ) by A11, A10, Th9; ::_thesis: verum
end;
end;
end;
hence  for z being Element of R holds
( z = 1. R iff z = s2 / (gcd (r1,s2,Amp)) ) ; ::_thesis: verum
end;
A12: gcd (r1,r2,Amp) = 1. R by A1, Th43;
A13: ( ( r1 = 0. R or s1 = 0. R ) & r2 <> 0. R & s2 = 1. R implies for z being Element of R holds
( z = 1. R iff z = r2 / (gcd (s1,r2,Amp)) ) )
proof
assume that
A14: ( r1 = 0. R or s1 = 0. R ) and
A15: r2 <> 0. R and
 s2 = 1. R ; ::_thesis: for z being Element of R holds
( z = 1. R iff z = r2 / (gcd (s1,r2,Amp)) )
now__::_thesis:_(_(_s1_=_0._R_&_(_for_z_being_Element_of_R_holds_
(_z_=_1._R_iff_z_=_r2_/_(gcd_(s1,r2,Amp))_)_)_)_or_(_r1_=_0._R_&_(_for_z_being_Element_of_R_holds_
(_z_=_1._R_iff_z_=_r2_/_(gcd_(s1,r2,Amp))_)_)_)_)
percases ( s1 = 0. R or r1 = 0. R ) by A14;
case s1 = 0. R ; ::_thesis: for z being Element of R holds
( z = 1. R iff z = r2 / (gcd (s1,r2,Amp)) )
then  gcd (s1,r2,Amp) = r2 by A3, Th30;
hence  for z being Element of R holds
( z = 1. R iff z = r2 / (gcd (s1,r2,Amp)) ) by A15, Th9; ::_thesis: verum
end;
caseA16: r1 = 0. R ; ::_thesis: for z being Element of R holds
( z = 1. R iff z = r2 / (gcd (s1,r2,Amp)) )
A17: 1. R <> 0. R ;
A18: 1. R = r2 by A3, A12, A16, Th30;
then  gcd (s1,r2,Amp) = 1. R by Th32;
hence  for z being Element of R holds
( z = 1. R iff z = r2 / (gcd (s1,r2,Amp)) ) by A18, A17, Th9; ::_thesis: verum
end;
end;
end;
hence  for z being Element of R holds
( z = 1. R iff z = r2 / (gcd (s1,r2,Amp)) ) ; ::_thesis: verum
end;
A19: ( r2 = 1. R & s2 = 1. R & r2 <> 0. R & s2 = 1. R implies for z being Element of R holds
( z = 1. R iff z = r2 / (gcd (s1,r2,Amp)) ) )
proof
assume that
A20: r2 = 1. R and
 s2 = 1. R and
A21: r2 <> 0. R and
 s2 = 1. R ; ::_thesis: for z being Element of R holds
( z = 1. R iff z = r2 / (gcd (s1,r2,Amp)) )
 gcd (s1,r2,Amp) = 1. R by A20, Th32;
hence  for z being Element of R holds
( z = 1. R iff z = r2 / (gcd (s1,r2,Amp)) ) by A20, A21, Th9; ::_thesis: verum
end;
 ( r2 = 1. R & s2 = 1. R & s2 <> 0. R & r2 = 1. R implies for z being Element of R holds
( z = 1. R iff z = s2 / (gcd (r1,s2,Amp)) ) )
proof
assume that
 r2 = 1. R and
A22: s2 = 1. R and
A23: s2 <> 0. R and
 r2 = 1. R ; ::_thesis: for z being Element of R holds
( z = 1. R iff z = s2 / (gcd (r1,s2,Amp)) )
 gcd (r1,s2,Amp) = 1. R by A22, Th32;
hence  for z being Element of R holds
( z = 1. R iff z = s2 / (gcd (r1,s2,Amp)) ) by A22, A23, Th9; ::_thesis: verum
end;
hence  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)) ) ) ) by A6, A13, A19; ::_thesis: verum
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
let R be gcdDomain; ::_thesis: 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
let Amp be AmpleSet of R; ::_thesis: 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
let r1, r2, s1, s2 be Element of R; ::_thesis: ( Amp is multiplicative & r1,r2 are_normalized_wrt Amp & s1,s2 are_normalized_wrt Amp implies mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp )
assume that
A1: Amp is multiplicative and
A2: r1,r2 are_normalized_wrt Amp and
A3: s1,s2 are_normalized_wrt Amp ; ::_thesis: mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp
A4: gcd (r1,r2,Amp) = 1. R by A2, Def15;
then A5: r1,r2 are_co-prime by Def14;
 s2 in Amp by A3, Def15;
then A6: s2 = NF (s2,Amp) by Def9;
 r2 in Amp by A2, Def15;
then A7: r2 = NF (r2,Amp) by Def9;
A8: r2 <> 0. R by A2, Def15;
then A9: gcd (s1,r2,Amp) <> 0. R by Th33;
A10: gcd (s1,s2,Amp) = 1. R by A3, Def15;
then A11: s1,s2 are_co-prime by Def14;
A12: s2 <> 0. R by A3, Def15;
then A13: gcd (r1,s2,Amp) <> 0. R by Th33;
now__::_thesis:_(_(_(_r1_=_0._R_or_s1_=_0._R_)_&_mult1_(r1,r2,s1,s2,Amp),_mult2_(r1,r2,s1,s2,Amp)_are_normalized_wrt_Amp_)_or_(_r2_=_1._R_&_s2_=_1._R_&_mult1_(r1,r2,s1,s2,Amp),_mult2_(r1,r2,s1,s2,Amp)_are_normalized_wrt_Amp_)_or_(_s2_<>_0._R_&_r2_=_1._R_&_mult1_(r1,r2,s1,s2,Amp),_mult2_(r1,r2,s1,s2,Amp)_are_normalized_wrt_Amp_)_or_(_r2_<>_0._R_&_s2_=_1._R_&_mult1_(r1,r2,s1,s2,Amp),_mult2_(r1,r2,s1,s2,Amp)_are_normalized_wrt_Amp_)_or_(_not_r1_=_0._R_&_not_s1_=_0._R_&_(_not_r2_=_1._R_or_not_s2_=_1._R_)_&_(_not_s2_<>_0._R_or_not_r2_=_1._R_)_&_(_not_r2_<>_0._R_or_not_s2_=_1._R_)_&_mult1_(r1,r2,s1,s2,Amp),_mult2_(r1,r2,s1,s2,Amp)_are_normalized_wrt_Amp_)_)
percases ( 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 ( not r1 = 0. R & not s1 = 0. R & ( not r2 = 1. R or not s2 = 1. R ) & ( not s2 <> 0. R or not r2 = 1. R ) & ( not r2 <> 0. R or not s2 = 1. R ) ) ) ;
caseA14: ( r1 = 0. R or s1 = 0. R ) ; ::_thesis: mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp
A15: ( 1. R in Amp & 1. R <> 0. R ) by Th22;
A16: mult2 (r1,r2,s1,s2,Amp) = 1. R by A5, A11, A7, A6, A14, Def19;
then  gcd ((mult1 (r1,r2,s1,s2,Amp)),(mult2 (r1,r2,s1,s2,Amp)),Amp) = 1. R by Th32;
hence  mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp by A16, A15, Def15; ::_thesis: verum
end;
caseA17: ( r2 = 1. R & s2 = 1. R ) ; ::_thesis: mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp
A18: ( 1. R in Amp & 1. R <> 0. R ) by Th22;
A19: mult2 (r1,r2,s1,s2,Amp) = 1. R by A5, A11, A7, A17, Def19;
then  gcd ((mult1 (r1,r2,s1,s2,Amp)),(mult2 (r1,r2,s1,s2,Amp)),Amp) = 1. R by Th32;
hence  mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp by A19, A18, Def15; ::_thesis: verum
end;
caseA20: ( s2 <> 0. R & r2 = 1. R ) ; ::_thesis: mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp
then A21: gcd (s1,r2,Amp) = 1. R by Th32;
then  r2 / (gcd (s1,r2,Amp)) = 1. R by A20, Th9;
then A22: s2 / (gcd (r1,s2,Amp)) = (s2 / (gcd (r1,s2,Amp))) * (r2 / (gcd (s1,r2,Amp))) by VECTSP_1:def_4;
A23: gcd (r1,s2,Amp) divides r1 by Def12;
then  gcd (r1,s2,Amp) divides r1 * s1 by Th7;
then A24: (r1 * s1) / (gcd (r1,s2,Amp)) = (r1 / (gcd (r1,s2,Amp))) * s1 by A13, A23, Th11
.= (r1 / (gcd (r1,s2,Amp))) * (s1 / (gcd (s1,r2,Amp))) by A21, Th10 ;
A25: mult2 (r1,r2,s1,s2,Amp) = s2 / (gcd (r1,s2,Amp)) by A5, A11, A7, A6, A20, Def19;
reconsider zz = gcd (r1,s2,Amp) as Element of Amp by Def12;
A26: ( gcd (r1,s2,Amp) divides s2 & gcd (r1,s2,Amp) <> 0. R ) by A12, Def12, Th33;
then A27: s2 / (gcd (r1,s2,Amp)) <> 0. R by A12, Th8;
 mult1 (r1,r2,s1,s2,Amp) = (r1 * s1) / (gcd (r1,s2,Amp)) by A20, Def18;
then A28: gcd ((mult1 (r1,r2,s1,s2,Amp)),(mult2 (r1,r2,s1,s2,Amp)),Amp) = 1. R by A4, A10, A8, A12, A25, A24, A22, Th41;
reconsider s2 = s2 as Element of Amp by A3, Def15;
 s2 / zz in Amp by A1, A26, Th27;
hence  mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp by A25, A28, A27, Def15; ::_thesis: verum
end;
caseA29: ( r2 <> 0. R & s2 = 1. R ) ; ::_thesis: mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp
then A30: gcd (r1,s2,Amp) = 1. R by Th32;
then  s2 / (gcd (r1,s2,Amp)) = 1. R by A29, Th9;
then A31: r2 / (gcd (s1,r2,Amp)) = (r2 / (gcd (s1,r2,Amp))) * (s2 / (gcd (r1,s2,Amp))) by VECTSP_1:def_4;
A32: gcd (s1,r2,Amp) divides s1 by Def12;
then  gcd (s1,r2,Amp) divides r1 * s1 by Th7;
then A33: (r1 * s1) / (gcd (s1,r2,Amp)) = r1 * (s1 / (gcd (s1,r2,Amp))) by A9, A32, Th11
.= (r1 / (gcd (r1,s2,Amp))) * (s1 / (gcd (s1,r2,Amp))) by A30, Th10 ;
A34: mult2 (r1,r2,s1,s2,Amp) = r2 / (gcd (s1,r2,Amp)) by A5, A11, A7, A6, A29, Def19;
reconsider zz = gcd (s1,r2,Amp) as Element of Amp by Def12;
A35: ( gcd (s1,r2,Amp) divides r2 & gcd (s1,r2,Amp) <> 0. R ) by A8, Def12, Th33;
then A36: r2 / (gcd (s1,r2,Amp)) <> 0. R by A8, Th8;
 mult1 (r1,r2,s1,s2,Amp) = (r1 * s1) / (gcd (s1,r2,Amp)) by A29, Def18;
then A37: gcd ((mult1 (r1,r2,s1,s2,Amp)),(mult2 (r1,r2,s1,s2,Amp)),Amp) = 1. R by A4, A10, A8, A12, A34, A33, A31, Th41;
reconsider r2 = r2 as Element of Amp by A2, Def15;
 r2 / zz in Amp by A1, A35, Th27;
hence  mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp by A34, A37, A36, Def15; ::_thesis: verum
end;
caseA38: ( not r1 = 0. R & not s1 = 0. R & ( not r2 = 1. R or not s2 = 1. R ) & ( not s2 <> 0. R or not r2 = 1. R ) & ( not r2 <> 0. R or not s2 = 1. R ) ) ; ::_thesis: mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp
reconsider z2 = gcd (s1,r2,Amp) as Element of Amp by Def12;
reconsider z1 = gcd (r1,s2,Amp) as Element of Amp by Def12;
A39: ( gcd (r1,s2,Amp) divides s2 & gcd (r1,s2,Amp) <> 0. R ) by A12, Def12, Th33;
then A40: s2 / (gcd (r1,s2,Amp)) <> 0. R by A12, Th8;
A41: mult2 (r1,r2,s1,s2,Amp) = (r2 / (gcd (s1,r2,Amp))) * (s2 / (gcd (r1,s2,Amp))) by A5, A11, A7, A6, A38, Def19;
 mult1 (r1,r2,s1,s2,Amp) = (r1 / (gcd (r1,s2,Amp))) * (s1 / (gcd (s1,r2,Amp))) by A38, Def18;
then A42: gcd ((mult1 (r1,r2,s1,s2,Amp)),(mult2 (r1,r2,s1,s2,Amp)),Amp) = 1. R by A4, A10, A8, A12, A41, Th41;
A43: ( gcd (s1,r2,Amp) divides r2 & gcd (s1,r2,Amp) <> 0. R ) by A8, Def12, Th33;
then A44: r2 / (gcd (s1,r2,Amp)) <> 0. R by A8, Th8;
reconsider s2 = s2 as Element of Amp by A3, Def15;
reconsider u = s2 / z1 as Element of Amp by A1, A39, Th27;
reconsider r2 = r2 as Element of Amp by A2, Def15;
reconsider v = r2 / z2 as Element of Amp by A1, A43, Th27;
A45: v * u <> 0. R by A40, A44, VECTSP_2:def_1;
 v * u in Amp by A1, Def10;
hence  mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp by A41, A42, A45, Def15; ::_thesis: verum
end;
end;
end;
hence  mult1 (r1,r2,s1,s2,Amp), mult2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp ; ::_thesis: verum
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
let R be gcdDomain; ::_thesis: 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)
let Amp be AmpleSet of R; ::_thesis: 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)
let r1, r2, s1, s2 be Element of R; ::_thesis: ( r1,r2 are_normalized_wrt Amp & s1,s2 are_normalized_wrt Amp implies (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1) )
assume that
A1: r1,r2 are_normalized_wrt Amp and
A2: s1,s2 are_normalized_wrt Amp ; ::_thesis: (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1)
 gcd (r1,r2,Amp) = 1. R by A1, Def15;
then A3: r1,r2 are_co-prime by Def14;
 s2 <> 0. R by A2, Def15;
then A4: gcd (r1,s2,Amp) <> 0. R by Th33;
 r2 in Amp by A1, Def15;
then A5: r2 = NF (r2,Amp) by Def9;
 gcd (s1,s2,Amp) = 1. R by A2, Def15;
then A6: s1,s2 are_co-prime by Def14;
 r2 <> 0. R by A1, Def15;
then A7: gcd (s1,r2,Amp) <> 0. R by Th33;
 s2 in Amp by A2, Def15;
then A8: s2 = NF (s2,Amp) by Def9;
now__::_thesis:_(_(_(_r1_=_0._R_or_s1_=_0._R_)_&_(mult1_(r1,r2,s1,s2,Amp))_*_(r2_*_s2)_=_(mult2_(r1,r2,s1,s2,Amp))_*_(r1_*_s1)_)_or_(_r2_=_1._R_&_s2_=_1._R_&_(mult1_(r1,r2,s1,s2,Amp))_*_(r2_*_s2)_=_(mult2_(r1,r2,s1,s2,Amp))_*_(r1_*_s1)_)_or_(_s2_<>_0._R_&_r2_=_1._R_&_(mult1_(r1,r2,s1,s2,Amp))_*_(r2_*_s2)_=_(mult2_(r1,r2,s1,s2,Amp))_*_(r1_*_s1)_)_or_(_r2_<>_0._R_&_s2_=_1._R_&_(mult1_(r1,r2,s1,s2,Amp))_*_(r2_*_s2)_=_(mult2_(r1,r2,s1,s2,Amp))_*_(r1_*_s1)_)_or_(_not_r1_=_0._R_&_not_s1_=_0._R_&_(_not_r2_=_1._R_or_not_s2_=_1._R_)_&_(_not_s2_<>_0._R_or_not_r2_=_1._R_)_&_(_not_r2_<>_0._R_or_not_s2_=_1._R_)_&_(mult1_(r1,r2,s1,s2,Amp))_*_(r2_*_s2)_=_(mult2_(r1,r2,s1,s2,Amp))_*_(r1_*_s1)_)_)
percases ( 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 ( not r1 = 0. R & not s1 = 0. R & ( not r2 = 1. R or not s2 = 1. R ) & ( not s2 <> 0. R or not r2 = 1. R ) & ( not r2 <> 0. R or not s2 = 1. R ) ) ) ;
caseA9: ( r1 = 0. R or s1 = 0. R ) ; ::_thesis: (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1)
then A10: mult1 (r1,r2,s1,s2,Amp) = 0. R by Def18;
now__::_thesis:_(_(_r1_=_0._R_&_(mult1_(r1,r2,s1,s2,Amp))_*_(r2_*_s2)_=_(mult2_(r1,r2,s1,s2,Amp))_*_(r1_*_s1)_)_or_(_s1_=_0._R_&_(mult1_(r1,r2,s1,s2,Amp))_*_(r2_*_s2)_=_(mult2_(r1,r2,s1,s2,Amp))_*_(r1_*_s1)_)_)
percases ( r1 = 0. R or s1 = 0. R ) by A9;
case r1 = 0. R ; ::_thesis: (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1)
then (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1) = (mult2 (r1,r2,s1,s2,Amp)) * (0. R) by VECTSP_1:7
.= 0. R by VECTSP_1:7 ;
hence  (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1) by A10, VECTSP_1:7; ::_thesis: verum
end;
case s1 = 0. R ; ::_thesis: (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1)
then (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1) = (mult2 (r1,r2,s1,s2,Amp)) * (0. R) by VECTSP_1:7
.= 0. R by VECTSP_1:7 ;
hence  (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1) by A10, VECTSP_1:7; ::_thesis: verum
end;
end;
end;
hence  (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1) ; ::_thesis: verum
end;
caseA11: ( r2 = 1. R & s2 = 1. R ) ; ::_thesis: (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1)
then  ( mult1 (r1,r2,s1,s2,Amp) = r1 * s1 & mult2 (r1,r2,s1,s2,Amp) = 1. R ) by A3, A6, A5, Def18, Def19;
hence  (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1) by A11, VECTSP_1:def_4; ::_thesis: verum
end;
caseA12: ( s2 <> 0. R & r2 = 1. R ) ; ::_thesis: (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1)
 gcd (r1,s2,Amp) divides r1 by Def12;
then A13: gcd (r1,s2,Amp) divides r1 * s1 by Th7;
then A14: gcd (r1,s2,Amp) divides (r1 * s1) * s2 by Th7;
A15: ((r1 * s1) / (gcd (r1,s2,Amp))) * (r2 * s2) = ((r1 * s1) / (gcd (r1,s2,Amp))) * s2 by A12, VECTSP_1:def_8
.= ((r1 * s1) * s2) / (gcd (r1,s2,Amp)) by A4, A13, A14, Th11 ;
A16: mult2 (r1,r2,s1,s2,Amp) = s2 / (gcd (r1,s2,Amp)) by A3, A6, A5, A8, A12, Def19;
A17: gcd (r1,s2,Amp) divides s2 by Def12;
then A18: gcd (r1,s2,Amp) divides s2 * r1 by Th7;
then A19: gcd (r1,s2,Amp) divides (s2 * r1) * s1 by Th7;
(s2 / (gcd (r1,s2,Amp))) * (r1 * s1) = ((s2 / (gcd (r1,s2,Amp))) * r1) * s1 by GROUP_1:def_3
.= ((s2 * r1) / (gcd (r1,s2,Amp))) * s1 by A4, A17, A18, Th11
.= ((s2 * r1) * s1) / (gcd (r1,s2,Amp)) by A4, A18, A19, Th11
.= ((r1 * s1) * s2) / (gcd (r1,s2,Amp)) by GROUP_1:def_3 ;
hence  (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1) by A12, A16, A15, Def18; ::_thesis: verum
end;
caseA20: ( r2 <> 0. R & s2 = 1. R ) ; ::_thesis: (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1)
 gcd (s1,r2,Amp) divides s1 by Def12;
then A21: gcd (s1,r2,Amp) divides s1 * r1 by Th7;
then A22: gcd (s1,r2,Amp) divides (s1 * r1) * r2 by Th7;
A23: ((r1 * s1) / (gcd (s1,r2,Amp))) * (r2 * s2) = ((r1 * s1) / (gcd (s1,r2,Amp))) * r2 by A20, VECTSP_1:def_4
.= ((r1 * s1) * r2) / (gcd (s1,r2,Amp)) by A7, A21, A22, Th11 ;
A24: mult2 (r1,r2,s1,s2,Amp) = r2 / (gcd (s1,r2,Amp)) by A3, A6, A5, A8, A20, Def19;
A25: gcd (s1,r2,Amp) divides r2 by Def12;
then A26: gcd (s1,r2,Amp) divides r2 * r1 by Th7;
then A27: gcd (s1,r2,Amp) divides (r2 * r1) * s1 by Th7;
(r2 / (gcd (s1,r2,Amp))) * (r1 * s1) = ((r2 / (gcd (s1,r2,Amp))) * r1) * s1 by GROUP_1:def_3
.= ((r2 * r1) / (gcd (s1,r2,Amp))) * s1 by A7, A25, A26, Th11
.= ((r2 * r1) * s1) / (gcd (s1,r2,Amp)) by A7, A26, A27, Th11
.= ((r1 * s1) * r2) / (gcd (s1,r2,Amp)) by GROUP_1:def_3 ;
hence  (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1) by A20, A24, A23, Def18; ::_thesis: verum
end;
caseA28: ( not r1 = 0. R & not s1 = 0. R & ( not r2 = 1. R or not s2 = 1. R ) & ( not s2 <> 0. R or not r2 = 1. R ) & ( not r2 <> 0. R or not s2 = 1. R ) ) ; ::_thesis: (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1)
A29: ( gcd (s1,r2,Amp) divides r2 & gcd (r1,s2,Amp) divides s2 ) by Def12;
then A30: (gcd (s1,r2,Amp)) * (gcd (r1,s2,Amp)) divides r2 * s2 by Th3;
then A31: (gcd (s1,r2,Amp)) * (gcd (r1,s2,Amp)) divides (r2 * s2) * r1 by Th7;
then A32: (gcd (s1,r2,Amp)) * (gcd (r1,s2,Amp)) divides ((r2 * s2) * r1) * s1 by Th7;
A33: ( gcd (r1,s2,Amp) divides r1 & gcd (s1,r2,Amp) divides s1 ) by Def12;
then A34: (gcd (r1,s2,Amp)) * (gcd (s1,r2,Amp)) divides r1 * s1 by Th3;
then A35: (gcd (r1,s2,Amp)) * (gcd (s1,r2,Amp)) divides (r1 * s1) * r2 by Th7;
then A36: (gcd (r1,s2,Amp)) * (gcd (s1,r2,Amp)) divides ((r1 * s1) * r2) * s2 by Th7;
A37: mult2 (r1,r2,s1,s2,Amp) = (r2 / (gcd (s1,r2,Amp))) * (s2 / (gcd (r1,s2,Amp))) by A3, A6, A5, A8, A28, Def19;
A38: (gcd (r1,s2,Amp)) * (gcd (s1,r2,Amp)) <> 0. R by A4, A7, VECTSP_2:def_1;
A39: ((r2 / (gcd (s1,r2,Amp))) * (s2 / (gcd (r1,s2,Amp)))) * (r1 * s1) = ((r2 * s2) / ((gcd (s1,r2,Amp)) * (gcd (r1,s2,Amp)))) * (r1 * s1) by A4, A7, A29, Th14
.= (((r2 * s2) / ((gcd (s1,r2,Amp)) * (gcd (r1,s2,Amp)))) * r1) * s1 by GROUP_1:def_3
.= (((r2 * s2) * r1) / ((gcd (s1,r2,Amp)) * (gcd (r1,s2,Amp)))) * s1 by A38, A30, A31, Th11
.= (((r2 * s2) * r1) * s1) / ((gcd (s1,r2,Amp)) * (gcd (r1,s2,Amp))) by A38, A31, A32, Th11
.= (r1 * ((r2 * s2) * s1)) / ((gcd (s1,r2,Amp)) * (gcd (r1,s2,Amp))) by GROUP_1:def_3
.= (r1 * ((s1 * r2) * s2)) / ((gcd (s1,r2,Amp)) * (gcd (r1,s2,Amp))) by GROUP_1:def_3
.= ((r1 * (s1 * r2)) * s2) / ((gcd (s1,r2,Amp)) * (gcd (r1,s2,Amp))) by GROUP_1:def_3
.= (((r1 * s1) * r2) * s2) / ((gcd (s1,r2,Amp)) * (gcd (r1,s2,Amp))) by GROUP_1:def_3 ;
((r1 / (gcd (r1,s2,Amp))) * (s1 / (gcd (s1,r2,Amp)))) * (r2 * s2) = ((r1 * s1) / ((gcd (r1,s2,Amp)) * (gcd (s1,r2,Amp)))) * (r2 * s2) by A4, A7, A33, Th14
.= (((r1 * s1) / ((gcd (r1,s2,Amp)) * (gcd (s1,r2,Amp)))) * r2) * s2 by GROUP_1:def_3
.= (((r1 * s1) * r2) / ((gcd (r1,s2,Amp)) * (gcd (s1,r2,Amp)))) * s2 by A34, A35, A38, Th11
.= (((r1 * s1) * r2) * s2) / ((gcd (r1,s2,Amp)) * (gcd (s1,r2,Amp))) by A35, A36, A38, Th11 ;
hence  (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1) by A28, A37, A39, Def18; ::_thesis: verum
end;
end;
end;
hence  (mult1 (r1,r2,s1,s2,Amp)) * (r2 * s2) = (mult2 (r1,r2,s1,s2,Amp)) * (r1 * s1) ; ::_thesis: verum
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
let F be almost_left_invertible commutative Ring; ::_thesis: for a, b being Element of F st a <> 0. F & b <> 0. F holds
(a ") * (b ") = (b * a) "
let a, b be Element of F; ::_thesis: ( a <> 0. F & b <> 0. F implies (a ") * (b ") = (b * a) " )
assume that
A1: a <> 0. F and
A2: b <> 0. F ; ::_thesis: (a ") * (b ") = (b * a) "
A3: (b * a) * ((a ") * (b ")) = ((b * a) * (a ")) * (b ") by GROUP_1:def_3
.= (b * (a * (a "))) * (b ") by GROUP_1:def_3
.= (b * (1_ F)) * (b ") by A1, VECTSP_1:def_10
.= b * (b ") by VECTSP_1:def_4
.= 1_ F by A2, VECTSP_1:def_10 ;
 b * a <> 0. F by A1, A2, VECTSP_1:12;
hence  (a ") * (b ") = (b * a) " by A3, VECTSP_1:def_10; ::_thesis: verum
end;