:: GCD_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

registration
cluster non empty commutative right_unital -> non empty left_unital multLoopStr ;
coherence
for b1 being non empty multLoopStr st b1 is commutative & b1 is right_unital holds
b1 is left_unital
proof end;
end;

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

registration
cluster -> unital doubleLoopStr ;
coherence
for b1 being Ring holds b1 is unital
;
end;

registration
cluster F_Real -> domRing-like ;
coherence
F_Real is domRing-like
proof end;
end;

registration
cluster non empty Abelian add-associative right_zeroed right_complementable unital associative commutative strict distributive Field-like non degenerated domRing-like 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 unital & not b1 is degenerated & b1 is Field-like )
proof end;
end;

theorem Th1: :: GCD_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being commutative domRing-like Ring
for a, b, c being Element of R st a <> 0. R holds
( ( a * b = a * c implies b = c ) & ( b * a = c * a implies b = c ) )
proof end;

definition
let R be non empty HGrStr ;
let x, y be Element of R;
pred x 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 HGrStr
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 unital multLoopStr ;
let x, y be Element of R;
:: original: divides
redefine pred x divides y;
reflexivity
for x being Element of R holds x divides x
proof end;
end;

definition
let R be non empty multLoopStr ;
let x be Element of R;
attr x 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;
pred x 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 unital multLoopStr ;
let x, y be Element of R;
:: original: is_associated_to
redefine pred x is_associated_to y;
reflexivity
for x being Element of R holds x is_associated_to x
proof end;
end;

definition
let R be commutative domRing-like Ring;
let x, y be Element of R;
assume A1: y divides x ;
assume A2: y <> 0. R ;
func x / y -> Element of R means :Def4: :: GCD_1:def 4
it * y = x;
existence
ex b1 being Element of R st b1 * y = x
proof end;
uniqueness
for b1, b2 being Element of R st b1 * y = x & b2 * y = x holds
b1 = b2
by A2, Th1;
end;

:: deftheorem Def4 defines / GCD_1:def 4 :
for R being commutative domRing-like Ring
for x, y being Element of R st y divides x & y <> 0. R holds
for b4 being Element of R holds
( b4 = x / y iff b4 * y = x );

theorem Th2: :: GCD_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty associative multLoopStr
for a, b, c being Element of R st a divides b & b divides c holds
a divides c
proof end;

theorem Th3: :: GCD_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty associative commutative multLoopStr
for a, b, c, d being Element of R st b divides a & d divides c holds
b * d divides a * c
proof end;

theorem Th4: :: GCD_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th5: :: GCD_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty associative multLoopStr
for a, b, c being Element of R st a divides b holds
c * a divides c * b
proof end;

theorem Th6: :: GCD_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty multLoopStr
for a, b being Element of R holds
( a divides a * b & ( R is commutative implies b divides a * b ) )
proof end;

theorem Th7: :: GCD_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty associative multLoopStr
for a, b, c being Element of R st a divides b holds
a divides b * c
proof end;

theorem Th8: :: GCD_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being commutative domRing-like Ring
for a, b being Element of R st b divides a & b <> 0. R holds
( a / b = 0. R iff a = 0. R )
proof end;

theorem Th9: :: GCD_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being commutative domRing-like Ring
for a being Element of R st a <> 0. R holds
a / a = 1. R
proof end;

theorem Th10: :: GCD_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being commutative non degenerated domRing-like Ring
for a being Element of R holds a / (1. R) = a
proof end;

theorem Th11: :: GCD_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being commutative domRing-like Ring
for a, b, c being Element of R st c <> 0. R holds
( ( c divides a * b & c divides a implies (a * b) / c = (a / c) * b ) & ( c divides a * b & c divides b implies (a * b) / c = a * (b / c) ) )
proof end;

theorem Th12: :: GCD_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being commutative domRing-like Ring
for a, b, c being Element of R st c <> 0. R & c divides a & c divides b & c divides a + b holds
(a / c) + (b / c) = (a + b) / c
proof end;

theorem :: GCD_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being commutative domRing-like Ring
for a, b, c being Element of R st c <> 0. R & c divides a & c divides b holds
( a / c = b / c iff a = b )
proof end;

theorem Th14: :: GCD_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being commutative domRing-like Ring
for a, b, c, d being Element of R st b <> 0. R & d <> 0. R & b divides a & d divides c holds
(a / b) * (c / d) = (a * c) / (b * d)
proof end;

theorem Th15: :: GCD_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being commutative domRing-like Ring
for a, b, c being Element of R st a <> 0. R & a * b divides a * c holds
b divides c
proof end;

theorem :: GCD_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being commutative domRing-like Ring
for a being Element of R st a is_associated_to 0. R holds
a = 0. R
proof end;

theorem Th17: :: GCD_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being commutative domRing-like Ring
for a, b being Element of R st a <> 0. R & a * b = a holds
b = 1. R
proof end;

theorem Th18: :: GCD_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being commutative domRing-like Ring
for a, b being Element of R holds
( a is_associated_to b iff ex c being Element of R st
( c is unital & a * c = b ) )
proof end;

theorem Th19: :: GCD_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

definition
let R be non empty multLoopStr ;
let a be Element of R;
func Class a -> Subset of R means :Def5: :: GCD_1:def 5
for b being Element of R holds
( b in it iff b is_associated_to a );
existence
ex b1 being Subset of R st
for b being Element of R holds
( b in b1 iff b is_associated_to a )
proof end;
uniqueness
for b1, b2 being Subset of R st ( for b being Element of R holds
( b in b1 iff b is_associated_to a ) ) & ( for b being Element of R holds
( b in b2 iff b is_associated_to a ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines Class GCD_1:def 5 :
for R being non empty multLoopStr
for a being Element of R
for b3 being Subset of R holds
( b3 = Class a iff for b being Element of R holds
( b in b3 iff b is_associated_to a ) );

registration
let R be non empty unital multLoopStr ;
let a be Element of R;
cluster Class a -> non empty ;
coherence
not Class a is empty
proof end;
end;

theorem Th20: :: GCD_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty associative multLoopStr
for a, b being Element of R st Class a meets Class b holds
Class a = Class b
proof end;

definition
let R be non empty multLoopStr ;
func Classes R -> Subset-Family of R means :Def6: :: GCD_1:def 6
for A being Subset of R holds
( A in it iff ex a being Element of R st A = Class a );
existence
ex b1 being Subset-Family of R st
for A being Subset of R holds
( A in b1 iff ex a being Element of R st A = Class a )
proof end;
uniqueness
for b1, b2 being Subset-Family of R st ( for A being Subset of R holds
( A in b1 iff ex a being Element of R st A = Class a ) ) & ( for A being Subset of R holds
( A in b2 iff ex a being Element of R st A = Class a ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines Classes GCD_1:def 6 :
for R being non empty multLoopStr
for b2 being Subset-Family of R holds
( b2 = Classes R iff for A being Subset of R holds
( A in b2 iff ex a being Element of R st A = Class a ) );

registration
let R be non empty multLoopStr ;
cluster Classes R -> non empty ;
coherence
not Classes R is empty
proof end;
end;

theorem Th21: :: GCD_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty unital multLoopStr
for X being Subset of R st X in Classes R holds
not X is empty
proof end;

definition
let R be non empty unital associative multLoopStr ;
mode Am of R -> non empty Subset of R means :Def7: :: GCD_1:def 7
( ( for a being Element of R ex z being Element of it st z is_associated_to a ) & ( for x, y being Element of it st x <> y holds
x is_not_associated_to y ) );
existence
ex b1 being non empty Subset of R st
( ( for a being Element of R ex z being Element of b1 st z is_associated_to a ) & ( for x, y being Element of b1 st x <> y holds
x is_not_associated_to y ) )
proof end;
end;

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

definition
let R be non empty unital associative multLoopStr ;
mode AmpleSet of R -> non empty Subset of R means :Def8: :: GCD_1:def 8
( it is Am of R & 1. R in it );
existence
ex b1 being non empty Subset of R st
( b1 is Am of R & 1. R in b1 )
proof end;
end;

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

theorem Th22: :: GCD_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty unital associative multLoopStr
for Amp being AmpleSet of R holds
( 1. R in Amp & ( for a being Element of R ex z being Element of Amp st z is_associated_to a ) & ( for x, y being Element of Amp st x <> y holds
x is_not_associated_to y ) )
proof end;

theorem :: GCD_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty unital associative multLoopStr
for Amp being AmpleSet of R
for x, y being Element of Amp st x is_associated_to y holds
x = y by Th22;

theorem Th24: :: GCD_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being commutative domRing-like Ring
for Amp being AmpleSet of R holds 0. R is Element of Amp
proof end;

definition
let R be non empty unital associative multLoopStr ;
let Amp be AmpleSet of R;
let x be Element of R;
func NF x,Amp -> Element of R means :Def9: :: GCD_1:def 9
( it in Amp & it is_associated_to x );
existence
ex b1 being Element of R st
( b1 in Amp & b1 is_associated_to x )
proof end;
uniqueness
for b1, b2 being Element of R st b1 in Amp & b1 is_associated_to x & b2 in Amp & b2 is_associated_to x holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines NF GCD_1:def 9 :
for R being non empty unital associative multLoopStr
for Amp being AmpleSet of R
for x, b4 being Element of R holds
( b4 = NF x,Amp iff ( b4 in Amp & b4 is_associated_to x ) );

theorem Th25: :: GCD_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being commutative domRing-like Ring
for Amp being AmpleSet of R holds
( NF (0. R),Amp = 0. R & NF (1. R),Amp = 1. R )
proof end;

theorem :: GCD_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 unital associative multLoopStr ;
let Amp be AmpleSet of R;
attr Amp 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 unital associative multLoopStr
for Amp being AmpleSet of R holds
( Amp is multiplicative iff for x, y being Element of Amp holds x * y in Amp );

theorem Th27: :: GCD_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being commutative domRing-like Ring
for Amp being AmpleSet of R st Amp is multiplicative holds
for x, y being Element of Amp st y divides x & y <> 0. R holds
x / y in Amp
proof end;

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

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

Lm1: now
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
per cases ( ( x <> 0. F & y <> 0. F ) or x = 0. F or y = 0. F ) ;
case A1: ( x <> 0. F & y <> 0. F ) ; :: thesis: ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) )

x = (1. F) * x by VECTSP_2:1;
then A2: 1. F divides x by Def1;
y = (1. F) * y by VECTSP_2:1;
then A3: 1. F divides y by Def1;
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 A4: ( zz divides x & zz divides y ) ; :: thesis: zz divides 1. F
now
per cases ( zz <> 0. F or zz = 0. F ) ;
case zz <> 0. F ; :: thesis: zz divides 1. F
then consider zz' being Element of F such that
A5: zz * zz' = 1. F by VECTSP_1:def 20;
thus zz divides 1. F by A5, Def1; :: thesis: verum
end;
case A6: zz = 0. F ; :: thesis: ( zz divides x implies zz divides 1. F )
assume zz divides x ; :: thesis: zz divides 1. F
then consider d being Element of F such that
A7: zz * d = x by Def1;
thus zz divides 1. F by A1, A6, A7, VECTSP_1:39; :: thesis: verum
end;
end;
end;
hence zz divides 1. F by A4; :: thesis: verum
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 ) ) by A2, A3; :: thesis: verum
end;
case A8: 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:39;
then A9: 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 A8, A9; :: thesis: verum
end;
case A10: 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:39;
then A11: 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 A10, A11; :: 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 gcd-like doubleLoopStr ;
existence
ex b1 being domRing st b1 is gcd-like
proof end;
end;

registration
cluster non empty unital associative commutative gcd-like multLoopStr ;
existence
ex b1 being non empty multLoopStr st
( b1 is gcd-like & b1 is associative & b1 is commutative & b1 is unital )
proof end;
end;

registration
cluster non empty unital associative commutative gcd-like multLoopStr_0 ;
existence
ex b1 being non empty multLoopStr_0 st
( b1 is gcd-like & b1 is associative & b1 is commutative & b1 is unital )
proof end;
end;

registration
cluster non empty add-associative right_zeroed right_complementable commutative right-distributive left-distributive right_unital left_unital Field-like -> non empty add-associative right_zeroed right_complementable commutative right-distributive left-distributive right_unital distributive left_unital Field-like gcd-like doubleLoopStr ;
coherence
for b1 being non empty add-associative right_zeroed right_complementable commutative right-distributive left-distributive right_unital left_unital Field-like doubleLoopStr holds b1 is gcd-like
proof end;
end;

registration
cluster non empty Abelian add-associative right_zeroed right_complementable unital associative commutative distributive non degenerated domRing-like gcd-like doubleLoopStr ;
existence
ex b1 being non empty doubleLoopStr st
( b1 is gcd-like & b1 is associative & b1 is commutative & b1 is unital & b1 is domRing-like & b1 is unital & b1 is distributive & not b1 is degenerated & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable )
proof end;
end;

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

definition
let R be non empty unital associative gcd-like multLoopStr ;
let Amp be AmpleSet of R;
let x, y be Element of R;
func gcd x,y,Amp -> Element of R means :Def12: :: GCD_1:def 12
( it in Amp & it divides x & it divides y & ( for z being Element of R st z divides x & z divides y holds
z divides it ) );
existence
ex b1 being Element of R st
( b1 in Amp & b1 divides x & b1 divides y & ( for z being Element of R st z divides x & z divides y holds
z divides b1 ) )
proof end;
uniqueness
for b1, b2 being Element of R st b1 in Amp & b1 divides x & b1 divides y & ( for z being Element of R st z divides x & z divides y holds
z divides b1 ) & b2 in Amp & b2 divides x & b2 divides y & ( for z being Element of R st z divides x & z divides y holds
z divides b2 ) holds
b1 = b2
proof end;
end;

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

theorem :: GCD_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th29: :: GCD_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being gcdDomain
for Amp being AmpleSet of R
for a, b, c being Element of R st c divides gcd a,b,Amp holds
( c divides a & c divides b )
proof end;

theorem Th30: :: GCD_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being gcdDomain
for Amp being AmpleSet of R
for a, b being Element of R holds gcd a,b,Amp = gcd b,a,Amp
proof end;

theorem Th31: :: GCD_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being gcdDomain
for Amp being AmpleSet of R
for a being Element of R holds
( gcd a,(0. R),Amp = NF a,Amp & gcd (0. R),a,Amp = NF a,Amp )
proof end;

theorem Th32: :: GCD_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being gcdDomain
for Amp being AmpleSet of R holds gcd (0. R),(0. R),Amp = 0. R
proof end;

theorem Th33: :: GCD_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being gcdDomain
for Amp being AmpleSet of R
for a being Element of R holds
( gcd a,(1. R),Amp = 1. R & gcd (1. R),a,Amp = 1. R )
proof end;

theorem Th34: :: GCD_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being gcdDomain
for Amp being AmpleSet of R
for a, b being Element of R holds
( gcd a,b,Amp = 0. R iff ( a = 0. R & b = 0. R ) )
proof end;

theorem Th35: :: GCD_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being gcdDomain
for Amp being AmpleSet of R
for a, b, c being Element of R st b is_associated_to c holds
( gcd a,b,Amp is_associated_to gcd a,c,Amp & gcd b,a,Amp is_associated_to gcd c,a,Amp )
proof end;

theorem Th36: :: GCD_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being gcdDomain
for Amp being AmpleSet of R
for a, b, c being Element of R holds gcd (gcd a,b,Amp),c,Amp = gcd a,(gcd b,c,Amp),Amp
proof end;

theorem Th37: :: GCD_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being gcdDomain
for Amp being AmpleSet of R
for a, b, c being Element of R holds gcd (a * c),(b * c),Amp is_associated_to c * (gcd a,b,Amp)
proof end;

theorem Th38: :: GCD_1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being gcdDomain
for Amp being AmpleSet of R
for a, b, c being Element of R st gcd a,b,Amp = 1. R holds
gcd a,(b * c),Amp = gcd a,c,Amp
proof end;

theorem Th39: :: GCD_1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being gcdDomain
for Amp being AmpleSet of R
for a, b, c being Element of R st c = gcd a,b,Amp & c <> 0. R holds
gcd (a / c),(b / c),Amp = 1. R
proof end;

theorem Th40: :: GCD_1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being gcdDomain
for Amp being AmpleSet of R
for a, b, c being Element of R holds gcd (a + (b * c)),c,Amp = gcd a,c,Amp
proof end;

theorem Th41: :: GCD_1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(r2 * (s2 / (gcd r2,s2,Amp))),Amp = gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(gcd r2,s2,Amp),Amp
proof end;

theorem Th42: :: GCD_1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being gcdDomain
for Amp being AmpleSet of R
for r1, r2, s1, s2 being Element of R st gcd r1,r2,Amp = 1. R & gcd s1,s2,Amp = 1. R & r2 <> 0. R & s2 <> 0. R holds
gcd ((r1 / (gcd r1,s2,Amp)) * (s1 / (gcd s1,r2,Amp))),((r2 / (gcd s1,r2,Amp)) * (s2 / (gcd r1,s2,Amp))),Amp = 1. R
proof end;

definition
let R be non empty unital associative gcd-like multLoopStr ;
let Amp be AmpleSet of R;
let x, y be Element of R;
pred x,y are_canonical_wrt Amp means :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 unital associative gcd-like multLoopStr
for Amp being AmpleSet of R
for x, y being Element of R holds
( x,y are_canonical_wrt Amp iff gcd x,y,Amp = 1. R );

theorem Th43: :: GCD_1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being gcdDomain
for Amp, Amp' being AmpleSet of R
for x, y being Element of R holds
( x,y are_canonical_wrt Amp iff x,y are_canonical_wrt Amp' )
proof end;

definition
let R be non empty unital associative gcd-like multLoopStr ;
let x, y be Element of R;
pred x,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 unital associative gcd-like multLoopStr
for x, y being Element of R holds
( x,y are_co-prime iff ex Amp being AmpleSet of R st gcd x,y,Amp = 1. R );

definition
let R be gcdDomain;
let x, y be Element of R;
:: original: are_co-prime
redefine pred x,y are_co-prime ;
symmetry
for x, y being Element of R st x,y are_co-prime holds
y,x are_co-prime
proof end;
end;

theorem Th44: :: GCD_1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being gcdDomain
for Amp being AmpleSet of R
for x, y being Element of R st x,y are_co-prime holds
gcd x,y,Amp = 1. R
proof end;

definition
let R be non empty unital associative gcd-like multLoopStr_0 ;
let Amp be AmpleSet of R;
let x, y be Element of R;
pred x,y are_normalized_wrt Amp means :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 unital associative gcd-like multLoopStr_0
for Amp being AmpleSet of R
for x, y being Element of R holds
( x,y are_normalized_wrt Amp iff ( gcd x,y,Amp = 1. R & y in Amp & y <> 0. R ) );

definition
let R be gcdDomain;
let Amp be AmpleSet of R;
let r1, r2, s1, s2 be Element of R;
assume A1: ( r1,r2 are_co-prime & s1,s2 are_co-prime & r2 = NF r2,Amp & s2 = NF s2,Amp ) ;
func add1 r1,r2,s1,s2,Amp -> Element of R equals :Def16: :: GCD_1:def 16
s1 if r1 = 0. R
r1 if s1 = 0. R
(r1 * s2) + (r2 * s1) if gcd r2,s2,Amp = 1. R
0. R if (r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp))) = 0. R
otherwise ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))) / (gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(gcd r2,s2,Amp),Amp);
coherence
( ( r1 = 0. R implies s1 is Element of R ) & ( s1 = 0. R implies r1 is Element of R ) & ( gcd r2,s2,Amp = 1. R implies (r1 * s2) + (r2 * s1) is Element of R ) & ( (r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp))) = 0. R implies 0. R is Element of R ) & ( not r1 = 0. R & not s1 = 0. R & not gcd r2,s2,Amp = 1. R & not (r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp))) = 0. R implies ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))) / (gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(gcd r2,s2,Amp),Amp) is Element of R ) )
;
consistency
for b1 being Element of R holds
( ( r1 = 0. R & s1 = 0. R implies ( b1 = s1 iff b1 = r1 ) ) & ( r1 = 0. R & gcd r2,s2,Amp = 1. R implies ( b1 = s1 iff b1 = (r1 * s2) + (r2 * s1) ) ) & ( r1 = 0. R & (r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp))) = 0. R implies ( b1 = s1 iff b1 = 0. R ) ) & ( s1 = 0. R & gcd r2,s2,Amp = 1. R implies ( b1 = r1 iff b1 = (r1 * s2) + (r2 * s1) ) ) & ( s1 = 0. R & (r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp))) = 0. R implies ( b1 = r1 iff b1 = 0. R ) ) & ( gcd r2,s2,Amp = 1. R & (r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp))) = 0. R implies ( b1 = (r1 * s2) + (r2 * s1) iff b1 = 0. R ) ) )
proof end;
end;

:: deftheorem Def16 defines add1 GCD_1:def 16 :
for R being gcdDomain
for Amp being AmpleSet of R
for r1, r2, s1, s2 being Element of R st r1,r2 are_co-prime & s1,s2 are_co-prime & r2 = NF r2,Amp & s2 = NF s2,Amp holds
( ( r1 = 0. R implies add1 r1,r2,s1,s2,Amp = s1 ) & ( s1 = 0. R implies add1 r1,r2,s1,s2,Amp = r1 ) & ( gcd r2,s2,Amp = 1. R implies add1 r1,r2,s1,s2,Amp = (r1 * s2) + (r2 * s1) ) & ( (r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp))) = 0. R implies add1 r1,r2,s1,s2,Amp = 0. R ) & ( not r1 = 0. R & not s1 = 0. R & not gcd r2,s2,Amp = 1. R & not (r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp))) = 0. R implies add1 r1,r2,s1,s2,Amp = ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))) / (gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(gcd r2,s2,Amp),Amp) ) );

definition
let R be gcdDomain;
let Amp be AmpleSet of R;
let r1, r2, s1, s2 be Element of R;
assume A1: ( r1,r2 are_co-prime & s1,s2 are_co-prime & r2 = NF r2,Amp & s2 = NF s2,Amp ) ;
func add2 r1,r2,s1,s2,Amp -> Element of R equals :Def17: :: GCD_1:def 17
s2 if r1 = 0. R
r2 if s1 = 0. R
r2 * s2 if gcd r2,s2,Amp = 1. R
1. R if (r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp))) = 0. R
otherwise (r2 * (s2 / (gcd r2,s2,Amp))) / (gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(gcd r2,s2,Amp),Amp);
coherence
( ( r1 = 0. R implies s2 is Element of R ) & ( s1 = 0. R implies r2 is Element of R ) & ( gcd r2,s2,Amp = 1. R implies r2 * s2 is Element of R ) & ( (r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp))) = 0. R implies 1. R is Element of R ) & ( not r1 = 0. R & not s1 = 0. R & not gcd r2,s2,Amp = 1. R & not (r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp))) = 0. R implies (r2 * (s2 / (gcd r2,s2,Amp))) / (gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(gcd r2,s2,Amp),Amp) is Element of R ) )
;
consistency
for b1 being Element of R holds
( ( r1 = 0. R & s1 = 0. R implies ( b1 = s2 iff b1 = r2 ) ) & ( r1 = 0. R & gcd r2,s2,Amp = 1. R implies ( b1 = s2 iff b1 = r2 * s2 ) ) & ( r1 = 0. R & (r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp))) = 0. R implies ( b1 = s2 iff b1 = 1. R ) ) & ( s1 = 0. R & gcd r2,s2,Amp = 1. R implies ( b1 = r2 iff b1 = r2 * s2 ) ) & ( s1 = 0. R & (r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp))) = 0. R implies ( b1 = r2 iff b1 = 1. R ) ) & ( gcd r2,s2,Amp = 1. R & (r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp))) = 0. R implies ( b1 = r2 * s2 iff b1 = 1. R ) ) )
proof end;
end;

:: deftheorem Def17 defines add2 GCD_1:def 17 :
for R being gcdDomain
for Amp being AmpleSet of R
for r1, r2, s1, s2 being Element of R st r1,r2 are_co-prime & s1,s2 are_co-prime & r2 = NF r2,Amp & s2 = NF s2,Amp holds
( ( r1 = 0. R implies add2 r1,r2,s1,s2,Amp = s2 ) & ( s1 = 0. R implies add2 r1,r2,s1,s2,Amp = r2 ) & ( gcd r2,s2,Amp = 1. R implies add2 r1,r2,s1,s2,Amp = r2 * s2 ) & ( (r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp))) = 0. R implies add2 r1,r2,s1,s2,Amp = 1. R ) & ( not r1 = 0. R & not s1 = 0. R & not gcd r2,s2,Amp = 1. R & not (r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp))) = 0. R implies add2 r1,r2,s1,s2,Amp = (r2 * (s2 / (gcd r2,s2,Amp))) / (gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(gcd r2,s2,Amp),Amp) ) );

theorem :: GCD_1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being gcdDomain
for Amp being AmpleSet of R
for r1, r2, s1, s2 being Element of R st Amp is multiplicative & r1,r2 are_normalized_wrt Amp & s1,s2 are_normalized_wrt Amp holds
add1 r1,r2,s1,s2,Amp, add2 r1,r2,s1,s2,Amp are_normalized_wrt Amp
proof end;

theorem :: GCD_1:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) * (r2 * s2) = (add2 r1,r2,s1,s2,Amp) * ((r1 * s2) + (s1 * r2))
proof 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 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 A1: ( r1,r2 are_co-prime & s1,s2 are_co-prime & r2 = NF r2,Amp & s2 = NF s2,Amp ) ;
func mult2 r1,r2,s1,s2,Amp -> Element of R equals :Def19: :: GCD_1:def 19
1. R if ( r1 = 0. R or s1 = 0. R )
1. R if ( r2 = 1. R & s2 = 1. R )
s2 / (gcd r1,s2,Amp) if ( s2 <> 0. R & r2 = 1. R )
r2 / (gcd s1,r2,Amp) if ( r2 <> 0. R & s2 = 1. R )
otherwise (r2 / (gcd s1,r2,Amp)) * (s2 / (gcd r1,s2,Amp));
coherence
( ( ( r1 = 0. R or s1 = 0. R ) implies 1. R is Element of R ) & ( r2 = 1. R & s2 = 1. R implies 1. R is Element of R ) & ( s2 <> 0. R & r2 = 1. R implies s2 / (gcd r1,s2,Amp) is Element of R ) & ( r2 <> 0. R & s2 = 1. R implies r2 / (gcd s1,r2,Amp) is Element of R ) & ( r1 = 0. R or s1 = 0. R or ( r2 = 1. R & s2 = 1. R ) or ( s2 <> 0. R & r2 = 1. R ) or ( r2 <> 0. R & s2 = 1. R ) or (r2 / (gcd s1,r2,Amp)) * (s2 / (gcd r1,s2,Amp)) is Element of R ) )
;
consistency
for b1 being Element of R holds
( ( ( r1 = 0. R or s1 = 0. R ) & r2 = 1. R & s2 = 1. R implies ( b1 = 1. R iff b1 = 1. R ) ) & ( ( r1 = 0. R or s1 = 0. R ) & s2 <> 0. R & r2 = 1. R implies ( b1 = 1. R iff b1 = s2 / (gcd r1,s2,Amp) ) ) & ( ( r1 = 0. R or s1 = 0. R ) & r2 <> 0. R & s2 = 1. R implies ( b1 = 1. R iff b1 = r2 / (gcd s1,r2,Amp) ) ) & ( r2 = 1. R & s2 = 1. R & s2 <> 0. R & r2 = 1. R implies ( b1 = 1. R iff b1 = s2 / (gcd r1,s2,Amp) ) ) & ( r2 = 1. R & s2 = 1. R & r2 <> 0. R & s2 = 1. R implies ( b1 = 1. R iff b1 = r2 / (gcd s1,r2,Amp) ) ) & ( s2 <> 0. R & r2 = 1. R & r2 <> 0. R & s2 = 1. R implies ( b1 = s2 / (gcd r1,s2,Amp) iff b1 = r2 / (gcd s1,r2,Amp) ) ) )
proof end;
end;

:: deftheorem Def19 defines mult2 GCD_1:def 19 :
for R being gcdDomain
for Amp being AmpleSet of R
for r1, r2, s1, s2 being Element of R st r1,r2 are_co-prime & s1,s2 are_co-prime & r2 = NF r2,Amp & s2 = NF s2,Amp holds
( ( ( r1 = 0. R or s1 = 0. R ) implies mult2 r1,r2,s1,s2,Amp = 1. R ) & ( r2 = 1. R & s2 = 1. R implies mult2 r1,r2,s1,s2,Amp = 1. R ) & ( s2 <> 0. R & r2 = 1. R implies mult2 r1,r2,s1,s2,Amp = s2 / (gcd r1,s2,Amp) ) & ( r2 <> 0. R & s2 = 1. R implies mult2 r1,r2,s1,s2,Amp = r2 / (gcd s1,r2,Amp) ) & ( r1 = 0. R or s1 = 0. R or ( r2 = 1. R & s2 = 1. R ) or ( s2 <> 0. R & r2 = 1. R ) or ( r2 <> 0. R & s2 = 1. R ) or mult2 r1,r2,s1,s2,Amp = (r2 / (gcd s1,r2,Amp)) * (s2 / (gcd r1,s2,Amp)) ) );

theorem :: GCD_1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being gcdDomain
for Amp being AmpleSet of R
for r1, r2, s1, s2 being Element of R st Amp is multiplicative & r1,r2 are_normalized_wrt Amp & s1,s2 are_normalized_wrt Amp holds
mult1 r1,r2,s1,s2,Amp, mult2 r1,r2,s1,s2,Amp are_normalized_wrt Amp
proof end;

theorem :: GCD_1:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) * (r2 * s2) = (mult2 r1,r2,s1,s2,Amp) * (r1 * s1)
proof end;

theorem :: GCD_1:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: GCD_1:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: GCD_1:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being non empty Abelian add-associative right_zeroed right_complementable distributive doubleLoopStr
for x, y being Element of F holds
( (- x) * y = - (x * y) & x * (- y) = - (x * y) ) by VECTSP_1:40, VECTSP_1:41;

theorem :: GCD_1:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: GCD_1:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being commutative Field-like Ring
for a, b being Element of F st a <> 0. F & b <> 0. F holds
(a " ) * (b " ) = (b * a) "
proof end;