b; end; theorem :: REALALG2:52 for R being preordered non degenerated Ring, P being Preordering of R holds 0.R

P-ordered for Element of R; cluster P-negative -> P-ordered for Element of R; end; registration let R be preordered non degenerated Ring; let P be Preordering of R; cluster P-positive for Element of R; cluster P-negative for Element of R; cluster non P-positive for Element of R; cluster non P-negative for Element of R; end; registration let R be preordered non degenerated Ring; let P be Preordering of R; cluster P-positive -> non zero non P-negative for Element of R; cluster P-negative -> non zero non P-positive for Element of R; end; registration let R be preordered non degenerated Ring; let P be Preordering of R; let a be P-ordered Element of R; cluster -a -> P-ordered; end; registration let F be Field; let a be non zero Element of F; cluster a" -> non zero; 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; end; registration let R be ordered non degenerated Ring; let O be Ordering of R; cluster non zero non O-positive -> O-negative for Element of R; cluster non zero non O-negative -> O-positive for Element of R; end; theorem :: REALALG2:62 for R being preordered Ring, P being Preordering of R, a being Element of R holds a is P-positive iff 0.R

Element of R equals
:: REALALG2:def 10
a if a in P,
-a if a in -P
otherwise -1.R;
end;
definition
let R be ordered Ring;
let O be Ordering of R;
let a be Element of R;
redefine func absolute_value(O,a) -> Element of R equals
:: REALALG2:def 11
a if a in O
otherwise -a;
end;
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 :: REALALG2:66
for R being preordered non degenerated Ring,
P being Preordering of R,
a being Element of R holds 0.R <=P, abs(P,a) iff a is P-ordered;
theorem :: REALALG2:67
for R being preordered non degenerated Ring,
P being Preordering of R,
a being Element of R holds not a is P-ordered iff abs(P,a) = -1.R;
theorem :: REALALG2:68
for R being preordered non degenerated Ring,
P being Preordering of R,
a being Element of R holds abs(P,a) = 0.R iff a = 0.R;
theorem :: REALALG2:69
for R being preordered domRing,
P being Preordering of R,
a being Element of R holds abs(P,a) = a iff 0.R <=P, a;
theorem :: REALALG2:70
for R being preordered domRing,
P being Preordering of R,
a being Element of R holds abs(P,a) = -a iff a <=P, 0.R;
theorem :: REALALG2:71
for R being preordered Ring,
P being Preordering of R,
a being Element of R holds abs(P,a) = abs(P,-a);
theorem :: REALALG2:72
for R being preordered non degenerated Ring,
P being Preordering of R,
a being Element of R
holds -abs(P,a) <=P, a & a <=P, abs(P,a) iff a is P-ordered;
theorem :: REALALG2:73
for F being preordered Field,
P being Preordering of F,
a being non zero P-ordered Element of F holds abs(P,a") = abs(P,a)";
theorem :: REALALG2:74
for R being preordered Ring,
P being Preordering of R,
a,b being Element of R holds abs(P,a-b) = abs(P,b-a);
theorem :: REALALG2:75
for R being preordered non degenerated Ring,
P being Preordering of R,
a being Element of R
holds (-abs(P,a) <=P, a & a <=P, abs(P,a)) iff a is P-ordered;
theorem :: REALALG2:76
for R being preordered non degenerated Ring,
P being Preordering of R,
a,b being P-ordered Element of R holds abs(P,a*b) = abs(P,a) * abs(P,b);
theorem :: REALALG2:77
for F being preordered Field,
P being Preordering of F
for a being non zero P-ordered Element of F,
b being P-ordered Element of F holds abs(P,b*a") = abs(P,b) * abs(P,a)";
theorem :: REALALG2:78
for R being preordered domRing,
P being Preordering of R,
a being P-ordered Element of R,
p being P-ordered non P-negative Element of R
holds abs(P,a) <=P, p iff (-p <=P, a & a <=P, p);
theorem :: REALALG2:79 :: triangle inequality
for R being preordered domRing,
P being Preordering of R,
a,b being P-ordered Element of R holds abs(P,a+b) <=P, abs(P,a) + abs(P,b);
begin :: Squares and square roots
definition
let R be Ring;
let a be square Element of R;
mode SquareRoot of a -> Element of R means
:: REALALG2:def 12
it^2 = a;
end;
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 square for Element of R;
end;
theorem :: REALALG2:80
for R being ordered domRing,
O being Ordering of R,
a,b being non O-negative Element of R holds a <=O, b iff a^2 <=O, b^2;
theorem :: REALALG2:81
for R being ordered domRing,
O being Ordering of R,
a,b being non O-negative Element of R holds a