:: 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 b₁ being Relation of X st b₁ is strongly_reflexive

proof end;

cluster Relation-like X -defined X -valued totally_connected for Element of bool [:X,X:];

existence
ex b₁ being Relation of X st b₁ is totally_connected

proof end;

end;

registration

let X be set ;

cluster strongly_reflexive -> reflexive for Element of bool [:X,X:];

coherence
for b₁ being Relation of X st b₁ is strongly_reflexive holds
b₁ is reflexive

proof end;

cluster totally_connected -> strongly_connected for Element of bool [:X,X:];

coherence
for b₁ being Relation of X st b₁ is totally_connected holds
b₁ 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 b₁ being Relation of X st b₁ is strongly_reflexive holds
not b₁ is empty

proof end;

cluster totally_connected -> non empty for Element of bool [:X,X:];

coherence
for b₁ being Relation of X st b₁ is totally_connected holds
not b₁ 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 b₁ being Element of R st b₁ 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 b₁ being Element of R st b₁ is square holds
b₁ 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 b₁ being Subset of R st b₁ is with_squares

proof end;

cluster with_sums_of_squares for Element of bool the carrier of R;

existence
ex b₁ being Subset of R st b₁ 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 b₁ being Subset of R st b₁ is with_squares holds
not b₁ is empty ;

cluster with_sums_of_squares -> non empty for Element of bool the carrier of R;

coherence
for b₁ being Subset of R st b₁ is with_sums_of_squares holds
not b₁ 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 b₁ being Subset of R st b₁ is with_sums_of_squares holds
b₁ is with_squares

proof end;

cluster add-closed with_squares -> with_sums_of_squares for Element of bool the carrier of R;

coherence
for b₁ being Subset of R st b₁ is with_squares & b₁ is add-closed holds
b₁ 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 b₁ being Subset of R st b₁ is prepositive_cone holds
not b₁ is empty ;

cluster positive_cone -> non empty for Element of bool the carrier of R;

coherence
for b₁ being Subset of R st b₁ is positive_cone holds
not b₁ 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 b₁ being Subset of R st b₁ is prepositive_cone holds
( b₁ is add-closed & b₁ is mult-closed & b₁ is negative-disjoint & b₁ 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 b₁ being Subset of R st b₁ is add-closed & b₁ is mult-closed & b₁ is negative-disjoint & b₁ is with_squares holds
b₁ 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 b₁ being Subset of R st b₁ is positive_cone holds
( b₁ is add-closed & b₁ is mult-closed & b₁ is negative-disjoint & b₁ is spanning )

proof end;

cluster add-closed mult-closed negative-disjoint spanning -> positive_cone for Element of bool the carrier of R;

coherence
for b₁ being Subset of R st b₁ is add-closed & b₁ is mult-closed & b₁ is negative-disjoint & b₁ is spanning holds
b₁ 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 b₁ being Subset of R st b₁ is positive_cone holds
b₁ 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 b₁ being Field st b₁ 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 b₁ being Field st b₁ 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 b₁ being Ring st b₁ is ordered holds
b₁ is preordered ;

end;

registration

let R be preordered Ring;

cluster prepositive_cone for Element of bool the carrier of R;

existence
ex b₁ being Subset of R st b₁ 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 b₁ being Subset of R st b₁ 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 b₁ being Relation of R st
( b₁ is strongly_reflexive & b₁ is antisymmetric & b₁ is transitive & b₁ is respecting_addition & b₁ 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 b₁ being Relation of R st
( b₁ is strongly_reflexive & b₁ is antisymmetric & b₁ is transitive & b₁ is respecting_addition & b₁ is respecting_multiplication & b₁ 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 b₁ being Subring of R holds b₁ is preordered

proof end;

end;

registration

let R be ordered Ring;

cluster -> ordered for Subring of R;

coherence
for b₁ being Subring of R holds b₁ 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;