Fractions: deciding equal value, normalizing to lowest terms with a positive denominator, and adding fractions

Goal and scope

(1) Decide whether (−6)/(−8) and 9/12 represent the same rational number; (2) bring (−6)/(−8) to lowest terms with a positive denominator and show that the value is unchanged; (3) compute 3/4+5/6 and show that 'numerator plus numerator over denominator plus denominator', giving 8/10, is not the sum; (4) explain why 3/0 is not a valid fraction representation.

Inside the MKO's scope: integer numerators and denominators with nonzero denominators (assumption a1), the value of p/q being the rational number p·(1/q). The guide proves the equality criterion ps=rq and the addition formula from rational arithmetic; it does not prove the general uniqueness of the lowest-terms positive-denominator representation (see open items), and does not change the canonical MKO or its English edition.

Givens and symbols

• mul_inverse_nonzero
• zero_product
• frac_rules
• mul_assoc
• mul_comm
• numeric_evaluation

• G1 — p, q, r and s are integers and every number used as a denominator is nonzero (MKO assumption a1); for q≠0, p/q denotes the rational number p·(1/q).
• G2 — The representations to handle: (−6)/(−8), 9/12, 3/4, 5/6 and 6/8, and the expression 3/0.

• \frac{p}{q} — a fraction representation, with value p·(1/q)
• ps=rq — the cross-product equation
• \gcd(m,n) — the greatest common divisor of m and n
• \mathbb{Q} — the rational numbers

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.
• zero_product · prerequisite — Zero-product property: in ℤ, ℚ, ℝ, ℂ (or any integral domain), uv=0 ⇔ u=0 or v=0.
• 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.
• mul_assoc · prerequisite — Associativity of multiplication: (uv)w=u(vw).
• mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• de_morgan_logic · prerequisite — De Morgan's laws for logic: ¬(P∧Q) ⇔ ¬P∨¬Q and ¬(P∨Q) ⇔ ¬P∧¬Q.
• 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.
• mul_one · prerequisite — Multiplicative identity: 1·u=u.
• modus_ponens · prerequisite — Modus ponens: from P and P⇒Q infer Q.
• iff_intro · prerequisite — Biconditional: P⇔Q holds exactly when both P⇒Q and Q⇒P hold.
• divides_def · prerequisite — Divisibility: for integers a, b, a∣b means there is an integer k with b=ak.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q.
• 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.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_fraction_def · cited — For integers p and q with q≠0, p/q represents a rational number. Two valid representations p/q and r/s have the same value exactly when ps=rq; reduction and positive-denominator normalization change the representation without changing the value. · mko-fraction
• gcd_def · prerequisite — For integers m, n not both 0, gcd(m,n) is the largest positive integer dividing both; p/q is in lowest terms with a positive denominator when q>0 and gcd(p,q)=1.
• L_cross · lemma — For integers p, q, r, s with q≠0 and s≠0: p/q=r/s ⇔ ps=rq.
• L_add · lemma — For integers p, q, r, s with q≠0 and s≠0: p/q+r/s=(ps+rq)/(qs).

Main derivation

\frac{-6}{-8},\ \frac{9}{12}

\text{valid representations, since}\ -8\neq 0,\ 12\neq 0

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

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

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

-72=-72

(-6)\cdot 12=9\cdot(-8)\ \text{true}

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

\frac{-6}{-8}

\frac{(-6)(-1)}{(-8)(-1)}=\frac{6}{8}

\frac{6}{8}

\frac{3\cdot 2}{4\cdot 2}=\frac{3}{4}

\frac{9}{12}

\frac{3\cdot 3}{4\cdot 3}=\frac{3}{4}

\frac{3}{4}

4>0,\ \gcd(3,4)=1:\ \text{lowest terms, positive denominator}

\frac{3}{4}+\frac{5}{6}

\frac{3\cdot 6+5\cdot 4}{4\cdot 6}=\frac{38}{24}

\frac{38}{24}

\frac{19\cdot 2}{12\cdot 2}=\frac{19}{12}

\frac{3+5}{4+6}=\frac{8}{10}\ \text{vs}\ \frac{19}{12}

8\cdot 12=96\neq 190=19\cdot 10,\ \text{so}\ \frac{8}{10}\neq\frac{19}{12}

\frac{6}{8}\ (=\tfrac{3}{4})\ \text{and}\ \frac{5}{6}

\frac{6+5}{8+6}=\frac{11}{14}\neq\frac{8}{10},\quad \frac{6\cdot 6+5\cdot 8}{8\cdot 6}=\frac{76}{48}=\frac{19}{12}

\frac{3}{0}

\text{not a valid representation: } 0\ \text{has no inverse}

S04,\ S08,\ S10,\ S11,\ S13

\frac{-6}{-8}=\frac{9}{12}=\frac{3}{4},\ \ \frac{3}{4}+\frac{5}{6}=\frac{19}{12}\neq\frac{8}{10},\ \ \frac{3}{0}\ \text{invalid}

Substeps and lemmas

q\neq 0,\ s\neq 0

qs\neq 0

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

ps=rq

ps=rq

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

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

\frac{ps}{qs}+\frac{rq}{qs}

\frac{ps}{qs}+\frac{rq}{qs}

\frac{ps+rq}{qs}

Reverse audits

• S14 · sufficient_goal_reduction · S04, S08, S10, S11, S13, and_intro_elim — Goal G: (1) to (4). Sufficient condition H: S04, S08, S10, S11 and S13 each hold; H⇒G by conjunction introduction. H is proved forwards from the lemmas and exact computation, and G is never used as a premise.
• S13 · premise_audit · mul_inverse_nonzero, mko_fraction_def — The conclusion says only that 3/0 is not a valid representation; cross products are not claimed to give it a value.
• S12 · premise_audit · L_cross, L_add, S06 — Every comparison goes through L_cross, and all denominators used (8, 6, 10, 14, 48, 12) are nonzero.
• S11 · premise_audit · L_cross, S10, numeric_evaluation — This uses L_cross in contrapositive form: unequal cross products give unequal values; both denominators 10 and 12 are nonzero.
• S10 · inverse_equivalence · frac_rules, gcd_def — Reduction changes the representation, not the value; N11 to N13 recompute it.
• S09.2 · inverse_equivalence · frac_rules, S02.1 — This is an identity for every nonzero c, so it holds both ways.
• S09.1 · inverse_equivalence · frac_rules, mul_comm — Scaling up and reducing undo each other; they need s≠0 and q≠0.
• S09 · inverse_equivalence · L_add — The lemma is an equality of numbers, so both sides name the same rational and the step is two-way; the lemma is proved in S09.1 and S09.2.
• S08 · premise_audit · gcd_def, S06, S07 — This step claims only that 3/4 meets the lowest-terms conditions; it does not claim that lowest-terms representations of rationals are unique in general, which needs a further theorem.
• S07 · inverse_equivalence · frac_rules, gcd_def — The backward move multiplies by 3; k=3≠0.
• S06 · inverse_equivalence · frac_rules, gcd_def — The backward move multiplies numerator and denominator by 2; both directions use only k=2≠0.
• S05 · inverse_equivalence · frac_rules, L_cross — Multiplying by −1 again returns the original representation; k≠0 is needed.
• S04 · premise_audit · S02, S03, modus_ponens — The conclusion comes from the cross products, not from comparing denominators.
• S03 · inverse_equivalence · numeric_evaluation — Exact evaluation does not change whether the equation holds (N1, N2).
• S02.3 · premise_audit · S02.1, frac_rules, eq_congruence — Multiplying by 1/(qs) needs qs≠0; if zero denominators were allowed, ps=rq would not lead back to any relation between values (see error control 2).
• S02.2 · premise_audit · eq_congruence, mul_inverse_nonzero, mul_assoc, mul_comm — The simplification needs 1/q and 1/s to exist, that is q≠0 and s≠0. This is the ⇒ direction; ⇐ is in S02.3.
• S02.1 · premise_audit · zero_product — Both denominators must be nonzero; if either is 0 then qs is 0.
• S02 · inverse_equivalence · L_cross, S01 — Both directions of the lemma are proved in S02.2 and S02.3.
• S01 · premise_audit · G1, mko_fraction_def — This step only checks the validity condition (nonzero denominators) and derives no relation between values.

Error controls and negative controls

Different denominators do not mean different values

The MKO points out that the written form of a fraction is not unique. (−6)/(−8), 6/8, 9/12 and 3/4 all have different denominators but the same value. To decide whether two representations are equal, compare the cross products ps and rq (L_cross), not the numerators or denominators.

A zero denominator does not mean zero

The MKO notes that a zero denominator does not mean zero. 0/5 is zero (zero numerator, nonzero denominator), but 3/0 is not a representation at all, because 0 has no inverse. The cross-product criterion holds only for nonzero denominators: forced onto 3/0 and 6/0, 3·0=6·0 would 'prove' them equal, which is meaningless.

Adding numerators and denominators separately is not fraction addition

The textual operation turns 3/4 and 5/6 into 8/10, but the true sum is 19/12, and 8·12=96≠190=19·10. Worse, writing 3/4 as 6/8 first gives 11/14≠8/10: the result depends on the notation, so it is not an operation on numbers. The correct formula is p/q+r/s=(ps+rq)/(qs) (L_add).

• 9/12 and (−6)/(−8) have different denominators, so their values differ → reject — (−6)·12=−72=9·(−8), so they are equal by L_cross.
• 3/0=0 → reject — 0 has no inverse, so 3/0 is not a valid representation; zero is represented by fractions such as 0/5, with zero numerator and nonzero denominator.
• 3/4+5/6=(3+5)/(4+6)=4/5 → reject — The sum is 19/12, and 4·12=48≠95=19·5.
• Since 3·0=6·0, we have 3/0=6/0 → reject — L_cross needs nonzero denominators; 3/0 and 6/0 name no numbers.

Result and limitations

(−6)/(−8)=9/12 because (−6)·12=−72=9·(−8); its lowest-terms positive-denominator form is 3/4, and reduction and normalization change only the representation. 3/4+5/6=(18+20)/24=38/24=19/12, while the 'add numerators and denominators separately' result 8/10 is not 19/12 and even changes with the notation. 3/0 is not a valid representation, and a zero denominator does not mean zero.

• This guide only verifies that 3/4 and 19/12 are in lowest terms with positive denominators; it does not prove the general uniqueness (every rational has exactly one such representation), which needs Euclid's lemma or Bézout's identity and is left for later.
• N17 is a polynomial-identity check in p, q, k showing that scaling preserves cross-product equality; it supplements S05 and S06, and the argument does not depend on it.

Verification and source binding

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 6d3a1d5f7536f8c32b52e78378a872546ab4eeaf24030466909289ff9ffaa771
• original source SHA-256: 6d3a1d5f7536f8c32b52e78378a872546ab4eeaf24030466909289ff9ffaa771
• Lean: NOT_RUN · independent AI: NOT_MEASURED

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