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

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

a,b\in\mathbb{R}

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

a<b

a+c<b+c

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

ps<rq

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

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

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

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

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

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

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

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

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

M\ \text{has a minimum}

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

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

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

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

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

m=m'

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

l\le u

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

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

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

\tfrac12\notin[l,u]

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

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

\text{S02 to S15}

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

Substeps and lemmas

a<b

a+c<b+c

a+c<b+c

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

q>0,\ s>0

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

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

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

ps<rq

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

M=\{a\}

\min M=a

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

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

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

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

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-multiplying

One 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 endpoints

The 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 none

M 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)