:: by Christoph Schwarzweller

::

:: Received March 17, 2017

:: Copyright (c) 2017-2019 Association of Mizar Users

:: 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 );

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 );

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 ;

existence

ex b_{1} being Relation of X st b_{1} is strongly_reflexive

ex b_{1} being Relation of X st b_{1} is totally_connected

end;
existence

ex b

proof end;

existence ex b

proof end;

registration

let X be set ;

coherence

for b_{1} being Relation of X st b_{1} is strongly_reflexive holds

b_{1} is reflexive

for b_{1} being Relation of X st b_{1} is totally_connected holds

b_{1} is strongly_connected

end;
coherence

for b

b

proof end;

coherence for b

b

proof end;

registration

let X be non empty set ;

coherence

for b_{1} being Relation of X st b_{1} is strongly_reflexive holds

not b_{1} is empty

for b_{1} being Relation of X st b_{1} is totally_connected holds

not b_{1} is empty

end;
coherence

for b

not b

proof end;

coherence for b

not b

proof 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;

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

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

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;

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;

end;
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;

for a, b, c being Element of L st a <=_ R,b holds

a + c <=_ R,b + c;

:: 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 );

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;

end;
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;

for a, b, c being Element of L st a <=_ R,b & 0. L <=_ R,c holds

a * c <=_ R,b * c;

:: 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 );

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 } = {}

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 } = {} )

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 }

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 }

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 }

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 }

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 } ))

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 } )

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 } )

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;

end;
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;

for s1, s2 being Element of L st s1 in S & s2 in S holds

s1 * s2 in S;

:: 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 );

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;

coherence

{ (- s) where s is Element of L : s in S } is Subset of L

end;
let S be Subset of L;

coherence

{ (- s) where s is Element of L : s in S } is Subset of L

proof 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 } ;

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;

reducibility

- (- S) = S

end;
let S be Subset of L;

reducibility

- (- S) = S

proof 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 )

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)

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)

for S1, S2 being Subset of L holds - (S1 \/ S2) = (- S1) \/ (- S2)

proof 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)} );

for L being non empty addLoopStr

for S being Subset of L holds

( S is negative-disjoint iff S /\ (- S) = {(0. L)} );

:: 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 );

for L being non empty addLoopStr

for S being Subset of L holds

( S is spanning iff S \/ (- S) = the carrier of L );

registration
end;

registration

let R be Ring;

ex b_{1} being Element of R st b_{1} is square

end;
cluster left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable square for Element of the carrier of R;

existence ex b

proof end;

definition

let R be Ring;

let a be Element of R;

end;
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 ) );

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 ) );

:: 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 ) ) );

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;

coherence

for b_{1} being Element of R st b_{1} is square holds

b_{1} is sum_of_squares
by AS0;

end;
coherence

for b

b

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
end;

registration
end;

registration

let R be commutative Ring;

let a, b be sum_of_squares Element of R;

coherence

a * b is sum_of_squares by S3;

end;
let a, b be sum_of_squares Element of R;

coherence

a * b is sum_of_squares by S3;

definition

let R be Ring;

{ a where a is Element of R : a is square } is Subset of R

{ a where a is Element of R : a is sum_of_squares } is Subset of R

end;
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 } ;

{ 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 } ;

{ a where a is Element of R : a is sum_of_squares } is Subset of R

proof 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 } ;

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 } ;

for R being Ring holds Quadratic_Sums_of R = { a where a is Element of R : a is sum_of_squares } ;

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

;

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

;

registration
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 );

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 );

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;

existence

ex b_{1} being Subset of R st b_{1} is with_squares

ex b_{1} being Subset of R st b_{1} is with_sums_of_squares

end;
existence

ex b

proof end;

existence ex b

proof end;

registration

let R be Ring;

coherence

for b_{1} being Subset of R st b_{1} is with_squares holds

not b_{1} is empty
;

coherence

for b_{1} being Subset of R st b_{1} is with_sums_of_squares holds

not b_{1} is empty
;

end;
coherence

for b

not b

coherence

for b

not b

registration

let R be Ring;

coherence

for b_{1} being Subset of R st b_{1} is with_sums_of_squares holds

b_{1} is with_squares

for b_{1} being Subset of R st b_{1} is with_squares & b_{1} is add-closed holds

b_{1} is with_sums_of_squares

end;
coherence

for b

b

proof end;

coherence for b

b

proof end;

registration
end;

registration
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;

definition

let R be Ring;

let S be Subset of R;

end;
let S be Subset of R;

:: 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 ) );

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 ) );

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;

coherence

for b_{1} being Subset of R st b_{1} is prepositive_cone holds

not b_{1} is empty
;

coherence

for b_{1} being Subset of R st b_{1} is positive_cone holds

not b_{1} is empty
;

end;
coherence

for b

not b

coherence

for b

not b

registration

let R be Ring;

for b_{1} being Subset of R st b_{1} is prepositive_cone holds

( b_{1} is add-closed & b_{1} is mult-closed & b_{1} is negative-disjoint & b_{1} is with_squares )

for b_{1} being Subset of R st b_{1} is add-closed & b_{1} is mult-closed & b_{1} is negative-disjoint & b_{1} is with_squares holds

b_{1} is prepositive_cone

end;
cluster prepositive_cone -> add-closed mult-closed negative-disjoint with_squares for Element of bool the carrier of R;

coherence for b

( b

proof end;

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

coherence for b

b

proof end;

registration

let R be Ring;

for b_{1} being Subset of R st b_{1} is positive_cone holds

( b_{1} is add-closed & b_{1} is mult-closed & b_{1} is negative-disjoint & b_{1} is spanning )

for b_{1} being Subset of R st b_{1} is add-closed & b_{1} is mult-closed & b_{1} is negative-disjoint & b_{1} is spanning holds

b_{1} is positive_cone

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

coherence for b

( b

proof end;

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

coherence for b

b

proof end;

registration

let R be Ring;

coherence

for b_{1} being Subset of R st b_{1} is positive_cone holds

b_{1} is prepositive_cone

end;
coherence

for b

b

proof 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 )

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 )

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;

end;
attr R is preordered means :defpord: :: REALALG1:def 16

ex P being Subset of R st P is prepositive_cone ;

ex P being Subset of R st P is prepositive_cone ;

:: 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 );

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 );

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

ex b_{1} being Field st b_{1} is preordered

ex b_{1} being Field st b_{1} is ordered
by EX;

end;

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_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

proof end;

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_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

registration

for b_{1} being Ring st b_{1} is ordered holds

b_{1} is preordered
;

end;

cluster non empty right_complementable associative Abelian add-associative right_zeroed well-unital distributive ordered -> preordered for doubleLoopStr ;

coherence for b

b

registration

let R be preordered Ring;

existence

ex b_{1} being Subset of R st b_{1} is prepositive_cone
by defpord;

end;
existence

ex b

registration
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

for P being Preordering of F

for a being non zero Element of F st a in P holds

a " in P

proof 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 );

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;

{ [a,b] where a, b is Element of R : a <= P,b } is Relation of R

end;
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 } ;

{ [a,b] where a, b is Element of R : a <= P,b } is Relation of R

proof 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 } ;

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
end;

registration

let R be preordered Ring;

let P be Preordering of R;

coherence

( OrdRel P is strongly_reflexive & OrdRel P is antisymmetric & OrdRel P is transitive )

end;
let P be Preordering of R;

coherence

( OrdRel P is strongly_reflexive & OrdRel P is antisymmetric & OrdRel P is transitive )

proof end;

registration

let R be preordered Ring;

let P be Preordering of R;

coherence

( OrdRel P is respecting_addition & OrdRel P is respecting_multiplication )

end;
let P be Preordering of R;

coherence

( OrdRel P is respecting_addition & OrdRel P is respecting_multiplication )

proof end;

registration
end;

registration

let R be preordered Ring;

ex b_{1} being Relation of R st

( b_{1} is strongly_reflexive & b_{1} is antisymmetric & b_{1} is transitive & b_{1} is respecting_addition & b_{1} is respecting_multiplication )

end;
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

( b

proof end;

registration

let R be ordered Ring;

ex b_{1} being Relation of R st

( b_{1} is strongly_reflexive & b_{1} is antisymmetric & b_{1} is transitive & b_{1} is respecting_addition & b_{1} is respecting_multiplication & b_{1} is totally_connected )

end;
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

( b

proof end;

definition

let R be preordered Ring;

mode OrderRelation of R is antisymmetric transitive strongly_reflexive respecting_addition respecting_multiplication Relation of R;

end;
mode OrderRelation of R is antisymmetric transitive strongly_reflexive respecting_addition respecting_multiplication Relation of R;

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;
mode total_OrderRelation of R is antisymmetric transitive strongly_reflexive totally_connected respecting_addition respecting_multiplication Relation of R;

definition

let R be Ring;

let Q be Relation of R;

{ a where a is Element of R : 0. R <=_ Q,a } is Subset of R

end;
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 } ;

{ a where a is Element of R : 0. R <=_ Q,a } is Subset of R

proof 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 } ;

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;

coherence

not Positives Q is empty

end;
let Q be strongly_reflexive Relation of R;

coherence

not Positives Q is empty

proof end;

registration

let R be preordered Ring;

let Q be OrderRelation of R;

coherence

( Positives Q is add-closed & Positives Q is mult-closed & Positives Q is negative-disjoint )

end;
let Q be OrderRelation of R;

coherence

( Positives Q is add-closed & Positives Q is mult-closed & Positives Q is negative-disjoint )

proof end;

registration

let R be ordered Ring;

let Q be total_OrderRelation of R;

coherence

Positives Q is spanning

end;
let Q be total_OrderRelation of R;

coherence

Positives Q is spanning

proof end;

theorem :: REALALG1:30

theorem :: REALALG1:31

theorem :: REALALG1:32

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;

coherence

for b_{1} being Subring of R holds b_{1} is preordered

end;
coherence

for b

proof end;

registration
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

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

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
end;

definition

{ r where r is Element of REAL : 0 <= r } is Subset of F_Real
end;

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 } ;

{ r where r is Element of REAL : 0 <= r } is Subset of F_Real

proof end;

:: deftheorem defines Positives(F_Real) REALALG1:def 21 :

Positives(F_Real) = { r where r is Element of REAL : 0 <= r } ;

Positives(F_Real) = { r where r is Element of REAL : 0 <= r } ;

registration

coherence

( Positives(F_Real) is add-closed & Positives(F_Real) is mult-closed & Positives(F_Real) is negative-disjoint & Positives(F_Real) is spanning )

end;
( 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;

definition

{ r where r is Element of RAT : 0 <= r } is Subset of F_Rat
end;

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 } ;

{ r where r is Element of RAT : 0 <= r } is Subset of F_Rat

proof end;

:: deftheorem defines Positives(F_Rat) REALALG1:def 22 :

Positives(F_Rat) = { r where r is Element of RAT : 0 <= r } ;

Positives(F_Rat) = { r where r is Element of RAT : 0 <= r } ;

registration

coherence

( Positives(F_Rat) is add-closed & Positives(F_Rat) is mult-closed & Positives(F_Rat) is negative-disjoint & Positives(F_Rat) is spanning )

end;
( 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;

definition

{ i where i is Element of INT : 0 <= i } is Subset of INT.Ring
end;

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 } ;

{ i where i is Element of INT : 0 <= i } is Subset of INT.Ring

proof end;

:: deftheorem defines Positives(INT.Ring) REALALG1:def 23 :

Positives(INT.Ring) = { i where i is Element of INT : 0 <= i } ;

Positives(INT.Ring) = { i where i is Element of INT : 0 <= i } ;

registration

coherence

( Positives(INT.Ring) is add-closed & Positives(INT.Ring) is mult-closed & Positives(INT.Ring) is negative-disjoint & Positives(INT.Ring) is spanning )

end;
( 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;

definition

let R be preordered Ring;

let P be Preordering of R;

{ p where p is Polynomial of R : LC p in P } is Subset of (Polynom-Ring R)

end;
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 } ;

{ p where p is Polynomial of R : LC p in P } is Subset of (Polynom-Ring R)

proof 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 } ;

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;

coherence

( Positives(Poly) P is add-closed & Positives(Poly) P is negative-disjoint )

end;
let P be Preordering of R;

coherence

( Positives(Poly) P is add-closed & Positives(Poly) P is negative-disjoint )

proof end;

registration

let R be preordered domRing;

let P be Preordering of R;

coherence

( Positives(Poly) P is mult-closed & Positives(Poly) P is with_sums_of_squares )

end;
let P be Preordering of R;

coherence

( Positives(Poly) P is mult-closed & Positives(Poly) P is with_sums_of_squares )

proof end;

registration
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) ;

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) ;

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;

{ 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)

end;
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 } ;

{ 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;

:: 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 } ;

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;

coherence

( LowPositives(Poly) P is add-closed & LowPositives(Poly) P is negative-disjoint )

end;
let P be Preordering of R;

coherence

( LowPositives(Poly) P is add-closed & LowPositives(Poly) P is negative-disjoint )

proof end;

registration

let R be preordered domRing;

let P be Preordering of R;

coherence

( LowPositives(Poly) P is mult-closed & LowPositives(Poly) P is with_sums_of_squares )

end;
let P be Preordering of R;

coherence

( LowPositives(Poly) P is mult-closed & LowPositives(Poly) P is with_sums_of_squares )

proof end;

registration

let R be non degenerated ordered Ring;

let O be Ordering of R;

coherence

LowPositives(Poly) O is spanning

end;
let O be Ordering of R;

coherence

LowPositives(Poly) O is spanning

proof 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) ;

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) ;

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

for P being Preordering of R holds Positives(Poly) P <> LowPositives(Poly) P

proof end;