:: Formally Real Fields
:: by Christoph Schwarzweller
::
:: Received November 29, 2017
:: Copyright (c) 2017-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ARYTM_3, FUNCT_1, RELAT_1, RLVECT_1, VECTSP_1, ALGSTR_0, TARSKI,
STRUCT_0, SUBSET_1, SUPINF_2, NAT_1, PYTHTRIP, GLIB_000, VECTSP_2,
CARD_1, MESFUNC1, INT_1, WELLORD2, RELAT_2, ORDERS_1, GROUP_1, BINOP_1,
NUMBERS, FUNCSDOM, XXREAL_0, WELLORD1, IDEAL_1, COMPLEX1, FINSEQ_1,
CARD_3, ZFMISC_1, XBOOLE_0, ARYTM_1, GAUSSINT, INT_3, SQUARE_1, XCMPLX_0,
RING_3, NEWTON, INTERVA1, REALALG1, MEMBERED, RAT_1, GROUP_4, REALALG2,
FUNCT_7, PARTFUN1, POLYNOM5, POLYNOM2, QMAX_1, ARROW, ORDINAL4, HURWITZ,
RING_5, CAT_7, FUNCOP_1;
notations TARSKI, ZFMISC_1, XBOOLE_0, SUBSET_1, RELAT_1, RELAT_2, WELLORD1,
ORDERS_1, FUNCT_1, FINSEQ_1, ALGSEQ_1, PARTFUN1, ORDINAL1, FINSEQ_7,
FUNCOP_1, SQUARE_1, XCMPLX_0, XXREAL_0, XXREAL_2, NAT_1, INT_1, RAT_1,
INT_3, NUMBERS, MEMBERED, STRUCT_0, BINOM, ALGSTR_0, GROUP_1, GROUP_2,
O_RING_1, RLVECT_1, VECTSP_1, VECTSP_2, POLYNOM4, POLYNOM5, HURWITZ,
GAUSSINT, IDEAL_1, RING_2, RING_3, ARROW, REALALG1, RING_5;
constructors BINOM, BINOP_2, O_RING_1, XXREAL_2, RING_3, TOPALG_7, ORDERS_1,
SQUARE_1, ALGSEQ_1, FINSEQ_7, ARROW, POLYNOM5, RING_5, HURWITZ, POLYNOM4,
REALALG1;
registrations ORDINAL1, XXREAL_0, XREAL_0, VECTSP_1, STRUCT_0, MEMBERED,
RLVECT_1, INT_1, VECTSP_2, NAT_1, INT_3, RELAT_1, ALGSTR_0, REALALG1,
GAUSSINT, CARD_1, FINSEQ_1, RING_5, FUNCOP_1, RAT_1;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
definitions TARSKI;
equalities XCMPLX_0, STRUCT_0, ALGSTR_0, VECTSP_1, XBOOLE_0, IDEAL_1,
O_RING_1, WELLORD1, INT_3, RING_3, GROUP_2, SQUARE_1, REALALG1;
expansions STRUCT_0, XBOOLE_0, TARSKI, ARROW, O_RING_1, IDEAL_1, RING_3,
REALALG1;
theorems GROUP_1, VECTSP_1, TARSKI, BINOM, FUNCT_1, RLVECT_1, RING_3,
XBOOLE_0, NAT_1, GAUSSINT, RELAT_1, XXREAL_0, XREAL_1, FINSEQ_1, RELAT_2,
VECTSP_2, ORDERS_1, WELLORD2, FINSEQ_4, FINSEQ_7, GROEB_2, RAT_1, INT_1,
NUMBERS, SQUARE_1, XREAL_0, GCD_1, REALALG1, XTUPLE_0, POLYNOM5,
O_RING_1, HURWITZ, RING_5, FINSEQ_3;
schemes NAT_1, INT_1;
begin :: Preliminaries
registration
let X,Y be non empty set;
cluster non empty X-defined Y-valued for Function;
existence
proof
take X --> the Element of Y;
thus thesis;
end;
end;
registration
cluster the carrier of F_Rat -> rational-membered;
coherence by GAUSSINT:def 14;
end;
theorem P0:
for L being right_zeroed non empty addLoopStr,
S,T being Subset of L
st 0.L in T holds S c= S + T
proof
let L be right_zeroed non empty addLoopStr, S,T be Subset of L;
assume A: 0.L in T;
let x be object;
assume B: x in S;
then reconsider a = x as Element of L;
a + 0.L in {c+b where c,b is Element of L : c in S & b in T} by A,B;
hence x in S + T by RLVECT_1:def 4;
end;
theorem
for L being right_unital non empty multLoopStr,
S,T being Subset of L
st 1.L in T holds S c= S * T
proof
let L be right_unital non empty multLoopStr, S,T be Subset of L;
assume A: 1.L in T;
now let x be object;
assume B: x in S;
then reconsider a = x as Element of L;
a * 1.L in
{s1 * s2 where s1,s2 is Element of L : s1 in S & s2 in T} by A,B;
hence x in S * T;
end;
hence thesis;
end;
theorem P1:
for L being add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr,
S being Subset of L st 0.L in S
for a being Element of L holds S c= S + a * S
proof
let L be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr,
S be Subset of L;
assume A: 0.L in S;
let a be Element of L;
a * 0.L in {a*i where i is Element of L : i in S} by A;
hence thesis by P0;
end;
theorem P2:
for L being add-associative right_zeroed right_complementable
right_unital right-distributive non empty doubleLoopStr,
S being Subset of L st 0.L in S & 1.L in S
for a being Element of L holds a in S + a * S
proof
let L be add-associative right_zeroed right_complementable right_unital
right-distributive non empty doubleLoopStr, S be Subset of L;
assume AS: 0.L in S & 1.L in S;
let a be Element of L;
a * 1.L in {a*i where i is Element of L : i in S} by AS;
then 0.L + a * 1.L in
{c+b where c,b is Element of L : c in S & b in a*S} by AS;
hence thesis;
end;
theorem c1:
for R being add-associative right_zeroed right_complementable
Abelian left-distributive non empty doubleLoopStr,
a,b being Element of R,
i being Integer holds i '*' (a * b) = (i '*' a) * b
proof
let R be add-associative right_zeroed right_complementable
Abelian left-distributive non empty doubleLoopStr,
a,b be Element of R,
i be Integer;
defpred P[Integer] means $1'*'(a*b) = ($1'*'a)*b;
A2: P[0]
proof
0 '*' a = 0.R by RING_3:59;
hence 0'*'(a*b) = (0'*'a) * b by RING_3:59;
end;
A3: for u being Integer holds P[u] implies P[u - 1] & P[u + 1]
proof
let u be Integer;
assume A4: P[u];
thus P[u-1]
proof
set k = u-1;
A6: (k+1)'*'(a*b) = (k'*'a+1'*'a)*b by A4,RING_3:62
.= (k'*'a) * b + (1'*'a)*b by VECTSP_1:def 3
.= (k'*'a) * b + a * b by RING_3:60;
(k'*'a) * b + 0.R = (k'*'a) * b + (a * b + - a* b) by RLVECT_1:5
.= (k+1)'*'(a*b) + - a * b by A6,RLVECT_1:def 3;
hence (k'*'a) * b = (k+1)'*'(a*b) + (-1) '*' (a * b) by RING_3:61
.= k '*' (a * b) by RING_3:62;
end;
thus P[u+1]
proof
set k = u+1;
A6: (k-1)'*'(a*b) = (k'*'a-1'*'a)*b by A4,RING_3:64
.= (k'*'a) * b + (-(1'*'a))*b by VECTSP_1:def 3
.= (k'*'a) * b + -((1'*'a)*b) by VECTSP_1:9
.= (k'*'a) * b - a * b by RING_3:60;
(k'*'a) * b + 0.R = (k'*'a) * b + (- a * b + a* b) by RLVECT_1:5
.= (k-1)'*'(a*b) + a * b by A6,RLVECT_1:def 3;
hence (k'*'a) * b = (k-1)'*'(a*b) + 1 '*' (a * b) by RING_3:60
.= k '*' (a * b) by RING_3:62;
end;
end;
for i being Integer holds P[i] from INT_1:sch 4(A2,A3);
hence thesis;
end;
theorem c1a:
for R being add-associative right_zeroed right_complementable
Abelian left-distributive non empty doubleLoopStr,
a being Element of R,
i being Integer holds i '*' (-a) = -(i '*' a)
proof
let R be add-associative right_zeroed right_complementable
Abelian left-distributive non empty doubleLoopStr,
a be Element of R,
i be Integer;
defpred P[Integer] means $1'*'(-a) = -($1'*'a);
A2: P[0]
proof
0 '*' (-a) = -0.R by RING_3:59 .= -(0'*'a) by RING_3:59;
hence 0'*'(-a) = -(0'*'a);
end;
A3: for u being Integer holds P[u] implies P[u - 1] & P[u + 1]
proof
let u be Integer;
assume A4: P[u];
thus P[u-1]
proof
set k = u-1;
A6: (k+1)'*'(-a) = -(k'*'a + 1'*'a) by A4,RING_3:62
.= -((k'*'a) + a) by RING_3:60
.= -(k'*'a) + -a by RLVECT_1:31;
thus -(k'*'a) = -(k'*'a) + 0.R
.= -(k'*'a) + (-a + a) by RLVECT_1:5
.= ((k+1)'*'(-a)) + a by A6,RLVECT_1:def 3
.= (k'*'(-a) + 1'*'(-a)) + a by RING_3:62
.= (k'*'(-a) + (-a)) + a by RING_3:60
.= k'*'(-a) + ((-a) + a) by RLVECT_1:def 3
.= k'*'(-a) + 0.R by RLVECT_1:5
.= k'*'(-a);
end;
thus P[u+1]
proof
set k = u+1;
A6: (k-1)'*'(-a) = -(k'*'a - 1'*'a) by A4,RING_3:64
.= -((k'*'a) - a) by RING_3:60
.= -(k'*'a) + --a by RLVECT_1:33;
thus -(k'*'a) = -(k'*'a) + 0.R
.= -(k'*'a) + (a + -a) by RLVECT_1:5
.= ((k-1)'*'(-a)) + -a by A6,RLVECT_1:def 3
.= (k'*'(-a) - 1'*'(-a)) + -a by RING_3:64
.= (k'*'(-a) - (-a)) + -a by RING_3:60
.= k'*'(-a) + ((-a) + a) by RLVECT_1:def 3
.= k'*'(-a) + 0.R by RLVECT_1:5
.= k'*'(-a);
end;
end;
for i being Integer holds P[i] from INT_1:sch 4(A2,A3);
hence thesis;
end;
registration
let R be Ring;
let a be Element of R;
cluster a^2 -> square;
coherence;
cluster a|^2 -> square;
coherence
proof
a|^2 = a^2 by RING_5:3;
hence thesis;
end;
end;
theorem P3:
for R being commutative Ring,
a,b being Element of R holds (a + b)^2 = a^2 + 2 '*' a * b + b^2
proof
let R be commutative Ring; let a,b be Element of R;
thus (a + b)^2 = a * (a + b) + b * (a + b) by VECTSP_1:def 7
.= (a * a + a * b) + b * (a + b) by VECTSP_1:def 7
.= (a * a + a * b) + (b * a + b * b) by VECTSP_1:def 7
.= a * a + (a * b + (b * a + b * b)) by RLVECT_1:def 3
.= a^2 + ((a * b + b * a) + b * b) by RLVECT_1:def 3
.= a^2 + (2 '*' (a * b) + b^2) by RING_5:2
.= a^2 + 2 '*' (a * b) + b^2 by RLVECT_1:def 3
.= a^2 + 2 '*' a * b + b^2 by c1;
end;
theorem P4:
for R being commutative Ring,
a,b being Element of R holds (a - b)^2 = a^2 - 2 '*' a * b + b^2
proof
let R be commutative Ring; let a,b be Element of R;
thus (a - b)^2 = a^2 + 2 '*' a * (-b) + ((-b)^2) by P3
.= a^2 + 2 '*' (a * (-b)) + ((-b)^2) by c1
.= a^2 + 2 '*' (-(a * b)) + (-b)^2 by VECTSP_1:8
.= a^2 + -(2 '*' (a * b)) + (-b)^2 by c1a
.= a^2 - (2 '*' a * b) + (-b)^2 by c1
.= a^2 - (2 '*' a * b) + b^2 by VECTSP_1:10;
end;
theorem P4a:
for R being commutative Ring,
a,b being Element of R holds (a + b) * (a - b) = a^2 - b^2
proof
let R be commutative Ring; let a,b be Element of R;
thus (a + b) * (a - b) = a * (a - b) + b * (a - b) by VECTSP_1:def 7
.= a * a + a * (-b) + b * (a + -b) by VECTSP_1:def 7
.= (a * a + a * (-b)) + (b * a + b * (-b)) by VECTSP_1:def 7
.= a * a + (a * (-b) + (b * a + b * (-b))) by RLVECT_1:def 3
.= a * a + ((a * (-b) + b * a) + b * (-b)) by RLVECT_1:def 3
.= a * a + ((-(a * b) + b * a) + b * (-b)) by VECTSP_1:8
.= a * a + (0.R + b * (-b)) by RLVECT_1:5
.= a^2 - b^2 by VECTSP_1:8;
end;
P5b:
for R being non degenerated Ring holds Char R = 2 iff 2 '*' 1.R = 0.R
proof
let R be non degenerated Ring;
now assume AS: 2 '*' 1.R = 0.R;
now let m be positive Nat;
assume m < 2; then m < 1 + 1; then m <= 1 by NAT_1:13;
then m = 0 or ... or m = 1;
hence m '*' 1.R <> 0.R by RING_3:60;
end;
hence Char R = 2 by AS,RING_3:def 5;
end;
hence thesis by RING_3:def 5;
end;
theorem sq00:
for R being domRing,
a,b being Element of R holds a^2 = b^2 iff (a = b or a = -b)
proof
let R be domRing, a,b be Element of R;
hereby assume a^2 = b^2;
then 0.R = a^2 - b^2 by RLVECT_1:15
.= (a + b) * (a - b) by P4a;
then per cases by VECTSP_2:def 1;
suppose a + b = 0.R;
hence a = b or a = -b by RLVECT_1:6;
end;
suppose a - b = 0.R;
hence a = b or a = -b by RLVECT_1:21;
end;
end;
assume a = b or a = -b;
then per cases;
suppose a = b;
hence a^2 = b^2;
end;
suppose a = -b;
hence a^2 = b^2 by VECTSP_1:10;
end;
end;
theorem XZ:
for F being Field, a being non zero Element of F holds (-a)" = -(a")
proof
let F be Field, a be non zero Element of F;
X: a" is non zero & -a" is non zero by VECTSP_1:25;
(-a") * (-a) = (a") * a by VECTSP_1:10
.= 1_F by X,VECTSP_2:9;
hence (-a)" = -(a") by VECTSP_2:10;
end;
theorem YY:
for F being Field, a being non zero Element of F holds (-a")" = -a
proof
let F be Field, a be non zero Element of F;
X: a" is non zero & -a" is non zero by VECTSP_1:25;
(-a"") * (-a") = (a"") * a" by VECTSP_1:10
.= 1_F by X,VECTSP_2:9;
hence (-a")" = -a by VECTSP_2:10;
end;
theorem YZ:
for F being Field, a being non zero Element of F holds -((-a)") = a"
proof
let F be Field, a be non zero Element of F;
a" - -((-a)") = a" + -(a") by XZ
.= 0.F by RLVECT_1:5;
hence thesis by RLVECT_1:21;
end;
theorem P5a:
for F being Field,
a being Element of F,
b being non zero Element of F holds (a / b)^2 = (a^2) / (b^2)
proof
let F be Field; let a be Element of F, b be non zero Element of F;
H1: b <> 0.F;
thus (a / b)^2 = a * (b" * (a * b")) by GROUP_1:def 3
.= a * (a * (b" * b")) by GROUP_1:def 3
.= (a * a) * (b" * b") by GROUP_1:def 3
.= (a^2) / (b^2) by VECTSP_2:11,H1;
end;
theorem P5:
for F being Field st Char F <> 2
for a being Element of F
holds ((a + 1.F) / (2 '*' 1.F))^2 - ((a - 1.F) / (2 '*' 1.F))^2 = a
proof
let F be Field; assume AS: Char F <> 2; let a be Element of F;
2 '*' 1.F <> 0.F by AS,P5b;
then A1: (2 '*' 1.F) * (2 '*' 1.F) <> 0.F by VECTSP_1:12;
then C: (2 * 2) '*' 1.F <> 0.F by RING_3:67;
D: 2 '*' 1.F is non zero by AS,P5b;
thus ((a + 1.F) / (2 '*' 1.F))^2 - ((a - 1.F) / (2 '*' 1.F))^2
= (a + 1.F)^2 / (2 '*' 1.F)^2 - ((a - 1.F) / (2 '*' 1.F))^2 by D,P5a
.= (a + 1.F)^2 / (2 '*' 1.F)^2 - (a - 1.F)^2 / (2 '*' 1.F)^2 by D,P5a
.= ((a + 1.F)^2 - (a - 1.F)^2) / (2 '*' 1.F)^2 by A1,VECTSP_2:20
.= ((a^2 + 2 '*' a * 1.F + (1.F)^2) - (a - 1.F)^2)
/ (2 '*' 1.F)^2 by P3
.= ((a^2 + 2 '*' a + (1.F)^2) - (a^2 - 2 '*' a * 1.F + (1.F)^2))
/ (2 '*' 1.F)^2 by P4
.= ((a^2 + 2 '*' a + (1.F)^2) + (-(a^2 + -(2 '*' a)) + -(1.F)^2))
/ (2 '*' 1.F)^2 by RLVECT_1:31
.= ((a^2 + 2 '*' a + (1.F)^2) + (-(a^2) + --(2 '*' a) + -(1.F)^2))
/ (2 '*' 1.F)^2 by RLVECT_1:31
.= ((a^2 + 2 '*' a) + ((1.F)^2 + ((-(1.F)^2) + (-(a^2) + (2 '*' a)))))
/ (2 '*' 1.F)^2 by RLVECT_1:def 3
.= ((a^2 + 2 '*' a) + (((1.F)^2 + (-(1.F)^2)) + (-(a^2) + (2 '*' a))))
/ (2 '*' 1.F)^2 by RLVECT_1:def 3
.= ((a^2 + 2 '*' a) + (0.F + (-(a^2) + (2 '*' a))))
/ (2 '*' 1.F)^2 by RLVECT_1:5
.= (2 '*' a + ((a^2) + (-(a^2) + (2 '*' a)))) / (2 '*' 1.F)^2
by RLVECT_1:def 3
.= (2 '*' a + (((a^2) + -(a^2)) + (2 '*' a))) / (2 '*' 1.F)^2
by RLVECT_1:def 3
.= (2 '*' a + (0.F + (2 '*' a))) / (2 '*' 1.F)^2 by RLVECT_1:5
.= ((2 + 2) '*' a) / (2 '*' 1.F)^2 by RING_3:62
.= (4 '*' a) / ((2 * 2) '*' 1.F) by RING_3:67
.= (4 '*' (1.F * a)) / (4 '*' 1.F)
.= ((4 '*' 1.F) * a) / (4 '*' 1.F) by c1
.= a / ((4 '*' 1.F) / (4 '*' 1.F)) by C,VECTSP_2:21
.= a / 1_F by C,VECTSP_2:17
.= a;
end;
registration
cluster preordered -> 0-characteristic for non degenerated Ring;
coherence by REALALG1:28;
end;
theorem v1a:
for R being preordered Ring,
P being Preordering of R holds (-P) * P = P * (-P)
proof
let R be preordered Ring, P be Preordering of R;
A: now let o be object;
assume o in (-P) * P;
then consider a,b being Element of R such that
A1: o = a * b & a in -P & b in P;
consider c being Element of R such that
A2: a = -c & c in P by A1;
A3: -b in -P by A1;
c * (-b) = -(c * b) by VECTSP_1:8
.= a * b by A2,VECTSP_1:9;
hence o in P * (-P) by A1,A2,A3;
end;
now let o be object;
assume o in P * (-P);
then consider a,b being Element of R such that
A1: o = a * b & a in P & b in -P;
consider c being Element of R such that
A2: b = -c & c in P by A1;
A3: -a in -P by A1;
(-a) * c = -(a * c) by VECTSP_1:9
.= a * b by A2,VECTSP_1:8;
hence o in (-P) * P by A1,A2,A3;
end;
hence thesis by A,TARSKI:2;
end;
theorem v1:
for R being preordered Ring,
P being Preordering of R holds (-P) + (-P) c= -P & (-P) * (-P) c= P
proof
let R be preordered Ring, P be Preordering of R;
X: P + P c= P & P * P c= P by REALALG1:def 14;
hereby let o be object;
assume o in (-P) + (-P);
then consider a,b being Element of R such that
A: o = a + b & a in -P & b in -P;
-a in -- P & -b in --P by A;
then (-a) + (-b) in P + P;
then -a + -b in P by X;
then -(a+b) in P by RLVECT_1:31;
then --(a+b) in -P;
hence o in -P by A;
end;
let o be object;
assume o in (-P) * (-P);
then consider a,b being Element of R such that
A: o = a * b & a in -P & b in -P;
-a in -- P & -b in --P by A;
then (-a) * (-b) in P * P;
then (-a) * (-b) in P by X;
hence o in P by A,VECTSP_1:10;
end;
theorem v2:
for R being preordered Ring,
P being Preordering of R holds (-P) * P c= -P & P * (-P) c= -P
proof
let R be preordered Ring, P be Preordering of R;
hereby let o be object;
assume o in (-P) * P;
then consider a,b being Element of R such that
A: o = a * b & a in -P & b in P;
-b in -P by A;
then B: a * (-b) in (-P) * (-P) by A;
(-P) * (-P) c= P by v1;
then a * (-b) in P by B;
then -(a * b) in P by VECTSP_1:8;
then --(a * b) in -P;
hence o in -P by A;
end; then
(-P) * P c= -P;
hence thesis by v1a;
end;
theorem spa:
for R being preordered Ring,
P being Preordering of R for n being Nat holds n '*' 1.R in P
proof
let R be preordered Ring, P be Preordering of R;
X: P + P c= P by REALALG1:def 14;
defpred P[Nat] means $1 '*' 1.R in P;
0 '*' 1.R = 0.R by RING_3:59; then
IA: P[0] by REALALG1:25;
IS: now let k be Nat;
assume IV: P[k];
A: (k+1) '*' 1.R = k '*' 1.R + 1 '*' 1.R by RING_3:62
.= k '*' 1.R + 1.R by RING_3:60;
1.R in P by REALALG1:25;
then (k+1) '*' 1.R in P + P by IV,A;
hence P[k+1] by X;
end;
I: for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
thus thesis by I;
end;
Lm8: for i be Integer holds i '*' 1.(INT.Ring) = i
proof
let i be Integer;
set R = INT.Ring;
defpred P[Integer] means $1 = $1 '*' 1.R;
0 '*' 1.R = 0.R by RING_3:59;
then A1: P[0];
A2: now let u be Integer;
assume A3: P[u];
(u-1) '*' 1.R = u '*' 1.R - 1 '*' 1.R by RING_3:64
.= u - 1 by A3,RING_3:60;
hence P[u-1];
(u+1) '*' 1.R = u '*' 1.R + 1 '*' 1.R by RING_3:62
.= u + 1 by A3,RING_3:60;
hence P[u+1];
end;
for k being Integer holds P[k] from INT_1:sch 4(A1,A2);
hence i '*' 1.(INT.Ring) = i;
end;
Lm9: for i be Integer holds i '*' 1.(F_Rat) = i
proof
let i be Integer;
set R = F_Rat;
defpred P[Integer] means $1 = $1 '*' 1.R;
0 '*' 1.R = 0.R by RING_3:59;
then A1: P[0] by GAUSSINT:def 14;
A2: now let u be Integer;
assume A3: P[u];
(u-1) '*' 1.R = u '*' 1.R - 1 '*' 1.R by RING_3:64
.= u - 1 by A3,GAUSSINT:def 14,RING_3:60;
hence P[u-1];
(u+1) '*' 1.R = u '*' 1.R + 1 '*' 1.R by RING_3:62
.= u + 1 by A3,GAUSSINT:def 14,RING_3:60;
hence P[u+1];
end;
for k being Integer holds P[k] from INT_1:sch 4(A1,A2);
hence i '*' 1.R = i;
end;
registration
cluster -> spanning for Preordering of INT.Ring;
coherence
proof
set R = INT.Ring;
let P be Preordering of INT.Ring;
now let o be object;
assume o in the carrier of R;
then consider n being Nat such that B: o = n or o = -n by INT_1:2;
A: n '*' 1.R = n by Lm8;
C: -(n '*' 1.R) = -n by Lm8;
per cases by B;
suppose o = n;
then o in P by A,spa;
hence o in P \/ (-P) by XBOOLE_0:def 3;
end;
suppose K: o = -n;
n in P by A,spa;
then -n in -P by C;
hence o in P \/ (-P) by K,XBOOLE_0:def 3;
end;
end;
then the carrier of R = P \/ (-P) by TARSKI:def 3;
hence P is spanning;
end;
cluster -> spanning for Preordering of F_Rat;
coherence
proof
set R = F_Rat;
let P be Preordering of R;
A: 0.(F_Rat) = 0 & 1.(F_Rat) = 1 by GAUSSINT:def 14;
E: P + P c= P & P * P c= P by REALALG1:def 14;
H: (-P) * P c= -P by v2;
now let o be object;
assume o in the carrier of R;
then reconsider p = o as Rational;
set m = numerator p, n = denominator p;
reconsider a=n,b=m as Element of F_Rat
by INT_1:def 2,NUMBERS:14,GAUSSINT:def 14;
G: a <> 0.R by GAUSSINT:def 14;
F: p = m * n" by RAT_1:15 .= b * a" by G,GAUSSINT:15;
per cases;
suppose m = 0;
then p = 0;
then o in P by A,REALALG1:25;
hence o in P\/-P by XBOOLE_0:def 3;
end;
suppose 0 < m;
then reconsider m1 = m as Element of NAT by INT_1:3;
C: n '*' 1.R = n & m1 '*' 1.R = m1 by Lm9;
then D: a in P & b in P by spa;
a is non zero by GAUSSINT:def 14;
then a" in P by C,spa,REALALG1:27;
then b * a" in P * P by D;
hence o in P\/-P by E,F,XBOOLE_0:def 3;
end;
suppose m < 0;
then reconsider m1 = -m as Element of NAT by INT_1:3;
E: n '*' 1.R = n & m1 '*' 1.R = m1 by Lm9;
then a in P & -b in P by spa;
then D: a in P & --b in -P;
a is non zero by GAUSSINT:def 14;
then a" in P by E,spa,REALALG1:27;
then b * a" in (-P) * P by D;
hence o in P\/-P by F,H,XBOOLE_0:def 3;
end;
end;
then the carrier of R = P \/ (-P) by TARSKI:def 3;
hence P is spanning;
end;
cluster -> spanning for Preordering of F_Real;
coherence
proof
set R = F_Real;
let P be Preordering of R;
A: SQ R c= P by REALALG1:def 14;
now let o be object;
assume o in the carrier of R;
then reconsider x = o as Element of REAL;
per cases;
suppose B: 0 <= x;
reconsider r = sqrt(x) as Element of REAL by XREAL_0:def 1;
reconsider a = r as Element of F_Real;
x = (sqrt x)^2 by SQUARE_1:def 2,B
.= a * a
.= a|^2 by RING_5:3;
then x in SQ R;
hence o in P \/-P by A,XBOOLE_0:def 3;
end;
suppose B:x <= 0;
reconsider r = sqrt(-x) as Element of REAL by XREAL_0:def 1;
reconsider a = r as Element of F_Real;
C: -x = (sqrt (-x))^2 by SQUARE_1:def 2,B
.= a * a
.= a|^2 by RING_5:3;
then -x in SQ R;
then -(a|^2) in -P by A,C;
hence o in P \/-P by C,XBOOLE_0:def 3;
end;
end;
then the carrier of R = P \/ (-P) by TARSKI:def 3;
hence P is spanning;
end;
end;
theorem
for P being Preordering of INT.Ring holds P = Positives(INT.Ring)
by REALALG1:40;
theorem
for P being Preordering of F_Rat holds P = Positives(F_Rat)
by REALALG1:38;
theorem
for P being Preordering of F_Real holds P = Positives(F_Real)
by REALALG1:36;
begin :: More on Ring Characteristics
theorem
for R being Ring holds Char R = 1 iff R is degenerated
proof
let R be Ring;
hereby assume Char R = 1;
then 1 '*' 1.R = 0.R & 1 <> 0 &
for m being positive Nat st m < 1 holds m '*' 1.R <> 0.R
by RING_3:def 5;
hence R is degenerated by RING_3:60;
end;
assume R is degenerated;
then A: 1 '*' 1.R = 0.R by RING_3:60;
for m being positive Nat st m < 1 holds m'*'1.R <> 0.R by NAT_1:14;
hence Char R = 1 by A,RING_3:def 5;
end;
theorem
for R being non degenerated Ring holds Char R = 2 iff 2 '*' 1.R = 0.R by P5b;
theorem char4:
for R being domRing
holds Char R = 0 iff
for a being non zero Element of R,
n being non zero Nat holds n '*' a <> 0.R
proof
let R be domRing;
hereby assume AS: Char R = 0;
now given a being non zero Element of R,
n being non zero Nat such that H: n '*' a = 0.R;
0.R = n '*' (1.R * a) by H
.= (n '*' 1.R) * a by c1;
then n '*' 1.R = 0.R by VECTSP_2:def 1;
hence contradiction by AS,RING_3:def 5;
end;
hence for a being non zero Element of R,
n being non zero Nat holds n '*' a <> 0.R;
end;
assume AS: for a being non zero Element of R,
n being non zero Nat holds n '*' a <> 0.R;
now
assume Char R <> 0;
then H1: CharSet R <> {} by RING_3:78;
let x be Element of CharSet R;
x in CharSet R by H1;
then ex n being positive Nat st x = n & n '*' 1.R = 0.R;
hence contradiction by AS;
end;
hence Char R = 0;
end;
theorem tA:
for R being 0-characteristic domRing,
a being Element of R
holds -a = a iff a = 0.R
proof
let R be 0-characteristic domRing, a be Element of R;
hereby assume -a = a;
then a + a = 0.R by RLVECT_1:5;
then C: 0.R = (1 '*' a) + a by RING_3:60
.= (1 '*' a) + (1 '*' a) by RING_3:60
.= (1+1) '*' a by RING_3:62;
Char R = 0 by RING_3:def 6;
then a is zero by C,char4;
hence a = 0.R;
end;
thus thesis;
end;
begin :: Maximal Preorderings
definition
let R be preordered Ring,
P be Preordering of R;
attr P is maximal means :defmax:
for Q being Preordering of R st P c= Q holds P = Q;
end;
theorem T2: :: Serre
for F being preordered Field,
P being Preordering of F,
a being Element of F
st not -a in P holds P + a * P is Preordering of F
proof
let F be preordered Field, P be Preordering of F, a be Element of F;
assume ASS: not -a in P;
X: 0.F in P & 1.F in P & P + P c= P & P * P c= P &
P /\ (-P) = {0.F} & SQ F c= P by REALALG1:25,REALALG1:def 14;
set S = P + a * P;
A: S + S c= S
proof let o be object;
assume o in S + S;
then consider c,b being Element of F such that
H1: o = c + b & c in S & b in S;
consider c1,c2 being Element of F such that
H2: c = c1 + c2 & c1 in P & c2 in a*P by H1;
consider b1,b2 being Element of F such that
H3: b = b1 + b2 & b1 in P & b2 in a*P by H1;
consider c3 being Element of F such that H4: c2 = a * c3 & c3 in P by H2;
consider b3 being Element of F such that H5: b2 = a * b3 & b3 in P by H3;
H6: c3 + b3 in P + P by H4,H5;
c2 + b2 = a * (c3 + b3) by H4,H5,VECTSP_1:def 3;
then H7: c2 + b2 in a * P by H6,X;
H8: c1 + b1 in P + P by H3,H2;
(c1+b1) + (c2+b2) = ((c1 + b1) + c2) + b2 by RLVECT_1:def 3
.= ((c1 + c2) + b1) + b2 by RLVECT_1:def 3
.= o by H1,H2,H3,RLVECT_1:def 3;
hence o in S by H8,H7,X;
end;
B: S * S c= S
proof let o be object;
assume o in S * S;
then consider c,b being Element of F such that
H1: o = c * b & c in S & b in S;
consider c1,c2 being Element of F such that
H2: c = c1 + c2 & c1 in P & c2 in a*P by H1;
consider b1,b2 being Element of F such that
H3: b = b1 + b2 & b1 in P & b2 in a*P by H1;
consider c3 being Element of F such that H4: c2 = a * c3 & c3 in P by H2;
consider b3 being Element of F such that H5: b2 = a * b3 & b3 in P by H3;
H6: o
= c1 * (b1 + a*b3) + (a*c3) * (b1 + a*b3) by H1,H2,H3,H4,H5,VECTSP_1:def 3
.= (c1 * b1 + c1 * (a * b3)) + (a * c3) * (b1 + a * b3) by VECTSP_1:def 2
.= (c1 * b1 + c1 * (a * b3)) +
((a * c3) * b1 + (a * c3) * (a * b3)) by VECTSP_1:def 2
.= c1 * b1 + (c1 * (a * b3) +
((a * c3) * b1 + (a * c3) * (a * b3))) by RLVECT_1:def 3
.= c1 * b1 + ((c1 * (a * b3) + (a * c3) * b1) +
(a * c3) * (a * b3)) by RLVECT_1:def 3
.= c1 * b1 + ((a * (c1 * b3) + (a * c3) * b1) +
(a * c3) * (a * b3)) by GROUP_1:def 3
.= c1 * b1 + ((a * (c1 * b3) + a * (c3 * b1)) +
(a * c3) * (a * b3)) by GROUP_1:def 3
.= c1 * b1 + (a * (c1 * b3 + c3 * b1) +
(a * c3) * (a * b3)) by VECTSP_1:def 2
.= c1 * b1 + (a * (c1 * b3 + c3 * b1) +
((a * c3) * a) * b3) by GROUP_1:def 3
.= c1 * b1 + (a * (c1 * b3 + c3 * b1) +
((a * a) * c3) * b3) by GROUP_1:def 3
.= c1 * b1 + (a * (c1 * b3 + c3 * b1) +
(a * a) * (c3 * b3)) by GROUP_1:def 3
.= (c1 * b1 + (a * a) * (c3 * b3)) + a * (c1 * b3 + c3 * b1)
by RLVECT_1:def 3;
E1: c1 * b1 in {c*b where c,b is Element of F : c in P & b in P} by H2,H3;
E2: c3 * b3 in {c*b where c,b is Element of F : c in P & b in P} by H4,H5;
a * a = (a|^1) * a by BINOM:8
.= (a|^1) * (a|^1) by BINOM:8
.= a|^(1+1) by BINOM:10
.= a^2 by RING_5:3;
then a * a in P by REALALG1:23;
then (a * a) * (c3 * b3) in {c*b where c,b is Element of F : c in P & b in P}
by E2,X;
then E3: c1 * b1 + (a * a) * (c3 * b3) in
{c1+c2 where c1,c2 is Element of F : c1 in P & c2 in P} by X,E1;
E4: c1 * b3 in {c*b where c,b is Element of F : c in P & b in P} by H2,H5;
c3 * b1 in {c*b where c,b is Element of F : c in P & b in P} by H4,H3;
then c1 * b3 + c3 * b1 in
{c1+c2 where c1,c2 is Element of F : c1 in P & c2 in P} by X,E4;
then a * (c1 * b3 + c3 * b1) in a * P by X;
hence o in S by H6,E3,X;
end;
P c= S by X,P1;
then C: SQ F c= S by X;
now assume -1.F in S;
then consider c1,c2 being Element of F such that
H2: -1.F = c1 + c2 & c1 in P & c2 in a*P;
consider c3 being Element of F such that H3: c2 = a * c3 & c3 in P by H2;
0.F = (c1 + a * c3) + 1.F by H2,H3,RLVECT_1:5
.= (c1 + 1.F) + a * c3 by RLVECT_1:def 3;
then H4: - a * c3 = ((c1 + 1.F) + a * c3) - a * c3
.= (c1 + 1.F) + (a * c3 + (- a * c3)) by RLVECT_1:def 3
.= (c1 + 1.F) + 0.F by RLVECT_1:5;
c3 <> 0.F by H2,H3,REALALG1:26;
then c3" * c3 = 1.F by VECTSP_1:def 10;
then H5: -a = (-a) * (c3 * c3")
.= ((-a) * c3) * c3" by GROUP_1:def 3
.= (c1 + 1.F) * c3" by H4,VECTSP_1:9;
H: c1+1.F in {c1+c2 where c1,c2 is Element of F : c1 in P & c2 in P} by H2,X;
c3 is non zero by H2,H3,REALALG1:26;
then c3" in P by H3,REALALG1:27;
then -a in {c1*c2 where c1,c2 is Element of F : c1 in P & c2 in P} by H5,H,X;
hence contradiction by ASS,X;
end;
then S /\ (-S) = {0.F} by C,B,REALALG1:21;
hence thesis by A,B,C,REALALG1:def 14;
end;
theorem T1:
for F being preordered Field,
P being Preordering of F holds P is maximal iff P is positive_cone
proof
let R be preordered Field, P be Preordering of R;
hereby assume AS: P is maximal;
now let x be object;
assume x in the carrier of R;
then reconsider a = x as Element of R;
now assume AS1: not(a in P);
now assume not(-a in P);
then reconsider Q = P + a * P as Preordering of R by T2;
C: 0.R in P by REALALG1:25;
then X: P = Q by AS,P1;
1.R in P by REALALG1:25;
hence contradiction by P2,C,X,AS1;
end;
then --a in -P;
hence a in -P;
end;
hence x in P \/ (-P) by XBOOLE_0:def 3;
end;
then the carrier of R c= P \/ (-P);
then P \/ (-P) = the carrier of R;
then P is spanning;
hence P is positive_cone;
end;
assume AS: P is positive_cone;
assume not P is maximal;
then consider Q being Preordering of R such that A: P c= Q & P <> Q;
P c< Q by A; then
consider a being object such that B: a in Q & not(a in P) by XBOOLE_0:6;
reconsider a as Element of R by B;
a in (-P) by AS,B,XBOOLE_0:def 3;
then -a in --P;
then --a in -Q by A;
then a in Q /\ (-Q) by B;
then a in {0.R} by REALALG1:def 7;
then a = 0.R by TARSKI:def 1;
hence contradiction by B,REALALG1:25;
end;
registration
let F be preordered Field;
cluster spanning -> maximal for Preordering of F;
coherence by T1;
cluster maximal -> spanning for Preordering of F;
coherence
proof
let P be Preordering of F;
assume P is maximal;
then P is positive_cone by T1;
hence thesis;
end;
end;
theorem T3:
for F being preordered Field,
P being Preordering of F
ex Q being Preordering of F st P c= Q & Q is maximal
proof
let F be preordered Field, P be Preordering of F;
set S = {O where O is Preordering of F: P c= O};
set R = RelIncl S;
A2: field R = S &
for Y,Z being set st Y in S & Z in S holds [Y,Z] in R iff Y c= Z
by WELLORD2:def 1;
A3: S has_upper_Zorn_property_wrt R
proof
now let Y be set;
assume AS: Y c= S & R|_2 Y is being_linear-order;
H1: now let z be set;
assume z in S;
then consider p being Preordering of F such that H: z = p & P c= p;
thus P c= z & z is Preordering of F by H;
end;
H2: P in S & R |_2 Y = R /\ [:Y,Y:];
H3: R|_2 Y is connected by AS,ORDERS_1:def 6;
H5: now let z1,z2 be set;
assume HH0: z1 in Y & z2 in Y;
per cases;
suppose z1 = z2;
hence z1 c= z2 or z2 c= z1;
end;
suppose HH1: z1 <> z2;
z1 in field(R|_2 Y) & z2 in field(R|_2 Y) by HH0,A2,AS,ORDERS_1:71;
then [z1,z2] in (R|_2 Y) or [z2,z1] in (R|_2 Y)
by H3,HH1,RELAT_2:def 6,RELAT_2:def 14;
then [z1,z2] in R or [z2,z1] in R by XBOOLE_0:def 4;
hence z1 c= z2 or z2 c= z1 by HH0,AS,WELLORD2:def 1;
end;
end;
set M = union Y;
per cases;
suppose Y = {};
then for y being set st y in Y holds [y,P] in R;
hence ex x being set st x in S &
for y being set st y in Y holds [y,x] in R by H2;
end;
suppose H: Y <> {};
A7: M c= the carrier of F
proof let o be object;
assume o in M;
then consider s being set such that H: o in s & s in Y by TARSKI:def 4;
s is Preordering of F by H1,H,AS;
hence o in the carrier of F by H;
end;
A8a: ex s being set st 0.F in s & s in Y
proof
set s = the Element of Y;
s in Y by H;
then s is Preordering of F by AS,H1;
hence thesis by H,REALALG1:25;
end;
then A8: 0.F in M by TARSKI:def 4;
reconsider M as non empty Subset of F by A7,A8a,TARSKI:def 4;
A6: M is Preordering of F
proof
A10: M + M c= M
proof
let o be object;
assume o in M + M;
then consider a,b being Element of F such that
A11: o = a + b & a in M & b in M;
consider sa being set such that A12: a in sa & sa in Y
by A11,TARSKI:def 4;
consider sb being set such that A13: b in sb & sb in Y
by A11,TARSKI:def 4;
reconsider sa,sb as Preordering of F by A12,A13,AS,H1;
A16: sa + sa c= sa & sb + sb c= sb by REALALG1:def 14;
per cases by A12,A13,H5;
suppose sa c= sb;
then a + b in sb + sb by A12,A13;
hence o in M by A16,A11,A13,TARSKI:def 4;
end;
suppose sb c= sa;
then a + b in sa + sa by A12,A13;
hence o in M by A16,A11,A12,TARSKI:def 4;
end;
end;
A11: M * M c= M
proof
let o be object;
assume o in M * M;
then consider a,b being Element of F such that
A11: o = a * b & a in M & b in M;
consider sa being set such that A12: a in sa & sa in Y
by A11,TARSKI:def 4;
consider sb being set such that A13: b in sb & sb in Y
by A11,TARSKI:def 4;
reconsider sa,sb as Preordering of F by A12,A13,AS,H1;
A16: sa * sa c= sa & sb * sb c= sb by REALALG1:def 14;
per cases by A12,A13,H5;
suppose sa c= sb;
then a * b in sb * sb by A12,A13;
hence o in M by A11,A13,A16,TARSKI:def 4;
end;
suppose sb c= sa;
then a * b in sa * sa by A12,A13;
hence o in M by A16,A11,A12,TARSKI:def 4;
end;
end;
A12: M /\ (-M) = {0.F}
proof
A13: now let o be object;
assume o in {0.F};
then A14: o = -0.F by TARSKI:def 1;
then o in -M by A8;
hence o in M /\ - M by A14,A8;
end;
now let o be object;
assume A14: o in M /\ - M;
then A14a: o in M & o in -M by XBOOLE_0:def 4;
then consider so being set such that A15: o in so & so in Y
by TARSKI:def 4;
consider p being Element of F such that A16: o = -p & p in M
by A14a;
consider sp being set such that A17: p in sp & sp in Y
by A16,TARSKI:def 4;
reconsider so,sp as Preordering of F by AS,A15,A17,H1;
reconsider o1 = o as Element of F by A14;
per cases by A15,A17,H5;
suppose A19: so c= sp;
o in -sp by A16,A17;
then o in sp /\ -sp by A19,A15;
hence o in {0.F} by REALALG1:def 14;
end;
suppose sp c= so;
then o in -so by A16,A17;
then o in so /\ -so by A15;
hence o in {0.F} by REALALG1:def 7;
end;
end;
hence thesis by A13,TARSKI:2;
end;
SQ F c= M
proof
let o be object;
assume A13: o in SQ F;
set s = the Element of Y;
s in Y by H;
then A15: P c= s by H1,AS;
SQ F c= P by REALALG1:def 14;
then o in s by A13,A15;
hence o in M by H,TARSKI:def 4;
end;
hence thesis by A10,A11,A12,REALALG1:def 14;
end;
P c= M
proof
let o be object;
assume H0: o in P;
set s = the Element of Y;
s in Y by H;
then P c= s by H1,AS;
hence o in M by H0,H,TARSKI:def 4;
end;
then A4: M in S by A6;
now let y be set;
assume A5: y in Y;
then y c= M by TARSKI:def 4;
hence [y,M] in R by AS,A4,A5,WELLORD2:def 1;
end;
hence ex x being set st x in S &
for y being set st y in Y holds [y,x] in R by A4;
end;
end;
hence thesis by ORDERS_1:def 10;
end;
R is_reflexive_in S & R is_transitive_in S by WELLORD2:19,20;
then R partially_orders S by WELLORD2:21,ORDERS_1:def 8;
then consider x being set such that
M: x is_maximal_in R by A2,A3,ORDERS_1:63;
x in field R by M,ORDERS_1:def 12;
then consider O being Preordering of F such that M1: x = O & P c= O by A2;
M4: O in S by M1;
now let Q be Preordering of F;
assume M2: O c= Q;
then P c= Q by M1;
then M5: Q in S;
then M3: Q in field R by WELLORD2:def 1;
[O,Q] in R by M4,M2,M5,WELLORD2:def 1;
hence O = Q by M3,M1,M,ORDERS_1:def 12;
end;
hence thesis by M1,defmax;
end;
registration
cluster -> ordered for preordered Field;
coherence
proof
let F be preordered Field;
ex Q being Preordering of F st the Preordering of F c= Q & Q is maximal by T3;
hence thesis;
end;
end;
theorem
for F being preordered Field,
P being Preordering of F holds P is maximal iff P is Ordering of F;
theorem T1a:
for F being preordered Field,
P being Preordering of F ex O being Ordering of F st P c= O
proof
let F be preordered Field, P be Preordering of F;
ex Q being Preordering of F st P c= Q & Q is maximal by T3;
hence thesis;
end;
definition
let R be ordered Ring;
let P be Preordering of R;
func /\(P,R) -> Subset of R equals
{x where x is Element of R :
for O being Ordering of R st P c= O holds x in O};
coherence
proof
now let x be object;
assume x in {x where x is Element of R :
for O being Ordering of R st P c= O holds x in O};
then ex x1 being Element of R st
x1 = x & for O being Ordering of R st P c= O holds x1 in O;
hence x in the carrier of R;
end;
hence thesis by TARSKI:def 3;
end;
end;
registration
let R be ordered Ring;
let P be Preordering of R;
cluster /\(P,R) -> non empty;
coherence
proof
for O being Ordering of R st P c= O holds 0.R in O by REALALG1:25;
then 0.R in {x where x is Element of R :
for O being Ordering of R st P c= O holds x in O};
hence thesis;
end;
end;
registration
let R be ordered Ring;
let P be Preordering of R;
cluster /\(P,R) -> add-closed mult-closed with_squares;
coherence
proof
set M = /\(P,R);
now let x,y be Element of R;
assume AS: x in M & y in M;
then consider a being Element of R such that
A: x = a & for O being Ordering of R st P c= O holds a in O;
consider b being Element of R such that
B: y = b & for O being Ordering of R st P c= O holds b in O by AS;
now let O be Ordering of R;
assume P c= O;
then a in O & b in O by A,B;
then C: a + b in O + O;
O + O c= O by REALALG1:def 14;
hence a + b in O by C;
end;
hence x + y in M by A,B;
end;
hence M is add-closed;
now let x,y be Element of R;
assume AS: x in M & y in M;
then consider a being Element of R such that
A: x = a & for O being Ordering of R st P c= O holds a in O;
consider b being Element of R such that
B: y = b & for O being Ordering of R st P c= O holds b in O by AS;
now let O be Ordering of R;
assume P c= O;
then a in O & b in O by A,B;
then C: a * b in O * O;
O * O c= O by REALALG1:def 14;
hence a * b in O by C;
end;
hence x * y in M by A,B;
end;
hence M is mult-closed;
X0: SQ R c= P by REALALG1:def 14;
now let o be object;
assume X2: o in SQ R;
then consider a being Element of R such that X1: o = a & a is square;
for O being Ordering of R st P c= O holds a in O by X0,X1,X2;
hence o in M by X1;
end;
then SQ R c= M;
hence M is with_squares;
end;
end;
s1: for F being preordered Field,
P being Preordering of F holds /\(P,F) = P
proof
let F be preordered Field, P be Preordering of F;
set M = /\(P,F);
A: now let o be object;
assume A1: o in P;
then reconsider a = o as Element of F;
for O being Ordering of F st P c= O holds a in O by A1;
hence o in M;
end;
now let o be object;
assume o in M;
then consider a being Element of F such that
A: o = a & for O being Ordering of F st P c= O holds a in O;
now assume B: not a in P;
then not -(-a) in P;
then reconsider P1 = P + (-a) * P as Preordering of F by T2;
consider O being Ordering of F such that H: P1 c= O by T1a;
H1: 0.F in P & 1.F in P by REALALG1:25;
then -a in P1 by P2;
then X: --a in -O by H;
P c= P1 by H1,P1;
then P c= O by H;
then a in O by A;
then a in O /\ -O by X;
then a in {0.F} by REALALG1:def 7;
then a = 0.F by TARSKI:def 1;
hence contradiction by B,REALALG1:25;
end;
hence o in P by A;
end;
hence thesis by A,TARSKI:2;
end;
registration
let F be ordered Field;
let P be Preordering of F;
cluster /\(P,F) -> negative-disjoint;
coherence by s1;
end;
theorem
for F being ordered Field,
P being Preordering of F holds /\(P,F) is Preordering of F;
theorem
for F being ordered Field,
P being Preordering of F holds /\(P,F) = P by s1;
begin :: Formally Real Fields
definition
let R be Ring;
attr R is formally_real means
not -1.R in QS R;
end;
lemma1:
for F being Field st F is formally_real holds QS F /\ (-QS F) = {0.F}
proof
let F be Field;
assume A: F is formally_real;
B: SQ F c= QS F by REALALG1:18;
QS F * QS F c= QS F
proof let o be object;
assume o in QS F * QS F;
then ex s1,s2 being Element of F st
o = s1 * s2 & s1 in QS F & s2 in QS F;
hence o in QS F by REALALG1:def 5;
end;
hence thesis by A,B,REALALG1:21;
end;
lemma2:
for R being preordered non degenerated Ring holds QS R <> the carrier of R
proof
let R be preordered non degenerated Ring;
set P = the Preordering of R;
QS R c= P & not -1.R in P by REALALG1:26,REALALG1:24;
hence thesis;
end;
lemma3:
for R being Field st Char R <> 2 & QS R <> the carrier of R
holds not -1.R in QS R
proof
let R be Field;
assume AS: Char R <> 2 & QS R <> the carrier of R;
assume -1.R in QS R; then
consider e being Element of R such that H: e = -1.R & e is sum_of_squares;
now let a be Element of R;
((a + 1.R) / (2 '*' 1.R))^2 + (-1.R) * ((a - 1.R) / (2 '*' 1.R))^2
= ((a + 1.R) / (2 '*' 1.R))^2 + -(1.R * ((a - 1.R) / (2 '*' 1.R))^2)
by VECTSP_1:9
.= ((a + 1.R) / (2 '*' 1.R))^2 - ((a - 1.R) / (2 '*' 1.R))^2
.= a by AS,P5;
hence a in QS R by H;
end;
then the carrier of R c= QS R;
hence contradiction by AS;
end;
theorem T0:
for F being Field st Char F <> 2 holds
F is formally_real iff QS F is prepositive_cone
proof
let F be Field;
assume AS: Char F <> 2;
hereby assume F is formally_real;
then QS F is negative-disjoint by lemma1;
hence QS F is prepositive_cone;
end;
assume QS F is prepositive_cone;
then F is preordered;
hence F is formally_real by AS,lemma3,lemma2;
end;
theorem
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
let F be Field;
assume AS: Char F <> 2;
hereby assume F is formally_real;
then QS F is negative-disjoint by lemma1;
hence ex P being Subset of F st P is prepositive_cone;
end;
assume ex P being Subset of F st P is prepositive_cone;
then F is preordered;
hence F is formally_real by AS,lemma3,lemma2;
end;
theorem T2:
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
let F be Field;
assume AS: Char F <> 2;
hereby assume F is formally_real;
then QS F is negative-disjoint by lemma1;
then F is preordered;
then F is ordered;
hence ex P being Subset of F st P is positive_cone;
end;
assume ex P being Subset of F st P is positive_cone;
then F is ordered;
hence F is formally_real by AS,lemma3,lemma2;
end;
theorem
for F being Field st Char F <> 2
holds F is formally_real iff QS F <> the carrier of F by lemma3;
registration
cluster formally_real -> ordered for Field;
coherence
proof
let F be Field;
assume F is formally_real;
then QS F is negative-disjoint by lemma1;
then F is preordered;
hence thesis;
end;
cluster ordered -> formally_real for Field;
coherence
proof
let F be Field;
assume AS: F is ordered;
then Char F = 0 by REALALG1:28;
hence thesis by AS,T2;
end;
end;
registration
cluster preordered -> formally_real for non degenerated Ring;
coherence
proof
let R be non degenerated Ring;
assume R is preordered;
then reconsider R as preordered Ring;
QS R c= the Preordering of R by REALALG1:24;
hence thesis by REALALG1:26;
end;
end;
registration
cluster formally_real for Field;
existence
proof
take F_Real;
thus thesis;
end;
end;
registration
let F be formally_real Field;
cluster QS F -> negative-disjoint;
coherence
proof
Char F = 0 by REALALG1:28;
then QS F is prepositive_cone by T0;
hence thesis;
end;
end;
theorem
for F being formally_real Field holds QS F is Preordering of F;
theorem :: Artin
for F being formally_real Field,
a being Element of F
holds (for O being Ordering of F holds a in O) iff a in QS F
proof
let F be formally_real Field, a be Element of F;
reconsider Q = QS F as Preordering of F;
hereby assume for O being Ordering of F holds a in O;
then for O being Ordering of F st Q c= O holds a in O;
then a in /\(Q,F);
hence a in QS F by s1;
end;
assume AS: a in QS F;
let O be Ordering of F;
QS F c= O by REALALG1:24;
hence a in O by AS;
end;
theorem
for r being Element of F_Rat st 0 <= r holds r is sum_of_squares
proof
let r be Element of F_Rat;
assume AS: 0 <= r;
r in { r where r is Element of RAT : 0 <= r } by AS,GAUSSINT:def 14;
then r in QS F_Rat by REALALG1:38;
then ex s being Element of F_Rat st s = r & s is sum_of_squares;
hence thesis;
end;
definition
let R be ZeroStr;
let f be (the carrier of R)-valued Function;
attr f is trivial means
for i being object st i in dom f holds f.i = 0.R;
end;
definition
let R be Ring;
let f be non empty FinSequence of R;
attr f is quadratic means :dq:
for i being Element of dom f holds f.i is square;
end;
registration
let R be non degenerated Ring;
cluster <*1.R*> -> quadratic non trivial for non empty FinSequence of R;
coherence
proof
set f = <*1.R*>;
1 in Seg 1 by FINSEQ_1:2,TARSKI:def 1;
then B: 1 in dom f by FINSEQ_1:38;
D: f.1 = 1.R;
now let i be Element of dom f;
dom f = Seg 1 by FINSEQ_1:38;
then i = 1 by TARSKI:def 1,FINSEQ_1:2;
hence f.i is square;
end;
hence thesis by D,B;
end;
end;
registration
let R be non degenerated Ring;
cluster quadratic non trivial for non empty FinSequence of R;
existence
proof
take <*1.R*>;
thus thesis;
end;
end;
theorem :: Artin-Schreier
for F being Field holds
F is formally_real iff
for f being quadratic non empty FinSequence of F
st Sum f = 0.F holds f is trivial
proof
let F be Field;
hereby assume AS: F is formally_real;
now assume not(for f being quadratic non empty FinSequence of F
st Sum f = 0.F holds f is trivial);
then consider f being quadratic non empty FinSequence of F such that
H1: Sum f = 0.F & f is non trivial;
consider i being Element of dom f such that H2: f.i <> 0.F by H1;
H7: len Swap(f,i,len f) = len f by FINSEQ_7:18;
then reconsider g = Swap(f,i,len f) as non empty FinSequence of F;
reconsider m = len f - 1 as Nat;
reconsider p = g|(Seg m) as FinSequence of F by FINSEQ_1:18;
p ^ <*f.i*> = g
proof
m + 1 = len g by FINSEQ_7:18;
then m <= len g by NAT_1:13;
then X2: len p = m & dom p = Seg m by FINSEQ_1:17;
X1: len(p ^ <*f.i*>) = len p + len<*f.i*> by FINSEQ_1:22
.= m + 1 by X2,FINSEQ_1:40
.= len g by FINSEQ_7:18;
now let k be Nat;
assume X3: 1 <= k & k <= len g;
then per cases by XXREAL_0:1;
suppose X4: k = len g;
then len p + 1 = k by X2,FINSEQ_7:18;
then X5: len p < k by NAT_1:13;
X7: 1 <= i <= len f & 1 <= len f by FINSEQ_1:20,FINSEQ_3:25;
thus (p ^ <*f.i*>).k = <*f.i*>.(k - len p) by X1,X4,X5,FINSEQ_1:24
.= f.i by X2,X4,H7
.= f/.i by X7,FINSEQ_4:15
.= g/.(len f) by X7,FINSEQ_7:31
.= g.k by X7,X4,H7,FINSEQ_4:15;
end;
suppose k < len g;
then k + 1 <= len g by NAT_1:13;
then (k + 1) - 1 <= len g - 1 by XREAL_1:9;
then X4: k <= m by FINSEQ_7:18;
then k in dom p by X2,X3,FINSEQ_1:1;
hence (p ^ <*f.i*>).k = p.k by FINSEQ_1:def 7
.= g.k by X2,X3,X4,FUNCT_1:47,FINSEQ_1:1;
end;
end;
hence thesis by X1,FINSEQ_1:14;
end;
then Sum p + Sum <*f.i*> = Sum g by RLVECT_1:41 .= 0.F by H1,GROEB_2:2;
then H4: Sum p * Sum<*f.i*>" = (-Sum<*f.i*>) * Sum<*f.i*>" by RLVECT_1:6
.= -(Sum<*f.i*> * Sum<*f.i*>") by VECTSP_1:9
.= -(Sum<*f.i*> * (f.i)") by RLVECT_1:44
.= -(f.i * (f.i)") by RLVECT_1:44
.= - 1.F by H2,VECTSP_1:def 10;
H5: Sum p in QS F
proof
now let j be Nat;
assume I0: j in dom p;
ex k being Element of dom f st p.j = f.k
proof
I2: dom p c= dom g by RELAT_1:60;
p.j = g.j by I0,FUNCT_1:47;
then I1: p.j in rng g by I0,I2,FUNCT_1:def 3;
p.j in rng f by I1,FINSEQ_7:22;
then ex x being object st
x in dom f & p.j = f.x by FUNCT_1:def 3;
hence thesis;
end;
then consider k being Element of dom f such that I1: p.j = f.k;
f.k is square by dq;
hence ex a being Element of F st p.j = a^2 by I1;
end;
then Sum p is sum_of_squares;
hence thesis;
end;
H6: Sum<*f.i*>" in QS F
proof
f.i is square by dq;
then consider a being Element of F such that I1: f.i = a^2;
I0: a <> 0.F by I1,H2;
(a")|^2 = a" * a" by RING_5:3
.= (f.i)" by I1,VECTSP_2:11,I0;
then (f.i)" in QS F;
hence thesis by RLVECT_1:44;
end;
QS F is mult-closed;
hence contradiction by AS,H4,H5,H6;
end;
hence for f being quadratic non empty FinSequence of F
st Sum f = 0.F holds f is trivial;
end;
assume AS: for f being quadratic non empty FinSequence of F
st Sum f = 0.F holds f is trivial;
now assume -1.F in QS F;
then consider e being Element of F such that
H1: e = -1.F & e is sum_of_squares;
consider f being FinSequence of F such that
H2: Sum f = -1.F &
for i being Nat st i in dom f ex a being Element of F st f.i = a^2
by H1;
set g = f ^ <*(1.F)*>;
H3: Sum g = Sum f + Sum<*(1.F)*> by RLVECT_1:41
.= -1.F + 1.F by H2,RLVECT_1:44
.= 0.F by RLVECT_1:5;
H5b: len g = len f + len<*(1.F)*> by FINSEQ_1:22
.= len f + 1 by FINSEQ_1:39;
then len f < len g by NAT_1:19;
then H5: g.(len g) = <*(1.F)*>.(len g - len f) by FINSEQ_1:24
.= 1.F by H5b;
H5a: 1 <= len g by H5b,NAT_1:11;
H4: g is quadratic
proof
now let i be Element of dom g;
I1: 1 <= i <= len g by FINSEQ_3:25;
per cases;
suppose i = len g;
hence g.i is square by H5;
end;
suppose i <> len g;
then i < ((len g) - 1) + 1 by I1,XXREAL_0:1;
then i2: i <= len f by H5b,NAT_1:13;
then i in dom f by I1,FINSEQ_3:25;
then g.i = f.i by FINSEQ_1:def 7;
hence g.i is square by i2,H2,I1,FINSEQ_3:25;
end;
end;
hence thesis;
end;
g is non trivial by H5,H5a,FINSEQ_3:25;
hence contradiction by H3,H4,AS;
end;
hence F is formally_real;
end;
registration
cluster -> non algebraic-closed for formally_real Field;
coherence
proof
let F be formally_real Field;
set P = the Ordering of F;
set p = npoly(F,2);
D: deg p = 2 by RING_5:43;
A: deg p + 1 = (len p - 1) + 1 by HURWITZ:def 2;
now assume F is algebraic-closed;
then consider a being Element of F such that
B: a is_a_root_of p by A,D,POLYNOM5:def 9,POLYNOM5:def 8;
0.F = eval(p,a) by B,POLYNOM5:def 7
.= a|^2 - -1.F by RING_5:46;
then -1.F = a|^2 by RLVECT_1:21 .= a^2 by RING_5:3;
then -1.F in QS F;
hence contradiction by REALALG1:26;
end;
hence thesis;
end;
end;
begin :: Order relations and strict order relations revisited
lemOP:
for R being preordered Ring,
P being Preordering of R,
a,b being Element of R holds a <=P, b iff a <=_(OrdRel P), b
proof
let R be preordered Ring, P be Preordering of R;
let a,b be Element of R;
now assume a <=_(OrdRel P), b;
then consider a1,b1 being Element of R such that
H: [a,b] = [a1,b1] & a1 <= P,b1;
a = a1 & b = b1 by H,XTUPLE_0:1;
hence a <=P, b by H;
end;
hence thesis;
end;
theorem c10a:
for R being preordered Ring,
P being Preordering of R,
a,b being Element of R holds a <=P, b iff (-b) <=P, (-a)
proof
let R be preordered Ring, P be Preordering of R, a,b be Element of R;
(-a) - (-b) = -a + b;
hence thesis;
end;
theorem c1:
for R being preordered Ring,
P being Preordering of R,
a being Element of R holds a <=P, a
proof
let R be preordered Ring, P be Preordering of R;
let a be Element of R;
a <=_(OrdRel P), a by REALALG1:1;
hence thesis by lemOP;
end;
theorem c2:
for R being preordered Ring,
P being Preordering of R,
a,b being Element of R st a <=P, b & b <=P, a holds a = b
proof
let R be preordered Ring, P be Preordering of R;
let a,b be Element of R;
assume a <=P, b & b <=P, a;
then a <=_(OrdRel P), b & b <=_(OrdRel P), a;
hence thesis by REALALG1:2;
end;
theorem c3:
for R being preordered Ring,
P being Preordering of R,
a,b,c being Element of R st a <=P, b & b <=P, c holds a <=P, c
proof
let R be preordered Ring, P be Preordering of R;
let a,b,c be Element of R;
assume a <=P, b & b <=P, c;
then a <=_(OrdRel P), b & b <=_(OrdRel P), c;
hence thesis by lemOP,REALALG1:3;
end;
theorem c4:
for R being preordered Ring,
P being Preordering of R,
a,b,c being Element of R st a <=P, b holds a+c <=P, b+c
proof
let R be preordered Ring, P be Preordering of R, a,b,c be Element of R;
assume a <= P, b;
then a <=_(OrdRel P), b;
hence thesis by lemOP,REALALG1:def 3;
end;
theorem c5:
for R being preordered Ring,
P being Preordering of R,
a,b,c being Element of R st a <= P,b & 0.R <=P, c holds a*c <= P, b*c
proof
let R be preordered Ring, P be Preordering of R, a,b,c be Element of R;
assume a <= P, b & 0.R <=P, c;
then a <=_(OrdRel P), b & 0.R <=_(OrdRel P), c;
hence thesis by lemOP,REALALG1:def 4;
end;
theorem c55:
for R being preordered Ring,
P being Preordering of R,
a,b,c being Element of R st a <= P,b & c <=P, 0.R holds b*c <= P, a*c
proof
let R be preordered Ring, P be Preordering of R, a,b,c be Element of R;
assume AS: a <= P, b & c <=P, 0.R;
then -0.R <=P, (-c);
then A: a * (-c) <=P, b * (-c) by AS,c5;
B: -(b * (-c)) = (-b) * (-c) by VECTSP_1:9 .= b * c by VECTSP_1:10;
-(a * (-c)) = (-a) * (-c) by VECTSP_1:9 .= a * c by VECTSP_1:10;
hence thesis by A,B,c10a;
end;
theorem avb4:
for R being ordered Ring,
O being Ordering of R,
a,b being Element of R holds a <=O, b or b <=O ,a
proof
let R be ordered Ring, O be Ordering of R, a,b be Element of R;
X: O \/ -O = the carrier of R by REALALG1:def 8;
assume not(a <=O, b);
then b - a in -O by X,XBOOLE_0:def 3;
then -(b - a) in --O;
hence b <=O, a by RLVECT_1:33;
end;
theorem fi1:
for F being preordered Field,
P being Preordering of F,
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
let F be preordered Field, P be Preordering of F,
a,b be non zero Element of F;
assume AS: 0.F <=P, a & 0.F <=P, b;
then X: 0.F <=P, a" & 0.F <=P, b" by REALALG1:27;
Y: a <> 0.F & b <> 0.F;
hereby assume a <=P, b;
then a * a" <=P, b * a" by X,c5;
then 1.F <=P, b * a" by Y,VECTSP_1:def 10;
then 1.F * b" <= P, (b * a") * b" by X,c5;
then b" <= P, (b" * b) * a" by GROUP_1:def 3;
then b" <= P, 1.F * a" by Y,VECTSP_1:def 10;
hence b" <=P, a";
end;
assume b" <=P, a";
then b" * b <=P, a" * b by AS,c5;
then 1.F <=P, a" * b by Y,VECTSP_1:def 10;
then 1.F * a <=P, (a" * b) * a by AS,c5;
then a <=P, (a" * a) * b by GROUP_1:def 3;
then a <=P, 1.F * b by Y,VECTSP_1:def 10;
hence a <=P, b;
end;
theorem fi2:
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 <=P, b iff b" <=P, a"
proof
let F be preordered Field, P be Preordering of F,
a,b be non zero Element of F;
assume AS: a <=P, 0.F & b <=P, 0.F;
Y: a <> 0.F & b <> 0.F;
-a <> -0.F & -b <> -0.F;
then -a is non zero & -b is non zero;
then -((-a)") <=P, -0.F & -((-b)") <=P, -0.F by AS,REALALG1:27;
then X: a" <=P, -0.F & b" <=P, -0.F by YZ;
hereby assume a <=P, b;
then b * a" <=P, a * a" by X,c55;
then b * a" <=P, 1.F by Y,VECTSP_1:def 10;
then 1.F * b" <= P, (b * a") * b" by X,c55;
then b" <= P, (b" * b) * a" by GROUP_1:def 3;
then b" <= P, 1.F * a" by Y,VECTSP_1:def 10;
hence b" <=P, a";
end;
assume b" <=P, a";
then a" * b <=P, b" * b by AS,c55;
then a" * b <=P, 1.F by Y,VECTSP_1:def 10;
then 1.F * a <=P, (a" * b) * a by AS,c55;
then a <=P, (a" * a) * b by GROUP_1:def 3;
then a <=P, 1.F * b by Y,VECTSP_1:def 10;
hence a <=P, b;
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
a <=P, b & a <> b;
end;
theorem c20:
for R being preordered non degenerated Ring,
P being Preordering of R holds 0.R <P, 1.R & -1.R <P, 0.R
proof
let R be preordered non degenerated Ring, P be Preordering of R;
0.R <=P, 1.R by REALALG1:25;
hence 0.R <P, 1.R;
-1.R <=P, 0.R by REALALG1:25;
hence -1.R <P, 0.R;
end;
theorem c10:
for R being preordered Ring,
P being Preordering of R,
a,b being Element of R holds a <P, b iff (-b) <P, (-a)
by c10a,RLVECT_1:18;
theorem
for R being ordered Ring,
O being Ordering of R,
a,b being Element of R holds a <O, b or b <O ,a or a = b by avb4;
theorem avb5:
for R being preordered Ring,
P being Preordering of R,
a,b,c being Element of R st a <P, b & b <=P, c holds a <P, c by c2,c3;
theorem avb6:
for R being preordered Ring,
P being Preordering of R,
a,b,c being Element of R st a <=P, b & b <P, c holds a <P, c by c2,c3;
theorem
for R being preordered Ring,
P being Preordering of R,
a,b,c being Element of R st a <P, b holds a + c <P, b + c
by c4,RLVECT_1:8;
theorem
for R being preordered domRing,
P being Preordering of R,
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
for R being preordered domRing,
P being Preordering of R,
a,b,c being Element of R st a <P, b & c <P, 0.R holds b * c <P, a * c
proof
let R be preordered domRing, P be Preordering of R, a,b,c be Element of R;
assume AS: a <P, b & c <P, 0.R;
then -0.R <P, (-c) by c10a,RLVECT_1:18;
then A: a * (-c) <P, b * (-c) by AS,c5,GCD_1:1;
B: -(b * (-c)) = (-b) * (-c) by VECTSP_1:9 .= b * c by VECTSP_1:10;
-(a * (-c)) = (-a) * (-c) by VECTSP_1:9 .= a * c by VECTSP_1:10;
hence thesis by A,B,c10a,RLVECT_1:18;
end;
theorem
for F being preordered Field,
P being Preordering of F,
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
let F be preordered Field, P be Preordering of F,
a,b be non zero Element of F;
assume AS: 0.F <=P, a & 0.F <=P, b;
Y: 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,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 <P, b iff b" <P, a"
proof
let F be preordered Field, P be Preordering of F,
a,b be non zero Element of F;
assume AS: a <=P, 0.F & b <=P, 0.F;
Y: 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 <P, a
proof
let R be preordered Ring, P be Preordering of R, a be Element of R;
hereby assume a is P-positive;
then a in P & not a in {0.R} by XBOOLE_0:def 5;
then 0.R <=P, a & a <> 0.R by TARSKI:def 1;
hence 0.R <P, a;
end;
assume 0.R <P, a;
then 0.R <=P, a & a <> 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 <P, 0.R
proof
let R be preordered Ring, P be Preordering of R, a be Element of R;
hereby assume a is P-negative;
then a in -P & not a in {0.R} by XBOOLE_0:def 5;
then -a in --P & not a in {0.R};
then a <=P, 0.R & a <> 0.R by TARSKI:def 1;
hence a <P, 0.R;
end;
assume a <P, 0.R;
then a <=P, 0.R & 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 <P, a by x1;
then B: 0.R <=P, a;
now assume a in -P \ {0.R};
then a is P-negative;
then -0.R <P, -a by x2,c10;
then 0.R <=P, -a;
then --a in -P;
then a in P /\ -P by B;
then a in {0.R} by REALALG1:def 7;
hence contradiction by A,TARSKI:def 1;
end;
hence thesis by A;
end;
cluster P-negative -> 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, 0.R by x2;
then a <=P, 0.R;
then B: --a in -P;
now assume a in P \ {0.R};
then a is P-positive;
then 0.R <P, a by x1;
then 0.R <=P, a;
then a in P /\ -P by B;
then a in {0.R} by REALALG1:def 7;
hence contradiction by A,TARSKI:def 1;
end;
hence thesis by A;
end;
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;
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 <O,a) by x1;
then a <O, 0.R or a = 0.R by avb4;
hence thesis by A,x2;
end;
cluster non zero non O-negative -> O-positive for Element of R;
coherence;
end;
theorem
for R being preordered Ring,
P being Preordering of R,
a being Element of R holds a is P-positive iff 0.R <P, a by x1;
theorem
for R being preordered Ring,
P being Preordering of R,
a being Element of R holds a is P-negative iff a <P, 0.R by x2;
theorem x1a:
for R being preordered Ring,
P being Preordering of R
for a being P-ordered Element of R holds a is non P-negative iff 0.R <=P, a
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-negative;
then per cases by XBOOLE_0:def 5;
suppose not a in -P;
hence 0.R <=P, a by H,XBOOLE_0:def 3;
end;
suppose a in {0.R};
then a = 0.R by TARSKI:def 1;
hence 0.R <=P, a by c1;
end;
end;
assume C: 0.R <=P, a;
per cases;
suppose a = 0.R;
then a in {0.R} by TARSKI:def 1;
hence a is non P-negative 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-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 :: redefines absolute_value (REALALG2, definition)
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 <O, abs(O,a) by avb5,c20;
per cases;
suppose a in O;
hence a is O-ordered by XBOOLE_0:def 3;
end;
suppose a in -O;
hence a is O-ordered by XBOOLE_0:def 3;
end;
suppose not(a in O) & not(a in -O);
hence a is O-ordered by C,defa;
end;
end;
assume a is O-ordered;
then per cases by XBOOLE_0:def 3;
suppose a in O;
hence 0.R <=O, abs(O,a) by defa;
end;
suppose D: a in -O;
then -a in --O;
hence 0.R <=O, abs(O,a) by D,defa;
end;
end;
theorem av00:
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
proof
let R be preordered non degenerated Ring, P be Preordering of R,
a be Element of R;
hereby assume not a is P-ordered;
then not(a in P) & not(a in -P) by XBOOLE_0:def 3;
hence abs(P,a) = -1.R by defa;
end;
assume AS: abs(P,a) = -1.R;
assume a is P-ordered;
then 0.R <=P, abs(P,a) by av0;
hence contradiction by AS,REALALG1:26;
end;
theorem
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
proof
let R be preordered non degenerated Ring, O be Preordering of R,
a be Element of R;
hereby assume B: abs(O,a) = 0.R;
now assume abs(O,a) = -1.R;
then -1.R + 1.R = 0.R + 1.R by B;
hence contradiction by RLVECT_1:5;
end;
then C: a is O-ordered by av00;
per cases;
suppose a in O;
hence a = 0.R by B,defa;
end;
suppose not a in O;
then a in -O by C,XBOOLE_0:def 3;
then -a = 0.R by B,defa;
then --a = 0.R;
hence a = 0.R;
end;
end;
thus thesis by REALALG1:25,defa;
end;
theorem av2:
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
proof
let R be preordered domRing, O be Preordering of R, a be Element of R;
hereby assume B: abs(O,a) = a;
per cases;
suppose a in O;
hence 0.R <=O, a;
end;
suppose a in -O;
then a = -a by B,defa;
then a = 0.R by tA;
hence 0.R <=O, a by c1;
end;
suppose D: not(a in O) & not(a in -O);
then -a = --1.R by B,defa;
then -a in O by REALALG1:25;
then --a in -O;
hence 0.R <=O, a by D;
end;
end;
thus thesis by defa;
end;
theorem av3:
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
proof
let R be preordered domRing, O be Preordering of R,
a be Element of R;
hereby assume B: abs(O,a) = -a;
per cases;
suppose a in -O;
then -a in --O;
hence a <=O, 0.R;
end;
suppose a in O;
hence a <=O, 0.R by B,defa;
end;
suppose D: not(a in O) & not(a in -O);
then --a = -- 1.R by B,defa;
hence a <=O, 0.R by D,REALALG1:25;
end;
end;
assume a <=O, 0.R;
then --a in -O;
hence abs(O,a) = -a by defa;
end;
theorem
for R being preordered Ring,
P being Preordering of R,
a being Element of R holds abs(P,a) = abs(P,-a)
proof
let R be preordered Ring, O be Preordering of R, a be Element of R;
per cases;
suppose D: a in -O;
then E: abs(O,a) = -a by defa;
-a in --O by D;
hence abs(O,a) = abs(O,-a) by E,defa;
end;
suppose D: a in O;
then E: abs(O,a) = a by defa;
-a in -O & --a = a by D;
hence abs(O,a) = abs(O,-a) by E,defa;
end;
suppose D: not(a in O) & not(a in -O);
then E: abs(O,a) = -1.R by defa;
not(-a in O) & not(-a in -O)
proof
assume -a in O or -a in -O;
then --a in -O or --a in --O;
hence contradiction by D;
end;
hence abs(O,a) = abs(O,-a) by E,defa;
end;
end;
theorem
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
proof
let R be preordered non degenerated Ring, O be Preordering of R,
a be Element of R;
hereby assume AS: -abs(O,a) <=O, a & a <=O, abs(O,a);
per cases;
suppose a in -O;
hence a is O-ordered by XBOOLE_0:def 3;
end;
suppose a in O;
hence a is O-ordered by XBOOLE_0:def 3;
end;
suppose not(a in O) & not(a in -O);
then 1.R <=O, a & a <=O, -1.R by AS,defa;
then F: 1.R <=O, - 1.R by c3;
-1.R <O, 0.R by c20;
then -1.R <O, 1.R by c20,avb6;
hence a is O-ordered by F,c2;
end;
end;
assume G: a is O-ordered;
Y: 0.R <=O, abs(O,a) by G,av0; then
X: abs(O,a) in O & O + O c= O by REALALG1:def 14;
per cases by G,XBOOLE_0:def 3;
suppose A: a in O;
then C: abs(O,a) = a by defa;
then B: abs(O,a) - a = 0.R by RLVECT_1:15;
a + abs(O,a) in O + O by C,A;
hence -abs(O,a) <=O,a by X;
thus a <=O, abs(O,a) by B,REALALG1:25;
end;
suppose A: a in -O;
then abs(O,a) = -a by defa;
then abs(O,a) - (-a) = 0.R by RLVECT_1:15;
then abs(O,a) + a in O by REALALG1:25;
hence -abs(O,a) <=O,a;
-a in --O by A;
then abs(O,a) + -a in O+O by Y;
hence a <=O, abs(O,a) by X;
end;
end;
theorem sq2:
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)"
proof
let F be preordered Field, P be Preordering of F,
a be non zero P-ordered Element of F;
AS: a in P \/ -P by defppp;
Y: a <> 0.F; -a <> -0.F; then
X: a" is non zero & -a" is non zero & -a is non zero;
abs(P,a") * abs(P,a) = 1_F
proof
per cases by AS,XBOOLE_0:def 3;
suppose K: a in P;
then 0.F <=P, a;
then L: abs(P,a) = a by av2;
0.F <=P, a" by K,REALALG1:27;
then abs(P,a") = a" by av2;
hence abs(P,a") * abs(P,a) = 1_F by Y,L,VECTSP_2:9;
end;
suppose a in -P;
then K: -a in --P;
then --a <=P, 0.F;
then L: abs(P,a) = -a by av3;
-((-a)") <=P, 0.F by K,X,REALALG1:27;
then a" <=P, 0.F by YZ;
then abs(P,a") = -(a") by av3;
hence abs(P,a")*abs(P,a) = a" * a by L,VECTSP_1:10
.= 1_F by Y,VECTSP_2:9;
end;
end;
hence thesis by VECTSP_2:10;
end;
theorem
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)
proof
let R be preordered Ring, O be Preordering of R, a,b be Element of R;
per cases;
suppose A: a-b in O;
then -(a-b) in -O;
then b-a in -O by RLVECT_1:33;
hence abs(O,b-a) = -(b-a) by defa
.= a-b by RLVECT_1:33
.= abs(O,a-b) by A,defa;
end;
suppose A: a-b in -O;
then -(a-b) in --O;
then B: b-a in O by RLVECT_1:33;
thus abs(O,a-b) = -(a-b) by A,defa
.= b-a by RLVECT_1:33
.= abs(O,b-a) by B,defa;
end;
suppose A: not(a-b in O) & not(a-b in -O);
then B: abs(O,a-b) = -1.R by defa;
not(b-a in O) & not(b-a in -O)
proof
assume b-a in O or b-a in -O;
then -(b-a) in -O or -(b-a) in --O;
hence contradiction by A,RLVECT_1:33;
end;
hence abs(O,a-b) = abs(O,b-a) by B,defa;
end;
end;
theorem ineq2:
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
proof
let R be preordered non degenerated Ring, P be Preordering of R,
a be Element of R;
hereby assume AS: -abs(P,a) <=P, a & a <=P, abs(P,a);
now assume not a is P-ordered;
then B: --1.R <=P, a & a <=P, -1.R by AS,av00;
0.R <P, 1.R & -1.R <P, 0.R by c20;
then -1.R <P, 1.R by c2,c3;
then a <P, 1.R by B,c2,c3;
hence contradiction by B,c2;
end;
hence a is P-ordered;
end;
X: P + P c= P by REALALG1:def 14;
now assume a in P \/ -P;
then per cases by XBOOLE_0:def 3;
suppose A: a in P;
then B: abs(P,a) = a by defa;
then a + abs(P,a) in P + P by A;
hence -abs(P,a) <=P, a & a <=P, abs(P,a) by X,B,c1;
end;
suppose a in -P;
then A1: abs(P,a) = -a & -a in --P by defa;
then B: - abs(P,a) = --a & -a in P;
abs(P,a) + -a in P + P by A1;
hence -abs(P,a) <=P, a & a <=P, abs(P,a) by X,B,c1;
end;
end;
hence thesis;
end;
theorem abs10:
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)
proof
let R be preordered non degenerated Ring, P be Preordering of R,
a,b be P-ordered Element of R;
AS: (a in P \/ -P & b in P \/ -P) by defppp;
X: P * P c= P by REALALG1:def 14;
Y: (-P) * P c= -P & P * (-P) c= -P by v2;
Z: (-P) * (-P) c= P by v1;
per cases by AS,XBOOLE_0:def 3;
suppose A: a in P;
per cases by AS,XBOOLE_0:def 3;
suppose A1: b in P;
then B: abs(P,a) = a & abs(P,b) = b by A,defa;
a * b in P * P by A,A1;
hence abs(P,a) * abs(P,b) = abs(P,a*b) by X,defa,B;
end;
suppose A1: b in -P;
then B: abs(P,a) = a & abs(P,b) = -b by A,defa;
C: a * b in P * (-P) by A,A1;
thus abs(P,a) * abs(P,b) = -(a*b) by VECTSP_1:8,B
.= abs(P,a*b) by C,Y,defa;
end;
end;
suppose A: a in -P;
per cases by AS,XBOOLE_0:def 3;
suppose A1: b in -P;
then B: abs(P,a) = -a & abs(P,b) = -b by A,defa;
C: a * b in (-P) * (-P) by A,A1;
thus abs(P,a) * abs(P,b) = a * b by VECTSP_1:10,B
.= abs(P,a*b) by C,Z,defa;
end;
suppose A1: b in P;
then B: abs(P,a) = -a & abs(P,b) = b by A,defa;
C: a * b in (-P) * P by A,A1;
thus abs(P,a) * abs(P,b) = -(a*b) by VECTSP_1:9,B
.= abs(P,a*b) by C,Y,defa;
end;
end;
end;
theorem
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)"
proof
let F be preordered Field, P be Preordering of F,
a be non zero P-ordered Element of F, b be P-ordered Element of F;
thus abs(P,b*a") = abs(P,b) * abs(P,a") by abs10
.= abs(P,b) * abs(P,a)" by sq2;
end;
theorem ineq1:
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)
proof
let R be preordered domRing, P be Preordering of R,
a be P-ordered Element of R,
p be P-ordered non P-negative Element of R;
H: not(p in -P \ {0.R}) & p in P \/ -P by defn,defppp;
then not(p in -P) or p in {0.R} by XBOOLE_0:def 5;
then As: not(p in -P) or p = 0.R by TARSKI:def 1;
then AS: a in (P \/ (-P)) & 0.R <=P, p
by defppp,H,XBOOLE_0:def 3,REALALG1:25;
hereby assume A1: abs(P,a) <=P, p;
per cases by AS,XBOOLE_0:def 3;
suppose a in P;
then A2: 0.R <=P, a;
A3: a <=P, abs(P,a) by ineq2;
-p <=P, 0.R by As,H,XBOOLE_0:def 3,REALALG1:25;
hence -p <=P, a & a <=P, p by A3,A2,A1,c3;
end;
suppose a in -P;
then -a in --P;
then A3: --a <=P, 0.R;
-abs(P,a) <=P, a by ineq2;
then -a <= P, --abs(P,a) by c10a;
then -a <=P, p by A1,c3;
hence -p <=P, a & a <=P, p by A3,AS,c3,c10a;
end;
end;
assume A1: -p <=P, a & a <=P, p;
per cases by AS,XBOOLE_0:def 3;
suppose a in P;
then 0.R <=P, a;
hence abs(P,a) <=P, p by A1,av2;
end;
suppose a in -P;
then -a in --P;
then --a <=P, 0.R;
then abs(P,a) = -a by av3;
hence abs(P,a) <=P, p by A1,c10a;
end;
end;
::$N The Triangle Inequality
::$L https://en.wikipedia.org/wiki/Triangle_inequality The Triangle Inequality
theorem
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)
proof
let R be preordered domRing, P be Preordering of R,
a,b be P-ordered Element of R;
A1: 0.R <=P, abs(P,b) by av0;
0.R + abs(P,b) <=P, abs(P,a) + abs(P,b) by c4,av0;
then A: 0.R <=P, abs(P,a) + abs(P,b) by c3,A1;
per cases;
suppose a+b is non P-ordered;
then not(a+b in P) & not(a+b) in -P by XBOOLE_0:def 3;
then B: abs(P,a+b) = -1.R by defa;
-1.R <P, 0.R by c20;
hence thesis by B,A,c3;
end;
suppose AS1: a + b is P-ordered;
now assume abs(P,a) + abs(P,b) is P-negative;
then -0.R <P, -(abs(P,a) + abs(P,b)) by x2,c10;
then 0.R + (abs(P,a) + abs(P,b)) <P,
-(abs(P,a) + abs(P,b)) + (abs(P,a) + abs(P,b)) by c4,RLVECT_1:8;
then 0.R + 0.R <P, abs(P,a) + abs(P,b) + -(abs(P,a) + abs(P,b)) by A,c2,c3;
hence contradiction by RLVECT_1:5;
end;
then A1: abs(P,a) + abs(P,b) is P-ordered non P-negative by A,XBOOLE_0:def 3;
B: -(abs(P,a) + abs(P,b)) <=P, a + b
proof
-abs(P,a) <=P, a by ineq2;
then -abs(P,a) + -abs(P,b) <=P, a + -abs(P,b) by c4;
then B1: -(abs(P,a) + abs(P,b)) <=P, a + -abs(P,b) by RLVECT_1:31;
-abs(P,b) <=P, b by ineq2;
then a + -abs(P,b) <=P, a + b by c4;
hence thesis by B1,c3;
end;
B1: a + abs(P,b) <=P, abs(P,a) + abs(P,b) by c4,ineq2;
a + b <=P, (abs(P,a) + abs(P,b))
proof
a + b <=P, abs(P,b) + a by c4,ineq2;
hence thesis by B1,c3;
end;
hence thesis by AS1,A1,B,ineq1;
end;
end;
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 :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 <P, -0.R by AS,c10a;
b1^2 = a by defsqrt .= b2^2 by defsqrt;
then b1 = b2 or b1 = -b2 by sq00;
hence thesis by A,AS,c2;
end;
end;
theorem
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 is P-ordered & b is P-ordered;
then AS: 0.R <=P, a & 0.R <=P, b by x1a;
hereby assume K: a <P, b;
a is Sqrt of a^2 & b is Sqrt of b^2 by defsqrt;
hence a^2 <P, b^2 by K,AS,sq1,sq0;
end;
thus thesis by sq1;
end;
theorem
for R being preordered domRing,
P being Preordering of R,
a being P-ordered Element of R holds abs(P,a)^2 = a^2
proof
let R be preordered domRing, P be Preordering of R,
a be P-ordered Element of R;
a in P\/-P by defppp; then
per cases by XBOOLE_0:def 3;
suppose a in P;
then 0.R <=P, a;
hence thesis by av2;
end;
suppose a in -P;
then -a in --P;
then a <=P, 0.R;
hence abs(P,a)^2 = (-a)^2 by av3
.= a^2 by VECTSP_1:10;
end;
end;
theorem sq5:
for R being preordered Ring,
P being Preordering of R,
a being Element of R st a in -P \ {0.R} holds a is non square
proof
let R be preordered Ring, P be Preordering of R, a be Element of R;
assume a in -P \ {0.R};
then A: a in -P & not a in {0.R} by XBOOLE_0:def 5;
B: SQ R c= P & P /\ -P = {0.R} by REALALG1:def 14;
assume a is square;
then a in SQ R;
hence contradiction by A,B;
end;
theorem
for R being preordered Ring,
P being Preordering of R holds (-P) /\ (SQ R) = {0.R}
proof
let R be preordered Ring, P be Preordering of R;
0.R in P by REALALG1:25; then
C: -0.R in -P;
A: now let o be object;
assume o in {0.R};
then o = 0.R by TARSKI:def 1;
then o in -P & o in SQ R by C;
hence o in (-P) /\ (SQ R);
end;
now let o be object;
assume o in (-P) /\ (SQ R);
then H0: o in -P & o in SQ R by XBOOLE_0:def 4;
then consider a being Element of R such that H1: o = a & a is square;
not(a in -P \ {0.R}) by H1,sq5;
hence o in {0.R} by H0,H1,XBOOLE_0:def 5;
end;
hence thesis by A,TARSKI:2;
end;
theorem
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 by sq0;
lemsqrtex:
for R be ordered domRing, O be Ordering of R, a be square Element of R
ex b being Sqrt of a st b is non O-negative
proof
let R be ordered domRing, O be Ordering of R, a be square Element of R;
consider b being Element of R such that H: b^2 = a by O_RING_1:def 2;
reconsider b as Sqrt of a by H,defsqrt;
A: O \/ -O = the carrier of R by REALALG1:def 8;
per cases;
suppose C: b = 0.R;
take b;
thus thesis by C;
end;
suppose X: b <> 0.R;
per cases by A,XBOOLE_0:def 3;
suppose b in O;
then 0.R <=O, b;
then B: 0.R <O, b by X;
take b;
thus thesis by B,x1;
end;
suppose b in -O;
then -b in --O;
then 0.R <=O, -b;
then B: 0.R <O, -b by X;
set c = -b;
c^2 = b^2 by VECTSP_1:10;
then reconsider c as Sqrt of a by defsqrt;
take c;
thus thesis by B,x1;
end;
end;
end;
registration
let R be preordered Ring;
let P be Preordering of R;
cluster P-negative -> non square for Element of R;
coherence by sq5;
cluster non P-positive square -> zero for Element of R;
coherence
proof
let a be Element of R;
assume AS: a is non P-positive square;
then not a in P or a in {0.R} by XBOOLE_0:def 5;
then per cases by TARSKI:def 1;
suppose B: not a in P;
C: a in SQ R by AS;
D: SQ R c= QS R by REALALG1:18;
QS R c= P by REALALG1:24;
hence thesis by B,C,D;
end;
suppose a = 0.R;
hence thesis;
end;
end;
end;
registration
let R be ordered domRing;
let O be Ordering of R;
let a be square Element of R;
cluster non O-negative for Sqrt of a;
existence 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 O-positive for Sqrt of a;
existence
proof
consider b being Sqrt of a such that A: b is non O-negative by lemsqrtex;
B: now assume b = 0.R;
then 0.R = b^2;
hence contradiction by defsqrt;
end;
take b;
not b <O, 0.R by A,x2;
then 0.R <O, b by B,avb4;
hence thesis by x1;
end;
cluster O-negative for Sqrt of a;
existence
proof
consider b being Sqrt of a such that A: b is non O-negative by lemsqrtex;
B: now assume b = 0.R;
then 0.R = b^2;
hence contradiction by defsqrt;
end;
take -b;
C: (-b)^2 = b^2 by VECTSP_1:10
.= a by defsqrt;
not b <O, 0.R by A,x2;
then 0.R <O, b by B,avb4;
then -b <O, -0.R by c10a;
hence thesis by C,defsqrt,x2;
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:
it^2 = a;
existence
proof
consider b being Sqrt of a such that A: b is non O-negative by lemsqrtex;
reconsider b as non O-negative Sqrt of a by A;
take b;
thus thesis by defsqrt;
end;
uniqueness
proof
now let b1,b2 be non O-negative Element of R;
assume A: b1^2 = a & b2^2 = a;
then A1: b1 is Sqrt of a & b2 is Sqrt of a by defsqrt;
per cases;
suppose b1 = 0.R;
hence b1 = b2 by A,VECTSP_2:def 1;
end;
suppose X: b1 <> 0.R;
C: now assume not(0.R <=O, b1);
then b1 <=O, 0.R & (b1 <O, 0.R or b1 = 0.R) by avb4;
hence contradiction by X,x2;
end;
now assume not(0.R <=O, b2);
then b2 <=O, 0.R & (b2 <O, 0.R or b2 = 0.R) by avb4;
hence contradiction by x2,X,A,VECTSP_2:def 1;
end;
hence b1 = b2 by A1,C,sq0;
end;
end;
hence thesis;
end;
end;
theorem
for R being ordered domRing,
O being Ordering of R,
a being square Element of R,
b being Element of R
holds b is Sqrt of a iff (b = sqrt(O,a) or b = -sqrt(O,a))
proof
let R be ordered domRing, O be Ordering of R;
let a be square Element of R, b be Element of R;
hereby assume b is Sqrt of a;
then b^2 = a by defsqrt .= sqrt(O,a)^2 by defq;
hence b = sqrt(O,a) or b = -sqrt(O,a) by sq00;
end;
assume b = sqrt(O,a) or b = -sqrt(O,a);
then per cases;
suppose b = sqrt(O,a);
hence b is Sqrt of a;
end;
suppose B: b = -sqrt(O,a);
(-sqrt(O,a))^2 = sqrt(O,a)^2 by VECTSP_1:10;
hence b is Sqrt of a by B,defsqrt;
end;
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;
coherence
proof
a = sqrt(O,a)^2 by defq;
hence thesis;
end;
end;