for b₁ being commutative domRing-like Ring
for b₂, b₃, b₄ being Element of b₁ st b₂ <> 0. b₁ holds
( ( b₂ * b₃ = b₂ * b₄ implies b₃ = b₄ ) & ( b₃ * b₂ = b₄ * b₂ implies b₃ = b₄ ) )

proof end;

definition

let c₁ be non empty HGrStr ;
let c₂, c₃ be Element of c₁;
pred c₂ divides c₃ means :Def1: :: GCD_1:def 1
ex b₁ being Element of a₁ st a₃ = a₂ * b₁;

end;

:: deftheorem Def1 defines divides GCD_1:def 1 :

definition

let c₁ be non empty unital multLoopStr ;
let c₂, c₃ be Element of c₁;
redefine pred divides as c₂ divides c₃;
reflexivity

proof end;

end;

definition

let c₁ be non empty multLoopStr ;
let c₂ be Element of c₁;
attr a₂ is unital means :Def2: :: GCD_1:def 2
a₂ divides 1. a₁;

end;

:: deftheorem Def2 defines unital GCD_1:def 2 :

definition

let c₁ be non empty multLoopStr ;
let c₂, c₃ be Element of c₁;
pred c₂ is_associated_to c₃ means :Def3: :: GCD_1:def 3
( a₂ divides a₃ & a₃ divides a₂ );
symmetry ;

end;

:: deftheorem Def3 defines is_associated_to GCD_1:def 3 :

notation

let c₁ be non empty multLoopStr ;
let c₂, c₃ be Element of c₁;
antonym c₂ is_not_associated_to c₃ for c₂ is_associated_to c₃;

end;

definition

let c₁ be non empty unital multLoopStr ;
let c₂, c₃ be Element of c₁;
redefine pred is_associated_to as c₂ is_associated_to c₃;
reflexivity

proof end;

end;

definition

let c₁ be commutative domRing-like Ring;
let c₂, c₃ be Element of c₁;
assume E5: c₃ divides c₂ ;
assume E6: c₃ <> 0. c₁ ;
func c₂ / c₃ -> Element of a₁ means :Def4: :: GCD_1:def 4
a₄ * a₃ = a₂;
existence

proof end;

uniqueness by E6, Th1;

end;

:: deftheorem Def4 defines / GCD_1:def 4 :

theorem Th2: :: GCD_1:2

for b₁ being non empty associative multLoopStr
for b₂, b₃, b₄ being Element of b₁ st b₂ divides b₃ & b₃ divides b₄ holds
b₂ divides b₄

proof end;

theorem Th3: :: GCD_1:3

for b₁ being non empty associative commutative multLoopStr
for b₂, b₃, b₄, b₅ being Element of b₁ st b₃ divides b₂ & b₅ divides b₄ holds
b₃ * b₅ divides b₂ * b₄

proof end;

theorem Th4: :: GCD_1:4

for b₁ being non empty associative multLoopStr
for b₂, b₃, b₄ being Element of b₁ st b₂ is_associated_to b₃ & b₃ is_associated_to b₄ holds
b₂ is_associated_to b₄

proof end;

theorem Th5: :: GCD_1:5

for b₁ being non empty associative multLoopStr
for b₂, b₃, b₄ being Element of b₁ st b₂ divides b₃ holds
b₄ * b₂ divides b₄ * b₃

proof end;

theorem Th6: :: GCD_1:6

for b₁ being non empty multLoopStr
for b₂, b₃ being Element of b₁ holds
( b₂ divides b₂ * b₃ & ( b₁ is commutative implies b₃ divides b₂ * b₃ ) )

proof end;

theorem Th7: :: GCD_1:7

for b₁ being non empty associative multLoopStr
for b₂, b₃, b₄ being Element of b₁ st b₂ divides b₃ holds
b₂ divides b₃ * b₄

proof end;

theorem Th8: :: GCD_1:8

for b₁ being commutative domRing-like Ring
for b₂, b₃ being Element of b₁ st b₃ divides b₂ & b₃ <> 0. b₁ holds
( b₂ / b₃ = 0. b₁ iff b₂ = 0. b₁ )

proof end;

theorem Th9: :: GCD_1:9

for b₁ being commutative domRing-like Ring
for b₂ being Element of b₁ st b₂ <> 0. b₁ holds
b₂ / b₂ = 1. b₁

proof end;

theorem Th10: :: GCD_1:10

for b₁ being commutative non degenerated domRing-like Ring
for b₂ being Element of b₁ holds b₂ / (1. b₁) = b₂

proof end;

theorem Th11: :: GCD_1:11

for b₁ being commutative domRing-like Ring
for b₂, b₃, b₄ being Element of b₁ st b₄ <> 0. b₁ holds
( ( b₄ divides b₂ * b₃ & b₄ divides b₂ implies (b₂ * b₃) / b₄ = (b₂ / b₄) * b₃ ) & ( b₄ divides b₂ * b₃ & b₄ divides b₃ implies (b₂ * b₃) / b₄ = b₂ * (b₃ / b₄) ) )

proof end;

theorem Th12: :: GCD_1:12

for b₁ being commutative domRing-like Ring
for b₂, b₃, b₄ being Element of b₁ st b₄ <> 0. b₁ & b₄ divides b₂ & b₄ divides b₃ & b₄ divides b₂ + b₃ holds
(b₂ / b₄) + (b₃ / b₄) = (b₂ + b₃) / b₄

proof end;

theorem Th13: :: GCD_1:13

for b₁ being commutative domRing-like Ring
for b₂, b₃, b₄ being Element of b₁ st b₄ <> 0. b₁ & b₄ divides b₂ & b₄ divides b₃ holds
( b₂ / b₄ = b₃ / b₄ iff b₂ = b₃ )

proof end;

theorem Th14: :: GCD_1:14

for b₁ being commutative domRing-like Ring
for b₂, b₃, b₄, b₅ being Element of b₁ st b₃ <> 0. b₁ & b₅ <> 0. b₁ & b₃ divides b₂ & b₅ divides b₄ holds
(b₂ / b₃) * (b₄ / b₅) = (b₂ * b₄) / (b₃ * b₅)

proof end;

theorem Th15: :: GCD_1:15

for b₁ being commutative domRing-like Ring
for b₂, b₃, b₄ being Element of b₁ st b₂ <> 0. b₁ & b₂ * b₃ divides b₂ * b₄ holds
b₃ divides b₄

proof end;

theorem Th16: :: GCD_1:16

for b₁ being commutative domRing-like Ring
for b₂ being Element of b₁ st b₂ is_associated_to 0. b₁ holds
b₂ = 0. b₁

proof end;

theorem Th17: :: GCD_1:17

for b₁ being commutative domRing-like Ring
for b₂, b₃ being Element of b₁ st b₂ <> 0. b₁ & b₂ * b₃ = b₂ holds
b₃ = 1. b₁

proof end;

theorem Th18: :: GCD_1:18

for b₁ being commutative domRing-like Ring
for b₂, b₃ being Element of b₁ holds
( b₂ is_associated_to b₃ iff ex b₄ being Element of b₁ st
( b₄ is unital & b₂ * b₄ = b₃ ) )

proof end;

theorem Th19: :: GCD_1:19

for b₁ being commutative domRing-like Ring
for b₂, b₃, b₄ being Element of b₁ st b₄ <> 0. b₁ & b₄ * b₂ is_associated_to b₄ * b₃ holds
b₂ is_associated_to b₃

proof end;

definition

let c₁ be non empty multLoopStr ;
let c₂ be Element of c₁;
func Class c₂ -> Subset of a₁ means :Def5: :: GCD_1:def 5
for b₁ being Element of a₁ holds
( b₁ in a₃ iff b₁ is_associated_to a₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines Class GCD_1:def 5 :

registration

let c₁ be non empty unital multLoopStr ;
let c₂ be Element of c₁;
cluster Class a₂ -> non empty ;
coherence

proof end;

end;

theorem Th20: :: GCD_1:20

for b₁ being non empty associative multLoopStr
for b₂, b₃ being Element of b₁ st Class b₂ meets Class b₃ holds
Class b₂ = Class b₃

proof end;

definition

let c₁ be non empty multLoopStr ;
func Classes c₁ -> Subset-Family of a₁ means :Def6: :: GCD_1:def 6
for b₁ being Subset of a₁ holds
( b₁ in a₂ iff ex b₂ being Element of a₁ st b₁ = Class b₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines Classes GCD_1:def 6 :

registration

let c₁ be non empty multLoopStr ;
cluster Classes a₁ -> non empty ;
coherence

proof end;

end;

theorem Th21: :: GCD_1:21

for b₁ being non empty unital multLoopStr
for b₂ being Subset of b₁ st b₂ in Classes b₁ holds
not b₂ is empty

proof end;

definition

let c₁ be non empty unital associative multLoopStr ;
mode Am of c₁ -> non empty Subset of a₁ means :Def7: :: GCD_1:def 7
( ( for b₁ being Element of a₁ ex b₂ being Element of a₂ st b₂ is_associated_to b₁ ) & ( for b₁, b₂ being Element of a₂ st b₁ <> b₂ holds
b₁ is_not_associated_to b₂ ) );
existence

proof end;

end;

:: deftheorem Def7 defines Am GCD_1:def 7 :

definition

let c₁ be non empty unital associative multLoopStr ;
mode AmpleSet of c₁ -> non empty Subset of a₁ means :Def8: :: GCD_1:def 8
( a₂ is Am of a₁ & 1. a₁ in a₂ );
existence

proof end;

end;

:: deftheorem Def8 defines AmpleSet GCD_1:def 8 :

theorem Th22: :: GCD_1:22

for b₁ being non empty unital associative multLoopStr
for b₂ being AmpleSet of b₁ holds
( 1. b₁ in b₂ & ( for b₃ being Element of b₁ ex b₄ being Element of b₂ st b₄ is_associated_to b₃ ) & ( for b₃, b₄ being Element of b₂ st b₃ <> b₄ holds
b₃ is_not_associated_to b₄ ) )

proof end;

theorem Th23: :: GCD_1:23

for b₁ being non empty unital associative multLoopStr
for b₂ being AmpleSet of b₁
for b₃, b₄ being Element of b₂ st b₃ is_associated_to b₄ holds
b₃ = b₄ by Th22;

theorem Th24: :: GCD_1:24

for b₁ being commutative domRing-like Ring
for b₂ being AmpleSet of b₁ holds 0. b₁ is Element of b₂

proof end;

definition

let c₁ be non empty unital associative multLoopStr ;
let c₂ be AmpleSet of c₁;
let c₃ be Element of c₁;
func NF c₃,c₂ -> Element of a₁ means :Def9: :: GCD_1:def 9
( a₄ in a₂ & a₄ is_associated_to a₃ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines NF GCD_1:def 9 :

theorem Th25: :: GCD_1:25

for b₁ being commutative domRing-like Ring
for b₂ being AmpleSet of b₁ holds
( NF (0. b₁),b₂ = 0. b₁ & NF (1. b₁),b₂ = 1. b₁ )

proof end;

theorem Th26: :: GCD_1:26

for b₁ being commutative domRing-like Ring
for b₂ being AmpleSet of b₁
for b₃ being Element of b₁ holds
( b₃ in b₂ iff b₃ = NF b₃,b₂ ) by Def9;

definition

let c₁ be non empty unital associative multLoopStr ;
let c₂ be AmpleSet of c₁;
attr a₂ is multiplicative means :Def10: :: GCD_1:def 10
for b₁, b₂ being Element of a₂ holds b₁ * b₂ in a₂;

end;

:: deftheorem Def10 defines multiplicative GCD_1:def 10 :

theorem Th27: :: GCD_1:27

for b₁ being commutative domRing-like Ring
for b₂ being AmpleSet of b₁ st b₂ is multiplicative holds
for b₃, b₄ being Element of b₂ st b₄ divides b₃ & b₄ <> 0. b₁ holds
b₃ / b₄ in b₂

proof end;

definition

let c₁ be non empty multLoopStr ;
attr a₁ is gcd-like means :Def11: :: GCD_1:def 11
for b₁, b₂ being Element of a₁ ex b₃ being Element of a₁ st
( b₃ divides b₁ & b₃ divides b₂ & ( for b₄ being Element of a₁ st b₄ divides b₁ & b₄ divides b₂ holds
b₄ divides b₃ ) );

end;

:: deftheorem Def11 defines gcd-like GCD_1:def 11 :

E35: now

let c₁ be Field;
let c₂, c₃ be Element of c₁;

now

per cases ;

case E36: ( c₂ <> 0. c₁ & c₃ <> 0. c₁ ) ;

c₂ = (1. c₁) * c₂ by VECTSP_2:1;
then E37: 1. c₁ divides c₂ by Def1;
c₃ = (1. c₁) * c₃ by VECTSP_2:1;
then E38: 1. c₁ divides c₃ by Def1;
for b₁ being Element of c₁ st b₁ divides c₂ & b₁ divides c₃ holds
b₁ divides 1. c₁

proof

let c₄ be Element of c₁;
assume E39: ( c₄ divides c₂ & c₄ divides c₃ ) ;

now

per cases ;

case c₄ <> 0. c₁ ;

then consider c₅ being Element of c₁ such that
E40: c₄ * c₅ = 1. c₁ by VECTSP_1:def 20;
thus c₄ divides 1. c₁ by E40, Def1;

end;

case E40: c₄ = 0. c₁ ;

assume c₄ divides c₂ ;
then consider c₅ being Element of c₁ such that
E41: c₄ * c₅ = c₂ by Def1;
thus c₄ divides 1. c₁ by E36, E40, E41, VECTSP_1:39;

end;

hence c₄ divides 1. c₁ by E39;

end;

hence ex b₁ being Element of c₁ st
( b₁ divides c₂ & b₁ divides c₃ & ( for b₂ being Element of c₁ st b₂ divides c₂ & b₂ divides c₃ holds
b₂ divides b₁ ) ) by E37, E38;

end;

case E36: c₂ = 0. c₁ ;

c₃ * (0. c₁) = 0. c₁ by VECTSP_1:39;
then E37: c₃ divides 0. c₁ by Def1;
for b₁ being Element of c₁ st b₁ divides 0. c₁ & b₁ divides c₃ holds
b₁ divides c₃ ;
hence ex b₁ being Element of c₁ st
( b₁ divides c₂ & b₁ divides c₃ & ( for b₂ being Element of c₁ st b₂ divides c₂ & b₂ divides c₃ holds
b₂ divides b₁ ) ) by E36, E37;

end;

case E36: c₃ = 0. c₁ ;

c₂ * (0. c₁) = 0. c₁ by VECTSP_1:39;
then E37: c₂ divides 0. c₁ by Def1;
for b₁ being Element of c₁ st b₁ divides c₂ & b₁ divides 0. c₁ holds
b₁ divides c₂ ;
hence ex b₁ being Element of c₁ st
( b₁ divides c₂ & b₁ divides c₃ & ( for b₂ being Element of c₁ st b₂ divides c₂ & b₂ divides c₃ holds
b₂ divides b₁ ) ) by E36, E37;

end;

hence ex b₁ being Element of c₁ st
( b₁ divides c₂ & b₁ divides c₃ & ( for b₂ being Element of c₁ st b₂ divides c₂ & b₂ divides c₃ holds
b₂ divides b₁ ) ) ;

end;

registration

cluster gcd-like doubleLoopStr ;
existence

proof end;

end;

registration

cluster non empty unital associative commutative gcd-like multLoopStr ;
existence

proof end;

end;

registration

cluster non empty unital associative commutative gcd-like multLoopStr_0 ;
existence

proof end;

end;

registration end;

registration

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

proof end;

end;

definition

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

end;

definition

let c₁ be non empty unital associative gcd-like multLoopStr ;
let c₂ be AmpleSet of c₁;
let c₃, c₄ be Element of c₁;
func gcd c₃,c₄,c₂ -> Element of a₁ means :Def12: :: GCD_1:def 12
( a₅ in a₂ & a₅ divides a₃ & a₅ divides a₄ & ( for b₁ being Element of a₁ st b₁ divides a₃ & b₁ divides a₄ holds
b₁ divides a₅ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines gcd GCD_1:def 12 :

theorem Th28: :: GCD_1:28

canceled;

theorem Th29: :: GCD_1:29

for b₁ being gcdDomain
for b₂ being AmpleSet of b₁
for b₃, b₄, b₅ being Element of b₁ st b₅ divides gcd b₃,b₄,b₂ holds
( b₅ divides b₃ & b₅ divides b₄ )

proof end;

theorem Th30: :: GCD_1:30

for b₁ being gcdDomain
for b₂ being AmpleSet of b₁
for b₃, b₄ being Element of b₁ holds gcd b₃,b₄,b₂ = gcd b₄,b₃,b₂

proof end;

theorem Th31: :: GCD_1:31

for b₁ being gcdDomain
for b₂ being AmpleSet of b₁
for b₃ being Element of b₁ holds
( gcd b₃,(0. b₁),b₂ = NF b₃,b₂ & gcd (0. b₁),b₃,b₂ = NF b₃,b₂ )

proof end;

theorem Th32: :: GCD_1:32

for b₁ being gcdDomain
for b₂ being AmpleSet of b₁ holds gcd (0. b₁),(0. b₁),b₂ = 0. b₁

proof end;

theorem Th33: :: GCD_1:33

for b₁ being gcdDomain
for b₂ being AmpleSet of b₁
for b₃ being Element of b₁ holds
( gcd b₃,(1. b₁),b₂ = 1. b₁ & gcd (1. b₁),b₃,b₂ = 1. b₁ )

proof end;

theorem Th34: :: GCD_1:34

for b₁ being gcdDomain
for b₂ being AmpleSet of b₁
for b₃, b₄ being Element of b₁ holds
( gcd b₃,b₄,b₂ = 0. b₁ iff ( b₃ = 0. b₁ & b₄ = 0. b₁ ) )

proof end;

theorem Th35: :: GCD_1:35

for b₁ being gcdDomain
for b₂ being AmpleSet of b₁
for b₃, b₄, b₅ being Element of b₁ st b₄ is_associated_to b₅ holds
( gcd b₃,b₄,b₂ is_associated_to gcd b₃,b₅,b₂ & gcd b₄,b₃,b₂ is_associated_to gcd b₅,b₃,b₂ )

proof end;

theorem Th36: :: GCD_1:36

for b₁ being gcdDomain
for b₂ being AmpleSet of b₁
for b₃, b₄, b₅ being Element of b₁ holds gcd (gcd b₃,b₄,b₂),b₅,b₂ = gcd b₃,(gcd b₄,b₅,b₂),b₂

proof end;

theorem Th37: :: GCD_1:37

for b₁ being gcdDomain
for b₂ being AmpleSet of b₁
for b₃, b₄, b₅ being Element of b₁ holds gcd (b₃ * b₅),(b₄ * b₅),b₂ is_associated_to b₅ * (gcd b₃,b₄,b₂)

proof end;

theorem Th38: :: GCD_1:38

for b₁ being gcdDomain
for b₂ being AmpleSet of b₁
for b₃, b₄, b₅ being Element of b₁ st gcd b₃,b₄,b₂ = 1. b₁ holds
gcd b₃,(b₄ * b₅),b₂ = gcd b₃,b₅,b₂

proof end;

theorem Th39: :: GCD_1:39

for b₁ being gcdDomain
for b₂ being AmpleSet of b₁
for b₃, b₄, b₅ being Element of b₁ st b₅ = gcd b₃,b₄,b₂ & b₅ <> 0. b₁ holds
gcd (b₃ / b₅),(b₄ / b₅),b₂ = 1. b₁

proof end;

theorem Th40: :: GCD_1:40

for b₁ being gcdDomain
for b₂ being AmpleSet of b₁
for b₃, b₄, b₅ being Element of b₁ holds gcd (b₃ + (b₄ * b₅)),b₅,b₂ = gcd b₃,b₅,b₂

proof end;

theorem Th41: :: GCD_1:41

for b₁ being gcdDomain
for b₂ being AmpleSet of b₁
for b₃, b₄, b₅, b₆ being Element of b₁ st gcd b₃,b₄,b₂ = 1. b₁ & gcd b₅,b₆,b₂ = 1. b₁ & b₄ <> 0. b₁ & b₆ <> 0. b₁ holds
gcd ((b₃ * (b₆ / (gcd b₄,b₆,b₂))) + (b₅ * (b₄ / (gcd b₄,b₆,b₂)))),(b₄ * (b₆ / (gcd b₄,b₆,b₂))),b₂ = gcd ((b₃ * (b₆ / (gcd b₄,b₆,b₂))) + (b₅ * (b₄ / (gcd b₄,b₆,b₂)))),(gcd b₄,b₆,b₂),b₂

proof end;

theorem Th42: :: GCD_1:42

for b₁ being gcdDomain
for b₂ being AmpleSet of b₁
for b₃, b₄, b₅, b₆ being Element of b₁ st gcd b₃,b₄,b₂ = 1. b₁ & gcd b₅,b₆,b₂ = 1. b₁ & b₄ <> 0. b₁ & b₆ <> 0. b₁ holds
gcd ((b₃ / (gcd b₃,b₆,b₂)) * (b₅ / (gcd b₅,b₄,b₂))),((b₄ / (gcd b₅,b₄,b₂)) * (b₆ / (gcd b₃,b₆,b₂))),b₂ = 1. b₁

proof end;

definition

let c₁ be non empty unital associative gcd-like multLoopStr ;
let c₂ be AmpleSet of c₁;
let c₃, c₄ be Element of c₁;
pred c₃,c₄ are_canonical_wrt c₂ means :Def13: :: GCD_1:def 13
gcd a₃,a₄,a₂ = 1. a₁;

end;

:: deftheorem Def13 defines are_canonical_wrt GCD_1:def 13 :

theorem Th43: :: GCD_1:43

for b₁ being gcdDomain
for b₂, b₃ being AmpleSet of b₁
for b₄, b₅ being Element of b₁ holds
( b₄,b₅ are_canonical_wrt b₂ iff b₄,b₅ are_canonical_wrt b₃ )

proof end;

definition

let c₁ be non empty unital associative gcd-like multLoopStr ;
let c₂, c₃ be Element of c₁;
pred c₂,c₃ are_co-prime means :Def14: :: GCD_1:def 14
ex b₁ being AmpleSet of a₁ st gcd a₂,a₃,b₁ = 1. a₁;

end;

:: deftheorem Def14 defines are_co-prime GCD_1:def 14 :

definition

let c₁ be gcdDomain;
let c₂, c₃ be Element of c₁;
redefine pred are_co-prime as c₂,c₃ are_co-prime ;
symmetry

proof end;

end;

theorem Th44: :: GCD_1:44

for b₁ being gcdDomain
for b₂ being AmpleSet of b₁
for b₃, b₄ being Element of b₁ st b₃,b₄ are_co-prime holds
gcd b₃,b₄,b₂ = 1. b₁

proof end;

definition

let c₁ be non empty unital associative gcd-like multLoopStr_0 ;
let c₂ be AmpleSet of c₁;
let c₃, c₄ be Element of c₁;
pred c₃,c₄ are_normalized_wrt c₂ means :Def15: :: GCD_1:def 15
( gcd a₃,a₄,a₂ = 1. a₁ & a₄ in a₂ & a₄ <> 0. a₁ );

end;

:: deftheorem Def15 defines are_normalized_wrt GCD_1:def 15 :

definition

let c₁ be gcdDomain;
let c₂ be AmpleSet of c₁;
let c₃, c₄, c₅, c₆ be Element of c₁;
assume E56: ( c₃,c₄ are_co-prime & c₅,c₆ are_co-prime & c₄ = NF c₄,c₂ & c₆ = NF c₆,c₂ ) ;
func add1 c₃,c₄,c₅,c₆,c₂ -> Element of a₁ equals :Def16: :: GCD_1:def 16
a₅ if a₃ = 0. a₁
a₃ if a₅ = 0. a₁
(a₃ * a₆) + (a₄ * a₅) if gcd a₄,a₆,a₂ = 1. a₁
0. a₁ if (a₃ * (a₆ / (gcd a₄,a₆,a₂))) + (a₅ * (a₄ / (gcd a₄,a₆,a₂))) = 0. a₁
otherwise ((a₃ * (a₆ / (gcd a₄,a₆,a₂))) + (a₅ * (a₄ / (gcd a₄,a₆,a₂)))) / (gcd ((a₃ * (a₆ / (gcd a₄,a₆,a₂))) + (a₅ * (a₄ / (gcd a₄,a₆,a₂)))),(gcd a₄,a₆,a₂),a₂);
coherence ;
consistency

proof end;

end;

:: deftheorem Def16 defines add1 GCD_1:def 16 :

definition

let c₁ be gcdDomain;
let c₂ be AmpleSet of c₁;
let c₃, c₄, c₅, c₆ be Element of c₁;
assume E57: ( c₃,c₄ are_co-prime & c₅,c₆ are_co-prime & c₄ = NF c₄,c₂ & c₆ = NF c₆,c₂ ) ;
func add2 c₃,c₄,c₅,c₆,c₂ -> Element of a₁ equals :Def17: :: GCD_1:def 17
a₆ if a₃ = 0. a₁
a₄ if a₅ = 0. a₁
a₄ * a₆ if gcd a₄,a₆,a₂ = 1. a₁
1. a₁ if (a₃ * (a₆ / (gcd a₄,a₆,a₂))) + (a₅ * (a₄ / (gcd a₄,a₆,a₂))) = 0. a₁
otherwise (a₄ * (a₆ / (gcd a₄,a₆,a₂))) / (gcd ((a₃ * (a₆ / (gcd a₄,a₆,a₂))) + (a₅ * (a₄ / (gcd a₄,a₆,a₂)))),(gcd a₄,a₆,a₂),a₂);
coherence ;
consistency

proof end;

end;

:: deftheorem Def17 defines add2 GCD_1:def 17 :

theorem Th45: :: GCD_1:45

for b₁ being gcdDomain
for b₂ being AmpleSet of b₁
for b₃, b₄, b₅, b₆ being Element of b₁ st b₂ is multiplicative & b₃,b₄ are_normalized_wrt b₂ & b₅,b₆ are_normalized_wrt b₂ holds
add1 b₃,b₄,b₅,b₆,b₂, add2 b₃,b₄,b₅,b₆,b₂ are_normalized_wrt b₂

proof end;

theorem Th46: :: GCD_1:46

for b₁ being gcdDomain
for b₂ being AmpleSet of b₁
for b₃, b₄, b₅, b₆ being Element of b₁ st b₂ is multiplicative & b₃,b₄ are_normalized_wrt b₂ & b₅,b₆ are_normalized_wrt b₂ holds
(add1 b₃,b₄,b₅,b₆,b₂) * (b₄ * b₆) = (add2 b₃,b₄,b₅,b₆,b₂) * ((b₃ * b₆) + (b₅ * b₄))

proof end;

definition

let c₁ be gcdDomain;
let c₂ be AmpleSet of c₁;
let c₃, c₄, c₅, c₆ be Element of c₁;
func mult1 c₃,c₄,c₅,c₆,c₂ -> Element of a₁ equals :Def18: :: GCD_1:def 18
0. a₁ if ( a₃ = 0. a₁ or a₅ = 0. a₁ )
a₃ * a₅ if ( a₄ = 1. a₁ & a₆ = 1. a₁ )
(a₃ * a₅) / (gcd a₃,a₆,a₂) if ( a₆ <> 0. a₁ & a₄ = 1. a₁ )
(a₃ * a₅) / (gcd a₅,a₄,a₂) if ( a₄ <> 0. a₁ & a₆ = 1. a₁ )
otherwise (a₃ / (gcd a₃,a₆,a₂)) * (a₅ / (gcd a₅,a₄,a₂));
coherence ;
consistency

proof end;

end;

:: deftheorem Def18 defines mult1 GCD_1:def 18 :

definition

let c₁ be gcdDomain;
let c₂ be AmpleSet of c₁;
let c₃, c₄, c₅, c₆ be Element of c₁;
assume E59: ( c₃,c₄ are_co-prime & c₅,c₆ are_co-prime & c₄ = NF c₄,c₂ & c₆ = NF c₆,c₂ ) ;
func mult2 c₃,c₄,c₅,c₆,c₂ -> Element of a₁ equals :Def19: :: GCD_1:def 19
1. a₁ if ( a₃ = 0. a₁ or a₅ = 0. a₁ )
1. a₁ if ( a₄ = 1. a₁ & a₆ = 1. a₁ )
a₆ / (gcd a₃,a₆,a₂) if ( a₆ <> 0. a₁ & a₄ = 1. a₁ )
a₄ / (gcd a₅,a₄,a₂) if ( a₄ <> 0. a₁ & a₆ = 1. a₁ )
otherwise (a₄ / (gcd a₅,a₄,a₂)) * (a₆ / (gcd a₃,a₆,a₂));
coherence ;
consistency

proof end;

end;

:: deftheorem Def19 defines mult2 GCD_1:def 19 :

theorem Th47: :: GCD_1:47

for b₁ being gcdDomain
for b₂ being AmpleSet of b₁
for b₃, b₄, b₅, b₆ being Element of b₁ st b₂ is multiplicative & b₃,b₄ are_normalized_wrt b₂ & b₅,b₆ are_normalized_wrt b₂ holds
mult1 b₃,b₄,b₅,b₆,b₂, mult2 b₃,b₄,b₅,b₆,b₂ are_normalized_wrt b₂

proof end;

theorem Th48: :: GCD_1:48

for b₁ being gcdDomain
for b₂ being AmpleSet of b₁
for b₃, b₄, b₅, b₆ being Element of b₁ st b₂ is multiplicative & b₃,b₄ are_normalized_wrt b₂ & b₅,b₆ are_normalized_wrt b₂ holds
(mult1 b₃,b₄,b₅,b₆,b₂) * (b₄ * b₆) = (mult2 b₃,b₄,b₅,b₆,b₂) * (b₃ * b₅)

proof end;

theorem Th49: :: GCD_1:49

canceled;

theorem Th50: :: GCD_1:50

canceled;

theorem Th51: :: GCD_1:51

for b₁ being non empty Abelian add-associative right_zeroed right_complementable distributive doubleLoopStr
for b₂, b₃ being Element of b₁ holds
( (- b₂) * b₃ = - (b₂ * b₃) & b₂ * (- b₃) = - (b₂ * b₃) ) by VECTSP_1:40, VECTSP_1:41;

theorem Th52: :: GCD_1:52

canceled;

theorem Th53: :: GCD_1:53

for b₁ being commutative Field-like Ring
for b₂, b₃ being Element of b₁ st b₂ <> 0. b₁ & b₃ <> 0. b₁ holds
(b₂ " ) * (b₃ " ) = (b₃ * b₂) "

proof end;