:: Formally Real Fields
:: by Christoph Schwarzweller
::
:: Received November 29, 2017
:: Copyright (c) 2017-2021 Association of Mizar Users


registration
let X, Y be non empty set ;
cluster Relation-like X -defined Y -valued Function-like non empty for set ;
existence
ex b1 being Function st
( not b1 is empty & b1 is X -defined & b1 is Y -valued )
proof end;
end;

registration
cluster the carrier of F_Rat -> rational-membered ;
coherence
the carrier of F_Rat is rational-membered by GAUSSINT:def 14;
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
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
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)
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)
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
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)
proof end;

registration
let R be Ring;
let a be Element of R;
cluster a ^2 -> square ;
coherence
a ^2 is square ;
cluster a |^ 2 -> square ;
coherence
a |^ 2 is square
proof end;
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)
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)
proof end;

theorem P4a: :: REALALG2:9
for R being commutative Ring
for a, b being Element of R holds (a + b) * (a - b) = (a ^2) - (b ^2)
proof end;

P5b: for R being non degenerated Ring holds
( Char R = 2 iff 2 '*' (1. R) = 0. R )
proof end;

theorem sq00: :: REALALG2:10
for R being domRing
for a, b being Element of R holds
( a ^2 = b ^2 iff ( a = b or a = - b ) )
proof end;

theorem XZ: :: REALALG2:11
for F being Field
for a being non zero Element of F holds (- a) " = - (a ")
proof end;

theorem YY: :: REALALG2:12
for F being Field
for a being non zero Element of F holds (- (a ")) " = - a
proof end;

theorem YZ: :: REALALG2:13
for F being Field
for a being non zero Element of F holds - ((- a) ") = a "
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)
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
proof end;

registration
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 b1 being non degenerated Ring st b1 is preordered holds
b1 is 0 -characteristic by REALALG1:28;
end;

theorem v1a: :: REALALG2:16
for R being preordered Ring
for P being Preordering of R holds (- P) * P = P * (- P)
proof end;

theorem v1: :: REALALG2:17
for R being preordered Ring
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 )
proof end;

theorem spa: :: REALALG2:19
for R being preordered Ring
for P being Preordering of R
for n being Nat holds n '*' (1. R) in 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
cluster prepositive_cone -> spanning for Element of bool the carrier of INT.Ring;
coherence
for b1 being Preordering of INT.Ring holds b1 is spanning
proof end;
cluster prepositive_cone -> spanning for Element of bool the carrier of F_Rat;
coherence
for b1 being Preordering of F_Rat holds b1 is spanning
proof end;
cluster prepositive_cone -> spanning for Element of bool the carrier of F_Real;
coherence
for b1 being Preordering of F_Real holds b1 is spanning
proof end;
end;

theorem :: REALALG2:20
for P being Preordering of INT.Ring holds P = Positives(INT.Ring) by REALALG1:40;

theorem :: REALALG2:21
for P being Preordering of F_Rat holds P = Positives(F_Rat) by REALALG1:38;

theorem :: REALALG2:22
for P being Preordering of F_Real holds P = Positives(F_Real) by REALALG1:36;

theorem :: REALALG2:23
for R being Ring holds
( Char R = 1 iff R is degenerated )
proof end;

theorem :: REALALG2:24
for R being non degenerated Ring holds
( Char R = 2 iff 2 '*' (1. R) = 0. R ) by P5b;

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

theorem tA: :: REALALG2:26
for R being 0 -characteristic domRing
for a being Element of R holds
( - a = a iff a = 0. R )
proof end;

definition
let R be preordered Ring;
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;
end;

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

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

registration
let F be preordered Field;
cluster spanning prepositive_cone -> maximal for Element of bool the carrier of F;
coherence
for b1 being Preordering of F st b1 is spanning holds
b1 is maximal by T1;
cluster prepositive_cone maximal -> spanning for Element of bool the carrier of F;
coherence
for b1 being Preordering of F st b1 is maximal holds
b1 is spanning
proof end;
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 )
proof end;

registration
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 b1 being preordered Field holds b1 is ordered
proof end;
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 ) ;

theorem T1a: :: REALALG2:31
for F being preordered Field
for P being Preordering of F ex O being Ordering of F st P c= O
proof end;

definition
let R be ordered Ring;
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 } is Subset of R
proof end;
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 } ;

registration
let R be ordered Ring;
let P be Preordering of R;
cluster /\ (P,R) -> non empty ;
coherence
not /\ (P,R) is empty
proof end;
end;

registration
let R be ordered Ring;
let P be Preordering of R;
cluster /\ (P,R) -> add-closed mult-closed with_squares ;
coherence
( /\ (P,R) is add-closed & /\ (P,R) is mult-closed & /\ (P,R) is with_squares )
proof end;
end;

s1: for F being preordered Field
for P being Preordering of F holds /\ (P,F) = P
proof end;

registration
let F be ordered Field;
let P be Preordering of F;
cluster /\ (P,F) -> negative-disjoint ;
coherence
/\ (P,F) is negative-disjoint by s1;
end;

theorem :: REALALG2:32
for F being ordered Field
for P being Preordering of F holds /\ (P,F) is Preordering of F ;

theorem :: REALALG2:33
for F being ordered Field
for P being Preordering of F holds /\ (P,F) = P by s1;

definition
let R be Ring;
attr R is formally_real means :: REALALG2:def 3
 not - (1. R) in QS R;
end;

:: deftheorem defines formally_real REALALG2:def 3 :
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 T0: :: REALALG2:34
for F being Field st Char F <> 2 holds
( F is formally_real iff QS F is prepositive_cone )
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 )
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 )
proof end;

theorem :: REALALG2:37
for F being Field st Char F <> 2 holds
( F is formally_real iff QS F <> the carrier of F ) by lemma3;

registration
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 b1 being Field st b1 is formally_real holds
b1 is ordered
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 b1 being Field st b1 is ordered holds
b1 is formally_real
proof end;
end;

registration
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 b1 being non degenerated Ring st b1 is preordered holds
b1 is formally_real
proof end;
end;

registration
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 b1 being Field st b1 is formally_real
proof end;
end;

registration
let F be formally_real Field;
cluster Quadratic_Sums_of F -> negative-disjoint ;
coherence
QS F is negative-disjoint
proof end;
end;

theorem :: REALALG2:38
for F being formally_real Field holds QS F is Preordering of F ;

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

theorem :: REALALG2:40
for r being Element of F_Rat st 0 <= r holds
r is sum_of_squares
proof end;

definition
let R be ZeroStr ;
let f be the carrier of R -valued Function;
attr f is trivial means :: REALALG2:def 4
 for i being object st i in dom f holds
f . i = 0. R;
end;

:: deftheorem defines trivial REALALG2:def 4 :
for R being ZeroStr
for f being the carrier of b1 -valued Function holds
( f is trivial iff for i being object st i in dom f holds
f . i = 0. R );

definition
let R be Ring;
let f be non empty FinSequence of R;
attr f is quadratic means :dq: :: REALALG2:def 5
 for i being Element of dom f holds f . i is square ;
end;

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

registration
let R be non degenerated Ring;
cluster <*(1. R)*> -> non empty non trivial quadratic for non empty FinSequence of R;
coherence
for b1 being non empty FinSequence of R st b1 = <*(1. R)*> holds
( b1 is quadratic & not b1 is trivial )
proof end;
end;

registration
let R be non degenerated Ring;
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 b1 being non empty FinSequence of R st
( b1 is quadratic & not b1 is trivial )
proof end;
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 )
proof end;

registration
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 b1 being formally_real Field holds not b1 is algebraic-closed
proof end;
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 )
proof end;

theorem c1: :: REALALG2:43
for R being preordered Ring
for P being Preordering of R
for a being Element of R holds a <= 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
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
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
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
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
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 )
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 " )
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 " )
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 :: REALALG2:def 6
( a <= P,b & a <> b );
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 ) );

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

theorem :: REALALG2:54
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 or a = b ) by avb4;

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;

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;

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;

theorem :: REALALG2:58
for R being preordered domRing
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 by c5, GCD_1:1;

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

definition
let R be preordered Ring;
let P be Preordering of R;
let a be Element of R;
attr a is P -ordered means :defppp: :: REALALG2:def 7
a in P \/ (- P);
attr a is P -positive means :: REALALG2:def 8
a in P \ {(0. R)};
attr a is P -negative means :defn: :: REALALG2:def 9
a in (- P) \ {(0. R)};
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) );

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

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

registration
let R be preordered Ring;
let P be Preordering of R;
cluster left_complementable right_complementable complementable P -ordered for Element of the carrier of R;
existence
ex b1 being Element of R st b1 is P -ordered
proof end;
end;

registration
let R be preordered Ring;
let P be Preordering of R;
cluster P -positive -> P -ordered for Element of the carrier of R;
coherence
for b1 being Element of R st b1 is P -positive holds
b1 is P -ordered
proof end;
cluster P -negative -> P -ordered for Element of the carrier of R;
coherence
for b1 being Element of R st b1 is P -negative holds
b1 is P -ordered
proof end;
end;

registration
let R be non degenerated preordered Ring;
let P be Preordering of R;
cluster left_complementable right_complementable complementable P -positive for Element of the carrier of R;
existence
ex b1 being Element of R st b1 is P -positive
proof end;
cluster left_complementable right_complementable complementable P -negative for Element of the carrier of R;
existence
ex b1 being Element of R st b1 is P -negative
proof end;
cluster left_complementable right_complementable complementable non P -positive for Element of the carrier of R;
existence
not for b1 being Element of R holds b1 is P -positive
proof end;
cluster left_complementable right_complementable complementable non P -negative for Element of the carrier of R;
existence
not for b1 being Element of R holds b1 is P -negative
proof end;
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;
cluster P -positive -> non zero non P -negative for Element of the carrier of R;
coherence
for b1 being Element of R st b1 is P -positive holds
( not b1 is zero & not b1 is P -negative )
proof end;
cluster P -negative -> non zero non P -positive for Element of the carrier of R;
coherence
for b1 being Element of R st b1 is P -negative holds
( not b1 is zero & not b1 is P -positive )
proof end;
end;

registration
let R be non degenerated preordered Ring;
let P be Preordering of R;
let a be P -ordered Element of R;
cluster - a -> P -ordered ;
coherence
- a is P -ordered
proof end;
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
let F be Field;
let a be non zero Element of F;
cluster / a -> non zero ;
coherence
not a " is zero
proof end;
end;

registration
let F be preordered Field;
let P be Preordering of F;
let a be non zero P -ordered Element of F;
cluster / a -> P -ordered ;
coherence
a " is P -ordered by defppp, lemsqf;
end;

registration
let R be non degenerated ordered Ring;
let O be Ordering of R;
cluster non zero non O -positive -> O -negative for Element of the carrier of R;
coherence
for b1 being Element of R st not b1 is zero & not b1 is O -positive holds
b1 is O -negative
proof end;
cluster non zero non O -negative -> O -positive for Element of the carrier of R;
coherence
for b1 being Element of R st not b1 is zero & not b1 is O -negative holds
b1 is O -positive ;
end;

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;

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;

theorem x1a: :: REALALG2:64
for R being preordered Ring
for P being Preordering of R
for a being b2 -ordered Element of R holds
( 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 b2 -ordered Element of R holds
( 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;
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 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 b1 being Element of R st a in P & a in - P holds
( b1 = a iff b1 = - a )
proof end;
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) ) );

definition
let R be ordered Ring;
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
absolute_value (O,a) is Element of R ;
consistency
for b1 being Element of R holds verum ;
compatibility
for b1 being Element of R holds
( ( a in O implies ( b1 = absolute_value (O,a) iff b1 = a ) ) & ( not a in O implies ( b1 = absolute_value (O,a) iff b1 = - a ) ) )
proof end;
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 ) );

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;

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

theorem sq2: :: REALALG2:73
for F being preordered Field
for P being Preordering of F
for a being non zero b2 -ordered Element of F holds abs (P,(a ")) = (abs (P,a)) "
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))
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 )
proof end;

theorem abs10: :: REALALG2:76
for R being non degenerated preordered Ring
for P being Preordering of R
for a, b being b2 -ordered Element of R holds abs (P,(a * b)) = (abs (P,a)) * (abs (P,b))
proof end;

theorem :: REALALG2:77
for F being preordered Field
for P being Preordering of F
for a being non zero b2 -ordered Element of F
for b being b2 -ordered Element of F holds abs (P,(b * (a "))) = (abs (P,b)) * ((abs (P,a)) ")
proof end;

theorem ineq1: :: REALALG2:78
for R being preordered domRing
for P being Preordering of R
for a being b2 -ordered Element of R
for p being b2 -ordered non b2 -negative Element of R holds
( 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 b2 -ordered Element of R holds abs (P,(a + b)) <= P,(abs (P,a)) + (abs (P,b))
proof end;

definition
let R be Ring;
let a be square Element of R;
mode SquareRoot of a -> Element of R means :defsqrt: :: REALALG2:def 12
it ^2 = a;
existence
ex b1 being Element of R st b1 ^2 = a by O_RING_1:def 2;
end;

:: deftheorem defsqrt defines SquareRoot REALALG2:def 12 :
for R being Ring
for a being square Element of R
for b3 being Element of R holds
( b3 is SquareRoot of a iff b3 ^2 = a );

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

registration
let R be non degenerated Ring;
cluster non zero left_complementable right_complementable complementable square for Element of the carrier of R;
existence
ex b1 being Element of R st
( not b1 is zero & b1 is square )
proof end;
end;

theorem sq1: :: REALALG2:80
for R being ordered domRing
for O being Ordering of R
for a, b being non b2 -negative Element of R holds
( 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 b2 -negative Element of R holds
( 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 b2 -ordered Element of R holds (abs (P,a)) ^2 = a ^2
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
proof end;

theorem :: REALALG2:84
for R being preordered Ring
for P being Preordering of R holds (- P) /\ (SQ R) = {(0. R)}
proof end;

theorem :: REALALG2:85
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 by sq0;

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;
cluster P -negative -> non square for Element of the carrier of R;
coherence
for b1 being Element of R st b1 is P -negative holds
not b1 is square by sq5;
cluster square non P -positive -> zero for Element of the carrier of R;
coherence
for b1 being Element of R st not b1 is P -positive & b1 is square holds
b1 is zero
proof end;
end;

registration
let R be ordered domRing;
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 b1 being Sqrt of a holds b1 is O -negative by lemsqrtex;
end;

registration
let R be ordered domRing;
let O be Ordering of R;
let a be non zero square Element of R;
cluster left_complementable right_complementable complementable O -positive for SquareRoot of a;
existence
ex b1 being Sqrt of a st b1 is O -positive
proof end;
cluster left_complementable right_complementable complementable O -negative for SquareRoot of a;
existence
ex b1 being Sqrt of a st b1 is O -negative
proof end;
end;

definition
let R be ordered domRing;
let O be Ordering of R;
let a be square Element of R;
func sqrt (O,a) -> non O -negative Sqrt of a means :defq: :: REALALG2:def 13
it ^2 = a;
existence
ex b1 being non O -negative Sqrt of a st b1 ^2 = a
proof end;
uniqueness
for b1, b2 being non O -negative Sqrt of a st b1 ^2 = a & b2 ^2 = a holds
b1 = b2
proof end;
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 b4 being non b2 -negative Sqrt of a holds
( b4 = sqrt (O,a) iff b4 ^2 = a );

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

registration
let R be ordered domRing;
let O be Ordering of R;
let a be non zero square Element of R;
cluster sqrt (O,a) -> non zero non O -negative ;
coherence
not sqrt (O,a) is zero
proof end;
end;