:: 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 b₁ being Function st
( not b₁ is empty & b₁ is X -defined & b₁ 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 b₁ being non degenerated Ring st b₁ is preordered holds
b₁ 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 b₁ being Preordering of INT.Ring holds b₁ is spanning

proof end;

cluster prepositive_cone -> spanning for Element of bool the carrier of F_Rat;

coherence
for b₁ being Preordering of F_Rat holds b₁ is spanning

proof end;

cluster prepositive_cone -> spanning for Element of bool the carrier of F_Real;

coherence
for b₁ being Preordering of F_Real holds b₁ 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 b₁ being Preordering of F st b₁ is spanning holds
b₁ is maximal by T1;

cluster prepositive_cone maximal -> spanning for Element of bool the carrier of F;

coherence
for b₁ being Preordering of F st b₁ is maximal holds
b₁ 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 b₁ being preordered Field holds b₁ 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 b₁ being Field st b₁ is formally_real holds
b₁ 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 b₁ being Field st b₁ is ordered holds
b₁ 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 b₁ being non degenerated Ring st b₁ is preordered holds
b₁ 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 b₁ being Field st b₁ 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 b₁ -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 b₁ being non empty FinSequence of R st b₁ = <*(1. R)*> holds
( b₁ is quadratic & not b₁ 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 b₁ being non empty FinSequence of R st
( b₁ is quadratic & not b₁ 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 b₁ being formally_real Field holds not b₁ 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 b₁ being Element of R st b₁ 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 b₁ being Element of R st b₁ is P -positive holds
b₁ is P -ordered

proof end;

cluster P -negative -> P -ordered for Element of the carrier of R;

coherence
for b₁ being Element of R st b₁ is P -negative holds
b₁ 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 b₁ being Element of R st b₁ is P -positive

proof end;

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

existence
ex b₁ being Element of R st b₁ is P -negative

proof end;

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

existence
not for b₁ being Element of R holds b₁ is P -positive

proof end;

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

existence
not for b₁ being Element of R holds b₁ 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 b₁ being Element of R st b₁ is P -positive holds
( not b₁ is zero & not b₁ is P -negative )

proof end;

cluster P -negative -> non zero non P -positive for Element of the carrier of R;

coherence
for b₁ being Element of R st b₁ is P -negative holds
( not b₁ is zero & not b₁ 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 b₁ being Element of R st not b₁ is zero & not b₁ is O -positive holds
b₁ is O -negative

proof end;

cluster non zero non O -negative -> O -positive for Element of the carrier of R;

coherence
for b₁ being Element of R st not b₁ is zero & not b₁ is O -negative holds
b₁ 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 b₂ -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 b₂ -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 b₁ being Element of R st a in P & a in - P holds
( b₁ = a iff b₁ = - 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 b₁ being Element of R holds verum ;
compatibility
for b₁ being Element of R holds
( ( a in O implies ( b₁ = absolute_value (O,a) iff b₁ = a ) ) & ( not a in O implies ( b₁ = absolute_value (O,a) iff b₁ = - 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 b₂ -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 b₂ -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 b₂ -ordered Element of F
for b being b₂ -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 b₂ -ordered Element of R
for p being b₂ -ordered non b₂ -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 b₂ -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 b₁ being Element of R st b₁ ^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 b₃ being Element of R holds
( b₃ is SquareRoot of a iff b₃ ^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 b₁ being Element of R st
( not b₁ is zero & b₁ 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 b₂ -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 b₂ -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 b₂ -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 b₁ being Element of R st b₁ is P -negative holds
not b₁ is square by sq5;

cluster square non P -positive -> zero for Element of the carrier of R;

coherence
for b₁ being Element of R st not b₁ is P -positive & b₁ is square holds
b₁ 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 b₁ being Sqrt of a holds b₁ 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 b₁ being Sqrt of a st b₁ is O -positive

proof end;

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

existence
ex b₁ being Sqrt of a st b₁ 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 b₁ being non O -negative Sqrt of a st b₁ ^2 = a

proof end;

uniqueness
for b₁, b₂ being non O -negative Sqrt of a st b₁ ^2 = a & b₂ ^2 = a holds
b₁ = b₂

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 b₄ being non b₂ -negative Sqrt of a holds
( b₄ = sqrt (O,a) iff b₄ ^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;