theory OrderedField_ZF imports OrderedRing_ZF Field_ZF
begin
This theory covers basic facts about ordered fiels.
Definition and basic properties
Here we define ordered fields and proove their basic properties.
Ordered field is a notrivial ordered ring such that all non-zero elements have an inverse. We define the notion of being a ordered field as a statement about four sets. The first set, denoted K is the carrier of the field. The second set, denoted A represents the additive operation on K (recall that in ZF set theory functions are sets). The third set M represents the multiplicative operation on K. The fourth set r is the order relation on K.
definition
\( \text{IsAnOrdField}(K,A,M,r) \equiv ( \text{IsAnOrdRing}(K,A,M,r) \wedge \) \( (M \text{ is commutative on } K) \wedge \) \( \text{ TheNeutralElement}(K,A) \neq \text{ TheNeutralElement}(K,M) \wedge \) \( (\forall a\in K.\ a\neq \text{ TheNeutralElement}(K,A)\longrightarrow \) \( (\exists b\in K.\ M\langle a,b\rangle = \text{ TheNeutralElement}(K,M)))) \)
The next context (locale) defines notation used for ordered fields. We do that by extending the notation defined in the ring1 context that is used for ordered rings and adding some assumptions to make sure we are talking about ordered fields in this context. We should rename the carrier from \(R\) used in the ring1 context to \(K\), more appriopriate for fields. Theoretically the Isar locale facility supports such renaming, but we experienced diffculties using some lemmas from ring1 locale after renaming.
locale field1 = ring1 +
assumes mult_commute: \( M \text{ is commutative on } R \)
assumes not_triv: \( 0 \neq 1 \)
assumes inv_exists: \( \forall a\in R.\ a\neq 0 \longrightarrow (\exists b\in R.\ a\cdot b = 1 ) \)
defines \( R_0 \equiv R-\{ 0 \} \)
defines \( a^{-1} \equiv \text{GroupInv}(R_0,\text{restrict}(M,R_0\times R_0))(a) \)
The next lemma assures us that we are talking fields in the field1 context.
lemma (in field1) OrdField_ZF_1_L1:
shows \( \text{IsAnOrdField}(R,A,M,r) \) using OrdRing_ZF_1_L1, mult_commute, not_triv, inv_exists, IsAnOrdField_defOrdered field is a field, of course.
lemma OrdField_ZF_1_L1A:
assumes \( \text{IsAnOrdField}(K,A,M,r) \)
shows \( \text{IsAfield}(K,A,M) \) using assms, IsAnOrdField_def, IsAnOrdRing_def, IsAfield_defTheorems proven in field0 (about fields) context are valid in the field1 context (about ordered fields).
lemma (in field1) OrdField_ZF_1_L1B:
shows \( field0(R,A,M) \) using OrdField_ZF_1_L1, OrdField_ZF_1_L1A, field_field0We can use theorems proven in the field1 context whenever we talk about an ordered field.
lemma OrdField_ZF_1_L2:
assumes \( \text{IsAnOrdField}(K,A,M,r) \)
shows \( field1(K,A,M,r) \) using assms, IsAnOrdField_def, OrdRing_ZF_1_L2, ring1_def, IsAnOrdField_def, field1_axioms_def, field1_defIn ordered rings the existence of a right inverse for all positive elements implies the existence of an inverse for all non zero elements.
lemma (in ring1) OrdField_ZF_1_L3:
assumes A1: \( \forall a\in R_+.\ \exists b\in R.\ a\cdot b = 1 \) and A2: \( c\in R \), \( c\neq 0 \)
shows \( \exists b\in R.\ c\cdot b = 1 \)proof{
}
assume \( c\in R_+ \)
with A1 have \( \exists b\in R.\ c\cdot b = 1 \)
moreover {
}
ultimately show \( thesis \)
qed
assume \( c\notin R_+ \)
with A2 have \( ( - c) \in R_+ \) using OrdRing_ZF_3_L2A
with A1 obtain \( b \) where \( b\in R \) and \( ( - c)\cdot b = 1 \)
with A2 have \( ( - b) \in R \), \( c\cdot ( - b) = 1 \) using Ring_ZF_1_L3, Ring_ZF_1_L7
then have \( \exists b\in R.\ c\cdot b = 1 \)
Ordered fields are easier to deal with, because it is sufficient to show the existence of an inverse for the set of positive elements.
lemma (in ring1) OrdField_ZF_1_L4:
assumes \( 0 \neq 1 \) and \( M \text{ is commutative on } R \) and \( \forall a\in R_+.\ \exists b\in R.\ a\cdot b = 1 \)
shows \( \text{IsAnOrdField}(R,A,M,r) \) using assms, OrdRing_ZF_1_L1, OrdField_ZF_1_L3, IsAnOrdField_defThe set of positive field elements is closed under multiplication.
lemma (in field1) OrdField_ZF_1_L5:
shows \( R_+ \text{ is closed under } M \) using OrdField_ZF_1_L1B, field_has_no_zero_divs, OrdRing_ZF_3_L3The set of positive field elements is closed under multiplication: the explicit version.
lemma (in field1) pos_mul_closed:
assumes A1: \( 0 \lt a \), \( 0 \lt b \)
shows \( 0 \lt a\cdot b \)proof from A1 have \( a \in R_+ \) and \( b \in R_+ \) using OrdRing_ZF_3_L14
then show \( 0 \lt a\cdot b \) using OrdField_ZF_1_L5, IsOpClosed_def, PositiveSet_def
qed
In fields square of a nonzero element is positive.
lemma (in field1) OrdField_ZF_1_L6:
assumes \( a\in R \), \( a\neq 0 \)
shows \( a^2 \in R_+ \) using assms, OrdField_ZF_1_L1B, field_has_no_zero_divs, OrdRing_ZF_3_L15The next lemma restates the fact Field_ZF that out notation for the field inverse means what it is supposed to mean.
lemma (in field1) OrdField_ZF_1_L7:
assumes \( a\in R \), \( a\neq 0 \)
shows \( a\cdot (a^{-1}) = 1 \), \( (a^{-1})\cdot a = 1 \) using assms, OrdField_ZF_1_L1B, Field_ZF_1_L6A simple lemma about multiplication and cancelling of a positive field element.
lemma (in field1) OrdField_ZF_1_L7A:
assumes A1: \( a\in R \), \( b \in R_+ \)
shows \( a\cdot b\cdot b^{-1} = a \), \( a\cdot b^{-1}\cdot b = a \)proof from A1 have \( b\in R \), \( b\neq 0 \) using PositiveSet_def
with A1 show \( a\cdot b\cdot b^{-1} = a \) and \( a\cdot b^{-1}\cdot b = a \) using OrdField_ZF_1_L1B, Field_ZF_1_L7
qed
Some properties of the inverse of a positive element.
lemma (in field1) OrdField_ZF_1_L8:
assumes A1: \( a \in R_+ \)
shows \( a^{-1} \in R_+ \), \( a\cdot (a^{-1}) = 1 \), \( (a^{-1})\cdot a = 1 \)proof from A1 have I: \( a\in R \), \( a\neq 0 \) using PositiveSet_def
with A1 have \( a\cdot (a^{-1})^2 \in R_+ \) using OrdField_ZF_1_L1B, Field_ZF_1_L5, OrdField_ZF_1_L6, OrdField_ZF_1_L5, IsOpClosed_def
with I show \( a^{-1} \in R_+ \) using OrdField_ZF_1_L1B, Field_ZF_2_L1
from I show \( a\cdot (a^{-1}) = 1 \), \( (a^{-1})\cdot a = 1 \) using OrdField_ZF_1_L7
qed
If \(a\) is smaller than \(b\), then \((b-a)^{-1}\) is positive.
lemma (in field1) OrdField_ZF_1_L9:
assumes \( a \lt b \)
shows \( (b - a)^{-1} \in R_+ \) using assms, OrdRing_ZF_1_L14, OrdField_ZF_1_L8In ordered fields if at least one of \(a,b\) is not zero, then \(a^2+b^2 > 0\), in particular \(a^2+b^2\neq 0\) and exists the (multiplicative) inverse of \(a^2+b^2\).
lemma (in field1) OrdField_ZF_1_L10:
assumes A1: \( a\in R \), \( b\in R \) and A2: \( a \neq 0 \vee b \neq 0 \)
shows \( 0 \lt a^2 + b^2 \) and \( \exists c\in R.\ (a^2 + b^2)\cdot c = 1 \)proof from A1, A2 show \( 0 \lt a^2 + b^2 \) using OrdField_ZF_1_L1B, field_has_no_zero_divs, OrdRing_ZF_3_L19
then have \( (a^2 + b^2)^{-1} \in R \) and \( (a^2 + b^2)\cdot (a^2 + b^2)^{-1} = 1 \) using OrdRing_ZF_1_L3, PositiveSet_def, OrdField_ZF_1_L8
then show \( \exists c\in R.\ (a^2 + b^2)\cdot c = 1 \)
qed
Inequalities
In this section we develop tools to deal inequalities in fields.
We can multiply strict inequality by a positive element.
lemma (in field1) OrdField_ZF_2_L1:
assumes \( a \lt b \) and \( c\in R_+ \)
shows \( a\cdot c \lt b\cdot c \) using assms, OrdField_ZF_1_L1B, field_has_no_zero_divs, OrdRing_ZF_3_L13A special case of OrdField_ZF_2_L1 when we multiply an inverse by an element.
lemma (in field1) OrdField_ZF_2_L2:
assumes A1: \( a\in R_+ \) and A2: \( a^{-1} \lt b \)
shows \( 1 \lt b\cdot a \)proof from A1, A2 have \( (a^{-1})\cdot a \lt b\cdot a \) using OrdField_ZF_2_L1
with A1 show \( 1 \lt b\cdot a \) using OrdField_ZF_1_L8
qed
We can multiply an inequality by the inverse of a positive element.
lemma (in field1) OrdField_ZF_2_L3:
assumes \( a\leq b \) and \( c\in R_+ \)
shows \( a\cdot (c^{-1}) \leq b\cdot (c^{-1}) \) using assms, OrdField_ZF_1_L8, OrdRing_ZF_1_L9AWe can multiply a strict inequality by a positive element or its inverse.
lemma (in field1) OrdField_ZF_2_L4:
assumes \( a \lt b \) and \( c\in R_+ \)
shows \( a\cdot c \lt b\cdot c \), \( c\cdot a \lt c\cdot b \), \( a\cdot c^{-1} \lt b\cdot c^{-1} \) using assms, OrdField_ZF_1_L1B, field_has_no_zero_divs, OrdField_ZF_1_L8, OrdRing_ZF_3_L13We can put a positive factor on the other side of an inequality, changing it to its inverse.
lemma (in field1) OrdField_ZF_2_L5:
assumes A1: \( a\in R \), \( b\in R_+ \) and A2: \( a\cdot b \leq c \)
shows \( a \leq c\cdot b^{-1} \)proof from A1, A2 have \( a\cdot b\cdot b^{-1} \leq c\cdot b^{-1} \) using OrdField_ZF_2_L3
with A1 show \( a \leq c\cdot b^{-1} \) using OrdField_ZF_1_L7A
qed
We can put a positive factor on the other side of an inequality, changing it to its inverse, version with a product initially on the right hand side.
lemma (in field1) OrdField_ZF_2_L5A:
assumes A1: \( b\in R \), \( c\in R_+ \) and A2: \( a \leq b\cdot c \)
shows \( a\cdot c^{-1} \leq b \)proof from A1, A2 have \( a\cdot c^{-1} \leq b\cdot c\cdot c^{-1} \) using OrdField_ZF_2_L3
with A1 show \( a\cdot c^{-1} \leq b \) using OrdField_ZF_1_L7A
qed
We can put a positive factor on the other side of a strict inequality, changing it to its inverse, version with a product initially on the left hand side.
lemma (in field1) OrdField_ZF_2_L6:
assumes A1: \( a\in R \), \( b\in R_+ \) and A2: \( a\cdot b \lt c \)
shows \( a \lt c\cdot b^{-1} \)proof from A1, A2 have \( a\cdot b\cdot b^{-1} \lt c\cdot b^{-1} \) using OrdField_ZF_2_L4
with A1 show \( a \lt c\cdot b^{-1} \) using OrdField_ZF_1_L7A
qed
We can put a positive factor on the other side of a strict inequality, changing it to its inverse, version with a product initially on the right hand side.
lemma (in field1) OrdField_ZF_2_L6A:
assumes A1: \( b\in R \), \( c\in R_+ \) and A2: \( a \lt b\cdot c \)
shows \( a\cdot c^{-1} \lt b \)proof from A1, A2 have \( a\cdot c^{-1} \lt b\cdot c\cdot c^{-1} \) using OrdField_ZF_2_L4
with A1 show \( a\cdot c^{-1} \lt b \) using OrdField_ZF_1_L7A
qed
Sometimes we can reverse an inequality by taking inverse on both sides.
lemma (in field1) OrdField_ZF_2_L7:
assumes A1: \( a\in R_+ \) and A2: \( a^{-1} \leq b \)
shows \( b^{-1} \leq a \)proof from A1 have \( a^{-1} \in R_+ \) using OrdField_ZF_1_L8
with A2 have \( b \in R_+ \) using OrdRing_ZF_3_L7
then have T: \( b \in R_+ \), \( b^{-1} \in R_+ \) using OrdField_ZF_1_L8
with A1, A2 have \( b^{-1}\cdot a^{-1}\cdot a \leq b^{-1}\cdot b\cdot a \) using OrdRing_ZF_1_L9A
moreover
qed
from A1, A2, T have \( b^{-1} \in R \), \( a\in R \), \( a\neq 0 \), \( b\in R \), \( b\neq 0 \) using PositiveSet_def, OrdRing_ZF_1_L3
then have \( b^{-1}\cdot a^{-1}\cdot a = b^{-1} \) and \( b^{-1}\cdot b\cdot a = a \) using OrdField_ZF_1_L1B, Field_ZF_1_L7, Field_ZF_1_L6, Ring_ZF_1_L3
ultimately show \( b^{-1} \leq a \)
Sometimes we can reverse a strict inequality by taking inverse on both sides.
lemma (in field1) OrdField_ZF_2_L8:
assumes A1: \( a\in R_+ \) and A2: \( a^{-1} \lt b \)
shows \( b^{-1} \lt a \)proof from A1, A2 have \( a^{-1} \in R_+ \), \( a^{-1} \leq b \) using OrdField_ZF_1_L8
then have \( b \in R_+ \) using OrdRing_ZF_3_L7
then have \( b\in R \), \( b\neq 0 \) using PositiveSet_def
with A2 have \( b^{-1} \neq a \) using OrdField_ZF_1_L1B, Field_ZF_2_L4
with A1, A2 show \( b^{-1} \lt a \) using OrdField_ZF_2_L7
qed
A technical lemma about solving a strict inequality with three field elements and inverse of a difference.
lemma (in field1) OrdField_ZF_2_L9:
assumes A1: \( a \lt b \) and A2: \( (b - a)^{-1} \lt c \)
shows \( 1 + a\cdot c \lt b\cdot c \)proof from A1, A2 have \( (b - a)^{-1} \in R_+ \), \( (b - a)^{-1} \leq c \) using OrdField_ZF_1_L9
then have T1: \( c \in R_+ \) using OrdRing_ZF_3_L7
with A1, A2 have T2: \( a\in R \), \( b\in R \), \( c\in R \), \( c\neq 0 \), \( c^{-1} \in R \) using OrdRing_ZF_1_L3, OrdField_ZF_1_L8, PositiveSet_def
with A1, A2 have \( c^{-1} + a \lt b - a + a \) using OrdRing_ZF_1_L14, OrdField_ZF_2_L8, ring_strict_ord_trans_inv
with T1, T2 have \( (c^{-1} + a)\cdot c \lt b\cdot c \) using Ring_ZF_2_L1A, OrdField_ZF_2_L1
with T1, T2 show \( 1 + a\cdot c \lt b\cdot c \) using ring_oper_distr, OrdField_ZF_1_L8
qed
Definition of real numbers
The only purpose of this section is to define what does it mean to be a model of real numbers.
We define model of real numbers as any quadruple of sets \((K,A,M,r)\) such that \((K,A,M,r)\) is an ordered field and the order relation \(r\) is complete, that is every set that is nonempty and bounded above in this relation has a supremum.
definition
\( \text{IsAmodelOfReals}(K,A,M,r) \equiv \text{IsAnOrdField}(K,A,M,r) \wedge (r \text{ is complete }) \)
end
lemma (in ring1) OrdRing_ZF_1_L1: shows \( \text{IsAnOrdRing}(R,A,M,r) \)
Definition of IsAnOrdField:
\( \text{IsAnOrdField}(K,A,M,r) \equiv ( \text{IsAnOrdRing}(K,A,M,r) \wedge \)
\( (M \text{ is commutative on } K) \wedge \)
\( \text{ TheNeutralElement}(K,A) \neq \text{ TheNeutralElement}(K,M) \wedge \)
\( (\forall a\in K.\ a\neq \text{ TheNeutralElement}(K,A)\longrightarrow \)
\( (\exists b\in K.\ M\langle a,b\rangle = \text{ TheNeutralElement}(K,M)))) \)
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)) \)
Definition of IsAfield:
\( \text{IsAfield}(K,A,M) \equiv \)
\( ( \text{IsAring}(K,A,M) \wedge (M \text{ is commutative on } K) \wedge \)
\( \text{ TheNeutralElement}(K,A) \neq \text{ TheNeutralElement}(K,M) \wedge \)
\( (\forall a\in K.\ a\neq \text{ TheNeutralElement}(K,A)\longrightarrow \)
\( (\exists b\in K.\ M\langle a,b\rangle = \text{ TheNeutralElement}(K,M)))) \)
lemma (in field1) OrdField_ZF_1_L1: shows \( \text{IsAnOrdField}(R,A,M,r) \)
lemma OrdField_ZF_1_L1A:
assumes \( \text{IsAnOrdField}(K,A,M,r) \)
shows \( \text{IsAfield}(K,A,M) \) lemma field_field0:
assumes \( \text{IsAfield}(K,A,M) \)
shows \( field0(K,A,M) \) lemma OrdRing_ZF_1_L2:
assumes \( \text{IsAnOrdRing}(R,A,M,r) \)
shows \( ring1(R,A,M,r) \) lemma (in ring1) OrdRing_ZF_3_L2A:
assumes \( a\in R \), \( a\neq 0 \), \( a \notin R_+ \)
shows \( ( - a) \in R_+ \) 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 (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 ring1) OrdField_ZF_1_L3:
assumes \( \forall a\in R_+.\ \exists b\in R.\ a\cdot b = 1 \) and \( c\in R \), \( c\neq 0 \)
shows \( \exists b\in R.\ c\cdot b = 1 \) lemma (in field1) OrdField_ZF_1_L1B: shows \( field0(R,A,M) \)
lemma (in field0) field_has_no_zero_divs: shows \( \text{HasNoZeroDivs}(K,A,M) \)
lemma (in ring1) OrdRing_ZF_3_L3: shows \( (R_+ \text{ is closed under } M)\longleftrightarrow \text{HasNoZeroDivs}(R,A,M) \)
lemma (in ring1) OrdRing_ZF_3_L14:
assumes \( 0 \leq a \) and \( a\neq 0 \)
shows \( a \in R_+ \) lemma (in field1) OrdField_ZF_1_L5: shows \( R_+ \text{ is closed under } M \)
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 \)
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_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 field0) Field_ZF_1_L6:
assumes \( a\in K \), \( a\neq 0 \)
shows \( a\cdot a^{-1} = 1 \), \( a^{-1}\cdot a = 1 \) lemma (in field0) Field_ZF_1_L7:
assumes \( a\in K \), \( b\in K \), \( b\neq 0 \)
shows \( a\cdot b\cdot b^{-1} = a \), \( a\cdot b^{-1}\cdot b = a \) lemma (in field0) Field_ZF_1_L5:
assumes \( a\in K \), \( a\neq 0 \)
shows \( a^{-1} \in K_0 \), \( (a^{-1})^2 \in K_0 \), \( a^{-1} \in K \), \( a^{-1} \neq 0 \) lemma (in field1) OrdField_ZF_1_L6:
assumes \( a\in R \), \( a\neq 0 \)
shows \( a^2 \in R_+ \) lemma (in field0) Field_ZF_2_L1:
assumes \( a\in K \), \( a\neq 0 \)
shows \( a\cdot (a^{-1})^2 = a^{-1} \) lemma (in field1) OrdField_ZF_1_L7:
assumes \( a\in R \), \( a\neq 0 \)
shows \( a\cdot (a^{-1}) = 1 \), \( (a^{-1})\cdot a = 1 \) 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_+ \) lemma (in field1) OrdField_ZF_1_L8:
assumes \( a \in R_+ \)
shows \( a^{-1} \in R_+ \), \( a\cdot (a^{-1}) = 1 \), \( (a^{-1})\cdot a = 1 \) lemma (in ring1) OrdRing_ZF_3_L19:
assumes \( \text{HasNoZeroDivs}(R,A,M) \) and \( a\in R \), \( b\in R \) and \( a \neq 0 \vee b \neq 0 \)
shows \( 0 \lt a^2 + b^2 \) lemma (in ring1) OrdRing_ZF_1_L3:
assumes \( a\leq b \)
shows \( a\in R \), \( b\in R \) lemma (in ring1) OrdRing_ZF_3_L13:
assumes \( \text{HasNoZeroDivs}(R,A,M) \) and \( a \lt b \) and \( c\in R_+ \)
shows \( a\cdot c \lt b\cdot c \), \( c\cdot a \lt c\cdot b \) lemma (in field1) OrdField_ZF_2_L1:
assumes \( a \lt b \) and \( c\in R_+ \)
shows \( a\cdot c \lt b\cdot c \) 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 field1) OrdField_ZF_2_L3:
assumes \( a\leq b \) and \( c\in R_+ \)
shows \( a\cdot (c^{-1}) \leq b\cdot (c^{-1}) \) lemma (in field1) OrdField_ZF_1_L7A:
assumes \( a\in R \), \( b \in R_+ \)
shows \( a\cdot b\cdot b^{-1} = a \), \( a\cdot b^{-1}\cdot b = a \) lemma (in field1) OrdField_ZF_2_L4:
assumes \( a \lt b \) and \( c\in R_+ \)
shows \( a\cdot c \lt b\cdot c \), \( c\cdot a \lt c\cdot b \), \( a\cdot c^{-1} \lt b\cdot c^{-1} \) lemma (in ring1) OrdRing_ZF_3_L7:
assumes \( a \in R_+ \) and \( a\leq b \)
shows \( b \in R_+ \) lemma (in field0) Field_ZF_2_L4:
assumes \( a\in K \), \( a\neq 0 \) and \( b^{-1} \neq a \)
shows \( a^{-1} \neq b \) lemma (in field1) OrdField_ZF_2_L7:
assumes \( a\in R_+ \) and \( a^{-1} \leq b \)
shows \( b^{-1} \leq a \) lemma (in field1) OrdField_ZF_1_L9:
assumes \( a \lt b \)
shows \( (b - a)^{-1} \in R_+ \) lemma (in field1) OrdField_ZF_2_L8:
assumes \( a\in R_+ \) and \( a^{-1} \lt b \)
shows \( b^{-1} \lt a \) 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 \) lemma (in ring0) Ring_ZF_2_L1A:
assumes \( a\in R \), \( b\in R \)
shows \( a - b + b = a \), \( a + b - a = b \), \( ( - a) + b + a = b \), \( ( - a) + (b + a) = b \), \( a + (b - a) = b \) lemma (in ring0) ring_oper_distr:
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 \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8