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

0.F & b <> 0.F; a" = b" implies a = b proof assume a" = b"; then a * b" = 1.F by Y,VECTSP_1:def 10; then (a * b") * b = b; then a * (b * b") = b by GROUP_1:def 3; then a * 1.F = b by Y,VECTSP_1:def 10; hence a = b; end; hence thesis by AS,fi1; end; theorem for F being preordered Field, P being Preordering of F, a,b being non zero Element of F st a <=P, 0.F & b <=P, 0.F holds a

0.F & b <> 0.F; a" = b" implies a = b proof assume a" = b"; then a * b" = 1.F by Y,VECTSP_1:def 10; then (a * b") * b = b; then a * (b * b") = b by GROUP_1:def 3; then a * 1.F = b by Y,VECTSP_1:def 10; hence a = b; end; hence thesis by AS,fi2; 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: a in P \/ (-P); attr a is P-positive means a in P \ {0.R}; attr a is P-negative means :defn: a in (-P) \ {0.R}; end; registration let R be preordered Ring; let P be Preordering of R; cluster P-ordered for Element of R; existence proof take 1.R; 1.R in P by REALALG1:25; hence thesis by XBOOLE_0:def 3; end; end; registration let R be preordered Ring; let P be Preordering of R; cluster P-positive -> P-ordered for Element of R; coherence proof let a be Element of R; assume a is P-positive; then a in P by XBOOLE_0:def 5; hence a in P \/ (-P) by XBOOLE_0:def 3; end; cluster P-negative -> P-ordered for Element of R; coherence proof let a be Element of R; assume a is P-negative; then a in -P by XBOOLE_0:def 5; hence a in P \/ (-P) by XBOOLE_0:def 3; end; end; registration let R be preordered non degenerated Ring; let P be Preordering of R; cluster P-positive for Element of R; existence proof take 1.R; 1.R in P & not 1.R in {0.R} by REALALG1:25,TARSKI:def 1; hence thesis by XBOOLE_0:def 5; end; cluster P-negative for Element of R; existence proof take -1.R; --1.R <> -0.R; then 1.R in P & -1.R <> 0.R by REALALG1:25; then -1.R in -P & not -1.R in {0.R} by TARSKI:def 1; hence thesis by XBOOLE_0:def 5; end; cluster non P-positive for Element of R; existence proof take 0.R; 0.R in {0.R} by TARSKI:def 1; hence thesis by XBOOLE_0:def 5; end; cluster non P-negative for Element of R; existence proof take 0.R; 0.R in {0.R} by TARSKI:def 1; hence thesis by XBOOLE_0:def 5; end; end; x1: for R being preordered Ring, P being Preordering of R, a being Element of R holds a is P-positive iff 0.R

0.R by TARSKI:def 1; hence 0.R

0.R; then a in P & not a in {0.R} by TARSKI:def 1; hence a is P-positive by XBOOLE_0:def 5; end; x2: for R being preordered Ring, P being Preordering of R, a being Element of R holds a is P-negative iff a

0.R by TARSKI:def 1; hence a

0.R; then --a in -P & not a in {0.R} by TARSKI:def 1; hence a is P-negative by XBOOLE_0:def 5; 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; coherence proof let a be Element of R; assume a is P-positive; then A: 0.R

non zero non P-positive for Element of R; coherence proof let a be Element of R; assume a is P-negative; then A: a

P-ordered;
coherence
proof
a in P \/ (-P) by defppp;
then -a in -(P \/ (-P));
then -a in (-P) \/ (--P) by REALALG1:16;
hence thesis;
end;
end;
lemsqf:
for F being preordered Field,
P being Preordering of F,
a being non zero Element of F holds a in P\/-P iff a" in P\/-P
proof
let F be preordered Field, P be Preordering of F,
a be non zero Element of F;
-a <> -0.F; then
X: a" is non zero & -a" is non zero & -a is non zero by VECTSP_1:25;
hereby assume a in P\/-P;
then per cases by XBOOLE_0:def 3;
suppose a in P;
then a" in P by REALALG1:27;
hence a" in P\/-P by XBOOLE_0:def 3;
end;
suppose a in -P;
then -a in --P;
then (-a)" in P by X,REALALG1:27;
then -((-a)") in -P;
then a" in -P by YZ;
hence a" in P\/-P by XBOOLE_0:def 3;
end;
end;
assume a" in P\/-P;
then per cases by XBOOLE_0:def 3;
suppose a" in P;
then a"" in P by X,REALALG1:27;
hence a in P\/-P by XBOOLE_0:def 3;
end;
suppose a" in -P;
then -a" in --P;
then (-a")" in P by X,REALALG1:27;
then -a in P by YY;
then --a in -P;
hence a in P\/-P by XBOOLE_0:def 3;
end;
end;
registration
let F be Field;
let a be non zero Element of F;
cluster a" -> non zero;
coherence
proof
A: a <> 0.F;
assume a" is zero;
then 0.F = a * a" .= 1.F by A,VECTSP_1:def 10;
hence contradiction;
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 by defppp,lemsqf;
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;
coherence
proof
let a be Element of R;
assume A: a is non zero non O-positive;
then a <> 0.R & not(0.R 0.R;
now assume a in -P;
then a in {0.R} by C,H;
hence contradiction by D,TARSKI:def 1;
end;
hence a is non P-negative by XBOOLE_0:def 5;
end;
end;
theorem
for R being preordered Ring,
P being Preordering of R
for a being P-ordered Element of R holds a is non P-positive iff a <=P, 0.R
proof
let R be preordered Ring, P be Preordering of R;
let a be P-ordered Element of R;
H: a in P \/ -P & P /\ -P = {0.R} by REALALG1:def 14,defppp;
hereby assume a is non P-positive;
then per cases by XBOOLE_0:def 5;
suppose not a in P;
then a in -P by H,XBOOLE_0:def 3;
then -a in --P;
hence a <=P, 0.R;
end;
suppose a in {0.R};
then a = 0.R by TARSKI:def 1;
hence a <=P, 0.R by c1;
end;
end;
assume a <=P, 0.R;
then C: --a in -P;
per cases;
suppose a = 0.R;
then a in {0.R} by TARSKI:def 1;
hence a is non P-positive by XBOOLE_0:def 5;
end;
suppose D: a <> 0.R;
now assume a in P;
then a in {0.R} by C,H;
hence contradiction by D,TARSKI:def 1;
end;
hence a is non P-positive by XBOOLE_0:def 5;
end;
end;
begin :: Absolute Values
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:
a if a in P,
-a if a in -P
otherwise -1.R;
coherence;
consistency
proof
let r be Element of R;
thus (a in P & a in -P) implies (r = a iff r = -a)
proof
assume a in P & a in -P;
then A: a in P /\ -P;
P /\ -P = {0.R} by REALALG1:def 14;
then a = 0.R by A,TARSKI:def 1;
hence thesis;
end;
end;
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
a if a in O
otherwise -a;
coherence;
consistency;
compatibility
proof
let r be Element of R;
thus a in O implies (r = absolute_value(O,a) iff r = a) by defa;
thus not(a in O) implies (r = absolute_value(O,a) iff r = -a)
proof
assume AS: not(a in O);
O \/ -O = the carrier of R by REALALG1:def 8;
then a in -O by AS,XBOOLE_0:def 3;
hence thesis by defa;
end;
end;
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 av0:
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
proof
let R be preordered non degenerated Ring, O be Preordering of R,
a be Element of R;
hereby assume 0.R <=O, abs(O,a);
then C: -1.R Element of R means :defsqrt:
it^2 = a;
existence by O_RING_1:def 2;
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;
existence
proof
take 1.R;
thus thesis;
end;
end;
theorem sq1:
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
proof
let R be ordered domRing, P be Ordering of R,
a,b be non P-negative Element of R;
the carrier of R = P \/ -P by REALALG1:def 8;
then A: a is P-ordered & b is P-ordered;
then AS: 0.R <=P, a & 0.R <=P, b by x1a;
per cases;
suppose K: a = 0.R;
SQ R c= P & b^2 in SQ R by REALALG1:def 14;
hence thesis by A,x1a,K;
end;
suppose K: a <> 0.R;
hereby assume a <=P, b;
then a * a <= P, b * a & a * b <= P, b * b by AS,c5;
hence a^2 <= P, b^2 by c3;
end;
C: P * (-P) c= -P & P + P c= P by v2,REALALG1:def 14;
B: a + b in P + P by AS;
D: the carrier of R = P \/ -P by REALALG1:def 8;
assume a^2 <=P, b^2;
then A: (b + a) * (b - a) in P by P4a;
per cases by D,XBOOLE_0:def 3;
suppose b - a in -P;
then (b + a) * (b - a) in P * (-P) by B,C;
then (b + a) * (b - a) in P /\ -P by A,C;
then (b + a) * (b - a) in {0.R} by REALALG1:def 7;
then D: (b + a) * (b - a) = 0.R by TARSKI:def 1;
per cases by D,VECTSP_2:def 1;
suppose b + a = 0.R;
then a = -b by RLVECT_1:6;
then a in -P by AS;
then a in P /\ -P by AS;
then a in {0.R} by REALALG1:def 7;
hence a <=P, b by K,TARSKI:def 1;
end;
suppose b - a = 0.R;
hence a <=P, b by REALALG1:25;
end;
end;
suppose b - a in P;
hence a <=P, b;
end;
end;
end;
sq0:
for R being preordered domRing,
P being Preordering of R,
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
let R be preordered domRing, P be Preordering of R, a be square Element of R;
let b1,b2 being Sqrt of a;
assume AS: 0.R <=P, b1 & 0.R <=P, b2;
per cases;
suppose A: b1 = 0.R;
then 0.R = b1^2
.= a by defsqrt
.= b2^2 by defsqrt .= b2 * b2;
hence thesis by A,VECTSP_2:def 1;
end;
suppose b1 <> 0.R;
then A: -b1 0.R;
per cases by A,XBOOLE_0:def 3;
suppose b in O;
then 0.R <=O, b;
then B: 0.R