:: Ordered Rings and Fields :: by Christoph Schwarzweller :: :: Received March 17, 2017 :: Copyright (c) 2017-2021 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, REALSET1, GLIB_000, VECTSP_2, CARD_1, MESFUNC1, INT_3, LATTICES, ORDINAL4, INT_1, ALGSEQ_1, COMPLFLD, BINOP_1, NUMBERS, IDEAL_1, C0SP1, SQUARE_1, RATFUNC1, FUNCSDOM, XXREAL_0, HURWITZ, GROUP_1, FINSEQ_1, CARD_3, ZFMISC_1, COMPLEX1, POLYNOM1, POLYNOM3, XBOOLE_0, ARYTM_1, GAUSSINT, XCMPLX_0, RING_3, INTERVA1, RELAT_2, PARTFUN1, REALALG1, QMAX_1, ARROW, O_RING_1; notations TARSKI, ZFMISC_1, XBOOLE_0, SUBSET_1, DOMAIN_1, RELAT_1, RELAT_2, FUNCT_1, FINSEQ_1, REALSET1, RELSET_1, PARTFUN1, ORDINAL1, FUNCT_2, BINOP_1, XCMPLX_0, SQUARE_1, XXREAL_0, XREAL_0, CARD_1, XXREAL_2, COMPLEX1, NAT_1, INT_1, NAT_D, RAT_1, INT_3, NUMBERS, STRUCT_0, BINOM, ALGSTR_0, GROUP_1, GROUP_2, O_RING_1, VFUNCT_1, RATFUNC1, POLYNOM1, ALGSEQ_1, POLYNOM3, HURWITZ, RLVECT_1, VECTSP_2, VECTSP_1, COMPLFLD, GAUSSINT, IDEAL_1, C0SP1, RING_3, ALG_1, UPROOTS, ARROW; constructors BINOM, REALSET1, BINOP_2, RINGCAT1, ARYTM_2, ARYTM_3, XXREAL_2, RING_3, GAUSSINT, NAT_D, TOPALG_7, RATFUNC1, FINSEQ_1, GROUP_4, COMPLEX1, FVSUM_1, XXREAL_0, XREAL_0, SQUARE_1, POLYNOM3, ALGSEQ_1, VFUNCT_1, HURWITZ, UPROOTS, ARROW, O_RING_1, GROUP_2; registrations ORDINAL1, XXREAL_0, XREAL_0, RELSET_1, VECTSP_1, STRUCT_0, MEMBERED, NUMBERS, RLVECT_1, INT_1, INT_3, COMPLFLD, RATFUNC1, POLYNOM4, POLYNOM3, RAT_1, REALSET1, GAUSSINT, NAT_1, ALGSTR_1, SUBSET_1, RELAT_2, FUNCT_2, RING_3, XCMPLX_0, FINSEQ_1, NAT_2, CARD_1, VFUNCT_1, XBOOLE_0; requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM; begin :: On Order Relations definition let X be set; let R be Relation of X; attr R is strongly_reflexive means :: REALALG1:def 1 R is_reflexive_in X; attr R is totally_connected means :: REALALG1:def 2 R is_strongly_connected_in X; end; registration let X be set; cluster strongly_reflexive for Relation of X; cluster totally_connected for Relation of X; end; registration let X be set; cluster strongly_reflexive -> reflexive for Relation of X; cluster totally_connected -> strongly_connected for Relation of X; end; registration let X be non empty set; cluster strongly_reflexive -> non empty for Relation of X; cluster totally_connected -> non empty for Relation of X; end; theorem :: REALALG1:1 for X being non empty set for R being strongly_reflexive Relation of X for x being Element of X holds x <=_R,x; theorem :: REALALG1:2 for X being non empty set for R being antisymmetric Relation of X for x,y being Element of X st x <=_R,y & y <=_R,x holds x = y; theorem :: REALALG1:3 for X being non empty set for R being transitive Relation of X for x,y,z being Element of X st x <=_R,y & y <=_R,z holds x <=_R,z; theorem :: REALALG1:4 for X being non empty set for R being totally_connected Relation of X for x,y being Element of X holds x <=_R,y or y <=_R,x; definition let L be addLoopStr; let R be Relation of L; attr R is respecting_addition means :: REALALG1:def 3 for a,b,c being Element of L st a <=_R,b holds a+c <=_R,b+c; end; definition let L be multLoopStr_0; let R be Relation of L; attr R is respecting_multiplication means :: REALALG1:def 4 for a,b,c being Element of L st a <=_R,b & 0.L <=_R,c holds a*c <=_R,b*c; end; begin theorem :: REALALG1:5 for R being degenerated Ring, p being Polynomial of R holds {i where i is Nat : p.i <> 0.R} = {}; theorem :: REALALG1:6 for R being Ring, p being Polynomial of R holds p = 0_.(R) iff {i where i is Nat : p.i <> 0.R} = {}; theorem :: REALALG1:7 for R being Ring, p being Polynomial of R holds min* {i where i is Nat : (p+0_.R).i <> 0.R} = min* {i where i is Nat : p.i <> 0.R}; theorem :: REALALG1:8 for R being non degenerated Ring, p being Polynomial of R holds min* {i where i is Nat : (-p).i <> 0.R} = min* {i where i is Nat : p.i <> 0.R}; theorem :: REALALG1:9 for R being non degenerated Ring, p,q being non zero Polynomial of R st min* {i where i is Nat : p.i <> 0.R} > min* {i where i is Nat : q.i <> 0.R} holds min* {i where i is Nat : (p+q).i <> 0.R} = min* {i where i is Nat : q.i <> 0.R}; theorem :: REALALG1:10 for R being non degenerated Ring, p,q being non zero Polynomial of R st p + q <> 0_.(R) & min* {i where i is Nat : p.i <> 0.R} = min* {i where i is Nat : q.i <> 0.R} holds min* {i where i is Nat : (p+q).i <> 0.R} >= min* {i where i is Nat : p.i <> 0.R}; theorem :: REALALG1:11 for R being non degenerated Ring, p,q being non zero Polynomial of R st p.(min* {i where i is Nat : p.i <> 0.R}) + q.(min* {i where i is Nat : q.i <> 0.R}) <> 0.R holds min* {i where i is Nat : (p+q).i <> 0.R} = min( min* {i where i is Nat : p.i <> 0.R}, min* {i where i is Nat : q.i <> 0.R}); theorem :: REALALG1:12 for R being non degenerated Ring, p,q being non zero Polynomial of R st p *' q <> 0_.(R) holds min* {i where i is Nat : (p*'q).i <> 0.R} >= min* {i where i is Nat : p.i <> 0.R} + min* {i where i is Nat : q.i <> 0.R}; theorem :: REALALG1:13 for R being domRing, p,q being non zero Polynomial of R holds min* {i where i is Nat : (p*'q).i <> 0.R} = min* {i where i is Nat : p.i <> 0.R} + min* {i where i is Nat : q.i <> 0.R}; begin :: Preliminaries definition let L be non empty multLoopStr; let S be Subset of L; attr S is mult-closed means :: REALALG1:def 5 for s1,s2 being Element of L st s1 in S & s2 in S holds s1 * s2 in S; end; definition ::: compare GROUP_1A let L be non empty addLoopStr; let S be Subset of L; func -S -> Subset of L equals :: REALALG1:def 6 { -s where s is Element of L : s in S }; end; registration let L be add-associative right_zeroed right_complementable non empty addLoopStr; let S be Subset of L; reduce -(-S) to S; end; theorem :: REALALG1:14 for L being add-associative right_zeroed right_complementable non empty addLoopStr for S being Subset of L for a being Element of L holds a in S iff -a in -S; theorem :: REALALG1:15 for L being add-associative right_zeroed right_complementable non empty addLoopStr for S1,S2 being Subset of L holds -(S1 /\ S2) = (-S1) /\ (-S2); theorem :: REALALG1:16 for L being add-associative right_zeroed right_complementable non empty addLoopStr for S1,S2 being Subset of L holds -(S1 \/ S2) = (-S1) \/ (-S2); definition let L be non empty addLoopStr; let S be Subset of L; attr S is negative-disjoint means :: REALALG1:def 7 S /\ (-S) = {0.L}; end; definition let L be non empty addLoopStr; let S be Subset of L; attr S is spanning means :: REALALG1:def 8 S \/ (-S) = the carrier of L; end; begin :: Squares and Sums of Squares notation let R be Ring; let a be Element of R; synonym a is square for a is being_a_square; end; registration let R be Ring; cluster 0.R -> square; cluster 1.R -> square; end; registration let R be Ring; cluster square for Element of R; end; definition ::: should be unified with O_RING_1; definition there should be ::: tuned accordingly let R be Ring; let a be Element of R; attr a is sum_of_squares means :: REALALG1:def 9 ex f being FinSequence of R st Sum f = a & for i being Nat st i in dom f ex a being Element of R st f.i = a^2; end; registration let R be Ring; cluster square -> sum_of_squares for Element of R; end; registration let R be commutative Ring; let a,b be square Element of R; cluster a * b -> square; end; registration let R be Ring; let a,b be sum_of_squares Element of R; cluster a + b -> sum_of_squares; end; registration let R be commutative Ring; let a,b be sum_of_squares Element of R; cluster a * b -> sum_of_squares; end; definition let R be Ring; func Squares_of R -> Subset of R equals :: REALALG1:def 10 { a where a is Element of R : a is square }; func Quadratic_Sums_of R -> Subset of R equals :: REALALG1:def 11 { a where a is Element of R : a is sum_of_squares }; end; notation let R be Ring; synonym SQ R for Squares_of R; synonym QS R for Quadratic_Sums_of R; end; registration let R be Ring; cluster SQ R -> non empty; cluster QS R -> non empty; end; definition let R be Ring; let S be Subset of R; attr S is with_squares means :: REALALG1:def 12 SQ R c= S; attr S is with_sums_of_squares means :: REALALG1:def 13 QS R c= S; end; registration let R be Ring; cluster with_squares for Subset of R; cluster with_sums_of_squares for Subset of R; end; registration let R be Ring; cluster with_squares -> non empty for Subset of R; cluster with_sums_of_squares -> non empty for Subset of R; end; registration let R be Ring; cluster with_sums_of_squares -> with_squares for Subset of R; cluster with_squares add-closed -> with_sums_of_squares for Subset of R; end; registration let R be Ring; cluster SQ R -> with_squares; cluster QS R -> with_sums_of_squares; end; theorem :: REALALG1:17 for R being Ring holds 0.R in SQ R & 1.R in SQ R; theorem :: REALALG1:18 for R being Ring holds SQ R c= QS R; registration let R be Ring; cluster QS R -> add-closed; end; registration let R be commutative Ring; cluster QS R -> mult-closed; end; theorem :: REALALG1:19 for R being Ring for S being Subring of R holds SQ S c= SQ R; theorem :: REALALG1:20 for R being Ring for S being Subring of R holds QS S c= QS R; begin :: Positive Cones and Orderings definition let R be Ring, S be Subset of R; attr S is prepositive_cone means :: REALALG1:def 14 S + S c= S & S * S c= S & S /\ (-S) = {0.R} & SQ R c= S; attr S is positive_cone means :: REALALG1:def 15 S + S c= S & S * S c= S & S /\ (-S) = {0.R} & S \/ (-S) = the carrier of R; end; registration let R be Ring; cluster prepositive_cone -> non empty for Subset of R; cluster positive_cone -> non empty for Subset of R; end; registration let R be Ring; cluster prepositive_cone -> add-closed mult-closed negative-disjoint with_squares for Subset of R; cluster add-closed mult-closed negative-disjoint with_squares -> prepositive_cone for Subset of R; end; registration let R be Ring; cluster positive_cone -> add-closed mult-closed negative-disjoint spanning for Subset of R; cluster add-closed mult-closed negative-disjoint spanning -> positive_cone for Subset of R; end; registration let R be Ring; cluster positive_cone -> prepositive_cone for Subset of R; end; theorem :: REALALG1:21 for F being Field for S being Subset of F st S * S c= S & SQ F c= S holds S /\ (-S) = {0.F} iff not -1.F in S; theorem :: REALALG1:22 for F being Field for S being Subset of F st S * S c= S & S \/ (-S) = the carrier of F holds S /\ (-S) = {0.F} iff not -1.F in S; definition let R be Ring; attr R is preordered means :: REALALG1:def 16 ex P being Subset of R st P is prepositive_cone; attr R is ordered means :: REALALG1:def 17 ex P being Subset of R st P is positive_cone; end; registration cluster preordered for Field; cluster ordered for Field; end; registration cluster ordered -> preordered for Ring; end; registration let R be preordered Ring; cluster prepositive_cone for Subset of R; end; registration let R be ordered Ring; cluster positive_cone for Subset of R; end; definition let R be preordered Ring; mode Preordering of R is prepositive_cone Subset of R; end; definition let R be ordered Ring; mode Ordering of R is positive_cone Subset of R; end; theorem :: REALALG1:23 for R being preordered Ring for P being Preordering of R for a being Element of R holds a^2 in P; theorem :: REALALG1:24 for R being preordered Ring for P being Preordering of R holds QS R c= P; theorem :: REALALG1:25 for R being preordered Ring for P being Preordering of R holds 0.R in P & 1.R in P; theorem :: REALALG1:26 for R being preordered non degenerated Ring for P being Preordering of R holds not -1.R in P; theorem :: REALALG1:27 for F being preordered Field for P being Preordering of F for a being non zero Element of F st a in P holds a" in P; theorem :: REALALG1:28 for R being preordered non degenerated Ring holds Char R = 0; theorem :: REALALG1:29 for R being ordered Ring for O,P being Ordering of R st O c= P holds O = P; begin :: Orderings vs. Order Relations definition let R be preordered Ring, P be Preordering of R; let a,b be Element of R; pred a <= P,b means :: REALALG1:def 18 b - a in P; end; definition let R be preordered Ring, P be Preordering of R; func OrdRel P -> Relation of R equals :: REALALG1:def 19 { [a,b] where a,b is Element of R : a <= P,b }; end; registration let R be preordered Ring; let P be Preordering of R; cluster OrdRel P -> non empty; end; registration let R be preordered Ring, P be Preordering of R; cluster OrdRel P -> strongly_reflexive antisymmetric transitive; end; registration let R be preordered Ring, P be Preordering of R; cluster OrdRel P -> respecting_addition respecting_multiplication; end; registration let R be ordered Ring, O be Ordering of R; cluster OrdRel O -> totally_connected; end; registration let R be preordered Ring; cluster strongly_reflexive antisymmetric transitive respecting_addition respecting_multiplication for Relation of R; end; registration let R be ordered Ring; cluster strongly_reflexive antisymmetric transitive respecting_addition respecting_multiplication totally_connected for Relation of R; end; definition let R be preordered Ring; mode OrderRelation of R is strongly_reflexive antisymmetric transitive respecting_addition respecting_multiplication Relation of R; end; definition let R be ordered Ring; mode total_OrderRelation of R is strongly_reflexive antisymmetric transitive respecting_addition respecting_multiplication totally_connected Relation of R; end; definition let R be Ring; let Q be Relation of R; func Positives Q -> Subset of R equals :: REALALG1:def 20 { a where a is Element of R : 0.R <=_Q,a }; end; registration let R be preordered Ring; let Q be strongly_reflexive Relation of R; cluster Positives Q -> non empty; end; registration let R be preordered Ring; let Q be OrderRelation of R; cluster Positives Q -> add-closed mult-closed negative-disjoint; end; registration let R be ordered Ring; let Q be total_OrderRelation of R; cluster Positives Q -> spanning; end; theorem :: REALALG1:30 for R being preordered Ring for P being Preordering of R holds OrdRel P is OrderRelation of R; theorem :: REALALG1:31 for R being ordered Ring for P being Ordering of R holds OrdRel P is total_OrderRelation of R; theorem :: REALALG1:32 for R being ordered Ring for Q being total_OrderRelation of R holds Positives Q is Ordering of R; begin registration let R be preordered Ring; cluster -> preordered for Subring of R; end; registration let R be ordered Ring; cluster -> ordered for Subring of R; end; theorem :: REALALG1:33 for R being preordered Ring for P being Preordering of R for S being Subring of R holds P /\ (the carrier of S) is Preordering of S; theorem :: REALALG1:34 for R being ordered Ring for O being Ordering of R for S being Subring of R holds O /\ (the carrier of S) is Ordering of S; registration cluster F_Complex -> non preordered; end; registration let n be non trivial Nat; cluster Z/n -> non preordered; end; definition func Positives(F_Real) -> Subset of F_Real equals :: REALALG1:def 21 { r where r is Element of REAL : 0 <= r }; end; registration cluster Positives(F_Real) -> add-closed mult-closed negative-disjoint spanning; end; registration cluster F_Real -> ordered; end; theorem :: REALALG1:35 Positives(F_Real) is Ordering of F_Real; theorem :: REALALG1:36 for O being Ordering of F_Real holds O = Positives(F_Real); definition func Positives(F_Rat) -> Subset of F_Rat equals :: REALALG1:def 22 { r where r is Element of RAT : 0 <= r }; end; registration cluster Positives(F_Rat) -> add-closed mult-closed negative-disjoint spanning; end; registration cluster F_Rat -> ordered; end; theorem :: REALALG1:37 Positives(F_Rat) is Ordering of F_Rat; theorem :: REALALG1:38 for O being Ordering of F_Rat holds O = Positives(F_Rat); definition func Positives(INT.Ring) -> Subset of INT.Ring equals :: REALALG1:def 23 { i where i is Element of INT : 0 <= i }; end; registration cluster Positives(INT.Ring) -> add-closed mult-closed negative-disjoint spanning; end; registration cluster INT.Ring -> ordered; end; theorem :: REALALG1:39 Positives(INT.Ring) is Ordering of INT.Ring; theorem :: REALALG1:40 for O being Ordering of INT.Ring holds O = Positives(INT.Ring); begin :: Ordered Polynomial Rings definition let R be preordered Ring; let P be Preordering of R; func Positives(Poly) P -> Subset of Polynom-Ring R equals :: REALALG1:def 24 { p where p is Polynomial of R : LC p in P }; end; registration let R be preordered non degenerated Ring; let P be Preordering of R; cluster Positives(Poly) P -> add-closed negative-disjoint; end; registration let R be preordered domRing; let P be Preordering of R; cluster Positives(Poly) P -> mult-closed with_sums_of_squares; end; registration let R be ordered Ring; let O be Ordering of R; cluster Positives(Poly) O -> spanning; end; registration let R be preordered domRing; cluster Polynom-Ring R -> preordered; end; registration let R be ordered domRing; cluster Polynom-Ring R -> ordered; end; theorem :: REALALG1:41 for R being preordered domRing for P being Preordering of R holds Positives(Poly) P is Preordering of Polynom-Ring R; theorem :: REALALG1:42 for R being ordered domRing for O being Ordering of R holds Positives(Poly) O is Ordering of Polynom-Ring R; definition let R be preordered Ring; let P be Preordering of R; func LowPositives(Poly) P -> Subset of Polynom-Ring R equals :: REALALG1:def 25 { p where p is Polynomial of R : p.(min*{i where i is Nat : p.i <> 0.R}) in P }; end; registration let R be preordered non degenerated Ring; let P be Preordering of R; cluster LowPositives(Poly) P -> add-closed negative-disjoint; end; registration let R be preordered domRing; let P be Preordering of R; cluster LowPositives(Poly) P -> mult-closed with_sums_of_squares; end; registration let R be ordered non degenerated Ring; let O be Ordering of R; cluster LowPositives(Poly) O -> spanning; end; theorem :: REALALG1:43 for R being preordered domRing for P being Preordering of R holds LowPositives(Poly) P is Preordering of Polynom-Ring R; theorem :: REALALG1:44 for R being ordered domRing for O being Ordering of R holds LowPositives(Poly) O is Ordering of Polynom-Ring R; theorem :: REALALG1:45 for R being preordered non degenerated Ring for P being Preordering of R holds Positives(Poly) P <> LowPositives(Poly) P;