theory OrderedRing_ZF imports Ring_ZF OrderedGroup_ZF_1
begin
In this theory file we consider ordered rings.
Definition and notation
This section defines ordered rings and sets up appriopriate notation.
We define ordered ring as a commutative ring with linear order that is preserved by translations and such that the set of nonnegative elements is closed under multiplication. Note that this definition does not guarantee that there are no zero divisors in the ring.
definition
\( \text{IsAnOrdRing}(R,A,M,r) \equiv \) \( ( \text{IsAring}(R,A,M) \wedge (M \text{ is commutative on } R) \wedge \) \( r\subseteq R\times R \wedge \text{IsLinOrder}(R,r) \wedge \) \( (\forall a b.\ \forall c\in R.\ \langle a,b\rangle \in r \longrightarrow \langle A\langle a,c\rangle ,A\langle b,c\rangle \rangle \in r) \wedge \) \( ( \text{Nonnegative}(R,A,r) \text{ is closed under } M)) \)
The next context (locale) defines notation used for ordered rings. We do that by extending the notation defined in the ring0 locale and adding some assumptions to make sure we are talking about ordered rings in this context.
locale ring1 = ring0 +
assumes mult_commut: \( M \text{ is commutative on } R \)
assumes ordincl: \( r \subseteq R\times R \)
assumes linord: \( \text{IsLinOrder}(R,r) \)
defines \( a \leq b \equiv \langle a,b\rangle \in r \)
defines \( a \lt b \equiv a\leq b \wedge a\neq b \)
assumes ordgroup: \( \forall a b.\ \forall c\in R.\ a\leq b \longrightarrow a + c \leq b + c \)
assumes pos_mult_closed: \( \text{Nonnegative}(R,A,r) \text{ is closed under } M \)
defines \( \vert a\vert \equiv \text{AbsoluteValue}(R,A,r)(a) \)
defines \( R_+ \equiv \text{PositiveSet}(R,A,r) \)
The next lemma assures us that we are talking about ordered rings in the ring1 context.
lemma (in ring1) OrdRing_ZF_1_L1:
shows \( \text{IsAnOrdRing}(R,A,M,r) \) using ring0_def, ringAssum, mult_commut, ordincl, linord, ordgroup, pos_mult_closed, IsAnOrdRing_defWe can use theorems proven in the ring1 context whenever we talk about an ordered ring.
lemma OrdRing_ZF_1_L2:
assumes \( \text{IsAnOrdRing}(R,A,M,r) \)
shows \( ring1(R,A,M,r) \) using assms, IsAnOrdRing_def, ring1_axioms.intro, ring0_def, ring1_defIn the ring1 context \(a\leq b\) implies that \(a,b\) are elements of the ring.
lemma (in ring1) OrdRing_ZF_1_L3:
assumes \( a\leq b \)
shows \( a\in R \), \( b\in R \) using assms, ordinclOrdered ring is an ordered group, hence we can use theorems proven in the group3 context.
lemma (in ring1) OrdRing_ZF_1_L4:
shows \( \text{IsAnOrdGroup}(R,A,r) \), \( r \text{ is total on } R \), \( A \text{ is commutative on } R \), \( group3(R,A,r) \)proof{
}
fix \( a \) \( b \) \( g \)
assume A1: \( g\in R \) and A2: \( a\leq b \)
with ordgroup have \( a + g \leq b + g \)
moreover
from ringAssum, A1, A2 have \( a + g = g + a \), \( b + g = g + b \) using OrdRing_ZF_1_L3, IsAring_def, IsCommutative_def
ultimately have \( a + g \leq b + g \), \( g + a \leq g + b \)
hence \( \forall g\in R.\ \forall a b.\ a\leq b \longrightarrow a + g \leq b + g \wedge g + a \leq g + b \)
with ringAssum, ordincl, linord show \( \text{IsAnOrdGroup}(R,A,r) \), \( group3(R,A,r) \), \( r \text{ is total on } R \), \( A \text{ is commutative on } R \) using IsAring_def, Order_ZF_1_L2, IsAnOrdGroup_def, group3_def, IsLinOrder_def
qed
The order relation in rings is transitive.
lemma (in ring1) ring_ord_transitive:
assumes A1: \( a\leq b \), \( b\leq c \)
shows \( a\leq c \)proof from A1 have \( group3(R,A,r) \), \( \langle a,b\rangle \in r \), \( \langle b,c\rangle \in r \) using OrdRing_ZF_1_L4
then have \( \langle a,c\rangle \in r \) by (rule Group_order_transitive )
then show \( a\leq c \)
qed
Transitivity for the strict order: if \(a
lemma (in ring1) ring_strict_ord_trans:
assumes A1: \( a \lt b \) and A2: \( b\leq c \)
shows \( a \lt c \)proof from A1, A2 have \( group3(R,A,r) \), \( \langle a,b\rangle \in r \wedge a\neq b \), \( \langle b,c\rangle \in r \) using OrdRing_ZF_1_L4
then have \( \langle a,c\rangle \in r \wedge a\neq c \) by (rule OrderedGroup_ZF_1_L4A )
then show \( a \lt c \)
qed
Another version of transitivity for the strict order:
if \(a\leq b\) and \(b
lemma (in ring1) ring_strict_ord_transit:
assumes A1: \( a\leq b \) and A2: \( b \lt c \)
shows \( a \lt c \)proof from A1, A2 have \( group3(R,A,r) \), \( \langle a,b\rangle \in r \), \( \langle b,c\rangle \in r \wedge b\neq c \) using OrdRing_ZF_1_L4
then have \( \langle a,c\rangle \in r \wedge a\neq c \) by (rule group_strict_ord_transit )
then show \( a \lt c \)
qed
The next lemma shows what happens when one element of an ordered ring is not greater or equal than another.
lemma (in ring1) OrdRing_ZF_1_L4A:
assumes A1: \( a\in R \), \( b\in R \) and A2: \( \neg (a\leq b) \)
shows \( b \leq a \), \( ( - a) \leq ( - b) \), \( a\neq b \)proof from A1, A2 have I: \( group3(R,A,r) \), \( r \text{ is total on } R \), \( a \in R \), \( b \in R \), \( \langle a, b\rangle \notin r \) using OrdRing_ZF_1_L4
then have \( \langle b,a\rangle \in r \) by (rule OrderedGroup_ZF_1_L8 )
then show \( b \leq a \)
from I have \( \langle \text{GroupInv}(R,A)(a), \text{GroupInv}(R,A)(b)\rangle \in r \) by (rule OrderedGroup_ZF_1_L8 )
then show \( ( - a) \leq ( - b) \)
from I show \( a\neq b \) by (rule OrderedGroup_ZF_1_L8 )
qed
A special case of OrdRing_ZF_1_L4A when one of the constants is \(0\). This is useful for many proofs by cases.
corollary (in ring1) ord_ring_split2:
assumes A1: \( a\in R \)
shows \( a\leq 0 \vee ( 0 \leq a \wedge a\neq 0 ) \)proof{
}
from A1 have I: \( a\in R \), \( 0 \in R \) using Ring_ZF_1_L2
moreover
assume A2: \( \neg (a\leq 0 ) \)
ultimately have \( 0 \leq a \) by (rule OrdRing_ZF_1_L4A )
moreover
from I, A2 have \( a\neq 0 \) by (rule OrdRing_ZF_1_L4A )
ultimately have \( 0 \leq a \wedge a\neq 0 \)
then show \( thesis \)
qed
Taking minus on both sides reverses an inequality.
lemma (in ring1) OrdRing_ZF_1_L4B:
assumes \( a\leq b \)
shows \( ( - b) \leq ( - a) \) using assms, OrdRing_ZF_1_L4, OrderedGroup_ZF_1_L5The next lemma just expands the condition that requires the set of nonnegative elements to be closed with respect to multiplication. These are properties of totally ordered groups.
lemma (in ring1) OrdRing_ZF_1_L5:
assumes \( 0 \leq a \), \( 0 \leq b \)
shows \( 0 \leq a\cdot b \) using pos_mult_closed, assms, OrdRing_ZF_1_L4, OrderedGroup_ZF_1_L2, IsOpClosed_defDouble nonnegative is nonnegative.
lemma (in ring1) OrdRing_ZF_1_L5A:
assumes A1: \( 0 \leq a \)
shows \( 0 \leq 2 \cdot a \) using assms, OrdRing_ZF_1_L4, OrderedGroup_ZF_1_L5G, OrdRing_ZF_1_L3, Ring_ZF_1_L3A sufficient (somewhat redundant) condition for a structure to be an ordered ring. It says that a commutative ring that is a totally ordered group with respect to the additive operation such that set of nonnegative elements is closed under multiplication, is an ordered ring.
lemma OrdRing_ZF_1_L6:
assumes \( \text{IsAring}(R,A,M) \), \( M \text{ is commutative on } R \), \( \text{Nonnegative}(R,A,r) \text{ is closed under } M \), \( \text{IsAnOrdGroup}(R,A,r) \), \( r \text{ is total on } R \)
shows \( \text{IsAnOrdRing}(R,A,M,r) \) using assms, IsAnOrdGroup_def, Order_ZF_1_L3, IsAnOrdRing_def\(a\leq b\) iff \(a-b\leq 0\). This is a fact from OrderedGroup.thy, where it is stated in multiplicative notation.
lemma (in ring1) OrdRing_ZF_1_L7:
assumes \( a\in R \), \( b\in R \)
shows \( a\leq b \longleftrightarrow a - b \leq 0 \) using assms, OrdRing_ZF_1_L4, OrderedGroup_ZF_1_L9Negative times positive is negative.
lemma (in ring1) OrdRing_ZF_1_L8:
assumes A1: \( a\leq 0 \) and A2: \( 0 \leq b \)
shows \( a\cdot b \leq 0 \)proof from A1, A2 have T1: \( a\in R \), \( b\in R \), \( a\cdot b \in R \) using OrdRing_ZF_1_L3, Ring_ZF_1_L4
from A1, A2 have \( 0 \leq ( - a)\cdot b \) using OrdRing_ZF_1_L4, OrderedGroup_ZF_1_L5A, OrdRing_ZF_1_L5
with T1 show \( a\cdot b \leq 0 \) using Ring_ZF_1_L7, OrdRing_ZF_1_L4, OrderedGroup_ZF_1_L5AA
qed
We can multiply both sides of an inequality by a nonnegative ring element. This property is sometimes (not here) used to define ordered rings.
lemma (in ring1) OrdRing_ZF_1_L9:
assumes A1: \( a\leq b \) and A2: \( 0 \leq c \)
shows \( a\cdot c \leq b\cdot c \), \( c\cdot a \leq c\cdot b \)proof from A1, A2 have T1: \( a\in R \), \( b\in R \), \( c\in R \), \( a\cdot c \in R \), \( b\cdot c \in R \) using OrdRing_ZF_1_L3, Ring_ZF_1_L4
with A1, A2 have \( (a - b)\cdot c \leq 0 \) using OrdRing_ZF_1_L7, OrdRing_ZF_1_L8
with T1 show \( a\cdot c \leq b\cdot c \) using Ring_ZF_1_L8, OrdRing_ZF_1_L7
with mult_commut, T1 show \( c\cdot a \leq c\cdot b \) using IsCommutative_def
qed
A special case of OrdRing_ZF_1_L9: we can multiply an inequality by a positive ring element.
lemma (in ring1) OrdRing_ZF_1_L9A:
assumes A1: \( a\leq b \) and A2: \( c\in R_+ \)
shows \( a\cdot c \leq b\cdot c \), \( c\cdot a \leq c\cdot b \)proof from A2 have \( 0 \leq c \) using PositiveSet_def
with A1 show \( a\cdot c \leq b\cdot c \), \( c\cdot a \leq c\cdot b \) using OrdRing_ZF_1_L9
qed
A square is nonnegative.
lemma (in ring1) OrdRing_ZF_1_L10:
assumes A1: \( a\in R \)
shows \( 0 \leq (a^2) \)proof{
}
assume \( 0 \leq a \)
then have \( 0 \leq (a^2) \) using OrdRing_ZF_1_L5
moreover {
}
ultimately show \( thesis \)
qed
assume \( \neg ( 0 \leq a) \)
with A1 have \( 0 \leq (( - a)^2) \) using OrdRing_ZF_1_L4, OrderedGroup_ZF_1_L8A, OrdRing_ZF_1_L5
with A1 have \( 0 \leq (a^2) \) using Ring_ZF_1_L14
\(1\) is nonnegative.
corollary (in ring1) ordring_one_is_nonneg:
shows \( 0 \leq 1 \)proof have \( 0 \leq (1 ^2) \) using Ring_ZF_1_L2, OrdRing_ZF_1_L10
then show \( 0 \leq 1 \) using Ring_ZF_1_L2, Ring_ZF_1_L3
qed
In nontrivial rings one is positive.
lemma (in ring1) ordring_one_is_pos:
assumes \( 0 \neq 1 \)
shows \( 1 \in R_+ \) using assms, Ring_ZF_1_L2, ordring_one_is_nonneg, PositiveSet_defNonnegative is not negative. Property of ordered groups.
lemma (in ring1) OrdRing_ZF_1_L11:
assumes \( 0 \leq a \)
shows \( \neg (a\leq 0 \wedge a\neq 0 ) \) using assms, OrdRing_ZF_1_L4, OrderedGroup_ZF_1_L5ABA negative element cannot be a square.
lemma (in ring1) OrdRing_ZF_1_L12:
assumes A1: \( a\leq 0 \), \( a\neq 0 \)
shows \( \neg (\exists b\in R.\ a = (b^2)) \)proof{
}
assume \( \exists b\in R.\ a = (b^2) \)
with A1 have \( False \) using OrdRing_ZF_1_L10, OrdRing_ZF_1_L11
then show \( thesis \)
qed
If \(a\leq b\), then \(0\leq b-a\).
lemma (in ring1) OrdRing_ZF_1_L13:
assumes \( a\leq b \)
shows \( 0 \leq b - a \) using assms, OrdRing_ZF_1_L4, OrderedGroup_ZF_1_L9DIf \(a
lemma (in ring1) OrdRing_ZF_1_L14:
assumes \( a\leq b \), \( a\neq b \)
shows \( 0 \leq b - a \), \( 0 \neq b - a \), \( b - a \in R_+ \) using assms, OrdRing_ZF_1_L4, OrderedGroup_ZF_1_L9EIf the difference is nonnegative, then \(a\leq b\).
lemma (in ring1) OrdRing_ZF_1_L15:
assumes \( a\in R \), \( b\in R \) and \( 0 \leq b - a \)
shows \( a\leq b \) using assms, OrdRing_ZF_1_L4, OrderedGroup_ZF_1_L9FA nonnegative number is does not decrease when multiplied by a number greater or equal \(1\).
lemma (in ring1) OrdRing_ZF_1_L16:
assumes A1: \( 0 \leq a \) and A2: \( 1 \leq b \)
shows \( a\leq a\cdot b \)proof from A1, A2 have T: \( a\in R \), \( b\in R \), \( a\cdot b \in R \) using OrdRing_ZF_1_L3, Ring_ZF_1_L4
from A1, A2 have \( 0 \leq a\cdot (b - 1 ) \) using OrdRing_ZF_1_L13, OrdRing_ZF_1_L5
with T show \( a\leq a\cdot b \) using Ring_ZF_1_L8, Ring_ZF_1_L2, Ring_ZF_1_L3, OrdRing_ZF_1_L15
qed
We can multiply the right hand side of an inequality between nonnegative ring elements by an element greater or equal \(1\).
lemma (in ring1) OrdRing_ZF_1_L17:
assumes A1: \( 0 \leq a \) and A2: \( a\leq b \) and A3: \( 1 \leq c \)
shows \( a\leq b\cdot c \)proof from A1, A2 have \( 0 \leq b \) by (rule ring_ord_transitive )
with A3 have \( b\leq b\cdot c \) using OrdRing_ZF_1_L16
with A2 show \( a\leq b\cdot c \) by (rule ring_ord_transitive )
qed
Strict order is preserved by translations.
lemma (in ring1) ring_strict_ord_trans_inv:
assumes \( a \lt b \) and \( c\in R \)
shows \( a + c \lt b + c \), \( c + a \lt c + b \) using assms, OrdRing_ZF_1_L4, group_strict_ord_transl_invWe can put an element on the other side of a strict inequality, changing its sign.
lemma (in ring1) OrdRing_ZF_1_L18:
assumes \( a\in R \), \( b\in R \) and \( a - b \lt c \)
shows \( a \lt c + b \) using assms, OrdRing_ZF_1_L4, OrderedGroup_ZF_1_L12BWe can add the sides of two inequalities, the first of them strict, and we get a strict inequality. Property of ordered groups.
lemma (in ring1) OrdRing_ZF_1_L19:
assumes \( a \lt b \) and \( c\leq d \)
shows \( a + c \lt b + d \) using assms, OrdRing_ZF_1_L4, OrderedGroup_ZF_1_L12CWe can add the sides of two inequalities, the second of them strict and we get a strict inequality. Property of ordered groups.
lemma (in ring1) OrdRing_ZF_1_L20:
assumes \( a\leq b \) and \( c \lt d \)
shows \( a + c \lt b + d \) using assms, OrdRing_ZF_1_L4, OrderedGroup_ZF_1_L12DAbsolute value for ordered rings
Absolute value is defined for ordered groups as a function that is the identity on the nonnegative set and the negative of the element (the inverse in the multiplicative notation) on the rest. In this section we consider properties of absolute value related to multiplication in ordered rings.
Absolute value of a product is the product of absolute values: the case when both elements of the ring are nonnegative.
lemma (in ring1) OrdRing_ZF_2_L1:
assumes \( 0 \leq a \), \( 0 \leq b \)
shows \( \vert a\cdot b\vert = \vert a\vert \cdot \vert b\vert \) using assms, OrdRing_ZF_1_L5, OrdRing_ZF_1_L4, OrderedGroup_ZF_1_L2, OrderedGroup_ZF_3_L2The absolue value of an element and its negative are the same.
lemma (in ring1) OrdRing_ZF_2_L2:
assumes \( a\in R \)
shows \( \vert - a\vert = \vert a\vert \) using assms, OrdRing_ZF_1_L4, OrderedGroup_ZF_3_L7AThe next lemma states that \(|a\cdot (-b)| = |(-a)\cdot b| = |(-a)\cdot (-b)| = |a\cdot b|\).
lemma (in ring1) OrdRing_ZF_2_L3:
assumes \( a\in R \), \( b\in R \)
shows \( \vert ( - a)\cdot b\vert = \vert a\cdot b\vert \), \( \vert a\cdot ( - b)\vert = \vert a\cdot b\vert \), \( \vert ( - a)\cdot ( - b)\vert = \vert a\cdot b\vert \) using assms, Ring_ZF_1_L4, Ring_ZF_1_L7, Ring_ZF_1_L7A, OrdRing_ZF_2_L2This lemma allows to prove theorems for the case of positive and negative elements of the ring separately.
lemma (in ring1) OrdRing_ZF_2_L4:
assumes \( a\in R \) and \( \neg ( 0 \leq a) \)
shows \( 0 \leq ( - a) \), \( 0 \neq a \) using assms, OrdRing_ZF_1_L4, OrderedGroup_ZF_1_L8AAbsolute value of a product is the product of absolute values.
lemma (in ring1) OrdRing_ZF_2_L5:
assumes A1: \( a\in R \), \( b\in R \)
shows \( \vert a\cdot b\vert = \vert a\vert \cdot \vert b\vert \)proof{
}
assume A2: \( 0 \leq a \)
have \( \vert a\cdot b\vert = \vert a\vert \cdot \vert b\vert \)proof
{
}
assume \( 0 \leq b \)
with A2 have \( \vert a\cdot b\vert = \vert a\vert \cdot \vert b\vert \) using OrdRing_ZF_2_L1
moreover {
}
ultimately show \( thesis \)
qed
assume \( \neg ( 0 \leq b) \)
with A1, A2 have \( \vert a\cdot ( - b)\vert = \vert a\vert \cdot \vert - b\vert \) using OrdRing_ZF_2_L4, OrdRing_ZF_2_L1
with A1 have \( \vert a\cdot b\vert = \vert a\vert \cdot \vert b\vert \) using OrdRing_ZF_2_L2, OrdRing_ZF_2_L3
moreover {
}
ultimately show \( thesis \)
qed
assume \( \neg ( 0 \leq a) \)
with A1 have A3: \( 0 \leq ( - a) \) using OrdRing_ZF_2_L4
have \( \vert a\cdot b\vert = \vert a\vert \cdot \vert b\vert \)proof
{
}
assume \( 0 \leq b \)
with A3 have \( \vert ( - a)\cdot b\vert = \vert - a\vert \cdot \vert b\vert \) using OrdRing_ZF_2_L1
with A1 have \( \vert a\cdot b\vert = \vert a\vert \cdot \vert b\vert \) using OrdRing_ZF_2_L2, OrdRing_ZF_2_L3
moreover {
}
ultimately show \( thesis \)
qed
assume \( \neg ( 0 \leq b) \)
with A1, A3 have \( \vert ( - a)\cdot ( - b)\vert = \vert - a\vert \cdot \vert - b\vert \) using OrdRing_ZF_2_L4, OrdRing_ZF_2_L1
with A1 have \( \vert a\cdot b\vert = \vert a\vert \cdot \vert b\vert \) using OrdRing_ZF_2_L2, OrdRing_ZF_2_L3
Triangle inequality. Property of linearly ordered abelian groups.
lemma (in ring1) ord_ring_triangle_ineq:
assumes \( a\in R \), \( b\in R \)
shows \( \vert a + b\vert \leq \vert a\vert + \vert b\vert \) using assms, OrdRing_ZF_1_L4, OrdGroup_triangle_ineqIf \(a\leq c\) and \(b\leq c\), then \(a+b\leq 2\cdot c\).
lemma (in ring1) OrdRing_ZF_2_L6:
assumes \( a\leq c \), \( b\leq c \)
shows \( a + b \leq 2 \cdot c \) using assms, OrdRing_ZF_1_L4, OrderedGroup_ZF_1_L5B, OrdRing_ZF_1_L3, Ring_ZF_1_L3Positivity in ordered rings
This section is about properties of the set of positive elements \( R_+ \).
The set of positive elements is closed under ring addition. This is a property of ordered groups, we just reference a theorem from OrderedGroup_ZF theory in the proof.
lemma (in ring1) OrdRing_ZF_3_L1:
shows \( R_+ \text{ is closed under } A \) using OrdRing_ZF_1_L4, OrderedGroup_ZF_1_L13Every element of a ring can be either in the postitive set, equal to zero or its opposite (the additive inverse) is in the positive set. This is a property of ordered groups, we just reference a theorem from OrderedGroup_ZF theory.
lemma (in ring1) OrdRing_ZF_3_L2:
assumes \( a\in R \)
shows \( \text{Exactly_1_of_3_holds} (a= 0 , a\in R_+, ( - a) \in R_+) \) using assms, OrdRing_ZF_1_L4, OrdGroup_decompIf a ring element \(a\neq 0\), and it is not positive, then \(-a\) is positive.
lemma (in ring1) OrdRing_ZF_3_L2A:
assumes \( a\in R \), \( a\neq 0 \), \( a \notin R_+ \)
shows \( ( - a) \in R_+ \) using assms, OrdRing_ZF_1_L4, OrdGroup_cases\( R_+ \) is closed under multiplication iff the ring has no zero divisors.
lemma (in ring1) OrdRing_ZF_3_L3:
shows \( (R_+ \text{ is closed under } M)\longleftrightarrow \text{HasNoZeroDivs}(R,A,M) \)proof assume A1: \( \text{HasNoZeroDivs}(R,A,M) \)
{
fix \( a \) \( b \)
assume \( a\in R_+ \), \( b\in R_+ \)
then have \( 0 \leq a \), \( a\neq 0 \), \( 0 \leq b \), \( b\neq 0 \) using PositiveSet_def
with A1 have \( a\cdot b \in R_+ \) using OrdRing_ZF_1_L5, Ring_ZF_1_L2, OrdRing_ZF_1_L3, Ring_ZF_1_L12, OrdRing_ZF_1_L4, OrderedGroup_ZF_1_L2A
then show \( R_+ \text{ is closed under } M \) using IsOpClosed_def
next
assume A2: \( R_+ \text{ is closed under } M \)
{
fix \( a \) \( b \)
assume A3: \( a\in R \), \( b\in R \) and \( a\neq 0 \), \( b\neq 0 \)
with A2 have \( \vert a\cdot b\vert \in R_+ \) using OrdRing_ZF_1_L4, OrderedGroup_ZF_3_L12, IsOpClosed_def, OrdRing_ZF_2_L5
with A3 have \( a\cdot b \neq 0 \) using PositiveSet_def, Ring_ZF_1_L4, OrdRing_ZF_1_L4, OrderedGroup_ZF_3_L2A
then show \( \text{HasNoZeroDivs}(R,A,M) \) using HasNoZeroDivs_def
qed
Another (in addition to OrdRing_ZF_1_L6 sufficient condition that defines order in an ordered ring starting from the positive set.
theorem (in ring0) ring_ord_by_positive_set:
assumes A1: \( M \text{ is commutative on } R \) and A2: \( P\subseteq R \), \( P \text{ is closed under } A \), \( 0 \notin P \) and A3: \( \forall a\in R.\ a\neq 0 \longrightarrow (a\in P) \text{ Xor } (( - a) \in P) \) and A4: \( P \text{ is closed under } M \) and A5: \( r = \text{OrderFromPosSet}(R,A,P) \)
shows \( \text{IsAnOrdGroup}(R,A,r) \), \( \text{IsAnOrdRing}(R,A,M,r) \), \( r \text{ is total on } R \), \( \text{PositiveSet}(R,A,r) = P \), \( \text{Nonnegative}(R,A,r) = P \cup \{ 0 \} \), \( \text{HasNoZeroDivs}(R,A,M) \)proof from A2, A3, A5 show I: \( \text{IsAnOrdGroup}(R,A,r) \), \( r \text{ is total on } R \) and II: \( \text{PositiveSet}(R,A,r) = P \) and III: \( \text{Nonnegative}(R,A,r) = P \cup \{ 0 \} \) using Ring_ZF_1_L1, Group_ord_by_positive_set
from A2, A4, III have \( \text{Nonnegative}(R,A,r) \text{ is closed under } M \) using Ring_ZF_1_L16
with ringAssum, A1, I show \( \text{IsAnOrdRing}(R,A,M,r) \) using OrdRing_ZF_1_L6
with A4, II show \( \text{HasNoZeroDivs}(R,A,M) \) using OrdRing_ZF_1_L2, OrdRing_ZF_3_L3
qed
Nontrivial ordered rings are infinite. More precisely we assume that the neutral element of the additive operation is not equal to the multiplicative neutral element and show that the the set of positive elements of the ring is not a finite subset of the ring and the ring is not a finite subset of itself.
theorem (in ring1) ord_ring_infinite:
assumes \( 0 \neq 1 \)
shows \( R_+ \notin Fin(R) \), \( R \notin Fin(R) \) using assms, Ring_ZF_1_L17, OrdRing_ZF_1_L4, Linord_group_infiniteIf every element of a nontrivial ordered ring can be dominated by an element from \(B\), then we \(B\) is not bounded and not finite.
lemma (in ring1) OrdRing_ZF_3_L4:
assumes \( 0 \neq 1 \) and \( \forall a\in R.\ \exists b\in B.\ a\leq b \)
shows \( \neg \text{IsBoundedAbove}(B,r) \), \( B \notin Fin(R) \) using assms, Ring_ZF_1_L17, OrdRing_ZF_1_L4, OrderedGroup_ZF_2_L2AIf \(m\) is greater or equal the multiplicative unit, then the set \(\{m\cdot n: n\in R\}\) is infinite (unless the ring is trivial).
lemma (in ring1) OrdRing_ZF_3_L5:
assumes A1: \( 0 \neq 1 \) and A2: \( 1 \leq m \)
shows \( \{m\cdot x.\ x\in R_+\} \notin Fin(R) \), \( \{m\cdot x.\ x\in R\} \notin Fin(R) \), \( \{( - m)\cdot x.\ x\in R\} \notin Fin(R) \)proof from A2 have T: \( m\in R \) using OrdRing_ZF_1_L3
from A2 have \( 0 \leq 1 \), \( 1 \leq m \) using ordring_one_is_nonneg
then have I: \( 0 \leq m \) by (rule ring_ord_transitive )
let \( B = \{m\cdot x.\ x\in R_+\} \)
{
fix \( a \)
assume A3: \( a\in R \)
then have \( a\leq 0 \vee ( 0 \leq a \wedge a\neq 0 ) \) using ord_ring_split2
moreover {
}
moreover {
}
ultimately have \( \exists b\in B.\ a\leq b \)
assume A4: \( a\leq 0 \)
from A1 have \( m\cdot 1 \in B \) using ordring_one_is_pos
with T have \( m\in B \) using Ring_ZF_1_L3
moreover
from A4, I have \( a\leq m \) by (rule ring_ord_transitive )
ultimately have \( \exists b\in B.\ a\leq b \)
assume A4: \( 0 \leq a \wedge a\neq 0 \)
with A3 have \( m\cdot a \in B \) using PositiveSet_def
moreover
from A2, A4 have \( 1 \cdot a \leq m\cdot a \) using OrdRing_ZF_1_L9
with A3 have \( a \leq m\cdot a \) using Ring_ZF_1_L3
ultimately have \( \exists b\in B.\ a\leq b \)
then have \( \forall a\in R.\ \exists b\in B.\ a\leq b \)
with A1 show \( B \notin Fin(R) \) using OrdRing_ZF_3_L4
moreover
qed
have \( B \subseteq \{m\cdot x.\ x\in R\} \) using PositiveSet_def
ultimately show \( \{m\cdot x.\ x\in R\} \notin Fin(R) \) using Fin_subset
with T show \( \{( - m)\cdot x.\ x\in R\} \notin Fin(R) \) using Ring_ZF_1_L18
If \(m\) is less or equal than the negative of multiplicative unit, then the set \(\{m\cdot n: n\in R\}\) is infinite (unless the ring is trivial).
lemma (in ring1) OrdRing_ZF_3_L6:
assumes A1: \( 0 \neq 1 \) and A2: \( m \leq - 1 \)
shows \( \{m\cdot x.\ x\in R\} \notin Fin(R) \)proof from A2 have \( ( - ( - 1 )) \leq - m \) using OrdRing_ZF_1_L4B
with A1 have \( \{( - m)\cdot x.\ x\in R\} \notin Fin(R) \) using Ring_ZF_1_L2, Ring_ZF_1_L3, OrdRing_ZF_3_L5
with A2 show \( \{m\cdot x.\ x\in R\} \notin Fin(R) \) using OrdRing_ZF_1_L3, Ring_ZF_1_L18
qed
All elements greater or equal than an element of \( R_+ \) belong to \( R_+ \). Property of ordered groups.
lemma (in ring1) OrdRing_ZF_3_L7:
assumes A1: \( a \in R_+ \) and A2: \( a\leq b \)
shows \( b \in R_+ \)proof from A1, A2 have \( group3(R,A,r) \), \( a \in \text{PositiveSet}(R,A,r) \), \( \langle a,b\rangle \in r \) using OrdRing_ZF_1_L4
then have \( b \in \text{PositiveSet}(R,A,r) \) by (rule OrderedGroup_ZF_1_L19 )
then show \( b \in R_+ \)
qed
A special case of OrdRing_ZF_3_L7: a ring element greater or equal than \(1\) is positive.
corollary (in ring1) OrdRing_ZF_3_L8:
assumes A1: \( 0 \neq 1 \) and A2: \( 1 \leq a \)
shows \( a \in R_+ \)proof from A1, A2 have \( 1 \in R_+ \), \( 1 \leq a \) using ordring_one_is_pos
then show \( a \in R_+ \) by (rule OrdRing_ZF_3_L7 )
qed
Adding a positive element to \(a\) strictly increases \(a\). Property of ordered groups.
lemma (in ring1) OrdRing_ZF_3_L9:
assumes A1: \( a\in R \), \( b\in R_+ \)
shows \( a \leq a + b \), \( a \neq a + b \) using assms, OrdRing_ZF_1_L4, OrderedGroup_ZF_1_L22A special case of OrdRing_ZF_3_L9: in nontrivial rings adding one to \(a\) increases \(a\).
corollary (in ring1) OrdRing_ZF_3_L10:
assumes A1: \( 0 \neq 1 \) and A2: \( a\in R \)
shows \( a \leq a + 1 \), \( a \neq a + 1 \) using assms, ordring_one_is_pos, OrdRing_ZF_3_L9If \(a\) is not greater than \(b\), then it is strictly less than \(b+1\).
lemma (in ring1) OrdRing_ZF_3_L11:
assumes A1: \( 0 \neq 1 \) and A2: \( a\leq b \)
shows \( a \lt b + 1 \)proof from A1, A2 have I: \( b \lt b + 1 \) using OrdRing_ZF_1_L3, OrdRing_ZF_3_L10
with A2 show \( a \lt b + 1 \) by (rule ring_strict_ord_transit )
qed
For any ring element \(a\) the greater of \(a\) and \(1\) is a positive element that is greater or equal than \(m\). If we add \(1\) to it we get a positive element that is strictly greater than \(m\). This holds in nontrivial rings.
lemma (in ring1) OrdRing_ZF_3_L12:
assumes A1: \( 0 \neq 1 \) and A2: \( a\in R \)
shows \( a \leq \text{GreaterOf}(r,1 ,a) \), \( \text{GreaterOf}(r,1 ,a) \in R_+ \), \( \text{GreaterOf}(r,1 ,a) + 1 \in R_+ \), \( a \leq \text{GreaterOf}(r,1 ,a) + 1 \), \( a \neq \text{GreaterOf}(r,1 ,a) + 1 \)proof from linord have \( r \text{ is total on } R \) using IsLinOrder_def
moreover
from A2 have \( 1 \in R \), \( a\in R \) using Ring_ZF_1_L2
ultimately have \( 1 \leq \text{GreaterOf}(r,1 ,a) \) and I: \( a \leq \text{GreaterOf}(r,1 ,a) \) using Order_ZF_3_L2
with A1 show \( a \leq \text{GreaterOf}(r,1 ,a) \) and \( \text{GreaterOf}(r,1 ,a) \in R_+ \) using OrdRing_ZF_3_L8
with A1 show \( \text{GreaterOf}(r,1 ,a) + 1 \in R_+ \) using ordring_one_is_pos, OrdRing_ZF_3_L1, IsOpClosed_def
from A1, I show \( a \leq \text{GreaterOf}(r,1 ,a) + 1 \), \( a \neq \text{GreaterOf}(r,1 ,a) + 1 \) using OrdRing_ZF_3_L11
qed
We can multiply strict inequality by a positive element.
lemma (in ring1) OrdRing_ZF_3_L13:
assumes A1: \( \text{HasNoZeroDivs}(R,A,M) \) and A2: \( a \lt b \) and A3: \( c\in R_+ \)
shows \( a\cdot c \lt b\cdot c \), \( c\cdot a \lt c\cdot b \)proof from A2, A3 have T: \( a\in R \), \( b\in R \), \( c\in R \), \( c\neq 0 \) using OrdRing_ZF_1_L3, PositiveSet_def
from A2, A3 have \( a\cdot c \leq b\cdot c \) using OrdRing_ZF_1_L9A
moreover
from A1, A2, T have \( a\cdot c \neq b\cdot c \) using Ring_ZF_1_L12A
ultimately show \( a\cdot c \lt b\cdot c \)
moreover
qed
from mult_commut, T have \( a\cdot c = c\cdot a \) and \( b\cdot c = c\cdot b \) using IsCommutative_def
ultimately show \( c\cdot a \lt c\cdot b \)
A sufficient condition for an element to be in the set of positive ring elements.
lemma (in ring1) OrdRing_ZF_3_L14:
assumes \( 0 \leq a \) and \( a\neq 0 \)
shows \( a \in R_+ \) using assms, OrdRing_ZF_1_L3, PositiveSet_defIf a ring has no zero divisors, the square of a nonzero element is positive.
lemma (in ring1) OrdRing_ZF_3_L15:
assumes \( \text{HasNoZeroDivs}(R,A,M) \) and \( a\in R \), \( a\neq 0 \)
shows \( 0 \leq a^2 \), \( a^2 \neq 0 \), \( a^2 \in R_+ \) using assms, OrdRing_ZF_1_L10, Ring_ZF_1_L12, OrdRing_ZF_3_L14In rings with no zero divisors we can (strictly) increase a positive element by multiplying it by an element that is greater than \(1\).
lemma (in ring1) OrdRing_ZF_3_L16:
assumes \( \text{HasNoZeroDivs}(R,A,M) \) and \( a \in R_+ \) and \( 1 \leq b \), \( 1 \neq b \)
shows \( a\leq a\cdot b \), \( a \neq a\cdot b \) using assms, PositiveSet_def, OrdRing_ZF_1_L16, OrdRing_ZF_1_L3, Ring_ZF_1_L12CIf the right hand side of an inequality is positive we can multiply it by a number that is greater than one.
lemma (in ring1) OrdRing_ZF_3_L17:
assumes A1: \( \text{HasNoZeroDivs}(R,A,M) \) and A2: \( b\in R_+ \) and A3: \( a\leq b \) and A4: \( 1 \lt c \)
shows \( a \lt b\cdot c \)proof from A1, A2, A4 have \( b \lt b\cdot c \) using OrdRing_ZF_3_L16
with A3 show \( a \lt b\cdot c \) by (rule ring_strict_ord_transit )
qed
We can multiply a right hand side of an inequality between positive numbers by a number that is greater than one.
lemma (in ring1) OrdRing_ZF_3_L18:
assumes A1: \( \text{HasNoZeroDivs}(R,A,M) \) and A2: \( a \in R_+ \) and A3: \( a\leq b \) and A4: \( 1 \lt c \)
shows \( a \lt b\cdot c \)proof from A2, A3 have \( b \in R_+ \) using OrdRing_ZF_3_L7
with A1, A3, A4 show \( a \lt b\cdot c \) using OrdRing_ZF_3_L17
qed
In ordered rings with no zero divisors if at least one of \(a,b\) is not zero, then \(0 < a^2+b^2\), in particular \(a^2+b^2\neq 0\).
lemma (in ring1) OrdRing_ZF_3_L19:
assumes A1: \( \text{HasNoZeroDivs}(R,A,M) \) and A2: \( a\in R \), \( b\in R \) and A3: \( a \neq 0 \vee b \neq 0 \)
shows \( 0 \lt a^2 + b^2 \)proof{
}
assume \( a \neq 0 \)
with A1, A2 have \( 0 \leq a^2 \), \( a^2 \neq 0 \) using OrdRing_ZF_3_L15
then have \( 0 \lt a^2 \)
moreover
from A2 have \( 0 \leq b^2 \) using OrdRing_ZF_1_L10
ultimately have \( 0 + 0 \lt a^2 + b^2 \) using OrdRing_ZF_1_L19
then have \( 0 \lt a^2 + b^2 \) using Ring_ZF_1_L2, Ring_ZF_1_L3
moreover {
}
ultimately show \( 0 \lt a^2 + b^2 \)
qed
assume A4: \( a = 0 \)
then have \( a^2 + b^2 = 0 + b^2 \) using Ring_ZF_1_L2, Ring_ZF_1_L6
also
from A2 have \( \ldots = b^2 \) using Ring_ZF_1_L4, Ring_ZF_1_L3
finally have \( a^2 + b^2 = b^2 \)
moreover
from A3, A4 have \( b \neq 0 \)
with A1, A2 have \( 0 \leq b^2 \) and \( b^2 \neq 0 \) using OrdRing_ZF_3_L15
hence \( 0 \lt b^2 \)
ultimately have \( 0 \lt a^2 + b^2 \)
end
Definition of IsAnOrdRing:
\( \text{IsAnOrdRing}(R,A,M,r) \equiv \)
\( ( \text{IsAring}(R,A,M) \wedge (M \text{ is commutative on } R) \wedge \)
\( r\subseteq R\times R \wedge \text{IsLinOrder}(R,r) \wedge \)
\( (\forall a b.\ \forall c\in R.\ \langle a,b\rangle \in r \longrightarrow \langle A\langle a,c\rangle ,A\langle b,c\rangle \rangle \in r) \wedge \)
\( ( \text{Nonnegative}(R,A,r) \text{ is closed under } M)) \)
lemma (in ring1) OrdRing_ZF_1_L3:
assumes \( a\leq b \)
shows \( a\in R \), \( b\in R \)Definition of IsAring:
\( \text{IsAring}(R,A,M) \equiv \text{IsAgroup}(R,A) \wedge (A \text{ is commutative on } R) \wedge \)
\( \text{IsAmonoid}(R,M) \wedge \text{IsDistributive}(R,A,M) \)
Definition of IsCommutative:
\( f \text{ is commutative on } G \equiv \forall x\in G.\ \forall y\in G.\ f\langle x,y\rangle = f\langle y,x\rangle \)
lemma Order_ZF_1_L2:
assumes \( \text{IsLinOrder}(X,r) \)
shows \( \text{IsPartOrder}(X,r) \)Definition of IsAnOrdGroup:
\( \text{IsAnOrdGroup}(G,P,r) \equiv \)
\( ( \text{IsAgroup}(G,P) \wedge r\subseteq G\times G \wedge \text{IsPartOrder}(G,r) \wedge (\forall g\in G.\ \forall a b.\ \)
\( \langle a,b\rangle \in r \longrightarrow \langle P\langle a,g\rangle ,P\langle b,g\rangle \rangle \in r \wedge \langle P\langle g,a\rangle ,P\langle g,b\rangle \rangle \in r ) ) \)
Definition of IsLinOrder:
\( \text{IsLinOrder}(X,r) \equiv \text{antisym}(r) \wedge \text{trans}(r) \wedge (r \text{ is total on } X) \)
lemma (in ring1) OrdRing_ZF_1_L4: shows \( \text{IsAnOrdGroup}(R,A,r) \), \( r \text{ is total on } R \), \( A \text{ is commutative on } R \), \( group3(R,A,r) \)
lemma (in group3) Group_order_transitive:
assumes \( a\leq b \), \( b\leq c \)
shows \( a\leq c \) lemma (in group3) OrderedGroup_ZF_1_L4A:
assumes \( a \lt b \) and \( b\leq c \)
shows \( a \lt c \) lemma (in group3) group_strict_ord_transit:
assumes \( a\leq b \) and \( b \lt c \)
shows \( a \lt c \) lemma (in group3) OrderedGroup_ZF_1_L8:
assumes \( r \text{ is total on } G \) and \( a\in G \), \( b\in G \) and \( \neg (a\leq b) \)
shows \( b \leq a \), \( a^{-1} \leq b^{-1} \), \( a\neq b \), \( b \lt a \) lemma (in ring0) Ring_ZF_1_L2: shows \( 0 \in R \), \( 1 \in R \), \( ( - 0 ) = 0 \)
lemma (in ring1) OrdRing_ZF_1_L4A:
assumes \( a\in R \), \( b\in R \) and \( \neg (a\leq b) \)
shows \( b \leq a \), \( ( - a) \leq ( - b) \), \( a\neq b \) lemma (in group3) OrderedGroup_ZF_1_L5:
assumes \( a\leq b \)
shows \( b^{-1}\leq a^{-1} \) lemma (in group3) OrderedGroup_ZF_1_L2: shows \( g\in G^+ \longleftrightarrow 1 \leq g \)
Definition of IsOpClosed:
\( A \text{ is closed under } f \equiv \forall x\in A.\ \forall y\in A.\ f\langle x,y\rangle \in A \)
lemma (in group3) OrderedGroup_ZF_1_L5G:
assumes \( a\leq b \) and \( 1 \leq c \)
shows \( a\leq b\cdot c \), \( a\leq c\cdot b \) lemma (in ring0) Ring_ZF_1_L3:
assumes \( a\in R \)
shows \( ( - a) \in R \), \( ( - ( - a)) = a \), \( a + 0 = a \), \( 0 + a = a \), \( a\cdot 1 = a \), \( 1 \cdot a = a \), \( a - a = 0 \), \( a - 0 = a \), \( 2 \cdot a = a + a \), \( ( - a) + a = 0 \) lemma Order_ZF_1_L3:
assumes \( \text{IsPartOrder}(X,r) \) and \( r \text{ is total on } X \)
shows \( \text{IsLinOrder}(X,r) \) lemma (in group3) OrderedGroup_ZF_1_L9:
assumes \( a\in G \), \( b\in G \)
shows \( a\leq b \longleftrightarrow a\cdot b^{-1} \leq 1 \) lemma (in ring0) Ring_ZF_1_L4:
assumes \( a\in R \), \( b\in R \)
shows \( a + b \in R \), \( a - b \in R \), \( a\cdot b \in R \), \( a + b = b + a \) lemma (in group3) OrderedGroup_ZF_1_L5A:
assumes \( a\leq 1 \)
shows \( 1 \leq a^{-1} \) lemma (in ring1) OrdRing_ZF_1_L5:
assumes \( 0 \leq a \), \( 0 \leq b \)
shows \( 0 \leq a\cdot b \) lemma (in ring0) Ring_ZF_1_L7:
assumes \( a\in R \), \( b\in R \)
shows \( ( - a)\cdot b = - (a\cdot b) \), \( a\cdot ( - b) = - (a\cdot b) \), \( ( - a)\cdot b = a\cdot ( - b) \) lemma (in group3) OrderedGroup_ZF_1_L5AA:
assumes \( a\in G \) and \( 1 \leq a^{-1} \)
shows \( a\leq 1 \) lemma (in ring1) OrdRing_ZF_1_L7:
assumes \( a\in R \), \( b\in R \)
shows \( a\leq b \longleftrightarrow a - b \leq 0 \) lemma (in ring1) OrdRing_ZF_1_L8:
assumes \( a\leq 0 \) and \( 0 \leq b \)
shows \( a\cdot b \leq 0 \) lemma (in ring0) Ring_ZF_1_L8:
assumes \( a\in R \), \( b\in R \), \( c\in R \)
shows \( a\cdot (b - c) = a\cdot b - a\cdot c \), \( (b - c)\cdot a = b\cdot a - c\cdot a \)Definition of PositiveSet:
\( \text{PositiveSet}(L,A,r) \equiv \)
\( \{x\in L.\ \langle \text{ TheNeutralElement}(L,A),x\rangle \in r \wedge \text{ TheNeutralElement}(L,A)\neq x\} \)
lemma (in ring1) OrdRing_ZF_1_L9:
assumes \( a\leq b \) and \( 0 \leq c \)
shows \( a\cdot c \leq b\cdot c \), \( c\cdot a \leq c\cdot b \) corollary (in group3) OrderedGroup_ZF_1_L8A:
assumes \( r \text{ is total on } G \) and \( a\in G \) and \( \neg (1 \leq a) \)
shows \( 1 \leq a^{-1} \), \( 1 \neq a \), \( a\leq 1 \) lemma (in ring0) Ring_ZF_1_L14:
assumes \( a\in R \)
shows \( ( - a)^2 = ((a)^2) \) lemma (in ring1) OrdRing_ZF_1_L10:
assumes \( a\in R \)
shows \( 0 \leq (a^2) \) corollary (in ring1) ordring_one_is_nonneg: shows \( 0 \leq 1 \)
lemma (in group3) OrderedGroup_ZF_1_L5AB:
assumes \( 1 \leq a \)
shows \( a^{-1}\leq 1 \) and \( \neg (a\leq 1 \wedge a\neq 1 ) \) lemma (in ring1) OrdRing_ZF_1_L11:
assumes \( 0 \leq a \)
shows \( \neg (a\leq 0 \wedge a\neq 0 ) \) lemma (in group3) OrderedGroup_ZF_1_L9D:
assumes \( a\leq b \)
shows \( 1 \leq b\cdot a^{-1} \) lemma (in group3) OrderedGroup_ZF_1_L9E:
assumes \( a\leq b \), \( a\neq b \)
shows \( 1 \leq b\cdot a^{-1} \), \( 1 \neq b\cdot a^{-1} \), \( b\cdot a^{-1} \in G_+ \) lemma (in group3) OrderedGroup_ZF_1_L9F:
assumes \( a\in G \), \( b\in G \) and \( 1 \leq b\cdot a^{-1} \)
shows \( a\leq b \) lemma (in ring1) OrdRing_ZF_1_L13:
assumes \( a\leq b \)
shows \( 0 \leq b - a \) lemma (in ring1) OrdRing_ZF_1_L15:
assumes \( a\in R \), \( b\in R \) and \( 0 \leq b - a \)
shows \( a\leq b \) lemma (in ring1) ring_ord_transitive:
assumes \( a\leq b \), \( b\leq c \)
shows \( a\leq c \) lemma (in ring1) OrdRing_ZF_1_L16:
assumes \( 0 \leq a \) and \( 1 \leq b \)
shows \( a\leq a\cdot b \) lemma (in group3) group_strict_ord_transl_inv:
assumes \( a \lt b \) and \( c\in G \)
shows \( a\cdot c \lt b\cdot c \) and \( c\cdot a \lt c\cdot b \) lemma (in group3) OrderedGroup_ZF_1_L12B:
assumes \( a\in G \), \( b\in G \) and \( a\cdot b^{-1} \lt c \)
shows \( a \lt c\cdot b \) lemma (in group3) OrderedGroup_ZF_1_L12C:
assumes \( a \lt b \) and \( c\leq d \)
shows \( a\cdot c \lt b\cdot d \) lemma (in group3) OrderedGroup_ZF_1_L12D:
assumes \( a\leq b \) and \( c \lt d \)
shows \( a\cdot c \lt b\cdot d \) lemma (in group3) OrderedGroup_ZF_3_L2:
assumes \( a\in G^+ \)
shows \( \vert a\vert = a \) lemma (in group3) OrderedGroup_ZF_3_L7A:
assumes \( r \text{ is total on } G \) and \( a\in G \)
shows \( \vert a^{-1}\vert = \vert a\vert \) lemma (in ring0) Ring_ZF_1_L7A:
assumes \( a\in R \), \( b\in R \)
shows \( ( - a)\cdot ( - b) = a\cdot b \) lemma (in ring1) OrdRing_ZF_2_L2:
assumes \( a\in R \)
shows \( \vert - a\vert = \vert a\vert \) lemma (in ring1) OrdRing_ZF_2_L1:
assumes \( 0 \leq a \), \( 0 \leq b \)
shows \( \vert a\cdot b\vert = \vert a\vert \cdot \vert b\vert \) lemma (in ring1) OrdRing_ZF_2_L4:
assumes \( a\in R \) and \( \neg ( 0 \leq a) \)
shows \( 0 \leq ( - a) \), \( 0 \neq a \) lemma (in ring1) OrdRing_ZF_2_L3:
assumes \( a\in R \), \( b\in R \)
shows \( \vert ( - a)\cdot b\vert = \vert a\cdot b\vert \), \( \vert a\cdot ( - b)\vert = \vert a\cdot b\vert \), \( \vert ( - a)\cdot ( - b)\vert = \vert a\cdot b\vert \) theorem (in group3) OrdGroup_triangle_ineq:
assumes \( P \text{ is commutative on } G \) and \( r \text{ is total on } G \) and \( a\in G \), \( b\in G \)
shows \( \vert a\cdot b\vert \leq \vert a\vert \cdot \vert b\vert \) lemma (in group3) OrderedGroup_ZF_1_L5B:
assumes \( a\leq b \) and \( c\leq d \)
shows \( a\cdot c \leq b\cdot d \) lemma (in group3) OrderedGroup_ZF_1_L13: shows \( G_+ \text{ is closed under } P \)
lemma (in group3) OrdGroup_decomp:
assumes \( r \text{ is total on } G \) and \( a\in G \)
shows \( \text{Exactly_1_of_3_holds} (a=1 ,a\in G_+,a^{-1}\in G_+) \) lemma (in group3) OrdGroup_cases:
assumes \( r \text{ is total on } G \) and \( a\in G \) and \( a\neq 1 \), \( a\notin G_+ \)
shows \( a^{-1} \in G_+ \) lemma (in ring0) Ring_ZF_1_L12:
assumes \( \text{HasNoZeroDivs}(R,A,M) \) and \( a\in R \), \( a\neq 0 \), \( b\in R \), \( b\neq 0 \)
shows \( a\cdot b\neq 0 \) lemma (in group3) OrderedGroup_ZF_1_L2A: shows \( g\in G_+ \longleftrightarrow (1 \leq g \wedge g\neq 1 ) \)
lemma (in group3) OrderedGroup_ZF_3_L12:
assumes \( r \text{ is total on } G \) and \( a\in G \) and \( a\neq 1 \)
shows \( \vert a\vert \in G_+ \) lemma (in ring1) OrdRing_ZF_2_L5:
assumes \( a\in R \), \( b\in R \)
shows \( \vert a\cdot b\vert = \vert a\vert \cdot \vert b\vert \) lemma (in group3) OrderedGroup_ZF_3_L2A: shows \( \vert 1 \vert = 1 \)
Definition of HasNoZeroDivs:
\( \text{HasNoZeroDivs}(R,A,M) \equiv (\forall a\in R.\ \forall b\in R.\ \)
\( M\langle a,b\rangle = \text{ TheNeutralElement}(R,A) \longrightarrow \)
\( a = \text{ TheNeutralElement}(R,A) \vee b = \text{ TheNeutralElement}(R,A)) \)
lemma (in ring0) Ring_ZF_1_L1: shows \( monoid0(R,M) \), \( group0(R,A) \), \( A \text{ is commutative on } R \)
theorem (in group0) Group_ord_by_positive_set:
assumes \( P \text{ is commutative on } G \) and \( H\subseteq G \), \( H \text{ is closed under } P \), \( 1 \notin H \) and \( \forall a\in G.\ a\neq 1 \longrightarrow (a\in H) \text{ Xor } (a^{-1}\in H) \)
shows \( \text{IsAnOrdGroup}(G,P, \text{OrderFromPosSet}(G,P,H)) \), \( \text{OrderFromPosSet}(G,P,H) \text{ is total on } G \), \( \text{PositiveSet}(G,P, \text{OrderFromPosSet}(G,P,H)) = H \), \( \text{Nonnegative}(G,P, \text{OrderFromPosSet}(G,P,H)) = H \cup \{1 \} \) lemma (in ring0) Ring_ZF_1_L16:
assumes \( H \subseteq R \) and \( H \text{ is closed under } M \)
shows \( (H \cup \{ 0 \}) \text{ is closed under } M \) lemma OrdRing_ZF_1_L6:
assumes \( \text{IsAring}(R,A,M) \), \( M \text{ is commutative on } R \), \( \text{Nonnegative}(R,A,r) \text{ is closed under } M \), \( \text{IsAnOrdGroup}(R,A,r) \), \( r \text{ is total on } R \)
shows \( \text{IsAnOrdRing}(R,A,M,r) \) lemma OrdRing_ZF_1_L2:
assumes \( \text{IsAnOrdRing}(R,A,M,r) \)
shows \( ring1(R,A,M,r) \) lemma (in ring1) OrdRing_ZF_3_L3: shows \( (R_+ \text{ is closed under } M)\longleftrightarrow \text{HasNoZeroDivs}(R,A,M) \)
lemma (in ring0) Ring_ZF_1_L17: shows \( R = \{ 0 \} \longleftrightarrow 0 =1 \)
theorem (in group3) Linord_group_infinite:
assumes \( r \text{ is total on } G \) and \( G \neq \{1 \} \)
shows \( G_+ \notin Fin(G) \), \( G \notin Fin(G) \) lemma (in group3) OrderedGroup_ZF_2_L2A:
assumes \( r \text{ is total on } G \) and \( G \neq \{1 \} \) and \( \forall a\in G.\ \exists b\in A.\ a\leq b \)
shows \( \forall a\in G.\ \exists b\in A.\ a\neq b \wedge a\leq b \), \( \neg \text{IsBoundedAbove}(A,r) \), \( A \notin Fin(G) \) corollary (in ring1) ord_ring_split2:
assumes \( a\in R \)
shows \( a\leq 0 \vee ( 0 \leq a \wedge a\neq 0 ) \) lemma (in ring1) ordring_one_is_pos:
assumes \( 0 \neq 1 \)
shows \( 1 \in R_+ \) lemma (in ring1) OrdRing_ZF_3_L4:
assumes \( 0 \neq 1 \) and \( \forall a\in R.\ \exists b\in B.\ a\leq b \)
shows \( \neg \text{IsBoundedAbove}(B,r) \), \( B \notin Fin(R) \) lemma (in ring0) Ring_ZF_1_L18:
assumes \( m\in R \)
shows \( \{m\cdot x.\ x\in R\} = \{( - m)\cdot x.\ x\in R\} \) lemma (in ring1) OrdRing_ZF_1_L4B:
assumes \( a\leq b \)
shows \( ( - b) \leq ( - a) \) lemma (in ring1) OrdRing_ZF_3_L5:
assumes \( 0 \neq 1 \) and \( 1 \leq m \)
shows \( \{m\cdot x.\ x\in R_+\} \notin Fin(R) \), \( \{m\cdot x.\ x\in R\} \notin Fin(R) \), \( \{( - m)\cdot x.\ x\in R\} \notin Fin(R) \) lemma (in group3) OrderedGroup_ZF_1_L19:
assumes \( a \in G_+ \) and \( a\leq b \)
shows \( b \in G_+ \) lemma (in ring1) OrdRing_ZF_3_L7:
assumes \( a \in R_+ \) and \( a\leq b \)
shows \( b \in R_+ \) lemma (in group3) OrderedGroup_ZF_1_L22:
assumes \( a\in G \), \( b\in G_+ \)
shows \( a\leq a\cdot b \), \( a \neq a\cdot b \), \( a\cdot b \in G \) lemma (in ring1) OrdRing_ZF_3_L9:
assumes \( a\in R \), \( b\in R_+ \)
shows \( a \leq a + b \), \( a \neq a + b \) corollary (in ring1) OrdRing_ZF_3_L10:
assumes \( 0 \neq 1 \) and \( a\in R \)
shows \( a \leq a + 1 \), \( a \neq a + 1 \) lemma (in ring1) ring_strict_ord_transit:
assumes \( a\leq b \) and \( b \lt c \)
shows \( a \lt c \) lemma Order_ZF_3_L2:
assumes \( r \text{ is total on } X \) and \( x\in X \), \( y\in X \)
shows \( \langle x, \text{GreaterOf}(r,x,y)\rangle \in r \), \( \langle y, \text{GreaterOf}(r,x,y)\rangle \in r \), \( \langle \text{SmallerOf}(r,x,y),x\rangle \in r \), \( \langle \text{SmallerOf}(r,x,y),y\rangle \in r \) corollary (in ring1) OrdRing_ZF_3_L8:
assumes \( 0 \neq 1 \) and \( 1 \leq a \)
shows \( a \in R_+ \) lemma (in ring1) OrdRing_ZF_3_L1: shows \( R_+ \text{ is closed under } A \)
lemma (in ring1) OrdRing_ZF_3_L11:
assumes \( 0 \neq 1 \) and \( a\leq b \)
shows \( a \lt b + 1 \) lemma (in ring1) OrdRing_ZF_1_L9A:
assumes \( a\leq b \) and \( c\in R_+ \)
shows \( a\cdot c \leq b\cdot c \), \( c\cdot a \leq c\cdot b \) lemma (in ring0) Ring_ZF_1_L12A:
assumes \( \text{HasNoZeroDivs}(R,A,M) \) and \( a\in R \), \( b\in R \), \( c\in R \) and \( a\cdot c = b\cdot c \) and \( c\neq 0 \)
shows \( a=b \) lemma (in ring1) OrdRing_ZF_3_L14:
assumes \( 0 \leq a \) and \( a\neq 0 \)
shows \( a \in R_+ \) lemma (in ring0) Ring_ZF_1_L12C:
assumes \( \text{HasNoZeroDivs}(R,A,M) \) and \( a\in R \), \( b\in R \) and \( 0 \neq a \), \( 1 \neq b \)
shows \( a \neq a\cdot b \) lemma (in ring1) OrdRing_ZF_3_L16:
assumes \( \text{HasNoZeroDivs}(R,A,M) \) and \( a \in R_+ \) and \( 1 \leq b \), \( 1 \neq b \)
shows \( a\leq a\cdot b \), \( a \neq a\cdot b \) lemma (in ring1) OrdRing_ZF_3_L17:
assumes \( \text{HasNoZeroDivs}(R,A,M) \) and \( b\in R_+ \) and \( a\leq b \) and \( 1 \lt c \)
shows \( a \lt b\cdot c \) lemma (in ring1) OrdRing_ZF_3_L15:
assumes \( \text{HasNoZeroDivs}(R,A,M) \) and \( a\in R \), \( a\neq 0 \)
shows \( 0 \leq a^2 \), \( a^2 \neq 0 \), \( a^2 \in R_+ \) lemma (in ring1) OrdRing_ZF_1_L19:
assumes \( a \lt b \) and \( c\leq d \)
shows \( a + c \lt b + d \) lemma (in ring0) Ring_ZF_1_L6:
assumes \( x\in R \)
shows \( 0 \cdot x = 0 \), \( x\cdot 0 = 0 \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8