:: Ordered Rings and Fields
:: by Christoph Schwarzweller
::
:: Received March 17, 2017
:: Copyright (c) 2017-2021 Association of Mizar Users


definition
let X be set ;
let R be Relation of X;
attr R is strongly_reflexive means :defstr: :: REALALG1:def 1
R is_reflexive_in X;
attr R is totally_connected means :Rtot: :: REALALG1:def 2
R is_strongly_connected_in X;
end;

:: deftheorem defstr defines strongly_reflexive REALALG1:def 1 :
for X being set
for R being Relation of X holds
( R is strongly_reflexive iff R is_reflexive_in X );

:: deftheorem Rtot defines totally_connected REALALG1:def 2 :
for X being set
for R being Relation of X holds
( R is totally_connected iff R is_strongly_connected_in X );

registration
let X be set ;
cluster Relation-like X -defined X -valued strongly_reflexive for Element of bool [:X,X:];
existence
ex b1 being Relation of X st b1 is strongly_reflexive
proof end;
cluster Relation-like X -defined X -valued totally_connected for Element of bool [:X,X:];
existence
ex b1 being Relation of X st b1 is totally_connected
proof end;
end;

registration
let X be set ;
cluster strongly_reflexive -> reflexive for Element of bool [:X,X:];
coherence
for b1 being Relation of X st b1 is strongly_reflexive holds
b1 is reflexive
proof end;
cluster totally_connected -> strongly_connected for Element of bool [:X,X:];
coherence
for b1 being Relation of X st b1 is totally_connected holds
b1 is strongly_connected
proof end;
end;

registration
let X be non empty set ;
cluster strongly_reflexive -> non empty for Element of bool [:X,X:];
coherence
for b1 being Relation of X st b1 is strongly_reflexive holds
not b1 is empty
proof end;
cluster totally_connected -> non empty for Element of bool [:X,X:];
coherence
for b1 being Relation of X st b1 is totally_connected holds
not b1 is empty
proof end;
end;

theorem :: REALALG1:1
for X being non empty set
for R being strongly_reflexive Relation of X
for x being Element of X holds x <=_ R,x by defstr, RELAT_2:def 1;

theorem lemanti: :: REALALG1:2
for X being non empty set
for R being antisymmetric Relation of X
for x, y being Element of X st x <=_ R,y & y <=_ R,x holds
x = y
proof end;

theorem lemtrans: :: REALALG1:3
for X being non empty set
for R being transitive Relation of X
for x, y, z being Element of X st x <=_ R,y & y <=_ R,z holds
x <=_ R,z
proof end;

theorem :: REALALG1:4
for X being non empty set
for R being totally_connected Relation of X
for x, y being Element of X holds
( x <=_ R,y or y <=_ R,x ) by Rtot, RELAT_2:def 7;

definition
let L be addLoopStr ;
let R be Relation of L;
attr R is respecting_addition means :respadd: :: REALALG1:def 3
for a, b, c being Element of L st a <=_ R,b holds
a + c <=_ R,b + c;
end;

:: deftheorem respadd defines respecting_addition REALALG1:def 3 :
for L being addLoopStr
for R being Relation of L holds
( R is respecting_addition iff for a, b, c being Element of L st a <=_ R,b holds
a + c <=_ R,b + c );

definition
let L be multLoopStr_0 ;
let R be Relation of L;
attr R is respecting_multiplication means :respmult: :: REALALG1:def 4
for a, b, c being Element of L st a <=_ R,b & 0. L <=_ R,c holds
a * c <=_ R,b * c;
end;

:: deftheorem respmult defines respecting_multiplication REALALG1:def 4 :
for L being multLoopStr_0
for R being Relation of L holds
( R is respecting_multiplication iff for a, b, c being Element of L st a <=_ R,b & 0. L <=_ R,c holds
a * c <=_ R,b * c );

lemmul: for L being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for p, q being Polynomial of L st p <> 0_. L & q <> 0_. L holds
(p *' q) . ((((len p) + (len q)) - 1) -' 1) = (p . ((len p) -' 1)) * (q . ((len q) -' 1))

proof end;

theorem :: REALALG1:5
for R being degenerated Ring
for p being Polynomial of R holds { i where i is Nat : p . i <> 0. R } = {}
proof end;

theorem lemlp0: :: REALALG1:6
for R being Ring
for p being Polynomial of R holds
( p = 0_. R iff { i where i is Nat : p . i <> 0. R } = {} )
proof end;

theorem lemlowp0: :: REALALG1:7
for R being Ring
for p being Polynomial of R holds min* { i where i is Nat : (p + (0_. R)) . i <> 0. R } = min* { i where i is Nat : p . i <> 0. R }
proof end;

lemlp1: for R being non degenerated Ring
for p being non zero Polynomial of R holds { i where i is Nat : p . i <> 0. R } is non empty Subset of NAT

proof end;

theorem lemlowp2: :: REALALG1:8
for R being non degenerated Ring
for p being Polynomial of R holds min* { i where i is Nat : (- p) . i <> 0. R } = min* { i where i is Nat : p . i <> 0. R }
proof end;

theorem lemlowp1a1: :: REALALG1:9
for R being non degenerated Ring
for p, q being non zero Polynomial of R st min* { i where i is Nat : p . i <> 0. R } > min* { i where i is Nat : q . i <> 0. R } holds
min* { i where i is Nat : (p + q) . i <> 0. R } = min* { i where i is Nat : q . i <> 0. R }
proof end;

theorem lemlowp1a2: :: REALALG1:10
for R being non degenerated Ring
for p, q being non zero Polynomial of R st p + q <> 0_. R & min* { i where i is Nat : p . i <> 0. R } = min* { i where i is Nat : q . i <> 0. R } holds
min* { i where i is Nat : (p + q) . i <> 0. R } >= min* { i where i is Nat : p . i <> 0. R }
proof end;

theorem lemlowp1b: :: REALALG1:11
for R being non degenerated Ring
for p, q being non zero Polynomial of R st (p . (min* { i where i is Nat : p . i <> 0. R } )) + (q . (min* { i where i is Nat : q . i <> 0. R } )) <> 0. R holds
min* { i where i is Nat : (p + q) . i <> 0. R } = min ((min* { i where i is Nat : p . i <> 0. R } ),(min* { i where i is Nat : q . i <> 0. R } ))
proof end;

theorem lemlowp3a: :: REALALG1:12
for R being non degenerated Ring
for p, q being non zero Polynomial of R st p *' q <> 0_. R holds
min* { i where i is Nat : (p *' q) . i <> 0. R } >= (min* { i where i is Nat : p . i <> 0. R } ) + (min* { i where i is Nat : q . i <> 0. R } )
proof end;

theorem lemlowp3b: :: REALALG1:13
for R being domRing
for p, q being non zero Polynomial of R holds min* { i where i is Nat : (p *' q) . i <> 0. R } = (min* { i where i is Nat : p . i <> 0. R } ) + (min* { i where i is Nat : q . i <> 0. R } )
proof end;

definition
let L be non empty multLoopStr ;
let S be Subset of L;
attr S is mult-closed means :: REALALG1:def 5
for s1, s2 being Element of L st s1 in S & s2 in S holds
s1 * s2 in S;
end;

:: deftheorem defines mult-closed REALALG1:def 5 :
for L being non empty multLoopStr
for S being Subset of L holds
( S is mult-closed iff for s1, s2 being Element of L st s1 in S & s2 in S holds
s1 * s2 in S );

definition
let L be non empty addLoopStr ;
let S be Subset of L;
func - S -> Subset of L equals :: REALALG1:def 6
{ (- s) where s is Element of L : s in S } ;
coherence
{ (- s) where s is Element of L : s in S } is Subset of L
proof end;
end;

:: deftheorem defines - REALALG1:def 6 :
for L being non empty addLoopStr
for S being Subset of L holds - S = { (- s) where s is Element of L : s in S } ;

registration
let L be non empty right_complementable add-associative right_zeroed addLoopStr ;
let S be Subset of L;
reduce - (- S) to S;
reducibility
- (- S) = S
proof end;
end;

theorem :: REALALG1:14
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for S being Subset of L
for a being Element of L holds
( a in S iff - a in - S )
proof end;

theorem min1: :: REALALG1:15
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for S1, S2 being Subset of L holds - (S1 /\ S2) = (- S1) /\ (- S2)
proof end;

theorem :: REALALG1:16
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for S1, S2 being Subset of L holds - (S1 \/ S2) = (- S1) \/ (- S2)
proof end;

definition
let L be non empty addLoopStr ;
let S be Subset of L;
attr S is negative-disjoint means :defneg: :: REALALG1:def 7
S /\ (- S) = {(0. L)};
end;

:: deftheorem defneg defines negative-disjoint REALALG1:def 7 :
for L being non empty addLoopStr
for S being Subset of L holds
( S is negative-disjoint iff S /\ (- S) = {(0. L)} );

definition
let L be non empty addLoopStr ;
let S be Subset of L;
attr S is spanning means :defsp: :: REALALG1:def 8
S \/ (- S) = the carrier of L;
end;

:: deftheorem defsp defines spanning REALALG1:def 8 :
for L being non empty addLoopStr
for S being Subset of L holds
( S is spanning iff S \/ (- S) = the carrier of L );

notation
let R be Ring;
let a be Element of R;
synonym square a for being_a_square ;
end;

registration
let R be Ring;
cluster 0. R -> square ;
coherence
0. R is square
proof end;
cluster 1. R -> square ;
coherence
1. R is square
proof end;
end;

registration
let R be Ring;
cluster square for Element of the carrier of R;
existence
ex b1 being Element of R st b1 is square
proof end;
end;

definition
let R be Ring;
let a be Element of R;
attr a is sum_of_squares means :: REALALG1:def 9
ex f being FinSequence of R st
( Sum f = a & ( for i being Nat st i in dom f holds
ex a being Element of R st f . i = a ^2 ) );
end;

:: deftheorem defines sum_of_squares REALALG1:def 9 :
for R being Ring
for a being Element of R holds
( a is sum_of_squares iff ex f being FinSequence of R st
( Sum f = a & ( for i being Nat st i in dom f holds
ex a being Element of R st f . i = a ^2 ) ) );

AS0: for R being Ring
for a being Element of R st a is square holds
a is sum_of_squares

proof end;

registration
let R be Ring;
cluster square -> sum_of_squares for Element of the carrier of R;
coherence
for b1 being Element of R st b1 is square holds
b1 is sum_of_squares
by AS0;
end;

S1: for R being Ring
for a, b being Element of R st a is sum_of_squares & b is sum_of_squares holds
a + b is sum_of_squares

proof end;

S2: for R being commutative Ring
for a, b being Element of R st a is square & b is sum_of_squares holds
a * b is sum_of_squares

proof end;

SM1: for R being commutative Ring
for a, b being Element of R st a is square & b is square holds
a * b is square

proof end;

S3: for R being commutative Ring
for a, b being Element of R st a is sum_of_squares & b is sum_of_squares holds
a * b is sum_of_squares

proof end;

registration
let R be commutative Ring;
let a, b be square Element of R;
cluster a * b -> square ;
coherence
a * b is square
by SM1;
end;

registration
let R be Ring;
let a, b be sum_of_squares Element of R;
cluster a + b -> sum_of_squares ;
coherence
a + b is sum_of_squares
by S1;
end;

registration
let R be commutative Ring;
let a, b be sum_of_squares Element of R;
cluster a * b -> sum_of_squares ;
coherence
a * b is sum_of_squares
by S3;
end;

definition
let R be Ring;
func Squares_of R -> Subset of R equals :: REALALG1:def 10
{ a where a is Element of R : a is square } ;
coherence
{ a where a is Element of R : a is square } is Subset of R
proof end;
func Quadratic_Sums_of R -> Subset of R equals :: REALALG1:def 11
{ a where a is Element of R : a is sum_of_squares } ;
coherence
{ a where a is Element of R : a is sum_of_squares } is Subset of R
proof end;
end;

:: deftheorem defines Squares_of REALALG1:def 10 :
for R being Ring holds Squares_of R = { a where a is Element of R : a is square } ;

:: deftheorem defines Quadratic_Sums_of REALALG1:def 11 :
for R being Ring holds Quadratic_Sums_of R = { a where a is Element of R : a is sum_of_squares } ;

notation
let R be Ring;
synonym SQ R for Squares_of R;
synonym QS R for Quadratic_Sums_of R;
end;

SQ0: for R being Ring holds 0. R in SQ R
;

QS0: for R being Ring holds 0. R in QS R
;

registration
let R be Ring;
cluster Squares_of R -> non empty ;
coherence
not SQ R is empty
by SQ0;
cluster Quadratic_Sums_of R -> non empty ;
coherence
not QS R is empty
by QS0;
end;

definition
let R be Ring;
let S be Subset of R;
attr S is with_squares means :: REALALG1:def 12
SQ R c= S;
attr S is with_sums_of_squares means :: REALALG1:def 13
QS R c= S;
end;

:: deftheorem defines with_squares REALALG1:def 12 :
for R being Ring
for S being Subset of R holds
( S is with_squares iff SQ R c= S );

:: deftheorem defines with_sums_of_squares REALALG1:def 13 :
for R being Ring
for S being Subset of R holds
( S is with_sums_of_squares iff QS R c= S );

registration
let R be Ring;
cluster with_squares for Element of bool the carrier of R;
existence
ex b1 being Subset of R st b1 is with_squares
proof end;
cluster with_sums_of_squares for Element of bool the carrier of R;
existence
ex b1 being Subset of R st b1 is with_sums_of_squares
proof end;
end;

registration
let R be Ring;
cluster with_squares -> non empty for Element of bool the carrier of R;
coherence
for b1 being Subset of R st b1 is with_squares holds
not b1 is empty
;
cluster with_sums_of_squares -> non empty for Element of bool the carrier of R;
coherence
for b1 being Subset of R st b1 is with_sums_of_squares holds
not b1 is empty
;
end;

registration
let R be Ring;
cluster with_sums_of_squares -> with_squares for Element of bool the carrier of R;
coherence
for b1 being Subset of R st b1 is with_sums_of_squares holds
b1 is with_squares
proof end;
cluster add-closed with_squares -> with_sums_of_squares for Element of bool the carrier of R;
coherence
for b1 being Subset of R st b1 is with_squares & b1 is add-closed holds
b1 is with_sums_of_squares
proof end;
end;

registration
let R be Ring;
cluster Squares_of R -> with_squares ;
coherence
SQ R is with_squares
;
cluster Quadratic_Sums_of R -> with_sums_of_squares ;
coherence
QS R is with_sums_of_squares
;
end;

theorem :: REALALG1:17
for R being Ring holds
( 0. R in SQ R & 1. R in SQ R ) ;

theorem :: REALALG1:18
for R being Ring holds SQ R c= QS R
proof end;

registration
let R be Ring;
cluster Quadratic_Sums_of R -> add-closed ;
coherence
QS R is add-closed
proof end;
end;

registration
let R be commutative Ring;
cluster Quadratic_Sums_of R -> mult-closed ;
coherence
QS R is mult-closed
proof end;
end;

lemminus: for R being Ring
for S being Subring of R
for a being Element of R
for b being Element of S st a = b holds
- a = - b

proof end;

lemminus1: for R being Ring
for S being Subring of R
for S1 being Subset of R
for S2 being Subset of S st S1 = S2 holds
- S1 = - S2

proof end;

lemsum: for R being Ring
for S being Subring of R
for f being FinSequence of R
for g being FinSequence of S st f = g holds
Sum f = Sum g

proof end;

theorem SQsub: :: REALALG1:19
for R being Ring
for S being Subring of R holds SQ S c= SQ R
proof end;

theorem :: REALALG1:20
for R being Ring
for S being Subring of R holds QS S c= QS R
proof end;

definition
let R be Ring;
let S be Subset of R;
attr S is prepositive_cone means :defppc: :: REALALG1:def 14
( S + S c= S & S * S c= S & S /\ (- S) = {(0. R)} & SQ R c= S );
attr S is positive_cone means :defpc: :: REALALG1:def 15
( S + S c= S & S * S c= S & S /\ (- S) = {(0. R)} & S \/ (- S) = the carrier of R );
end;

:: deftheorem defppc defines prepositive_cone REALALG1:def 14 :
for R being Ring
for S being Subset of R holds
( S is prepositive_cone iff ( S + S c= S & S * S c= S & S /\ (- S) = {(0. R)} & SQ R c= S ) );

:: deftheorem defpc defines positive_cone REALALG1:def 15 :
for R being Ring
for S being Subset of R holds
( S is positive_cone iff ( S + S c= S & S * S c= S & S /\ (- S) = {(0. R)} & S \/ (- S) = the carrier of R ) );

registration
let R be Ring;
cluster prepositive_cone -> non empty for Element of bool the carrier of R;
coherence
for b1 being Subset of R st b1 is prepositive_cone holds
not b1 is empty
;
cluster positive_cone -> non empty for Element of bool the carrier of R;
coherence
for b1 being Subset of R st b1 is positive_cone holds
not b1 is empty
;
end;

registration
let R be Ring;
cluster prepositive_cone -> add-closed mult-closed negative-disjoint with_squares for Element of bool the carrier of R;
coherence
for b1 being Subset of R st b1 is prepositive_cone holds
( b1 is add-closed & b1 is mult-closed & b1 is negative-disjoint & b1 is with_squares )
proof end;
cluster add-closed mult-closed negative-disjoint with_squares -> prepositive_cone for Element of bool the carrier of R;
coherence
for b1 being Subset of R st b1 is add-closed & b1 is mult-closed & b1 is negative-disjoint & b1 is with_squares holds
b1 is prepositive_cone
proof end;
end;

registration
let R be Ring;
cluster positive_cone -> add-closed mult-closed negative-disjoint spanning for Element of bool the carrier of R;
coherence
for b1 being Subset of R st b1 is positive_cone holds
( b1 is add-closed & b1 is mult-closed & b1 is negative-disjoint & b1 is spanning )
proof end;
cluster add-closed mult-closed negative-disjoint spanning -> positive_cone for Element of bool the carrier of R;
coherence
for b1 being Subset of R st b1 is add-closed & b1 is mult-closed & b1 is negative-disjoint & b1 is spanning holds
b1 is positive_cone
proof end;
end;

registration
let R be Ring;
cluster positive_cone -> prepositive_cone for Element of bool the carrier of R;
coherence
for b1 being Subset of R st b1 is positive_cone holds
b1 is prepositive_cone
proof end;
end;

theorem X1: :: REALALG1:21
for F being Field
for S being Subset of F st S * S c= S & SQ F c= S holds
( S /\ (- S) = {(0. F)} iff not - (1. F) in S )
proof end;

theorem :: REALALG1:22
for F being Field
for S being Subset of F st S * S c= S & S \/ (- S) = the carrier of F holds
( S /\ (- S) = {(0. F)} iff not - (1. F) in S )
proof end;

definition
let R be Ring;
attr R is preordered means :defpord: :: REALALG1:def 16
ex P being Subset of R st P is prepositive_cone ;
attr R is ordered means :deford: :: REALALG1:def 17
ex P being Subset of R st P is positive_cone ;
end;

:: deftheorem defpord defines preordered REALALG1:def 16 :
for R being Ring holds
( R is preordered iff ex P being Subset of R st P is prepositive_cone );

:: deftheorem deford defines ordered REALALG1:def 17 :
for R being Ring holds
( R is ordered iff ex P being Subset of R st P is positive_cone );

lemEX: for S being Subset of F_Real st S = { x where x is Element of REAL : 0 <= x } holds
S is positive_cone

proof end;

EX: F_Real is ordered
proof end;

registration
cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable left_complementable right_complementable almost_left_cancelable almost_right_cancelable almost_left_invertible unital associative commutative Abelian add-associative right_zeroed V116() right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like V189() V190() V191() V192() Euclidian V295( INT.Ring ) preordered for doubleLoopStr ;
existence
ex b1 being Field st b1 is preordered
proof end;
cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable left_complementable right_complementable almost_left_cancelable almost_right_cancelable almost_left_invertible unital associative commutative Abelian add-associative right_zeroed V116() right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like V189() V190() V191() V192() Euclidian V295( INT.Ring ) ordered for doubleLoopStr ;
existence
ex b1 being Field st b1 is ordered
by EX;
end;

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

registration
let R be preordered Ring;
cluster prepositive_cone for Element of bool the carrier of R;
existence
ex b1 being Subset of R st b1 is prepositive_cone
by defpord;
end;

registration
let R be ordered Ring;
cluster positive_cone for Element of bool the carrier of R;
existence
ex b1 being Subset of R st b1 is positive_cone
by deford;
end;

definition
let R be preordered Ring;
mode Preordering of R is prepositive_cone Subset of R;
end;

definition
let R be ordered Ring;
mode Ordering of R is positive_cone Subset of R;
end;

theorem ord1: :: REALALG1:23
for R being preordered Ring
for P being Preordering of R
for a being Element of R holds a ^2 in P
proof end;

theorem ord2: :: REALALG1:24
for R being preordered Ring
for P being Preordering of R holds QS R c= P
proof end;

theorem ord3: :: REALALG1:25
for R being preordered Ring
for P being Preordering of R holds
( 0. R in P & 1. R in P )
proof end;

theorem ord4: :: REALALG1:26
for R being non degenerated preordered Ring
for P being Preordering of R holds not - (1. R) in P
proof end;

theorem ord5: :: REALALG1:27
for F being preordered Field
for P being Preordering of F
for a being non zero Element of F st a in P holds
a " in P
proof end;

theorem tchar: :: REALALG1:28
for R being non degenerated preordered Ring holds Char R = 0
proof end;

theorem ordsub: :: REALALG1:29
for R being ordered Ring
for O, P being Ordering of R st O c= P holds
O = P
proof end;

definition
let R be preordered Ring;
let P be Preordering of R;
let a, b be Element of R;
pred a <= P,b means :: REALALG1:def 18
b - a in P;
end;

:: deftheorem defines <= REALALG1:def 18 :
for R being preordered Ring
for P being Preordering of R
for a, b being Element of R holds
( a <= P,b iff b - a in P );

definition
let R be preordered Ring;
let P be Preordering of R;
func OrdRel P -> Relation of R equals :: REALALG1:def 19
{ [a,b] where a, b is Element of R : a <= P,b } ;
coherence
{ [a,b] where a, b is Element of R : a <= P,b } is Relation of R
proof end;
end;

:: deftheorem defines OrdRel REALALG1:def 19 :
for R being preordered Ring
for P being Preordering of R holds OrdRel P = { [a,b] where a, b is Element of R : a <= P,b } ;

registration
let R be preordered Ring;
let P be Preordering of R;
cluster OrdRel P -> non empty ;
coherence
not OrdRel P is empty
proof end;
end;

registration
let R be preordered Ring;
let P be Preordering of R;
cluster OrdRel P -> antisymmetric transitive strongly_reflexive ;
coherence
( OrdRel P is strongly_reflexive & OrdRel P is antisymmetric & OrdRel P is transitive )
proof end;
end;

registration
let R be preordered Ring;
let P be Preordering of R;
cluster OrdRel P -> respecting_addition respecting_multiplication ;
coherence
( OrdRel P is respecting_addition & OrdRel P is respecting_multiplication )
proof end;
end;

registration
let R be ordered Ring;
let O be Ordering of R;
cluster OrdRel O -> totally_connected ;
coherence
OrdRel O is totally_connected
proof end;
end;

registration
let R be preordered Ring;
cluster Relation-like the carrier of R -defined the carrier of R -valued antisymmetric transitive strongly_reflexive respecting_addition respecting_multiplication for Element of bool [: the carrier of R, the carrier of R:];
existence
ex b1 being Relation of R st
( b1 is strongly_reflexive & b1 is antisymmetric & b1 is transitive & b1 is respecting_addition & b1 is respecting_multiplication )
proof end;
end;

registration
let R be ordered Ring;
cluster Relation-like the carrier of R -defined the carrier of R -valued antisymmetric transitive strongly_reflexive totally_connected respecting_addition respecting_multiplication for Element of bool [: the carrier of R, the carrier of R:];
existence
ex b1 being Relation of R st
( b1 is strongly_reflexive & b1 is antisymmetric & b1 is transitive & b1 is respecting_addition & b1 is respecting_multiplication & b1 is totally_connected )
proof end;
end;

definition
let R be preordered Ring;
mode OrderRelation of R is antisymmetric transitive strongly_reflexive respecting_addition respecting_multiplication Relation of R;
end;

definition
let R be ordered Ring;
mode total_OrderRelation of R is antisymmetric transitive strongly_reflexive totally_connected respecting_addition respecting_multiplication Relation of R;
end;

definition
let R be Ring;
let Q be Relation of R;
func Positives Q -> Subset of R equals :: REALALG1:def 20
{ a where a is Element of R : 0. R <=_ Q,a } ;
coherence
{ a where a is Element of R : 0. R <=_ Q,a } is Subset of R
proof end;
end;

:: deftheorem defines Positives REALALG1:def 20 :
for R being Ring
for Q being Relation of R holds Positives Q = { a where a is Element of R : 0. R <=_ Q,a } ;

registration
let R be preordered Ring;
let Q be strongly_reflexive Relation of R;
cluster Positives Q -> non empty ;
coherence
not Positives Q is empty
proof end;
end;

registration
let R be preordered Ring;
let Q be OrderRelation of R;
cluster Positives Q -> add-closed mult-closed negative-disjoint ;
coherence
( Positives Q is add-closed & Positives Q is mult-closed & Positives Q is negative-disjoint )
proof end;
end;

registration
let R be ordered Ring;
let Q be total_OrderRelation of R;
cluster Positives Q -> spanning ;
coherence
Positives Q is spanning
proof end;
end;

theorem :: REALALG1:30
for R being preordered Ring
for P being Preordering of R holds OrdRel P is OrderRelation of R ;

theorem :: REALALG1:31
for R being ordered Ring
for P being Ordering of R holds OrdRel P is total_OrderRelation of R ;

theorem :: REALALG1:32
for R being ordered Ring
for Q being total_OrderRelation of R holds Positives Q is Ordering of R ;

lemsubpreord: for R being preordered Ring
for P being Preordering of R
for S being Subring of R
for Q being Subset of S st Q = P /\ the carrier of S holds
Q is prepositive_cone

proof end;

lemsubord: for R being ordered Ring
for O being Ordering of R
for S being Subring of R
for Q being Subset of S st Q = O /\ the carrier of S holds
Q is positive_cone

proof end;

registration
let R be preordered Ring;
cluster -> preordered for Subring of R;
coherence
for b1 being Subring of R holds b1 is preordered
proof end;
end;

registration
let R be ordered Ring;
cluster -> ordered for Subring of R;
coherence
for b1 being Subring of R holds b1 is ordered
proof end;
end;

theorem :: REALALG1:33
for R being preordered Ring
for P being Preordering of R
for S being Subring of R holds P /\ the carrier of S is Preordering of S
proof end;

theorem :: REALALG1:34
for R being ordered Ring
for O being Ordering of R
for S being Subring of R holds O /\ the carrier of S is Ordering of S
proof end;

registration
cluster F_Complex -> non preordered ;
coherence
not F_Complex is preordered
proof end;
end;

registration
let n be non trivial Nat;
cluster INT.Ring n -> non preordered ;
coherence
not Z/ n is preordered
proof end;
end;

definition
func Positives(F_Real) -> Subset of F_Real equals :: REALALG1:def 21
{ r where r is Element of REAL : 0 <= r } ;
coherence
{ r where r is Element of REAL : 0 <= r } is Subset of F_Real
proof end;
end;

:: deftheorem defines Positives(F_Real) REALALG1:def 21 :
Positives(F_Real) = { r where r is Element of REAL : 0 <= r } ;

registration
cluster Positives(F_Real) -> add-closed mult-closed negative-disjoint spanning ;
coherence
( Positives(F_Real) is add-closed & Positives(F_Real) is mult-closed & Positives(F_Real) is negative-disjoint & Positives(F_Real) is spanning )
proof end;
end;

registration
cluster F_Real -> ordered ;
coherence
F_Real is ordered
proof end;
end;

theorem :: REALALG1:35
Positives(F_Real) is Ordering of F_Real ;

theorem :: REALALG1:36
for O being Ordering of F_Real holds O = Positives(F_Real)
proof end;

definition
func Positives(F_Rat) -> Subset of F_Rat equals :: REALALG1:def 22
{ r where r is Element of RAT : 0 <= r } ;
coherence
{ r where r is Element of RAT : 0 <= r } is Subset of F_Rat
proof end;
end;

:: deftheorem defines Positives(F_Rat) REALALG1:def 22 :
Positives(F_Rat) = { r where r is Element of RAT : 0 <= r } ;

registration
cluster Positives(F_Rat) -> add-closed mult-closed negative-disjoint spanning ;
coherence
( Positives(F_Rat) is add-closed & Positives(F_Rat) is mult-closed & Positives(F_Rat) is negative-disjoint & Positives(F_Rat) is spanning )
proof end;
end;

registration
cluster F_Rat -> ordered ;
coherence
F_Rat is ordered
proof end;
end;

theorem :: REALALG1:37
Positives(F_Rat) is Ordering of F_Rat ;

theorem :: REALALG1:38
for O being Ordering of F_Rat holds O = Positives(F_Rat)
proof end;

definition
func Positives(INT.Ring) -> Subset of INT.Ring equals :: REALALG1:def 23
{ i where i is Element of INT : 0 <= i } ;
coherence
{ i where i is Element of INT : 0 <= i } is Subset of INT.Ring
proof end;
end;

:: deftheorem defines Positives(INT.Ring) REALALG1:def 23 :
Positives(INT.Ring) = { i where i is Element of INT : 0 <= i } ;

registration
cluster Positives(INT.Ring) -> add-closed mult-closed negative-disjoint spanning ;
coherence
( Positives(INT.Ring) is add-closed & Positives(INT.Ring) is mult-closed & Positives(INT.Ring) is negative-disjoint & Positives(INT.Ring) is spanning )
proof end;
end;

registration
cluster INT.Ring -> ordered ;
coherence
INT.Ring is ordered
proof end;
end;

theorem :: REALALG1:39
Positives(INT.Ring) is Ordering of INT.Ring ;

theorem :: REALALG1:40
for O being Ordering of INT.Ring holds O = Positives(INT.Ring)
proof end;

definition
let R be preordered Ring;
let P be Preordering of R;
func Positives(Poly) P -> Subset of (Polynom-Ring R) equals :: REALALG1:def 24
{ p where p is Polynomial of R : LC p in P } ;
coherence
{ p where p is Polynomial of R : LC p in P } is Subset of (Polynom-Ring R)
proof end;
end;

:: deftheorem defines Positives(Poly) REALALG1:def 24 :
for R being preordered Ring
for P being Preordering of R holds Positives(Poly) P = { p where p is Polynomial of R : LC p in P } ;

lemminuspoly: for R being Ring
for a being Element of (Polynom-Ring R)
for b being Polynomial of R st a = b holds
- a = - b

proof end;

registration
let R be non degenerated preordered Ring;
let P be Preordering of R;
cluster Positives(Poly) P -> add-closed negative-disjoint ;
coherence
( Positives(Poly) P is add-closed & Positives(Poly) P is negative-disjoint )
proof end;
end;

registration
let R be preordered domRing;
let P be Preordering of R;
cluster Positives(Poly) P -> mult-closed with_sums_of_squares ;
coherence
( Positives(Poly) P is mult-closed & Positives(Poly) P is with_sums_of_squares )
proof end;
end;

registration
let R be ordered Ring;
let O be Ordering of R;
cluster Positives(Poly) O -> spanning ;
coherence
Positives(Poly) O is spanning
proof end;
end;

registration
let R be preordered domRing;
cluster Polynom-Ring R -> preordered ;
coherence
Polynom-Ring R is preordered
proof end;
end;

registration
let R be ordered domRing;
cluster Polynom-Ring R -> ordered ;
coherence
Polynom-Ring R is ordered
proof end;
end;

theorem :: REALALG1:41
for R being preordered domRing
for P being Preordering of R holds Positives(Poly) P is Preordering of (Polynom-Ring R) ;

theorem :: REALALG1:42
for R being ordered domRing
for O being Ordering of R holds Positives(Poly) O is Ordering of (Polynom-Ring R) ;

definition
let R be preordered Ring;
let P be Preordering of R;
func LowPositives(Poly) P -> Subset of (Polynom-Ring R) equals :: REALALG1:def 25
{ p where p is Polynomial of R : p . (min* { i where i is Nat : p . i <> 0. R } ) in P } ;
coherence
{ p where p is Polynomial of R : p . (min* { i where i is Nat : p . i <> 0. R } ) in P } is Subset of (Polynom-Ring R)
proof end;
end;

:: deftheorem defines LowPositives(Poly) REALALG1:def 25 :
for R being preordered Ring
for P being Preordering of R holds LowPositives(Poly) P = { p where p is Polynomial of R : p . (min* { i where i is Nat : p . i <> 0. R } ) in P } ;

lemlowp1: for R being non degenerated preordered Ring
for P being Preordering of R
for p, q being non zero Polynomial of R st p . (min* { i where i is Nat : p . i <> 0. R } ) in P & q . (min* { i where i is Nat : q . i <> 0. R } ) in P holds
(p + q) . (min* { i where i is Nat : (p + q) . i <> 0. R } ) in P

proof end;

lemlowp3: for R being domRing
for p, q being non zero Polynomial of R holds (p *' q) . (min* { i where i is Nat : (p *' q) . i <> 0. R } ) = (p . (min* { i where i is Nat : p . i <> 0. R } )) * (q . (min* { i where i is Nat : q . i <> 0. R } ))

proof end;

registration
let R be non degenerated preordered Ring;
let P be Preordering of R;
cluster LowPositives(Poly) P -> add-closed negative-disjoint ;
coherence
( LowPositives(Poly) P is add-closed & LowPositives(Poly) P is negative-disjoint )
proof end;
end;

registration
let R be preordered domRing;
let P be Preordering of R;
cluster LowPositives(Poly) P -> mult-closed with_sums_of_squares ;
coherence
( LowPositives(Poly) P is mult-closed & LowPositives(Poly) P is with_sums_of_squares )
proof end;
end;

registration
let R be non degenerated ordered Ring;
let O be Ordering of R;
cluster LowPositives(Poly) O -> spanning ;
coherence
LowPositives(Poly) O is spanning
proof end;
end;

theorem :: REALALG1:43
for R being preordered domRing
for P being Preordering of R holds LowPositives(Poly) P is Preordering of (Polynom-Ring R) ;

theorem :: REALALG1:44
for R being ordered domRing
for O being Ordering of R holds LowPositives(Poly) O is Ordering of (Polynom-Ring R) ;

theorem :: REALALG1:45
for R being non degenerated preordered Ring
for P being Preordering of R holds Positives(Poly) P <> LowPositives(Poly) P
proof end;