:: by Christoph Schwarzweller

::

:: Received February 4, 1999

:: Copyright (c) 1999-2012 Association of Mizar Users

begin

definition

for b_{1} being Element of K6(K7(K7(INT,INT),INT)) holds

( b_{1} = multint iff for a, b being Element of INT holds b_{1} . (a,b) = multreal . (a,b) )
end;

redefine func multint means :Def1: :: INT_3:def 1

for a, b being Element of INT holds it . (a,b) = multreal . (a,b);

compatibility for a, b being Element of INT holds it . (a,b) = multreal . (a,b);

for b

( b

proof end;

:: deftheorem Def1 defines multint INT_3:def 1 :

for b_{1} being Element of K6(K7(K7(INT,INT),INT)) holds

( b_{1} = multint iff for a, b being Element of INT holds b_{1} . (a,b) = multreal . (a,b) );

for b

( b

definition

compatibility

for b_{1} being Element of K6(K7(INT,INT)) holds

( b_{1} = compint iff for a being Element of INT holds b_{1} . a = compreal . a )

end;
for b

( b

proof end;

:: deftheorem defines compint INT_3:def 2 :

for b_{1} being Element of K6(K7(INT,INT)) holds

( b_{1} = compint iff for a being Element of INT holds b_{1} . a = compreal . a );

for b

( b

definition

doubleLoopStr(# INT,addint,multint,(In (1,INT)),(In (0,INT)) #) is doubleLoopStr ;

end;

func INT.Ring -> doubleLoopStr equals :: INT_3:def 3

doubleLoopStr(# INT,addint,multint,(In (1,INT)),(In (0,INT)) #);

coherence doubleLoopStr(# INT,addint,multint,(In (1,INT)),(In (0,INT)) #);

doubleLoopStr(# INT,addint,multint,(In (1,INT)),(In (0,INT)) #) is doubleLoopStr ;

:: deftheorem defines INT.Ring INT_3:def 3 :

INT.Ring = doubleLoopStr(# INT,addint,multint,(In (1,INT)),(In (0,INT)) #);

INT.Ring = doubleLoopStr(# INT,addint,multint,(In (1,INT)),(In (0,INT)) #);

Lm1: for x being Element of INT.Ring holds x in REAL

proof end;

registration
end;

registration

let a, b be Element of INT.Ring;

let c, d be Integer;

compatibility

( a = c & b = d implies a * b = c * d )

( a = c & b = d implies a + b = c + d )

end;
let c, d be Integer;

compatibility

( a = c & b = d implies a * b = c * d )

proof end;

compatibility ( a = c & b = d implies a + b = c + d )

proof end;

set M = INT.Ring ;

Lm2: 0 in INT

by INT_1:def 2;

then Lm3: 0 = 0. INT.Ring

by FUNCT_7:def 1;

Lm4: 1_ INT.Ring = 1

proof end;

registration

( INT.Ring is Abelian & INT.Ring is add-associative & INT.Ring is right_zeroed & INT.Ring is right_complementable & INT.Ring is distributive & INT.Ring is commutative & INT.Ring is associative & INT.Ring is domRing-like & not INT.Ring is degenerated )
end;

cluster INT.Ring -> non degenerated right_complementable associative commutative Abelian add-associative right_zeroed distributive domRing-like ;

coherence ( INT.Ring is Abelian & INT.Ring is add-associative & INT.Ring is right_zeroed & INT.Ring is right_complementable & INT.Ring is distributive & INT.Ring is commutative & INT.Ring is associative & INT.Ring is domRing-like & not INT.Ring is degenerated )

proof end;

registration
end;

definition

let a be Element of INT.Ring;

|.a.| is Element of INT.Ring

for b_{1} being Element of INT.Ring holds

( ( a >= 0. INT.Ring implies ( b_{1} = |.a.| iff b_{1} = a ) ) & ( not a >= 0. INT.Ring implies ( b_{1} = |.a.| iff b_{1} = - a ) ) )
by Lm3, ABSVALUE:def 1;

consistency

for b_{1} being Element of INT.Ring holds verum
;

end;
:: original: |.

redefine func abs a -> Element of INT.Ring equals :: INT_3:def 4

a if a >= 0. INT.Ring

otherwise - a;

coherence redefine func abs a -> Element of INT.Ring equals :: INT_3:def 4

a if a >= 0. INT.Ring

otherwise - a;

|.a.| is Element of INT.Ring

proof end;

compatibility for b

( ( a >= 0. INT.Ring implies ( b

consistency

for b

:: deftheorem defines abs INT_3:def 4 :

for a being Element of INT.Ring holds

( ( a >= 0. INT.Ring implies abs a = a ) & ( not a >= 0. INT.Ring implies abs a = - a ) );

for a being Element of INT.Ring holds

( ( a >= 0. INT.Ring implies abs a = a ) & ( not a >= 0. INT.Ring implies abs a = - a ) );

definition

ex b_{1} being Function of the carrier of INT.Ring,NAT st

for a being Element of INT.Ring holds b_{1} . a = absreal . a

for b_{1}, b_{2} being Function of the carrier of INT.Ring,NAT st ( for a being Element of INT.Ring holds b_{1} . a = absreal . a ) & ( for a being Element of INT.Ring holds b_{2} . a = absreal . a ) holds

b_{1} = b_{2}
end;

func absint -> Function of the carrier of INT.Ring,NAT means :Def5: :: INT_3:def 5

for a being Element of INT.Ring holds it . a = absreal . a;

existence for a being Element of INT.Ring holds it . a = absreal . a;

ex b

for a being Element of INT.Ring holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines absint INT_3:def 5 :

for b_{1} being Function of the carrier of INT.Ring,NAT holds

( b_{1} = absint iff for a being Element of INT.Ring holds b_{1} . a = absreal . a );

for b

( b

Lm5: for a being Integer holds

( a = 0 or absreal . a >= 1 )

proof end;

Lm6: for a, b being Element of INT.Ring st b <> 0. INT.Ring holds

for b9 being Integer st b9 = b & 0 <= b9 holds

ex q, r being Element of INT.Ring st

( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) )

proof end;

Lm7: for a, b being Element of INT.Ring st b <> 0. INT.Ring holds

for b9 being Integer st b9 = b & 0 <= b9 holds

ex q, r being Element of INT.Ring st

( a = (q * b) + r & 0. INT.Ring <= r & r < abs b )

proof end;

theorem Th2: :: INT_3:2

for a, b, q1, q2, r1, r2 being Element of INT.Ring st b <> 0. INT.Ring & a = (q1 * b) + r1 & 0. INT.Ring <= r1 & r1 < abs b & a = (q2 * b) + r2 & 0. INT.Ring <= r2 & r2 < abs b holds

( q1 = q2 & r1 = r2 )

( q1 = q2 & r1 = r2 )

proof end;

definition

let a, b be Element of INT.Ring;

assume A1: b <> 0. INT.Ring ;

ex b_{1}, r being Element of INT.Ring st

( a = (b_{1} * b) + r & 0. INT.Ring <= r & r < abs b )

for b_{1}, b_{2} being Element of INT.Ring st ex r being Element of INT.Ring st

( a = (b_{1} * b) + r & 0. INT.Ring <= r & r < abs b ) & ex r being Element of INT.Ring st

( a = (b_{2} * b) + r & 0. INT.Ring <= r & r < abs b ) holds

b_{1} = b_{2}
by A1, Th2;

end;
assume A1: b <> 0. INT.Ring ;

func a div b -> Element of INT.Ring means :Def6: :: INT_3:def 6

ex r being Element of INT.Ring st

( a = (it * b) + r & 0. INT.Ring <= r & r < abs b );

existence ex r being Element of INT.Ring st

( a = (it * b) + r & 0. INT.Ring <= r & r < abs b );

ex b

( a = (b

proof end;

uniqueness for b

( a = (b

( a = (b

b

:: deftheorem Def6 defines div INT_3:def 6 :

for a, b being Element of INT.Ring st b <> 0. INT.Ring holds

for b_{3} being Element of INT.Ring holds

( b_{3} = a div b iff ex r being Element of INT.Ring st

( a = (b_{3} * b) + r & 0. INT.Ring <= r & r < abs b ) );

for a, b being Element of INT.Ring st b <> 0. INT.Ring holds

for b

( b

( a = (b

definition

let a, b be Element of INT.Ring;

assume A1: b <> 0. INT.Ring ;

ex b_{1}, q being Element of INT.Ring st

( a = (q * b) + b_{1} & 0. INT.Ring <= b_{1} & b_{1} < abs b )

for b_{1}, b_{2} being Element of INT.Ring st ex q being Element of INT.Ring st

( a = (q * b) + b_{1} & 0. INT.Ring <= b_{1} & b_{1} < abs b ) & ex q being Element of INT.Ring st

( a = (q * b) + b_{2} & 0. INT.Ring <= b_{2} & b_{2} < abs b ) holds

b_{1} = b_{2}
by A1, Th2;

end;
assume A1: b <> 0. INT.Ring ;

func a mod b -> Element of INT.Ring means :Def7: :: INT_3:def 7

ex q being Element of INT.Ring st

( a = (q * b) + it & 0. INT.Ring <= it & it < abs b );

existence ex q being Element of INT.Ring st

( a = (q * b) + it & 0. INT.Ring <= it & it < abs b );

ex b

( a = (q * b) + b

proof end;

uniqueness for b

( a = (q * b) + b

( a = (q * b) + b

b

:: deftheorem Def7 defines mod INT_3:def 7 :

for a, b being Element of INT.Ring st b <> 0. INT.Ring holds

for b_{3} being Element of INT.Ring holds

( b_{3} = a mod b iff ex q being Element of INT.Ring st

( a = (q * b) + b_{3} & 0. INT.Ring <= b_{3} & b_{3} < abs b ) );

for a, b being Element of INT.Ring st b <> 0. INT.Ring holds

for b

( b

( a = (q * b) + b

begin

:: deftheorem Def8 defines Euclidian INT_3:def 8 :

for I being non empty doubleLoopStr holds

( I is Euclidian iff ex f being Function of the carrier of I,NAT st

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

ex q, r being Element of I st

( a = (q * b) + r & ( r = 0. I or f . r < f . b ) ) );

for I being non empty doubleLoopStr holds

( I is Euclidian iff ex f being Function of the carrier of I,NAT st

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

ex q, r being Element of I st

( a = (q * b) + r & ( r = 0. I or f . r < f . b ) ) );

Lm8: for F being non empty almost_left_invertible associative commutative right_zeroed well-unital doubleLoopStr

for f being Function of the carrier of F,NAT

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

ex q, r being Element of F st

( a = (q * b) + r & ( r = 0. F or f . r < f . b ) )

proof end;

registration

ex b_{1} being Ring st

( b_{1} is strict & b_{1} is Euclidian & b_{1} is domRing-like & not b_{1} is degenerated & b_{1} is distributive & b_{1} is commutative )
end;

cluster non empty non degenerated right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like Euclidian for doubleLoopStr ;

existence ex b

( b

proof end;

registration

ex b_{1} being EuclidianRing st b_{1} is strict
end;

cluster non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like Euclidian for doubleLoopStr ;

existence ex b

proof end;

definition

let E be non empty Euclidian doubleLoopStr ;

ex b_{1} being Function of the carrier of E,NAT st

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

ex q, r being Element of E st

( a = (q * b) + r & ( r = 0. E or b_{1} . r < b_{1} . b ) )
by Def8;

end;
mode DegreeFunction of E -> Function of the carrier of E,NAT means :Def9: :: INT_3:def 9

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

ex q, r being Element of E st

( a = (q * b) + r & ( r = 0. E or it . r < it . b ) );

existence for a, b being Element of E st b <> 0. E holds

ex q, r being Element of E st

( a = (q * b) + r & ( r = 0. E or it . r < it . b ) );

ex b

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

ex q, r being Element of E st

( a = (q * b) + r & ( r = 0. E or b

:: deftheorem Def9 defines DegreeFunction INT_3:def 9 :

for E being non empty Euclidian doubleLoopStr

for b_{2} being Function of the carrier of E,NAT holds

( b_{2} is DegreeFunction of E iff for a, b being Element of E st b <> 0. E holds

ex q, r being Element of E st

( a = (q * b) + r & ( r = 0. E or b_{2} . r < b_{2} . b ) ) );

for E being non empty Euclidian doubleLoopStr

for b

( b

ex q, r being Element of E st

( a = (q * b) + r & ( r = 0. E or b

registration

for b_{1} being non empty non degenerated right_complementable associative commutative Abelian add-associative right_zeroed right-distributive well-unital domRing-like doubleLoopStr st b_{1} is Euclidian holds

b_{1} is gcd-like
by Th4;

end;

cluster non empty non degenerated right_complementable associative commutative Abelian add-associative right_zeroed right-distributive well-unital domRing-like Euclidian -> non empty non degenerated right_complementable associative commutative Abelian add-associative right_zeroed right-distributive well-unital domRing-like gcd-like for doubleLoopStr ;

coherence for b

b

definition

:: original: absint

redefine func absint -> DegreeFunction of INT.Ring ;

coherence

absint is DegreeFunction of INT.Ring

end;
redefine func absint -> DegreeFunction of INT.Ring ;

coherence

absint is DegreeFunction of INT.Ring

proof end;

theorem Th5: :: INT_3:5

for F being non empty almost_left_invertible associative commutative right_zeroed well-unital doubleLoopStr holds F is Euclidian

proof end;

registration

for b_{1} being non empty doubleLoopStr st b_{1} is commutative & b_{1} is associative & b_{1} is well-unital & b_{1} is almost_left_invertible & b_{1} is right_zeroed & b_{1} is almost_left_invertible holds

b_{1} is Euclidian
by Th5;

end;

cluster non empty almost_left_invertible associative commutative right_zeroed well-unital -> non empty Euclidian for doubleLoopStr ;

coherence for b

b

theorem :: INT_3:6

for F being non empty almost_left_invertible associative commutative right_zeroed well-unital doubleLoopStr

for f being Function of the carrier of F,NAT holds f is DegreeFunction of F

for f being Function of the carrier of F,NAT holds f is DegreeFunction of F

proof end;

begin

definition

let n be Nat;

assume A1: n > 0 ;

ex b_{1} being BinOp of (Segm n) st

for k, l being Element of Segm n holds b_{1} . (k,l) = (k * l) mod n

for b_{1}, b_{2} being BinOp of (Segm n) st ( for k, l being Element of Segm n holds b_{1} . (k,l) = (k * l) mod n ) & ( for k, l being Element of Segm n holds b_{2} . (k,l) = (k * l) mod n ) holds

b_{1} = b_{2}

end;
assume A1: n > 0 ;

func multint n -> BinOp of (Segm n) means :Def10: :: INT_3:def 10

for k, l being Element of Segm n holds it . (k,l) = (k * l) mod n;

existence for k, l being Element of Segm n holds it . (k,l) = (k * l) mod n;

ex b

for k, l being Element of Segm n holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def10 defines multint INT_3:def 10 :

for n being Nat st n > 0 holds

for b_{2} being BinOp of (Segm n) holds

( b_{2} = multint n iff for k, l being Element of Segm n holds b_{2} . (k,l) = (k * l) mod n );

for n being Nat st n > 0 holds

for b

( b

definition

let n be Nat;

assume A1: n > 0 ;

ex b_{1} being UnOp of (Segm n) st

for k being Element of Segm n holds b_{1} . k = (n - k) mod n

for b_{1}, b_{2} being UnOp of (Segm n) st ( for k being Element of Segm n holds b_{1} . k = (n - k) mod n ) & ( for k being Element of Segm n holds b_{2} . k = (n - k) mod n ) holds

b_{1} = b_{2}

end;
assume A1: n > 0 ;

func compint n -> UnOp of (Segm n) means :Def11: :: INT_3:def 11

for k being Element of Segm n holds it . k = (n - k) mod n;

existence for k being Element of Segm n holds it . k = (n - k) mod n;

ex b

for k being Element of Segm n holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def11 defines compint INT_3:def 11 :

for n being Nat st n > 0 holds

for b_{2} being UnOp of (Segm n) holds

( b_{2} = compint n iff for k being Element of Segm n holds b_{2} . k = (n - k) mod n );

for n being Nat st n > 0 holds

for b

( b

theorem Th7: :: INT_3:7

for n being Nat st n > 0 holds

for a, b being Element of Segm n holds

( ( a + b < n implies (addint n) . (a,b) = a + b ) & ( (addint n) . (a,b) = a + b implies a + b < n ) & ( a + b >= n implies (addint n) . (a,b) = (a + b) - n ) & ( (addint n) . (a,b) = (a + b) - n implies a + b >= n ) )

for a, b being Element of Segm n holds

( ( a + b < n implies (addint n) . (a,b) = a + b ) & ( (addint n) . (a,b) = a + b implies a + b < n ) & ( a + b >= n implies (addint n) . (a,b) = (a + b) - n ) & ( (addint n) . (a,b) = (a + b) - n implies a + b >= n ) )

proof end;

Lm9: for a, b being Nat st b <> 0 holds

ex k being Element of NAT st

( k * b <= a & a < (k + 1) * b )

proof end;

theorem Th8: :: INT_3:8

for n being Nat st n > 0 holds

for a, b being Element of Segm n

for k being Nat holds

( ( k * n <= a * b & a * b < (k + 1) * n ) iff (multint n) . (a,b) = (a * b) - (k * n) )

for a, b being Element of Segm n

for k being Nat holds

( ( k * n <= a * b & a * b < (k + 1) * n ) iff (multint n) . (a,b) = (a * b) - (k * n) )

proof end;

theorem :: INT_3:9

for n being Nat st n > 0 holds

for a being Element of Segm n holds

( ( a = 0 implies (compint n) . a = 0 ) & ( (compint n) . a = 0 implies a = 0 ) & ( a <> 0 implies (compint n) . a = n - a ) & ( (compint n) . a = n - a implies a <> 0 ) )

for a being Element of Segm n holds

( ( a = 0 implies (compint n) . a = 0 ) & ( (compint n) . a = 0 implies a = 0 ) & ( a <> 0 implies (compint n) . a = n - a ) & ( (compint n) . a = n - a implies a <> 0 ) )

proof end;

definition

let n be Nat;

doubleLoopStr(# (Segm n),(addint n),(multint n),(In (1,(Segm n))),(In (0,(Segm n))) #) is doubleLoopStr ;

end;
func INT.Ring n -> doubleLoopStr equals :: INT_3:def 12

doubleLoopStr(# (Segm n),(addint n),(multint n),(In (1,(Segm n))),(In (0,(Segm n))) #);

coherence doubleLoopStr(# (Segm n),(addint n),(multint n),(In (1,(Segm n))),(In (0,(Segm n))) #);

doubleLoopStr(# (Segm n),(addint n),(multint n),(In (1,(Segm n))),(In (0,(Segm n))) #) is doubleLoopStr ;

:: deftheorem defines INT.Ring INT_3:def 12 :

for n being Nat holds INT.Ring n = doubleLoopStr(# (Segm n),(addint n),(multint n),(In (1,(Segm n))),(In (0,(Segm n))) #);

for n being Nat holds INT.Ring n = doubleLoopStr(# (Segm n),(addint n),(multint n),(In (1,(Segm n))),(In (0,(Segm n))) #);

registration
end;

theorem Th10: :: INT_3:10

( INT.Ring 1 is degenerated & INT.Ring 1 is Ring & INT.Ring 1 is almost_left_invertible & INT.Ring 1 is unital & INT.Ring 1 is distributive & INT.Ring 1 is commutative )

proof end;

registration

ex b_{1} being Ring st

( b_{1} is strict & b_{1} is degenerated & b_{1} is unital & b_{1} is distributive & b_{1} is almost_left_invertible & b_{1} is commutative )
by Th10;

end;

cluster non empty degenerated right_complementable almost_left_invertible strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital for doubleLoopStr ;

existence ex b

( b

Lm10: now :: thesis: for a, n being Nat st a in Segm n & a > 0 holds

n - a in Segm n

n - a in Segm n

let a, n be Nat; :: thesis: ( a in Segm n & a > 0 implies n - a in Segm n )

assume a in Segm n ; :: thesis: ( a > 0 implies n - a in Segm n )

then a < n by NAT_1:44;

then A1: n - a is Element of NAT by INT_1:5;

assume a > 0 ; :: thesis: n - a in Segm n

then n - a < n - 0 by XREAL_1:15;

hence n - a in Segm n by A1, NAT_1:44; :: thesis: verum

end;
assume a in Segm n ; :: thesis: ( a > 0 implies n - a in Segm n )

then a < n by NAT_1:44;

then A1: n - a is Element of NAT by INT_1:5;

assume a > 0 ; :: thesis: n - a in Segm n

then n - a < n - 0 by XREAL_1:15;

hence n - a in Segm n by A1, NAT_1:44; :: thesis: verum

Lm11: for n being Nat st 1 < n holds

1. (INT.Ring n) = 1

proof end;

theorem Th12: :: INT_3:12

for p being Nat st p > 1 holds

( INT.Ring p is non empty non degenerated right_complementable almost_left_invertible associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr iff p is Prime )

( INT.Ring p is non empty non degenerated right_complementable almost_left_invertible associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr iff p is Prime )

proof end;

registration

let p be Prime;

( INT.Ring p is add-associative & INT.Ring p is right_zeroed & INT.Ring p is right_complementable & INT.Ring p is Abelian & INT.Ring p is commutative & INT.Ring p is associative & INT.Ring p is well-unital & INT.Ring p is distributive & INT.Ring p is almost_left_invertible & not INT.Ring p is degenerated )

end;
cluster INT.Ring p -> non degenerated right_complementable almost_left_invertible associative commutative Abelian add-associative right_zeroed well-unital distributive ;

coherence ( INT.Ring p is add-associative & INT.Ring p is right_zeroed & INT.Ring p is right_complementable & INT.Ring p is Abelian & INT.Ring p is commutative & INT.Ring p is associative & INT.Ring p is well-unital & INT.Ring p is distributive & INT.Ring p is almost_left_invertible & not INT.Ring p is degenerated )

proof end;

begin

:: from SCMRING3, 2011.08.19, A.T.

registration

ex b_{1} being Ring st

( b_{1} is strict & b_{1} is infinite )
end;

cluster non empty infinite right_complementable strict unital associative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital for doubleLoopStr ;

existence ex b

( b

proof end;