# The usual order on ℝ: translation, cross-multiplication with positive denominators, finite extrema and closed intervals

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-order-relation/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-order-relation-01 · production-20261019-adopted-96



## Goal and scope

Prove for all reals a, b, c that a<b ⇔ a+c<b+c; that p/q<r/s ⇔ ps<rq when q, s>0; and that a finite nonempty set of reals has a minimum, which is unique. Use these to compare the elements of M={−5/9, 1/3, −7/12, −1/2} (listed in this order), find the minimum and maximum of M, and decide whether the two endpoints and 1/2 belong to the closed interval [min M, max M].

Only the usual total order on the reals is considered (MKO a1), with the order axioms of order_basics as prerequisites; the reals are not constructed. Comparisons use rationals with positive denominators (a2); extrema are for nonempty finite sets, and a closed interval needs its lower endpoint no greater than its upper endpoint (a3). Existence of a maximum is covered by 'the same argument with ≥ in place of ≤'. Complex numbers, general partial orders and suprema of infinite sets are not treated; the canonical MKO and its English edition are not changed.





## Givens and symbols


- order_basics
- frac_rules
- add_inverse
- nat_induction
- numeric_evaluation


- G1 — The usual order ≤ on ℝ is reflexive, antisymmetric, transitive and total; a<b means a≤b and a≠b.
- G2 — M={−5/9, 1/3, −7/12, −1/2}, listed in this order; in positive-denominator form: (−5)/9, 1/3, (−7)/12, (−1)/2.
- G3 — Definitions: m is a minimum of a set M when m∈M and m≤x for all x∈M; a maximum likewise with ≥. For l≤u, the closed interval [l,u]={x∈ℝ ∣ l≤x and x≤u}.


- a\le b,\ a<b — the usual order and the strict order
- \frac{p}{q} — a rational with denominator q>0
- M — the finite set being compared
- \min M,\ \max M — the minimum and maximum elements
- [l,u] — the closed interval {x ∣ l≤x≤u}





## Rules and sources


- order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
- frac_rules · prerequisite — Fraction rules (all denominators nonzero): a/c+b/c=(a+b)/c; (a/b)(c/d)=(ac)/(bd); (a/b)/(c/d)=(ad)/(bc) (also needing c≠0); a/b=(ak)/(bk) for k≠0.
- add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
- nat_induction · prerequisite — Principle of induction: for a family P(n) starting at n₀, if P(n₀) holds and P(n)⇒P(n+1) for every n≥n₀, then P(n) holds for every n≥n₀.
- numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
- add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
- add_zero · prerequisite — Additive identity: u+0=u.
- mul_inverse_nonzero · prerequisite — Inverse of a nonzero number: in ℚ, ℝ or ℂ, if u≠0 there is 1/u with u·(1/u)=1, and v/u means v·(1/u). 0 has no inverse, so v/0 is undefined.
- mul_zero · prerequisite — Multiplying by zero: u·0=0. Reason: u·0=u·(0+0)=u·0+u·0; subtracting u·0 from both sides gives 0=u·0.
- contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
- mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
- mul_assoc · prerequisite — Associativity of multiplication: (uv)w=u(vw).
- logic_chain · prerequisite — Chaining: from P⇒Q and Q⇒R infer P⇒R; likewise for ⇔.
- case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
- and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
- mko_order · cited — On R, the usual total order ≤ is reflexive, antisymmetric and transitive; any two real numbers are comparable. Write a<b when a≤b and a≠b. For real a,b,c, a<b exactly when a+c<b+c. A finite nonempty real set has a minimum and a maximum; a closed interval [l,u] with l≤u includes both endpoints. · mko-order-relation
- min_max_def · prerequisite — Minimum: m∈M and m≤x for all x∈M; maximum: m∈M and m≥x for all x∈M.
- interval_def · prerequisite — Closed interval: for l≤u, x∈[l,u] ⇔ l≤x and x≤u.
- L_translate · lemma — For all reals a, b, c: a<b ⇔ a+c<b+c.
- L_cross · lemma — For reals p, r and q>0, s>0: p/q<r/s ⇔ ps<rq.
- L_finite_min · lemma — Every nonempty finite set of reals has a minimum.
- L_min_unique · lemma — A set of reals has at most one minimum (and likewise at most one maximum).





## Main derivation

S01 · definitionBefore

a,b\in\mathbb{R}

After

a<b\ :\iff\ a\le b\land a\neq b;\ \text{exactly one of}\ a<b,\ a=b,\ b<a

Conditions: none

Rule: mko_order · Uses: G1, mko_order

Leaf basis: mko_order + order_basics

Define the strict order as in the MKO. Totality (a≤b or b≤a) and antisymmetry (both together force a=b) give trichotomy: exactly one of a<b, a=b, b<a holds. This is the MKO's three-way comparison with outputs <, = or >.



S02 · equivalentBefore

a<b

After

a+c<b+c

Conditions: none

Rule: L_translate · Uses: S01

Leaf basis: order_basics + add_assoc + add_inverse + add_zero

By Lemma L_translate, adding c to both numbers does not change the comparison. ⇒ is S02.1 and ⇐ is S02.2.



S03 · equivalentBefore

\frac{p}{q}<\frac{r}{s}

After

ps<rq

Conditions: q>0; s>0

Rule: L_cross · Uses: S01

Leaf basis: order_basics + frac_rules + mul_inverse_nonzero

By Lemma L_cross: when both denominators are positive, comparing two fractions is the same as comparing the cross products. The proof is in S03.1 to S03.3; the positive-denominator condition cannot be dropped.



S04 · equivalentBefore

-\tfrac{7}{12}\ ?\ -\tfrac{5}{9}

After

(-7)\cdot9=-63<-60=(-5)\cdot12\ \Rightarrow\ -\tfrac{7}{12}<-\tfrac{5}{9}

Conditions: 12>0; 9>0

Rule: L_cross · Uses: S03, G2

Leaf basis: order_basics + numeric_evaluation

Take p=−7, q=12, r=−5, s=9; both denominators are positive. ps=−63 and rq=−60, and −60−(−63)=3>0, so −63<−60; by L_cross, −7/12<−5/9.



S05 · equivalentBefore

-\tfrac{5}{9}\ ?\ -\tfrac{1}{2}

After

(-5)\cdot2=-10<-9=(-1)\cdot9\ \Rightarrow\ -\tfrac{5}{9}<-\tfrac{1}{2}

Conditions: 9>0; 2>0

Rule: L_cross · Uses: S03, G2

Leaf basis: order_basics + numeric_evaluation

Take p=−5, q=9, r=−1, s=2: ps=−10, rq=−9 and −10<−9, so −5/9<−1/2.



S06 · equivalentBefore

-\tfrac{1}{2}\ ?\ \tfrac{1}{3}

After

(-1)\cdot3=-3<2=1\cdot2\ \Rightarrow\ -\tfrac{1}{2}<\tfrac{1}{3}

Conditions: 2>0; 3>0

Rule: L_cross · Uses: S03, G2

Leaf basis: order_basics + numeric_evaluation

Take p=−1, q=2, r=1, s=3: ps=−3, rq=2 and −3<2, so −1/2<1/3.



S07 · impliesBefore

-\tfrac{7}{12}<-\tfrac{5}{9},\ -\tfrac{5}{9}<-\tfrac{1}{2},\ -\tfrac{1}{2}<\tfrac{1}{3}

After

-\tfrac{7}{12}<-\tfrac{5}{9}<-\tfrac{1}{2}<\tfrac{1}{3}

Conditions: none

Rule: order_basics · Uses: S04, S05, S06

Leaf basis: order_basics + logic_chain

The three comparisons form a chain; by transitivity of <, each number in the chain is less than every number to its right, for example −7/12<−1/2, −7/12<1/3 and −5/9<1/3. All four elements of M are now ordered.



S08 · impliesBefore

M\subseteq\mathbb{R}\ \text{finite},\ M\neq\varnothing

After

M\ \text{has a minimum}

Conditions: M\neq\varnothing

Rule: L_finite_min · Uses: S01

Leaf basis: nat_induction + order_basics + case_analysis

The MKO asserts that a nonempty finite set of reals has a minimum and a maximum. By Lemma L_finite_min, the minimum exists, proved by induction on the number of elements n≥1 (S08.1, S08.2); the argument for the maximum is the same with ≥ in place of ≤.



S09 · impliesBefore

-\tfrac{7}{12}\in M,\ -\tfrac{7}{12}\le x\ \forall x\in M

After

\min M=-\tfrac{7}{12}

Conditions: none

Rule: min_max_def · Uses: S07, G2, min_max_def

Leaf basis: min_max_def + order_basics

−7/12 belongs to M (listed third), by S07 it is less than the other three elements, and −7/12≤−7/12 for itself, so it is the minimum. M lists −5/9 first, but extrema are decided by value, not by the order of listing.



S10 · impliesBefore

\tfrac{1}{3}\in M,\ \tfrac{1}{3}\ge x\ \forall x\in M

After

\max M=\tfrac{1}{3}

Conditions: none

Rule: min_max_def · Uses: S07, G2, min_max_def

Leaf basis: min_max_def + order_basics

1/3 belongs to M and by S07 the other three elements are all less than 1/3, so 1/3 is the maximum.



S11 · impliesBefore

m,m'\ \text{both minima of}\ M

After

m=m'

Conditions: none

Rule: L_min_unique · Uses: S09, S10

Leaf basis: min_max_def + order_basics

By Lemma L_min_unique the minimum is unique, so one may speak of 'the' minimum −7/12; the maximum 1/3 is likewise unique. The proof is in S11.1.



S12 · impliesBefore

l=-\tfrac{7}{12},\ u=\tfrac{1}{3}

After

l\le u

Conditions: none

Rule: order_basics · Uses: S07, S09, S10, G3

Leaf basis: order_basics + mko_order

MKO assumption a3 asks first to check that the lower endpoint of a closed interval is no greater than the upper one. By S07, l=−7/12<1/3=u, so l≤u and [l,u] is a valid closed interval.



S13 · impliesBefore

l\le l\le u,\ l\le u\le u

After

l\in[l,u],\ u\in[l,u],\ M\subseteq[l,u]

Conditions: l\le u

Rule: interval_def · Uses: S12, S09, S10, interval_def

Leaf basis: interval_def + mko_order

Membership in a closed interval is l≤x≤u. For x=l: l≤l (reflexivity) and l≤u (S12), so the left endpoint belongs to the interval; the right endpoint likewise. Every element x of M satisfies min M≤x≤max M (S09, S10), so M⊆[l,u].



S14 · impliesBefore

\tfrac{1}{3}<\tfrac{1}{2}\ \ (1\cdot2<1\cdot3)

After

\tfrac12\notin[l,u]

Conditions: none

Rule: interval_def · Uses: S03, S13, interval_def

Leaf basis: interval_def + contradiction + order_basics

By L_cross (p=1, q=3, r=1, s=2): 1·2=2<3=1·3, so 1/3<1/2. If 1/2≤1/3, antisymmetry together with 1/3≤1/2 would give 1/2=1/3, contradicting 1/3≠1/2; so 1/2≤u fails and 1/2 is not in the interval.



S15 · equivalentBefore

-\tfrac{7}{12}<-\tfrac{5}{9}

After

-\tfrac{7}{12}+\tfrac{7}{12}<-\tfrac{5}{9}+\tfrac{7}{12},\ \text{i.e.}\ 0<\tfrac{1}{36}

Conditions: none

Rule: L_translate · Uses: S02, S04

Leaf basis: order_basics + frac_rules + numeric_evaluation

Apply L_translate with c=7/12: −7/12<−5/9 ⇔ 0<−5/9+7/12. Compute −5/9+7/12=−20/36+21/36=1/36>0, consistent with S04. Translation does not change the comparison, so this is a rewriting, not a new kind of exercise.



S16 · impliesBefore

\text{S02 to S15}

After

\min M=-\tfrac{7}{12},\ \max M=\tfrac13,\ l,u\in[l,u],\ \tfrac12\notin[l,u]

Conditions: none

Rule: and_intro_elim · Uses: S02, S03, S08, S09, S10, S11, S13, S14

Leaf basis: and_intro_elim

Summary: translation invariance and positive-denominator cross-comparison are proved; a nonempty finite set has a unique minimum; M is ordered −7/12<−5/9<−1/2<1/3 with minimum −7/12 and maximum 1/3; the closed interval [−7/12,1/3] contains both endpoints and all of M, but not 1/2.







## Substeps and lemmas

S02.1 · impliesBefore

a<b

After

a+c<b+c

Conditions: none

Rule: order_basics · Uses: order_basics

Leaf basis: order_basics

(⇒) This is exactly the order axiom 'u<v ⇒ u+w<v+w' with u=a, v=b, w=c.



S02.2 · impliesBefore

a+c<b+c

After

(a+c)+(-c)<(b+c)+(-c),\ \text{i.e.}\ a<b

Conditions: none

Rule: order_basics · Uses: order_basics, add_inverse

Leaf basis: order_basics + add_assoc + add_inverse + add_zero

(⇐) Apply the same axiom to a+c<b+c with w=−c to get (a+c)+(−c)<(b+c)+(−c); simplifying both sides (associativity, c+(−c)=0, adding 0) gives a<b. S02.1 and S02.2 together prove Lemma L_translate.



S03.1 · impliesBefore

q>0,\ s>0

After

qs>0,\ \tfrac{1}{qs}>0

Conditions: q>0; s>0

Rule: order_basics · Uses: order_basics, mul_inverse_nonzero

Leaf basis: order_basics + mul_zero + mul_inverse_nonzero + contradiction

Multiply 0<q by s>0 to get 0·s<q·s, i.e. qs>0. Then qs≠0, so 1/(qs) exists; if 1/(qs)<0, multiplying by qs>0 would give 1<0, a contradiction, and 1/(qs)≠0 since (1/(qs))·qs=1, so 1/(qs)>0.



S03.2 · impliesBefore

\frac{p}{q}<\frac{r}{s}

After

\frac{p}{q}\cdot qs<\frac{r}{s}\cdot qs,\ \text{i.e.}\ ps<rq

Conditions: qs>0

Rule: order_basics · Uses: S03.1, frac_rules

Leaf basis: order_basics + frac_rules + mul_comm + mul_assoc

(⇒) Multiply both sides by the positive number qs, which keeps the order; simplify (p/q)·qs=ps and (r/s)·qs=rq (fraction rules, q, s≠0).



S03.3 · impliesBefore

ps<rq

After

\frac{ps}{qs}<\frac{rq}{qs},\ \text{i.e.}\ \frac{p}{q}<\frac{r}{s}

Conditions: \tfrac{1}{qs}>0

Rule: order_basics · Uses: S03.1, frac_rules

Leaf basis: order_basics + frac_rules

(⇐) Multiply both sides by the positive number 1/(qs) (S03.1), which keeps the order; cancel ps/(qs)=p/q and rq/(qs)=r/s. S03.1 to S03.3 together prove Lemma L_cross.



S08.1 · induction_baseBefore

M=\{a\}

After

\min M=a

Conditions: none

Rule: nat_induction · Uses: G3, min_max_def

Leaf basis: min_max_def + order_basics

Base n=1: M={a}. a∈M, and the only element x=a satisfies a≤a (reflexivity), so a is the minimum (and also the maximum).



S08.2 · induction_stepBefore

|M|=n+1,\ a\in M,\ m'=\min(M\setminus\{a\})

After

\min M=m'\ \text{if}\ m'\le a,\ \ \min M=a\ \text{if}\ a<m'

Conditions: n\ge1

Rule: nat_induction · Uses: S08.1, min_max_def, case_analysis

Leaf basis: nat_induction + case_analysis + order_basics + min_max_def

Inductive step: assume every nonempty set with n elements has a minimum (n≥1). Take |M|=n+1 and a∈M; M′=M∖{a} has n elements and, by the induction hypothesis, a minimum m′. By trichotomy there are two cases: if m′≤a, then m′ is no greater than every element of M′ and than a, so m′ is the minimum of M; if a<m′, then for x∈M′ we have a<m′≤x, so a≤x by transitivity, and a≤a, so a is the minimum. S08.1 and S08.2 together prove Lemma L_finite_min.



S11.1 · impliesBefore

m,m'\in M,\ m\le x,\ m'\le x\ \forall x\in M

After

m\le m',\ m'\le m\ \Rightarrow\ m=m'

Conditions: none

Rule: mko_order · Uses: min_max_def, G1

Leaf basis: min_max_def + mko_order

m is a minimum and m′∈M, so m≤m′; likewise m′≤m. By antisymmetry m=m′. The maximum is handled the same way with ≥. This step proves Lemma L_min_unique.







## Reverse audits


- S16 · sufficient_goal_reduction · S02, S03, S08, S09, S10, S11, S13, S14, and_intro_elim — Goal G is the proofs and decisions in the goal; the sufficient condition H is the conjunction of the step results, all proved forwards, and H⇒G uses only conjunction introduction.
- S15 · inverse_equivalence · L_translate, frac_rules, numeric_evaluation — L_translate is an equivalence; adding 7/12 and subtracting 7/12 undo each other.
- S14 · premise_audit · L_cross, interval_def, contradiction — Membership is a conjunction of two inequalities; refuting one of them suffices to exclude the point.
- S13 · premise_audit · interval_def, S12, mko_order — Endpoint membership uses only reflexivity and l≤u; open intervals are a different object and are not discussed here.
- S12 · premise_audit · S07, order_basics — From l<u, l≤u follows by the definition of the strict order.
- S11.1 · premise_audit · min_max_def, mko_order — Only that both minima belong to M and antisymmetry are used.
- S11 · premise_audit · L_min_unique — Uniqueness relies on antisymmetry.
- S10 · premise_audit · S07, min_max_def — Symmetric to S09.
- S09 · premise_audit · S07, min_max_def, order_basics — Both conditions (membership in M and being no greater than every element) are checked; x<y gives x≤y by the definition of the strict order.
- S08.2 · premise_audit · nat_induction, case_analysis, order_basics, min_max_def — It needs n≥1 so that M′ is nonempty and the induction hypothesis applies; the two cases are exhaustive by totality.
- S08.1 · premise_audit · min_max_def, order_basics — Only reflexivity is used; the two extrema of a singleton coincide.
- S08 · premise_audit · L_finite_min — Nonemptiness is essential: the induction starts at n=1, the empty set is outside its range, and it has no minimum.
- S07 · premise_audit · S04, S05, S06, order_basics — What is needed is the three adjacent comparisons and transitivity; the other three pairs need no further cross-multiplication.
- S06 · inverse_equivalence · L_cross, numeric_evaluation — As in S04, the denominators are positive and the equivalence applies.
- S05 · inverse_equivalence · L_cross, numeric_evaluation — As in S04, the denominators are positive and the equivalence applies.
- S04 · inverse_equivalence · L_cross, numeric_evaluation — L_cross is an equivalence and its conditions 12, 9>0 hold, so the fraction comparison and the integer comparison are true or false together.
- S03.3 · premise_audit · S03.1, order_basics, frac_rules — It needs 1/(qs)>0, supplied by S03.1.
- S03.2 · premise_audit · S03.1, order_basics, frac_rules — It needs qs>0; if qs<0, multiplication would reverse the inequality.
- S03.1 · premise_audit · order_basics, mul_inverse_nonzero, contradiction — A product of two positives is positive, and the reciprocal of a positive is positive; both depend on q, s>0.
- S03 · inverse_equivalence · L_cross — ⇒ and ⇐ are proved in the sub-steps, and both use the condition q, s>0.
- S02.2 · premise_audit · order_basics, add_assoc, add_inverse, add_zero — Every real c has an additive inverse −c, so this direction needs no extra condition.
- S02.1 · premise_audit · order_basics — A direct application of the axiom, valid for every real c.
- S02 · inverse_equivalence · L_translate — Both directions are proved, so this is an equivalence.
- S01 · premise_audit · G1, mko_order, order_basics — This only restates a definition and the axioms; trichotomy is also listed in order_basics as a prerequisite.





## Error controls and negative controls

Denominators must be positive before cross-multiplyingOne misconception identified in the MKO is ignoring the sign of denominators. Cross-multiplying 1/(−2) and 1/3 directly gives 1·3=3>−2=1·(−2) and wrongly suggests 1/(−2)>1/3; in fact 1/(−2)=−1/2<1/3. The cause is that multiplying by the negative (−2)·3 reverses the inequality. Rewriting with a positive denominator (−1)/2 first gives (−1)·3=−3<2 and the correct conclusion.

A closed interval contains its endpointsThe other misconception is to leave out the endpoints of a closed interval. l≤l≤u holds, so l∈[l,u] (S13). When l=u the interval has a single value, for example [2,2]={2}; it is the open interval that excludes endpoints, and that is a different object.

Extrema go by value, not order, and the empty set has noneM lists −5/9 first, but the minimum is −7/12 (S09). The empty set has no minimum because there is no m∈∅; the induction in S08 starts at n=1 and does not cover the empty set, so no extremum may be assigned to it.


- Cross-multiplying 1/(−2) and 1/3 gives 1·3=3>−2=1·(−2), so 1/(−2)>1/3 → reject — The denominator −2 is negative, so L_cross does not apply; 1/(−2)=−1/2<1/3.
- −7/12 is an endpoint, so it is not in [−7/12,1/3] → reject — −7/12≤−7/12≤1/3 holds; a closed interval contains its endpoints.
- The minimum of M is −5/9 because it is listed first → reject — −7/12<−5/9 (S04); the minimum is decided by value and is −7/12.
- The minimum of the empty set is 0 → reject — A minimum must belong to the set, and 0∉∅; the empty set has no minimum.





## Result and limitations

For all real a, b and c, a<b ⇔ a+c<b+c; for q, s>0, p/q<r/s ⇔ ps<rq; a nonempty finite set of reals has a unique minimum (and likewise maximum). The elements of M are ordered −7/12<−5/9<−1/2<1/3, so min M=−7/12 and max M=1/3 (regardless of the listing order); [−7/12,1/3] is a valid closed interval containing both endpoints and all of M, but not 1/2.


- The order axioms (order_basics) are used as prerequisites; they are not derived from a construction of the reals.
- Existence of a maximum is covered only by 'the same argument with ≥ in place of ≤' and is not written out step by step.





## Verification and source binding

14 declared checks for this guide; only the listed expressions are covered.


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 2cbe9fb81fea4fdafc3a0280d691e7cbfb470c6ed78948d6657b4f589caa62a8
- original source SHA-256: 2cbe9fb81fea4fdafc3a0280d691e7cbfb470c6ed78948d6657b4f589caa62a8
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-order-relation-01.json)