Rational number: different fraction representations of one rational, cross-multiplication and reduction

Goal and scope

Using the MKO's definition (there are integers p, q with q≠0 and x=p/q), prove that 6/(−8), −3/4 and 9/(−12) represent the same rational number, and reduce 6/(−8) exactly to the canonical form −3/4; prove 2/3≠3/5 by cross-multiplication; show that '5/0' denotes no number; show that the finite decimal −1.25=−5/4 and the integer 7=7/1 are rational; and, with positive denominators, prove −3/4<−2/3 by cross-multiplication.

Treats fractions inside ℝ (p/q means p·(1/q)), using only field operations and order. It proves two lemmas: cross-multiplication decides equality when denominators are nonzero, and decides order when denominators are positive. It does not prove uniqueness of the canonical form (reduced, positive denominator) and does not treat the link to Lean's Rat.divInt; it does not change the canonical MKO or its English edition.

Givens and symbols

• mul_inverse_nonzero
• frac_rules
• zero_product
• order_basics
• numeric_evaluation

• G1 — Work inside the reals ℝ, with the integers ℤ⊆ℝ; for q≠0, p/q means p·(1/q); 0 has no reciprocal.
• G2 — The MKO's definition: a number x is rational if there are integers p, q with q≠0 and x=p/q (assumptions a1, a2).
• G3 — Canonical display convention (MKO explanation): numerator and denominator are coprime (greatest common divisor 1), and the denominator is positive.
• G4 — Data: 6/(−8), −3/4, 9/(−12), 2/3, 3/5, the string '5/0', the finite decimal −1.25, the integer 7, and −2/3.

• \mathbb{Q} — the set of rational numbers
• \frac{p}{q} — p·(1/q), with q≠0
• (p,q) — a pair of integers representing a rational
• \gcd(a,b) — greatest common divisor
• k — the nonzero factor applied to numerator and denominator when reducing

Rules and sources

• 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.
• 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.
• zero_product · prerequisite — Zero-product property: in ℤ, ℚ, ℝ, ℂ (or any integral domain), uv=0 ⇔ u=0 or v=0.
• 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.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• mul_assoc · prerequisite — Associativity of multiplication: (uv)w=u(vw).
• mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
• mul_one · prerequisite — Multiplicative identity: 1·u=u.
• eq_congruence · prerequisite — Congruence of equality: if u=v, applying the same defined operation f to both sides gives f(u)=f(v). Operating on one side only is not an instance of this rule.
• neg_mul · prerequisite — Signs and multiplication: (−u)v=−(uv) and (−u)(−v)=uv.
• eq_refl_symm_trans · prerequisite — Properties of equality: u=u; if u=v then v=u; if u=v and v=w then u=w.
• divides_def · prerequisite — Divisibility: for integers a, b, a∣b means there is an integer k with b=ak.
• 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.
• exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_rat_def · cited — A number x is rational if there exist integers p and q with q≠0 such that x=p/q. Different integer pairs can represent the same rational number. · mko-rational-number
• canonical_def · prerequisite — Canonical form: p/q with gcd(|p|,q)=1 and q>0.
• gcd_def · prerequisite — For integers a, b not both 0, gcd(a,b) is the largest positive integer dividing both a and b.
• decimal_def · prerequisite — Finite decimal: the integer part plus the sum of the j-th digit after the point times 10^{−j}; for example 1.25=1+2/10+5/100.
• L_cross · lemma — For reals p, q, r, s with q≠0 and s≠0: p/q=r/s ⇔ ps=rq.
• L_cross_order · lemma — For reals p, q, r, s with q>0 and s>0: p/q<r/s ⇔ ps<rq.

Main derivation

x\in\mathbb{Q}

\exists p,q\in\mathbb{Z},\ q\neq 0:\ x=\frac{p}{q}

\frac{p}{q}=\frac{r}{s}\quad(q\neq0,\ s\neq0)

ps=rq

6\cdot 4=24=(-3)\cdot(-8)

\frac{6}{-8}=\frac{-3}{4}

6\cdot(-12)=-72=9\cdot(-8)

\frac{6}{-8}=\frac{9}{-12}=\frac{-3}{4}

\frac{6}{-8}

\frac{6\cdot(-\frac12)}{(-8)\cdot(-\frac12)}=\frac{-3}{4}

\frac{-3}{4}

\gcd(3,4)=1,\ 4>0:\ \text{canonical form}

2\cdot5=10\neq 9=3\cdot3

\frac{2}{3}\neq\frac{3}{5}

x\cdot 0=5\ \text{for some}\ x

0=5,\ \text{a contradiction}

-1.25

-\frac{125}{100}=-\frac{5}{4}\in\mathbb{Q}

n\in\mathbb{Z}

n=\frac{n}{1}\in\mathbb{Q}

(-3)\cdot3=-9<-8=(-2)\cdot4

\frac{-3}{4}<\frac{-2}{3}

\text{S04, S06 to S11}

\tfrac{6}{-8}=\tfrac{9}{-12}=\tfrac{-3}{4};\ \tfrac{2}{3}\neq\tfrac{3}{5};\ -1.25,\ 7\in\mathbb{Q};\ \tfrac{-3}{4}<\tfrac{-2}{3}

Substeps and lemmas

q\neq 0,\ s\neq 0

qs\neq 0,\ \frac{p}{q}\cdot qs=ps,\ \frac{r}{s}\cdot qs=rq

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

ps=rq

q>0,\ s>0,\ \frac{p}{q}<\frac{r}{s}

ps<rq

Reverse audits

• S12 · sufficient_goal_reduction · S03, S04, S05, S06, S07, S08, S09, S10, S11 — The goal is the list in the goal field. Sufficient condition H: S03 to S11 each hold; H gives the goal by conjunction only. Each item is proved forwards from the definition, the two lemmas and exact computation; the goal is never used as a premise.
• S11.1 · inverse_equivalence · order_basics, S02.1, mul_inverse_nonzero — Multiplying by the positive qs and by the positive 1/(qs) both keep the direction of the inequality and undo each other.
• S11 · inverse_equivalence · L_cross_order, numeric_evaluation — This guide proves the biconditional under the sufficient hypothesis that both denominators are positive; it does not claim that it fails in every other sign configuration.
• S10 · premise_audit · exists_intro, mul_one, forall_intro — The converse (every rational is an integer) is false; for example −5/4 is not an integer.
• S09 · premise_audit · decimal_def, exists_intro, L_cross, numeric_evaluation — Existence needs only one pair (p,q); the reduction is a separate equality.
• S08 · premise_audit · mul_zero, contradiction, mul_inverse_nonzero — The contradiction comes from x·0=0 for every x; this is exactly why 0 has no reciprocal.
• S07 · inverse_equivalence · L_cross, numeric_evaluation — P⇔Q is equivalent to ¬P⇔¬Q (N10).
• S06 · premise_audit · gcd_def, canonical_def, divides_def — It checks only that −3/4 is in canonical form; uniqueness of the canonical form is not proved here (open item).
• S05 · inverse_equivalence · frac_rules, numeric_evaluation — Backward: multiplying numerator and denominator by −2 returns to 6/(−8); k≠0 is the rule's condition.
• S04 · inverse_equivalence · L_cross, numeric_evaluation, eq_refl_symm_trans — Each equality comes from a biconditional and they are joined by transitivity of equality (N4 to N6).
• S03 · inverse_equivalence · L_cross, numeric_evaluation — L_cross is a biconditional; the computation can be redone (N1, N2, N3).
• S02.2 · inverse_equivalence · eq_congruence, mul_inverse_nonzero, S02.1 — Multiplying by qs and by 1/(qs) undo each other, given qs≠0.
• S02.1 · premise_audit · zero_product, mul_inverse_nonzero, mul_assoc, mul_comm — q≠0 and s≠0 are needed for 1/q and 1/s to exist.
• S02 · inverse_equivalence · L_cross — The lemma is a biconditional with both directions proved in the sub-steps; nonzero denominators cannot be dropped.
• S01 · premise_audit · mko_rat_def, G1 — q≠0 is part of the definition (assumption a2) and cannot be dropped; for q=0, p/q is undefined.

Error controls and negative controls

The denominator may not be zero

One misconception the MKO names is allowing a zero denominator. '5/0' looks like a fraction, but if it were a number x we would need x·0=5, while x·0 is always 0 (S08). So (5,0) represents no rational; by contrast 0/5=0 is a legitimate rational.

Different-looking fractions can be equal

Another misconception the MKO names is treating different-looking fractions as different values. 6/(−8), −3/4 and 9/(−12) look different yet are one rational (S03, S04); equality is decided by cross-multiplication L_cross, not by comparing numerators or denominators. For order, denominators must first be made positive: cross-multiplying 1/(−2) and 1/3 directly gives 1·3=3>−2=1·(−2) and would wrongly suggest 1/(−2)>1/3, while in fact −1/2<1/3 (N18, N19).

Reduction is an exact equality, not an approximation

The MKO warns against treating reduction as an approximation. 6/(−8)=−3/4 follows from a/b=(ak)/(bk) with k≠0 and is an exact equality (S05). What does change the value is rounding: writing −0.75 as −0.8, and −0.8≠−3/4 (N21).

• 5/0 is rational because 5 and 0 are both integers → reject — The definition requires q≠0, and no number x satisfies x·0=5 (S08).
• 6/(−8) and −3/4 look different, so they are different rationals → reject — The cross products 6·4=24=(−3)·(−8) agree, so by L_cross they are equal (S03).
• Reducing 6/(−8) to −3/4 is only an approximation → reject — a/b=(ak)/(bk) with k=−1/2≠0 is an exact equality (S05).
• Since 1·3>1·(−2), we have 1/(−2)>1/3 → reject — L_cross_order needs positive denominators; in fact −1/2<1/3 (N19).

Result and limitations

6/(−8), −3/4 and 9/(−12) are the same rational (cross products 24=24 and −72=−72), with canonical form −3/4 (gcd(3,4)=1, positive denominator), and the reduction is an exact equality; 2/3≠3/5 (10≠9); '5/0' denotes no number; −1.25=−125/100=−5/4 and 7=7/1 are rational; with positive denominators, −3/4<−2/3 (−9<−8).

• This guide only checks that −3/4 is in canonical form; it does not prove that each rational has exactly one canonical form (uniqueness needs, for example, Euclid's lemma).
• The link to Lean's Rat.divInt and the statements about nonzero denominators and normalized numerator and denominator (MKO formal next) is not treated here.

Verification and source binding

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 7082af66df1018fc25b71890f73e46bebc2e117da1918db747a20e274bd8bc19
• original source SHA-256: b6cd86f150bfd74850fefee9d1f793b0b5d8bf486f024406abf8d1a96e33ec1f
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)