:: Formally Real Fields :: by Christoph Schwarzweller :: :: Received November 29, 2017 :: Copyright (c) 2017 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, XXREAL_2, NAT_1, INT_3, RELAT_1, ALGSTR_0, RING_3, REALALG1, GAUSSINT, CARD_1, FINSEQ_1, RING_5, FUNCOP_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,RAT_1:11; F: p = m * n" by RAT_1:15 .= b * a" by G,GAUSSINT:15; per cases; suppose m = 0; then p = 0 by RAT_1:14; 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,RAT_1:11; 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,RAT_1:11; 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 by FINSEQ_1:40; 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 by FINSEQ_1:40; 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,FINSEQ_1:40 .= 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,FINSEQ_1:40; 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
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 abs(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 abs(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 = abs(O,a) iff r = a) by defa;
thus not(a in O) implies (r = abs(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;
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;
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