:: by Christoph Schwarzweller

::

:: Received November 29, 2017

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

registration

let X, Y be non empty set ;

existence

ex b_{1} being Function st

( not b_{1} is empty & b_{1} is X -defined & b_{1} is Y -valued )

end;
existence

ex b

( not b

proof end;

theorem P0: :: REALALG2:1

for L being non empty right_zeroed addLoopStr

for S, T being Subset of L st 0. L in T holds

S c= S + T

for S, T being Subset of L st 0. L in T holds

S c= S + T

proof end;

theorem :: REALALG2:2

for L being non empty right_unital multLoopStr

for S, T being Subset of L st 1. L in T holds

S c= S * T

for S, T being Subset of L st 1. L in T holds

S c= S * T

proof end;

theorem P1: :: REALALG2:3

for L being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr

for S being Subset of L st 0. L in S holds

for a being Element of L holds S c= S + (a * S)

for S being Subset of L st 0. L in S holds

for a being Element of L holds S c= S + (a * S)

proof end;

theorem P2: :: REALALG2:4

for L being non empty right_complementable add-associative right_zeroed right-distributive right_unital doubleLoopStr

for S being Subset of L st 0. L in S & 1. L in S holds

for a being Element of L holds a in S + (a * S)

for S being Subset of L st 0. L in S & 1. L in S holds

for a being Element of L holds a in S + (a * S)

proof end;

theorem c1: :: REALALG2:5

for R being non empty right_complementable Abelian add-associative right_zeroed left-distributive doubleLoopStr

for a, b being Element of R

for i being Integer holds i '*' (a * b) = (i '*' a) * b

for a, b being Element of R

for i being Integer holds i '*' (a * b) = (i '*' a) * b

proof end;

theorem c1a: :: REALALG2:6

for R being non empty right_complementable Abelian add-associative right_zeroed left-distributive doubleLoopStr

for a being Element of R

for i being Integer holds i '*' (- a) = - (i '*' a)

for a being Element of R

for i being Integer holds i '*' (- a) = - (i '*' a)

proof end;

registration

let R be Ring;

let a be Element of R;

coherence

a ^2 is square ;

coherence

a |^ 2 is square

end;
let a be Element of R;

coherence

a ^2 is square ;

coherence

a |^ 2 is square

proof end;

theorem P3: :: REALALG2:7

for R being commutative Ring

for a, b being Element of R holds (a + b) ^2 = ((a ^2) + ((2 '*' a) * b)) + (b ^2)

for a, b being Element of R holds (a + b) ^2 = ((a ^2) + ((2 '*' a) * b)) + (b ^2)

proof end;

theorem P4: :: REALALG2:8

for R being commutative Ring

for a, b being Element of R holds (a - b) ^2 = ((a ^2) - ((2 '*' a) * b)) + (b ^2)

for a, b being Element of R holds (a - b) ^2 = ((a ^2) - ((2 '*' a) * b)) + (b ^2)

proof end;

P5b: for R being non degenerated Ring holds

( Char R = 2 iff 2 '*' (1. R) = 0. R )

proof end;

theorem P5a: :: REALALG2:14

for F being Field

for a being Element of F

for b being non zero Element of F holds (a / b) ^2 = (a ^2) / (b ^2)

for a being Element of F

for b being non zero Element of F holds (a / b) ^2 = (a ^2) / (b ^2)

proof end;

theorem P5: :: REALALG2:15

for F being Field st Char F <> 2 holds

for a being Element of F holds (((a + (1. F)) / (2 '*' (1. F))) ^2) - (((a - (1. F)) / (2 '*' (1. F))) ^2) = a

for a being Element of F holds (((a + (1. F)) / (2 '*' (1. F))) ^2) - (((a - (1. F)) / (2 '*' (1. F))) ^2) = a

proof end;

registration

for b_{1} being non degenerated Ring st b_{1} is preordered holds

b_{1} is 0 -characteristic
by REALALG1:28;

end;

cluster non empty non degenerated right_complementable associative Abelian add-associative right_zeroed well-unital V144() preordered -> non degenerated 0 -characteristic for doubleLoopStr ;

coherence for b

b

theorem v1: :: REALALG2:17

for R being preordered Ring

for P being Preordering of R holds

( (- P) + (- P) c= - P & (- P) * (- P) c= P )

for P being Preordering of R holds

( (- P) + (- P) c= - P & (- P) * (- P) c= P )

proof end;

theorem v2: :: REALALG2:18

for R being preordered Ring

for P being Preordering of R holds

( (- P) * P c= - P & P * (- P) c= - P )

for P being Preordering of R holds

( (- P) * P c= - P & P * (- P) c= - P )

proof end;

Lm8: for i being Integer holds i '*' (1. INT.Ring) = i

proof end;

Lm9: for i being Integer holds i '*' (1. F_Rat) = i

proof end;

registration

coherence

for b_{1} being Preordering of INT.Ring holds b_{1} is spanning

for b_{1} being Preordering of F_Rat holds b_{1} is spanning

for b_{1} being Preordering of F_Real holds b_{1} is spanning

end;
for b

proof end;

coherence for b

proof end;

coherence for b

proof end;

theorem :: REALALG2:20

theorem :: REALALG2:22

theorem :: REALALG2:24

theorem char4: :: REALALG2:25

for R being domRing holds

( Char R = 0 iff for a being non zero Element of R

for n being non zero Nat holds n '*' a <> 0. R )

( Char R = 0 iff for a being non zero Element of R

for n being non zero Nat holds n '*' a <> 0. R )

proof end;

definition

let R be preordered Ring;

let P be Preordering of R;

end;
let P be Preordering of R;

attr P is maximal means :defmax: :: REALALG2:def 1

for Q being Preordering of R st P c= Q holds

P = Q;

for Q being Preordering of R st P c= Q holds

P = Q;

:: deftheorem defmax defines maximal REALALG2:def 1 :

for R being preordered Ring

for P being Preordering of R holds

( P is maximal iff for Q being Preordering of R st P c= Q holds

P = Q );

for R being preordered Ring

for P being Preordering of R holds

( P is maximal iff for Q being Preordering of R st P c= Q holds

P = Q );

theorem T2: :: REALALG2:27

for F being preordered Field

for P being Preordering of F

for a being Element of F st not - a in P holds

P + (a * P) is Preordering of F

for P being Preordering of F

for a being Element of F st not - a in P holds

P + (a * P) is Preordering of F

proof end;

theorem T1: :: REALALG2:28

for F being preordered Field

for P being Preordering of F holds

( P is maximal iff P is positive_cone )

for P being Preordering of F holds

( P is maximal iff P is positive_cone )

proof end;

registration

let F be preordered Field;

coherence

for b_{1} being Preordering of F st b_{1} is spanning holds

b_{1} is maximal
by T1;

coherence

for b_{1} being Preordering of F st b_{1} is maximal holds

b_{1} is spanning

end;
coherence

for b

b

coherence

for b

b

proof end;

theorem T3: :: REALALG2:29

for F being preordered Field

for P being Preordering of F ex Q being Preordering of F st

( P c= Q & Q is maximal )

for P being Preordering of F ex Q being Preordering of F st

( P c= Q & Q is maximal )

proof end;

registration

for b_{1} being preordered Field holds b_{1} is ordered
end;

cluster non empty non degenerated right_complementable almost_left_invertible associative commutative Abelian add-associative right_zeroed well-unital V144() preordered -> preordered ordered for doubleLoopStr ;

coherence for b

proof end;

theorem :: REALALG2:30

for F being preordered Field

for P being Preordering of F holds

( P is maximal iff P is Ordering of F ) ;

for P being Preordering of F holds

( P is maximal iff P is Ordering of F ) ;

definition

let R be ordered Ring;

let P be Preordering of R;

{ x where x is Element of R : for O being Ordering of R st P c= O holds

x in O } is Subset of R

end;
let P be Preordering of R;

func /\ (P,R) -> Subset of R equals :: REALALG2:def 2

{ x where x is Element of R : for O being Ordering of R st P c= O holds

x in O } ;

coherence { x where x is Element of R : for O being Ordering of R st P c= O holds

x in O } ;

{ x where x is Element of R : for O being Ordering of R st P c= O holds

x in O } is Subset of R

proof end;

:: deftheorem defines /\ REALALG2:def 2 :

for R being ordered Ring

for P being Preordering of R holds /\ (P,R) = { x where x is Element of R : for O being Ordering of R st P c= O holds

x in O } ;

for R being ordered Ring

for P being Preordering of R holds /\ (P,R) = { x where x is Element of R : for O being Ordering of R st P c= O holds

x in O } ;

registration
end;

registration

let R be ordered Ring;

let P be Preordering of R;

coherence

( /\ (P,R) is add-closed & /\ (P,R) is mult-closed & /\ (P,R) is with_squares )

end;
let P be Preordering of R;

coherence

( /\ (P,R) is add-closed & /\ (P,R) is mult-closed & /\ (P,R) is with_squares )

proof end;

s1: for F being preordered Field

for P being Preordering of F holds /\ (P,F) = P

proof end;

registration
end;

theorem :: REALALG2:32

theorem :: REALALG2:33

definition
end;

:: deftheorem defines formally_real REALALG2:def 3 :

for R being Ring holds

( R is formally_real iff not - (1. R) in QS R );

for R being Ring holds

( R is formally_real iff not - (1. R) in QS R );

lemma1: for F being Field st F is formally_real holds

(QS F) /\ (- (QS F)) = {(0. F)}

proof end;

lemma2: for R being non degenerated preordered Ring holds QS R <> the carrier of R

proof end;

lemma3: for R being Field st Char R <> 2 & QS R <> the carrier of R holds

not - (1. R) in QS R

proof end;

theorem :: REALALG2:35

for F being Field st Char F <> 2 holds

( F is formally_real iff ex P being Subset of F st P is prepositive_cone )

( F is formally_real iff ex P being Subset of F st P is prepositive_cone )

proof end;

theorem T2: :: REALALG2:36

for F being Field st Char F <> 2 holds

( F is formally_real iff ex P being Subset of F st P is positive_cone )

( F is formally_real iff ex P being Subset of F st P is positive_cone )

proof end;

theorem :: REALALG2:37

registration

for b_{1} being Field st b_{1} is formally_real holds

b_{1} is ordered

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

b_{1} is formally_real
end;

cluster non empty non degenerated right_complementable almost_left_invertible associative commutative Abelian add-associative right_zeroed well-unital V144() formally_real -> ordered for doubleLoopStr ;

coherence for b

b

proof end;

cluster non empty non degenerated right_complementable almost_left_invertible associative commutative Abelian add-associative right_zeroed well-unital V144() ordered -> formally_real for doubleLoopStr ;

coherence for b

b

proof end;

registration

for b_{1} being non degenerated Ring st b_{1} is preordered holds

b_{1} is formally_real
end;

cluster non empty non degenerated right_complementable associative Abelian add-associative right_zeroed well-unital V144() preordered -> non degenerated formally_real for doubleLoopStr ;

coherence for b

b

proof end;

registration

ex b_{1} being Field st b_{1} is formally_real
end;

cluster non empty non degenerated non trivial left_complementable right_complementable complementable almost_left_invertible unital associative commutative Abelian add-associative right_zeroed V139() right-distributive left-distributive right_unital well-unital V144() left_unital domRing-like Euclidian formally_real for doubleLoopStr ;

existence ex b

proof end;

theorem :: REALALG2:39

for F being formally_real Field

for a being Element of F holds

( ( for O being Ordering of F holds a in O ) iff a in QS F )

for a being Element of F holds

( ( for O being Ordering of F holds a in O ) iff a in QS F )

proof end;

:: deftheorem defines trivial REALALG2:def 4 :

for R being ZeroStr

for f being the carrier of b_{1} -valued Function holds

( f is trivial iff for i being object st i in dom f holds

f . i = 0. R );

for R being ZeroStr

for f being the carrier of b

( f is trivial iff for i being object st i in dom f holds

f . i = 0. R );

:: deftheorem dq defines quadratic REALALG2:def 5 :

for R being Ring

for f being non empty FinSequence of R holds

( f is quadratic iff for i being Element of dom f holds f . i is square );

for R being Ring

for f being non empty FinSequence of R holds

( f is quadratic iff for i being Element of dom f holds f . i is square );

registration

let R be non degenerated Ring;

coherence

for b_{1} being non empty FinSequence of R st b_{1} = <*(1. R)*> holds

( b_{1} is quadratic & not b_{1} is trivial )

end;
coherence

for b

( b

proof end;

registration

let R be non degenerated Ring;

ex b_{1} being non empty FinSequence of R st

( b_{1} is quadratic & not b_{1} is trivial )

end;
cluster Relation-like NAT -defined the carrier of R -valued Function-like non empty V34() FinSequence-like FinSubsequence-like non trivial quadratic for FinSequence of the carrier of R;

existence ex b

( b

proof end;

theorem :: REALALG2:41

for F being Field holds

( F is formally_real iff for f being non empty quadratic FinSequence of F st Sum f = 0. F holds

f is trivial )

( F is formally_real iff for f being non empty quadratic FinSequence of F st Sum f = 0. F holds

f is trivial )

proof end;

registration

for b_{1} being formally_real Field holds not b_{1} is algebraic-closed
end;

cluster non empty non degenerated right_complementable almost_left_invertible associative commutative Abelian add-associative right_zeroed well-unital V144() formally_real -> non algebraic-closed formally_real for doubleLoopStr ;

coherence for b

proof end;

lemOP: for R being preordered Ring

for P being Preordering of R

for a, b being Element of R holds

( a <= P,b iff a <=_ OrdRel P,b )

proof end;

theorem c10a: :: REALALG2:42

for R being preordered Ring

for P being Preordering of R

for a, b being Element of R holds

( a <= P,b iff - b <= P, - a )

for P being Preordering of R

for a, b being Element of R holds

( a <= P,b iff - b <= P, - a )

proof end;

theorem c2: :: REALALG2:44

for R being preordered Ring

for P being Preordering of R

for a, b being Element of R st a <= P,b & b <= P,a holds

a = b

for P being Preordering of R

for a, b being Element of R st a <= P,b & b <= P,a holds

a = b

proof end;

theorem c3: :: REALALG2:45

for R being preordered Ring

for P being Preordering of R

for a, b, c being Element of R st a <= P,b & b <= P,c holds

a <= P,c

for P being Preordering of R

for a, b, c being Element of R st a <= P,b & b <= P,c holds

a <= P,c

proof end;

theorem c4: :: REALALG2:46

for R being preordered Ring

for P being Preordering of R

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

a + c <= P,b + c

for P being Preordering of R

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

a + c <= P,b + c

proof end;

theorem c5: :: REALALG2:47

for R being preordered Ring

for P being Preordering of R

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

a * c <= P,b * c

for P being Preordering of R

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

a * c <= P,b * c

proof end;

theorem c55: :: REALALG2:48

for R being preordered Ring

for P being Preordering of R

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

b * c <= P,a * c

for P being Preordering of R

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

b * c <= P,a * c

proof end;

theorem avb4: :: REALALG2:49

for R being ordered Ring

for O being Ordering of R

for a, b being Element of R holds

( a <= O,b or b <= O,a )

for O being Ordering of R

for a, b being Element of R holds

( a <= O,b or b <= O,a )

proof end;

theorem fi1: :: REALALG2:50

for F being preordered Field

for P being Preordering of F

for a, b being non zero Element of F st 0. F <= P,a & 0. F <= P,b holds

( a <= P,b iff b " <= P,a " )

for P being Preordering of F

for a, b being non zero Element of F st 0. F <= P,a & 0. F <= P,b holds

( a <= P,b iff b " <= P,a " )

proof end;

theorem fi2: :: REALALG2:51

for F being preordered Field

for P being Preordering of F

for a, b being non zero Element of F st a <= P, 0. F & b <= P, 0. F holds

( a <= P,b iff b " <= P,a " )

for P being Preordering of F

for a, b being non zero Element of F st a <= P, 0. F & b <= P, 0. F holds

( a <= P,b iff b " <= P,a " )

proof end;

:: deftheorem defines < REALALG2:def 6 :

for R being preordered Ring

for P being Preordering of R

for a, b being Element of R holds

( a < P,b iff ( a <= P,b & a <> b ) );

for R being preordered Ring

for P being Preordering of R

for a, b being Element of R holds

( a < P,b iff ( a <= P,b & a <> b ) );

theorem c20: :: REALALG2:52

for R being non degenerated preordered Ring

for P being Preordering of R holds

( 0. R < P, 1. R & - (1. R) < P, 0. R )

for P being Preordering of R holds

( 0. R < P, 1. R & - (1. R) < P, 0. R )

proof end;

theorem c10: :: REALALG2:53

for R being preordered Ring

for P being Preordering of R

for a, b being Element of R holds

( a < P,b iff - b < P, - a ) by c10a, RLVECT_1:18;

for P being Preordering of R

for a, b being Element of R holds

( a < P,b iff - b < P, - a ) by c10a, RLVECT_1:18;

theorem :: REALALG2:54

theorem avb5: :: REALALG2:55

for R being preordered Ring

for P being Preordering of R

for a, b, c being Element of R st a < P,b & b <= P,c holds

a < P,c by c2, c3;

for P being Preordering of R

for a, b, c being Element of R st a < P,b & b <= P,c holds

a < P,c by c2, c3;

theorem avb6: :: REALALG2:56

for R being preordered Ring

for P being Preordering of R

for a, b, c being Element of R st a <= P,b & b < P,c holds

a < P,c by c2, c3;

for P being Preordering of R

for a, b, c being Element of R st a <= P,b & b < P,c holds

a < P,c by c2, c3;

theorem :: REALALG2:57

for R being preordered Ring

for P being Preordering of R

for a, b, c being Element of R st a < P,b holds

a + c < P,b + c by c4, RLVECT_1:8;

for P being Preordering of R

for a, b, c being Element of R st a < P,b holds

a + c < P,b + c by c4, RLVECT_1:8;

theorem :: REALALG2:58

theorem :: REALALG2:59

for R being preordered domRing

for P being Preordering of R

for a, b, c being Element of R st a < P,b & c < P, 0. R holds

b * c < P,a * c

for P being Preordering of R

for a, b, c being Element of R st a < P,b & c < P, 0. R holds

b * c < P,a * c

proof end;

theorem :: REALALG2:60

for F being preordered Field

for P being Preordering of F

for a, b being non zero Element of F st 0. F <= P,a & 0. F <= P,b holds

( a < P,b iff b " < P,a " )

for P being Preordering of F

for a, b being non zero Element of F st 0. F <= P,a & 0. F <= P,b holds

( a < P,b iff b " < P,a " )

proof end;

theorem :: REALALG2:61

for F being preordered Field

for P being Preordering of F

for a, b being non zero Element of F st a <= P, 0. F & b <= P, 0. F holds

( a < P,b iff b " < P,a " )

for P being Preordering of F

for a, b being non zero Element of F st a <= P, 0. F & b <= P, 0. F holds

( a < P,b iff b " < P,a " )

proof end;

:: deftheorem defppp defines -ordered REALALG2:def 7 :

for R being preordered Ring

for P being Preordering of R

for a being Element of R holds

( a is P -ordered iff a in P \/ (- P) );

for R being preordered Ring

for P being Preordering of R

for a being Element of R holds

( a is P -ordered iff a in P \/ (- P) );

:: deftheorem defines -positive REALALG2:def 8 :

for R being preordered Ring

for P being Preordering of R

for a being Element of R holds

( a is P -positive iff a in P \ {(0. R)} );

for R being preordered Ring

for P being Preordering of R

for a being Element of R holds

( a is P -positive iff a in P \ {(0. R)} );

:: deftheorem defn defines -negative REALALG2:def 9 :

for R being preordered Ring

for P being Preordering of R

for a being Element of R holds

( a is P -negative iff a in (- P) \ {(0. R)} );

for R being preordered Ring

for P being Preordering of R

for a being Element of R holds

( a is P -negative iff a in (- P) \ {(0. R)} );

registration

let R be preordered Ring;

let P be Preordering of R;

ex b_{1} being Element of R st b_{1} is P -ordered

end;
let P be Preordering of R;

cluster left_complementable right_complementable complementable P -ordered for Element of the carrier of R;

existence ex b

proof end;

registration

let R be preordered Ring;

let P be Preordering of R;

coherence

for b_{1} being Element of R st b_{1} is P -positive holds

b_{1} is P -ordered

for b_{1} being Element of R st b_{1} is P -negative holds

b_{1} is P -ordered

end;
let P be Preordering of R;

coherence

for b

b

proof end;

coherence for b

b

proof end;

registration

let R be non degenerated preordered Ring;

let P be Preordering of R;

ex b_{1} being Element of R st b_{1} is P -positive

ex b_{1} being Element of R st b_{1} is P -negative

not for b_{1} being Element of R holds b_{1} is P -positive

not for b_{1} being Element of R holds b_{1} is P -negative

end;
let P be Preordering of R;

cluster left_complementable right_complementable complementable P -positive for Element of the carrier of R;

existence ex b

proof end;

cluster left_complementable right_complementable complementable P -negative for Element of the carrier of R;

existence ex b

proof end;

cluster left_complementable right_complementable complementable non P -positive for Element of the carrier of R;

existence not for b

proof end;

cluster left_complementable right_complementable complementable non P -negative for Element of the carrier of R;

existence not for b

proof end;

x1: for R being preordered Ring

for P being Preordering of R

for a being Element of R holds

( a is P -positive iff 0. R < P,a )

proof end;

x2: for R being preordered Ring

for P being Preordering of R

for a being Element of R holds

( a is P -negative iff a < P, 0. R )

proof end;

registration

let R be non degenerated preordered Ring;

let P be Preordering of R;

coherence

for b_{1} being Element of R st b_{1} is P -positive holds

( not b_{1} is zero & not b_{1} is P -negative )

for b_{1} being Element of R st b_{1} is P -negative holds

( not b_{1} is zero & not b_{1} is P -positive )

end;
let P be Preordering of R;

coherence

for b

( not b

proof end;

coherence for b

( not b

proof end;

registration

let R be non degenerated preordered Ring;

let P be Preordering of R;

let a be P -ordered Element of R;

coherence

- a is P -ordered

end;
let P be Preordering of R;

let a be P -ordered Element of R;

coherence

- a is P -ordered

proof end;

lemsqf: for F being preordered Field

for P being Preordering of F

for a being non zero Element of F holds

( a in P \/ (- P) iff a " in P \/ (- P) )

proof end;

registration
end;

registration

let F be preordered Field;

let P be Preordering of F;

let a be non zero P -ordered Element of F;

coherence

a " is P -ordered by defppp, lemsqf;

end;
let P be Preordering of F;

let a be non zero P -ordered Element of F;

coherence

a " is P -ordered by defppp, lemsqf;

registration

let R be non degenerated ordered Ring;

let O be Ordering of R;

coherence

for b_{1} being Element of R st not b_{1} is zero & not b_{1} is O -positive holds

b_{1} is O -negative

for b_{1} being Element of R st not b_{1} is zero & not b_{1} is O -negative holds

b_{1} is O -positive
;

end;
let O be Ordering of R;

coherence

for b

b

proof end;

coherence for b

b

theorem :: REALALG2:62

for R being preordered Ring

for P being Preordering of R

for a being Element of R holds

( a is P -positive iff 0. R < P,a ) by x1;

for P being Preordering of R

for a being Element of R holds

( a is P -positive iff 0. R < P,a ) by x1;

theorem :: REALALG2:63

for R being preordered Ring

for P being Preordering of R

for a being Element of R holds

( a is P -negative iff a < P, 0. R ) by x2;

for P being Preordering of R

for a being Element of R holds

( a is P -negative iff a < P, 0. R ) by x2;

theorem x1a: :: REALALG2:64

for R being preordered Ring

for P being Preordering of R

for a being b_{2} -ordered Element of R holds

( not a is P -negative iff 0. R <= P,a )

for P being Preordering of R

for a being b

( not a is P -negative iff 0. R <= P,a )

proof end;

theorem :: REALALG2:65

for R being preordered Ring

for P being Preordering of R

for a being b_{2} -ordered Element of R holds

( not a is P -positive iff a <= P, 0. R )

for P being Preordering of R

for a being b

( not a is P -positive iff a <= P, 0. R )

proof end;

definition

let R be preordered Ring;

let P be Preordering of R;

let a be Element of R;

( ( a in P implies a is Element of R ) & ( a in - P implies - a is Element of R ) & ( not a in P & not a in - P implies - (1. R) is Element of R ) ) ;

consistency

for b_{1} being Element of R st a in P & a in - P holds

( b_{1} = a iff b_{1} = - a )

end;
let P be Preordering of R;

let a be Element of R;

func absolute_value (P,a) -> Element of R equals :defa: :: REALALG2:def 10

a if a in P

- a if a in - P

otherwise - (1. R);

coherence a if a in P

- a if a in - P

otherwise - (1. R);

( ( a in P implies a is Element of R ) & ( a in - P implies - a is Element of R ) & ( not a in P & not a in - P implies - (1. R) is Element of R ) ) ;

consistency

for b

( b

proof end;

:: deftheorem defa defines absolute_value REALALG2:def 10 :

for R being preordered Ring

for P being Preordering of R

for a being Element of R holds

( ( a in P implies absolute_value (P,a) = a ) & ( a in - P implies absolute_value (P,a) = - a ) & ( not a in P & not a in - P implies absolute_value (P,a) = - (1. R) ) );

for R being preordered Ring

for P being Preordering of R

for a being Element of R holds

( ( a in P implies absolute_value (P,a) = a ) & ( a in - P implies absolute_value (P,a) = - a ) & ( not a in P & not a in - P implies absolute_value (P,a) = - (1. R) ) );

definition

let R be ordered Ring;

let O be Ordering of R;

let a be Element of R;

absolute_value (O,a) is Element of R ;

consistency

for b_{1} being Element of R holds verum
;

compatibility

for b_{1} being Element of R holds

( ( a in O implies ( b_{1} = absolute_value (O,a) iff b_{1} = a ) ) & ( not a in O implies ( b_{1} = absolute_value (O,a) iff b_{1} = - a ) ) )

end;
let O be Ordering of R;

let a be Element of R;

:: original: absolute_value

redefine func absolute_value (O,a) -> Element of R equals :: REALALG2:def 11

a if a in O

otherwise - a;

coherence redefine func absolute_value (O,a) -> Element of R equals :: REALALG2:def 11

a if a in O

otherwise - a;

absolute_value (O,a) is Element of R ;

consistency

for b

compatibility

for b

( ( a in O implies ( b

proof end;

:: deftheorem defines absolute_value REALALG2:def 11 :

for R being ordered Ring

for O being Ordering of R

for a being Element of R holds

( ( a in O implies absolute_value (O,a) = a ) & ( not a in O implies absolute_value (O,a) = - a ) );

for R being ordered Ring

for O being Ordering of R

for a being Element of R holds

( ( a in O implies absolute_value (O,a) = a ) & ( not a in O implies absolute_value (O,a) = - a ) );

notation

let R be preordered Ring;

let P be Preordering of R;

let a be Element of R;

synonym abs (P,a) for absolute_value (P,a);

end;
let P be Preordering of R;

let a be Element of R;

synonym abs (P,a) for absolute_value (P,a);

theorem av0: :: REALALG2:66

for R being non degenerated preordered Ring

for P being Preordering of R

for a being Element of R holds

( 0. R <= P, abs (P,a) iff a is P -ordered )

for P being Preordering of R

for a being Element of R holds

( 0. R <= P, abs (P,a) iff a is P -ordered )

proof end;

theorem av00: :: REALALG2:67

for R being non degenerated preordered Ring

for P being Preordering of R

for a being Element of R holds

( not a is P -ordered iff abs (P,a) = - (1. R) )

for P being Preordering of R

for a being Element of R holds

( not a is P -ordered iff abs (P,a) = - (1. R) )

proof end;

theorem :: REALALG2:68

for R being non degenerated preordered Ring

for P being Preordering of R

for a being Element of R holds

( abs (P,a) = 0. R iff a = 0. R )

for P being Preordering of R

for a being Element of R holds

( abs (P,a) = 0. R iff a = 0. R )

proof end;

theorem av2: :: REALALG2:69

for R being preordered domRing

for P being Preordering of R

for a being Element of R holds

( abs (P,a) = a iff 0. R <= P,a )

for P being Preordering of R

for a being Element of R holds

( abs (P,a) = a iff 0. R <= P,a )

proof end;

theorem av3: :: REALALG2:70

for R being preordered domRing

for P being Preordering of R

for a being Element of R holds

( abs (P,a) = - a iff a <= P, 0. R )

for P being Preordering of R

for a being Element of R holds

( abs (P,a) = - a iff a <= P, 0. R )

proof end;

theorem :: REALALG2:71

for R being preordered Ring

for P being Preordering of R

for a being Element of R holds abs (P,a) = abs (P,(- a))

for P being Preordering of R

for a being Element of R holds abs (P,a) = abs (P,(- a))

proof end;

theorem :: REALALG2:72

for R being non degenerated preordered Ring

for P being Preordering of R

for a being Element of R holds

( ( - (abs (P,a)) <= P,a & a <= P, abs (P,a) ) iff a is P -ordered )

for P being Preordering of R

for a being Element of R holds

( ( - (abs (P,a)) <= P,a & a <= P, abs (P,a) ) iff a is P -ordered )

proof end;

theorem sq2: :: REALALG2:73

for F being preordered Field

for P being Preordering of F

for a being non zero b_{2} -ordered Element of F holds abs (P,(a ")) = (abs (P,a)) "

for P being Preordering of F

for a being non zero b

proof end;

theorem :: REALALG2:74

for R being preordered Ring

for P being Preordering of R

for a, b being Element of R holds abs (P,(a - b)) = abs (P,(b - a))

for P being Preordering of R

for a, b being Element of R holds abs (P,(a - b)) = abs (P,(b - a))

proof end;

theorem ineq2: :: REALALG2:75

for R being non degenerated preordered Ring

for P being Preordering of R

for a being Element of R holds

( ( - (abs (P,a)) <= P,a & a <= P, abs (P,a) ) iff a is P -ordered )

for P being Preordering of R

for a being Element of R holds

( ( - (abs (P,a)) <= P,a & a <= P, abs (P,a) ) iff a is P -ordered )

proof end;

theorem abs10: :: REALALG2:76

for R being non degenerated preordered Ring

for P being Preordering of R

for a, b being b_{2} -ordered Element of R holds abs (P,(a * b)) = (abs (P,a)) * (abs (P,b))

for P being Preordering of R

for a, b being b

proof end;

theorem :: REALALG2:77

for F being preordered Field

for P being Preordering of F

for a being non zero b_{2} -ordered Element of F

for b being b_{2} -ordered Element of F holds abs (P,(b * (a "))) = (abs (P,b)) * ((abs (P,a)) ")

for P being Preordering of F

for a being non zero b

for b being b

proof end;

theorem ineq1: :: REALALG2:78

for R being preordered domRing

for P being Preordering of R

for a being b_{2} -ordered Element of R

for p being b_{2} -ordered non b_{2} -negative Element of R holds

( abs (P,a) <= P,p iff ( - p <= P,a & a <= P,p ) )

for P being Preordering of R

for a being b

for p being b

( abs (P,a) <= P,p iff ( - p <= P,a & a <= P,p ) )

proof end;

theorem :: REALALG2:79

for R being preordered domRing

for P being Preordering of R

for a, b being b_{2} -ordered Element of R holds abs (P,(a + b)) <= P,(abs (P,a)) + (abs (P,b))

for P being Preordering of R

for a, b being b

proof end;

definition

let R be Ring;

let a be square Element of R;

existence

ex b_{1} being Element of R st b_{1} ^2 = a
by O_RING_1:def 2;

end;
let a be square Element of R;

existence

ex b

:: deftheorem defsqrt defines SquareRoot REALALG2:def 12 :

for R being Ring

for a being square Element of R

for b_{3} being Element of R holds

( b_{3} is SquareRoot of a iff b_{3} ^2 = a );

for R being Ring

for a being square Element of R

for b

( b

registration

let R be non degenerated Ring;

ex b_{1} being Element of R st

( not b_{1} is zero & b_{1} is square )

end;
cluster non zero left_complementable right_complementable complementable square for Element of the carrier of R;

existence ex b

( not b

proof end;

theorem sq1: :: REALALG2:80

for R being ordered domRing

for O being Ordering of R

for a, b being non b_{2} -negative Element of R holds

( a <= O,b iff a ^2 <= O,b ^2 )

for O being Ordering of R

for a, b being non b

( a <= O,b iff a ^2 <= O,b ^2 )

proof end;

sq0: for R being preordered domRing

for P being Preordering of R

for a being square Element of R

for b1, b2 being Sqrt of a st 0. R <= P,b1 & 0. R <= P,b2 holds

b1 = b2

proof end;

theorem :: REALALG2:81

for R being ordered domRing

for O being Ordering of R

for a, b being non b_{2} -negative Element of R holds

( a < O,b iff a ^2 < O,b ^2 )

for O being Ordering of R

for a, b being non b

( a < O,b iff a ^2 < O,b ^2 )

proof end;

theorem :: REALALG2:82

for R being preordered domRing

for P being Preordering of R

for a being b_{2} -ordered Element of R holds (abs (P,a)) ^2 = a ^2

for P being Preordering of R

for a being b

proof end;

theorem sq5: :: REALALG2:83

for R being preordered Ring

for P being Preordering of R

for a being Element of R st a in (- P) \ {(0. R)} holds

not a is square

for P being Preordering of R

for a being Element of R st a in (- P) \ {(0. R)} holds

not a is square

proof end;

theorem :: REALALG2:85

lemsqrtex: for R being ordered domRing

for O being Ordering of R

for a being square Element of R holds

not for b being Sqrt of a holds b is O -negative

proof end;

registration

let R be preordered Ring;

let P be Preordering of R;

coherence

for b_{1} being Element of R st b_{1} is P -negative holds

not b_{1} is square
by sq5;

coherence

for b_{1} being Element of R st not b_{1} is P -positive & b_{1} is square holds

b_{1} is zero

end;
let P be Preordering of R;

coherence

for b

not b

coherence

for b

b

proof end;

registration

let R be ordered domRing;

let O be Ordering of R;

let a be square Element of R;

not for b_{1} being Sqrt of a holds b_{1} is O -negative
by lemsqrtex;

end;
let O be Ordering of R;

let a be square Element of R;

cluster left_complementable right_complementable complementable non O -negative for SquareRoot of a;

existence not for b

registration

let R be ordered domRing;

let O be Ordering of R;

let a be non zero square Element of R;

existence

ex b_{1} being Sqrt of a st b_{1} is O -positive

ex b_{1} being Sqrt of a st b_{1} is O -negative

end;
let O be Ordering of R;

let a be non zero square Element of R;

existence

ex b

proof end;

existence ex b

proof end;

definition

let R be ordered domRing;

let O be Ordering of R;

let a be square Element of R;

existence

ex b_{1} being non O -negative Sqrt of a st b_{1} ^2 = a

for b_{1}, b_{2} being non O -negative Sqrt of a st b_{1} ^2 = a & b_{2} ^2 = a holds

b_{1} = b_{2}

end;
let O be Ordering of R;

let a be square Element of R;

existence

ex b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defq defines sqrt REALALG2:def 13 :

for R being ordered domRing

for O being Ordering of R

for a being square Element of R

for b_{4} being non b_{2} -negative Sqrt of a holds

( b_{4} = sqrt (O,a) iff b_{4} ^2 = a );

for R being ordered domRing

for O being Ordering of R

for a being square Element of R

for b

( b

theorem :: REALALG2:86

for R being ordered domRing

for O being Ordering of R

for a being square Element of R

for b being Element of R holds

( b is Sqrt of a iff ( b = sqrt (O,a) or b = - (sqrt (O,a)) ) )

for O being Ordering of R

for a being square Element of R

for b being Element of R holds

( b is Sqrt of a iff ( b = sqrt (O,a) or b = - (sqrt (O,a)) ) )

proof end;

registration

let R be ordered domRing;

let O be Ordering of R;

let a be non zero square Element of R;

coherence

not sqrt (O,a) is zero

end;
let O be Ordering of R;

let a be non zero square Element of R;

coherence

not sqrt (O,a) is zero

proof end;