let E be EuclidianRing; :: thesis: E is gcdDomain

set d = the DegreeFunction of E;

set d = the DegreeFunction of E;

now :: thesis: for x, y being Element of E ex z being Element of E st

( z divides x & z divides y & ( for zz being Element of E st zz divides x & zz divides y holds

zz divides z ) )

hence
E is gcdDomain
by GCD_1:def 11; :: thesis: verum( z divides x & z divides y & ( for zz being Element of E st zz divides x & zz divides y holds

zz divides z ) )

let x, y be Element of E; :: thesis: ex z being Element of E st

( z divides x & z divides y & ( for zz being Element of E st zz divides x & zz divides y holds

zz divides z ) )

( z divides x & z divides y & ( for zz being Element of E st zz divides x & zz divides y holds

zz divides z ) ) ; :: thesis: verum

end;( z divides x & z divides y & ( for zz being Element of E st zz divides x & zz divides y holds

zz divides z ) )

now :: thesis: ( ( x = 0. E & ex z being Element of E st

( z divides x & z divides y & ( for zz being Element of E st zz divides x & zz divides y holds

zz divides z ) ) ) or ( x <> 0. E & ex z being Element of E st

( z divides x & z divides y & ( for zz being Element of E st zz divides x & zz divides y holds

zz divides z ) ) ) )end;

hence
ex z being Element of E st ( z divides x & z divides y & ( for zz being Element of E st zz divides x & zz divides y holds

zz divides z ) ) ) or ( x <> 0. E & ex z being Element of E st

( z divides x & z divides y & ( for zz being Element of E st zz divides x & zz divides y holds

zz divides z ) ) ) )

per cases
( x = 0. E or x <> 0. E )
;

end;

case A1:
x = 0. E
; :: thesis: ex z being Element of E st

( z divides x & z divides y & ( for zz being Element of E st zz divides x & zz divides y holds

zz divides z ) )

( z divides x & z divides y & ( for zz being Element of E st zz divides x & zz divides y holds

zz divides z ) )

y * (0. E) = 0. E
;

then A2: y divides 0. E by GCD_1:def 1;

for zz being Element of E st zz divides x & zz divides y holds

zz divides y ;

hence ex z being Element of E st

( z divides x & z divides y & ( for zz being Element of E st zz divides x & zz divides y holds

zz divides z ) ) by A1, A2; :: thesis: verum

end;then A2: y divides 0. E by GCD_1:def 1;

for zz being Element of E st zz divides x & zz divides y holds

zz divides y ;

hence ex z being Element of E st

( z divides x & z divides y & ( for zz being Element of E st zz divides x & zz divides y holds

zz divides z ) ) by A1, A2; :: thesis: verum

case A3:
x <> 0. E
; :: thesis: ex z being Element of E st

( z divides x & z divides y & ( for zz being Element of E st zz divides x & zz divides y holds

zz divides z ) )

( z divides x & z divides y & ( for zz being Element of E st zz divides x & zz divides y holds

zz divides z ) )

set M = { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } ;

defpred S_{1}[ Nat] means ex z being Element of E st

( z in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } & z <> 0. E & $1 = the DegreeFunction of E . z );

((1. E) * x) + ((0. E) * y) = (1. E) * x by RLVECT_1:def 4

.= x ;

then A4: x in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } ;

ex k being Element of NAT st k = the DegreeFunction of E . x ;

then A5: ex k being Nat st S_{1}[k]
by A3, A4;

ex k being Nat st

( S_{1}[k] & ( for n being Nat st S_{1}[n] holds

k <= n ) ) from NAT_1:sch 5(A5);

then consider k being Nat such that

A6: ( S_{1}[k] & ( for n being Nat st S_{1}[n] holds

k <= n ) ) ;

consider g being Element of E such that

A7: g in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } and

A8: g <> 0. E and

A9: ( k = the DegreeFunction of E . g & ( for n being Nat st ex z being Element of E st

( z in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } & z <> 0. E & n = the DegreeFunction of E . z ) holds

k <= n ) ) by A6;

set G = { z where z is Element of E : ex r being Element of E st z = r * g } ;

A10: for z being object st z in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } holds

z in { z where z is Element of E : ex r being Element of E st z = r * g }

z divides g

.= y ;

then A27: y in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } ;

for z being object st z in { z where z is Element of E : ex r being Element of E st z = r * g } holds

z in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) }

( g divides x & g divides y )

( z divides x & z divides y & ( for zz being Element of E st zz divides x & zz divides y holds

zz divides z ) ) by A19; :: thesis: verum

end;defpred S

( z in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } & z <> 0. E & $1 = the DegreeFunction of E . z );

((1. E) * x) + ((0. E) * y) = (1. E) * x by RLVECT_1:def 4

.= x ;

then A4: x in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } ;

ex k being Element of NAT st k = the DegreeFunction of E . x ;

then A5: ex k being Nat st S

ex k being Nat st

( S

k <= n ) ) from NAT_1:sch 5(A5);

then consider k being Nat such that

A6: ( S

k <= n ) ) ;

consider g being Element of E such that

A7: g in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } and

A8: g <> 0. E and

A9: ( k = the DegreeFunction of E . g & ( for n being Nat st ex z being Element of E st

( z in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } & z <> 0. E & n = the DegreeFunction of E . z ) holds

k <= n ) ) by A6;

set G = { z where z is Element of E : ex r being Element of E st z = r * g } ;

A10: for z being object st z in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } holds

z in { z where z is Element of E : ex r being Element of E st z = r * g }

proof

A19:
for z being Element of E st z divides x & z divides y holds
let z be object ; :: thesis: ( z in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } implies z in { z where z is Element of E : ex r being Element of E st z = r * g } )

assume z in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } ; :: thesis: z in { z where z is Element of E : ex r being Element of E st z = r * g }

then consider z2 being Element of E such that

A11: z = z2 and

A12: ex s, t being Element of E st z2 = (s * x) + (t * y) ;

consider u, v being Element of E such that

A13: z2 = (u * x) + (v * y) by A12;

reconsider z = z as Element of E by A11;

consider q, r being Element of E such that

A14: z = (q * g) + r and

A15: ( r = 0. E or the DegreeFunction of E . r < the DegreeFunction of E . g ) by A8, Def9;

r in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) }

then z = q * g by A14, RLVECT_1:def 4;

hence z in { z where z is Element of E : ex r being Element of E st z = r * g } ; :: thesis: verum

end;assume z in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } ; :: thesis: z in { z where z is Element of E : ex r being Element of E st z = r * g }

then consider z2 being Element of E such that

A11: z = z2 and

A12: ex s, t being Element of E st z2 = (s * x) + (t * y) ;

consider u, v being Element of E such that

A13: z2 = (u * x) + (v * y) by A12;

reconsider z = z as Element of E by A11;

consider q, r being Element of E such that

A14: z = (q * g) + r and

A15: ( r = 0. E or the DegreeFunction of E . r < the DegreeFunction of E . g ) by A8, Def9;

r in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) }

proof

then
r = 0. E
by A9, A15;
consider z1 being Element of E such that

A16: g = z1 and

A17: ex s, t being Element of E st z1 = (s * x) + (t * y) by A7;

consider s, t being Element of E such that

A18: z1 = (s * x) + (t * y) by A17;

z + (- (q * g)) = r + ((q * g) + (- (q * g))) by A14, RLVECT_1:def 3

.= r + (0. E) by RLVECT_1:def 10

.= r by RLVECT_1:def 4 ;

then r = z + (- ((q * (s * x)) + (q * (t * y)))) by A16, A18, VECTSP_1:def 7

.= z + ((- (q * (s * x))) + (- (q * (t * y)))) by RLVECT_1:31

.= (((u * x) + (v * y)) + (- (q * (s * x)))) + (- (q * (t * y))) by A11, A13, RLVECT_1:def 3

.= (((u * x) + (- (q * (s * x)))) + (v * y)) + (- (q * (t * y))) by RLVECT_1:def 3

.= ((u * x) + (- (q * (s * x)))) + ((v * y) + (- (q * (t * y)))) by RLVECT_1:def 3

.= ((u * x) + ((- q) * (s * x))) + ((v * y) + (- (q * (t * y)))) by GCD_1:48

.= ((u * x) + ((- q) * (s * x))) + ((v * y) + ((- q) * (t * y))) by GCD_1:48

.= ((u * x) + (((- q) * s) * x)) + ((v * y) + ((- q) * (t * y))) by GROUP_1:def 3

.= ((u * x) + (((- q) * s) * x)) + ((v * y) + (((- q) * t) * y)) by GROUP_1:def 3

.= ((u + ((- q) * s)) * x) + ((v * y) + (((- q) * t) * y)) by VECTSP_1:def 7

.= ((u + ((- q) * s)) * x) + ((v + ((- q) * t)) * y) by VECTSP_1:def 7 ;

hence r in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } ; :: thesis: verum

end;A16: g = z1 and

A17: ex s, t being Element of E st z1 = (s * x) + (t * y) by A7;

consider s, t being Element of E such that

A18: z1 = (s * x) + (t * y) by A17;

z + (- (q * g)) = r + ((q * g) + (- (q * g))) by A14, RLVECT_1:def 3

.= r + (0. E) by RLVECT_1:def 10

.= r by RLVECT_1:def 4 ;

then r = z + (- ((q * (s * x)) + (q * (t * y)))) by A16, A18, VECTSP_1:def 7

.= z + ((- (q * (s * x))) + (- (q * (t * y)))) by RLVECT_1:31

.= (((u * x) + (v * y)) + (- (q * (s * x)))) + (- (q * (t * y))) by A11, A13, RLVECT_1:def 3

.= (((u * x) + (- (q * (s * x)))) + (v * y)) + (- (q * (t * y))) by RLVECT_1:def 3

.= ((u * x) + (- (q * (s * x)))) + ((v * y) + (- (q * (t * y)))) by RLVECT_1:def 3

.= ((u * x) + ((- q) * (s * x))) + ((v * y) + (- (q * (t * y)))) by GCD_1:48

.= ((u * x) + ((- q) * (s * x))) + ((v * y) + ((- q) * (t * y))) by GCD_1:48

.= ((u * x) + (((- q) * s) * x)) + ((v * y) + ((- q) * (t * y))) by GROUP_1:def 3

.= ((u * x) + (((- q) * s) * x)) + ((v * y) + (((- q) * t) * y)) by GROUP_1:def 3

.= ((u + ((- q) * s)) * x) + ((v * y) + (((- q) * t) * y)) by VECTSP_1:def 7

.= ((u + ((- q) * s)) * x) + ((v + ((- q) * t)) * y) by VECTSP_1:def 7 ;

hence r in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } ; :: thesis: verum

then z = q * g by A14, RLVECT_1:def 4;

hence z in { z where z is Element of E : ex r being Element of E st z = r * g } ; :: thesis: verum

z divides g

proof

((0. E) * x) + ((1. E) * y) =
(1. E) * y
by RLVECT_1:4
let z be Element of E; :: thesis: ( z divides x & z divides y implies z divides g )

assume that

A20: z divides x and

A21: z divides y ; :: thesis: z divides g

consider u being Element of E such that

A22: x = z * u by A20, GCD_1:def 1;

consider zz being Element of E such that

A23: g = zz and

A24: ex s, t being Element of E st zz = (s * x) + (t * y) by A7;

consider s, t being Element of E such that

A25: zz = (s * x) + (t * y) by A24;

consider v being Element of E such that

A26: y = z * v by A21, GCD_1:def 1;

g = ((s * u) * z) + (t * (v * z)) by A22, A26, A23, A25, GROUP_1:def 3

.= ((s * u) * z) + ((t * v) * z) by GROUP_1:def 3

.= ((s * u) + (t * v)) * z by VECTSP_1:def 7 ;

hence z divides g by GCD_1:def 1; :: thesis: verum

end;assume that

A20: z divides x and

A21: z divides y ; :: thesis: z divides g

consider u being Element of E such that

A22: x = z * u by A20, GCD_1:def 1;

consider zz being Element of E such that

A23: g = zz and

A24: ex s, t being Element of E st zz = (s * x) + (t * y) by A7;

consider s, t being Element of E such that

A25: zz = (s * x) + (t * y) by A24;

consider v being Element of E such that

A26: y = z * v by A21, GCD_1:def 1;

g = ((s * u) * z) + (t * (v * z)) by A22, A26, A23, A25, GROUP_1:def 3

.= ((s * u) * z) + ((t * v) * z) by GROUP_1:def 3

.= ((s * u) + (t * v)) * z by VECTSP_1:def 7 ;

hence z divides g by GCD_1:def 1; :: thesis: verum

.= y ;

then A27: y in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } ;

for z being object st z in { z where z is Element of E : ex r being Element of E st z = r * g } holds

z in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) }

proof

then A34:
{ z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } = { z where z is Element of E : ex r being Element of E st z = r * g }
by A10, TARSKI:2;
let z be object ; :: thesis: ( z in { z where z is Element of E : ex r being Element of E st z = r * g } implies z in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } )

assume z in { z where z is Element of E : ex r being Element of E st z = r * g } ; :: thesis: z in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) }

then consider z2 being Element of E such that

A28: z = z2 and

A29: ex s being Element of E st z2 = s * g ;

reconsider z = z as Element of E by A28;

consider u being Element of E such that

A30: z2 = u * g by A29;

consider z1 being Element of E such that

A31: g = z1 and

A32: ex s, t being Element of E st z1 = (s * x) + (t * y) by A7;

consider s, t being Element of E such that

A33: z1 = (s * x) + (t * y) by A32;

z = (u * (s * x)) + (u * (t * y)) by A28, A30, A31, A33, VECTSP_1:def 2

.= ((u * s) * x) + (u * (t * y)) by GROUP_1:def 3

.= ((u * s) * x) + ((u * t) * y) by GROUP_1:def 3 ;

hence z in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } ; :: thesis: verum

end;assume z in { z where z is Element of E : ex r being Element of E st z = r * g } ; :: thesis: z in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) }

then consider z2 being Element of E such that

A28: z = z2 and

A29: ex s being Element of E st z2 = s * g ;

reconsider z = z as Element of E by A28;

consider u being Element of E such that

A30: z2 = u * g by A29;

consider z1 being Element of E such that

A31: g = z1 and

A32: ex s, t being Element of E st z1 = (s * x) + (t * y) by A7;

consider s, t being Element of E such that

A33: z1 = (s * x) + (t * y) by A32;

z = (u * (s * x)) + (u * (t * y)) by A28, A30, A31, A33, VECTSP_1:def 2

.= ((u * s) * x) + (u * (t * y)) by GROUP_1:def 3

.= ((u * s) * x) + ((u * t) * y) by GROUP_1:def 3 ;

hence z in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } ; :: thesis: verum

( g divides x & g divides y )

proof

hence
ex z being Element of E st
( ex zz being Element of E st

( x = zz & ex r being Element of E st zz = r * g ) & ex zzz being Element of E st

( y = zzz & ex r being Element of E st zzz = r * g ) ) by A4, A27, A34;

hence ( g divides x & g divides y ) by GCD_1:def 1; :: thesis: verum

end;( x = zz & ex r being Element of E st zz = r * g ) & ex zzz being Element of E st

( y = zzz & ex r being Element of E st zzz = r * g ) ) by A4, A27, A34;

hence ( g divides x & g divides y ) by GCD_1:def 1; :: thesis: verum

( z divides x & z divides y & ( for zz being Element of E st zz divides x & zz divides y holds

zz divides z ) ) by A19; :: thesis: verum

( z divides x & z divides y & ( for zz being Element of E st zz divides x & zz divides y holds

zz divides z ) ) ; :: thesis: verum