Ratio and proportion: solving 3:4=x:10, checking back, and testing data for direct proportion

Goal and scope

Over the rationals: (1) prove that for b≠0 and d≠0 the proportion a:b=x:d has exactly one rational solution, x=ad/b; (2) use it to solve 3:4=x:10 and check back; (3) show that 4:3=x:10 has a different solution, so the order of a ratio matters; (4) decide whether the data (2,5), (4,10), (6,15), (8,21) fit a single direct proportion y=kx.

Inside the MKO's scope: numerical ratios over the rationals with nonzero consequents b and d (assumption a1). The data are pure numbers without units; ratios of quantities would first need their units and comparability stated (assumption a2). The guide draws no geometric similarity or causation from numerical proportion, and does not change the canonical MKO or its English edition.

Givens and symbols

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

• G1 — a, b, c, d and x are rational numbers with b≠0 and d≠0 (MKO assumption a1).
• G2 — The value of the ratio a:b is a/b; the proportion a:b=c:d means a/b=c/d.
• G3 — The data (xᵢ,yᵢ): (2,5), (4,10), (6,15), (8,21). 'The data fit a direct proportion y=kx' means that one rational number k satisfies yᵢ=k·xᵢ for every data point.

• a:b — a numerical ratio, with value a/b (b≠0)
• a:b=c:d — a proportion, meaning a/b=c/d
• x — the unknown term of a proportion
• k — the constant of a direct proportion y=kx
• (x_i,y_i) — the i-th data point

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.
• 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_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.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• mul_one · prerequisite — Multiplicative identity: 1·u=u.
• 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.
• logic_chain · prerequisite — Chaining: from P⇒Q and Q⇒R infer P⇒R; likewise for ⇔.
• set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements.
• iff_intro · prerequisite — Biconditional: P⇔Q holds exactly when both P⇒Q and Q⇒P hold.
• forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds.
• contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q.
• contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
• 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_ratio_def · cited — For rational numbers a, b, c, and d with b≠0 and d≠0, the value of the numerical ratio a:b is a/b. The proportion a:b=c:d means a/b=c/d and is equivalent to ad=bc. · mko-ratio-proportion
• L_cross · lemma — For rationals a, b, c, d with b≠0 and d≠0: a/b=c/d ⇔ ad=bc.
• L_solve · lemma — For a rational u and b≠0: bx=u ⇔ x=u/b.

Main derivation

a:b=x:d

\frac{a}{b}=\frac{x}{d}\quad (b\neq 0,\ d\neq 0)

\frac{a}{b}=\frac{x}{d}

ad=bx

ad=bx

x=\frac{ad}{b}

a:b=x:d

\{x\in\mathbb{Q}\mid a:b=x:d\}=\left\{\frac{ad}{b}\right\}

3:4=x:10

x=\frac{3\cdot 10}{4}=\frac{30}{4}=\frac{15}{2}

x=\frac{15}{2}

\frac{15/2}{10}=\frac{15}{20}=\frac{3}{4},\quad 3\cdot 10=30=4\cdot\frac{15}{2}

4:3=x:10

x=\frac{40}{3}\neq\frac{15}{2}

y_i=k\,x_i\quad (x_i\neq 0)

k=\frac{y_i}{x_i}

\frac{5}{2},\ \frac{10}{4},\ \frac{15}{6}

\frac{5}{2}=\frac{10}{4}=\frac{15}{6}

\frac{21}{8}\ \text{vs}\ \frac{5}{2}

21\cdot 2=42\neq 40=8\cdot 5,\ \text{so no single}\ k

0:0=x:5

\text{not a proportion, although}\ 0\cdot 5=0\cdot x\ \text{for every}\ x

S04,\ S05,\ S07,\ S10

x=\frac{ad}{b}\ \text{unique};\ 3:4=x:10\Leftrightarrow x=\frac{15}{2};\ 4:3=x:10\Leftrightarrow x=\frac{40}{3};\ \text{table not proportional}

Substeps and lemmas

\frac{a}{b}=\frac{c}{d}

ad=bc

ad=bc

\frac{a}{b}=\frac{c}{d}

bx=u

x=\frac{u}{b}

Reverse audits

• S12 · sufficient_goal_reduction · S04, S05, S07, S10, and_intro_elim — Goal G: (1) to (4). Sufficient condition H: S04, S05, S07 and S10 each hold; H⇒G by conjunction introduction. H is proved forwards from the definition, the lemmas and exact computation; G is never used as a premise.
• S11 · premise_audit · mko_ratio_def, mul_inverse_nonzero — The conclusion is only that this is not a proportion; no solution set for x is claimed.
• S10 · premise_audit · S08, S09, contradiction, L_cross — The contradiction comes from requiring one k at every point; equivalently (5/2)·8=20≠21 (N10).
• S09 · premise_audit · S08, L_cross, numeric_evaluation — Each point is compared with the same k; this concerns only the first three points and says nothing about the fourth or about points outside the table.
• S08 · inverse_equivalence · L_solve, G3 — Each data point is transformed by an equivalence; xᵢ≠0 is needed.
• S07 · premise_audit · S04, L_cross, contrapositive — The reversed ratio b:a needs the original antecedent a≠0; here a=3≠0. The inequality uses L_cross in contrapositive form: unequal cross products give unequal values.
• S06 · premise_audit · S05, L_cross, numeric_evaluation — This is an independent numerical check (N2, N3); it does not replace the uniqueness argument of S04.
• S05 · premise_audit · S04, forall_elim, frac_rules — Before applying S04 both consequents are checked to be nonzero; 30/4=15/2 is a reduction (N1).
• S04 · premise_audit · S02, S03, logic_chain, set_extensionality — Because every link is an equivalence, existence and uniqueness both follow; a one-way link would give only half of this.
• S03.1 · inverse_equivalence · mul_inverse_nonzero, eq_congruence, mul_assoc — Multiplying by 1/b and by b undo each other, given b≠0.
• S03 · inverse_equivalence · L_solve, eq_refl_symm_trans — Both directions of the lemma are proved in S03.1; b≠0 is needed.
• S02.2 · premise_audit · zero_product, frac_rules, eq_congruence — This is the ⇐ direction and needs bd≠0; if b=0 or d=0 were allowed, ad=bc would not lead back to any proportion (see error control 1).
• S02.1 · premise_audit · eq_congruence, mul_inverse_nonzero, mul_assoc, mul_comm — The simplification needs 1/b and 1/d to exist. This is the ⇒ direction.
• S02 · inverse_equivalence · L_cross — Both directions of the lemma are proved, and both need b≠0 and d≠0.
• S01 · premise_audit · G1, G2, mko_ratio_def — This step only unfolds the definition; the conditions b≠0 and d≠0 are needed in every later step.

Error controls and negative controls

Cross products cannot legalize a zero consequent

The MKO warns that equal cross products cannot make a representation with a zero denominator legal. For 0:0=x:5 the 'cross products' 0·5=0·x agree for every x, and for 3:0=6:0, 3·0=0·6 holds too, but 0:0, 3:0 and 6:0 are not ratios. Both directions of L_cross (S02.1, S02.2) use b≠0 and d≠0: first check that the consequents are nonzero, then compare cross products.

Equal ratios do not by themselves give geometric similarity

The MKO also notes that equal ratios do not automatically establish geometric similarity. For example, a parallelogram with sides 1 and 2 and an angle of 60°, and a rectangle with sides 2 and 4, have proportional corresponding sides (1:2=2:4), but one has a 60° angle and the other only 90° angles, so they are not similar. A numerical proportion is a statement about numbers; similarity or causation needs further conditions and proof (assumption a2).

Order matters, and finite data must be checked point by point

3:4 and 4:3 differ (cross products 9≠16), and writing the proportion backwards gives 40/3 instead of 15/2; a reversed ratio also needs the original antecedent to be nonzero. When testing for direct proportion, the same k must be checked at every data point: the first three points all give k=5/2, but the fourth, (8,21), does not, so one or a few points cannot settle all inputs (third paragraph of the MKO).

• Since 0·5=0·x, the proportion 0:0=x:5 holds for every x → reject — 0:0 has consequent 0 and is not a ratio; L_cross needs nonzero consequents.
• 3:4=4:3 → reject — Cross products 3·3=9≠16=4·4.
• The first three data points satisfy y=(5/2)x, so the whole table is directly proportional → reject — At the fourth point, (5/2)·8=20≠21.
• A parallelogram with sides 1 and 2 and a 60° angle has sides proportional to a 2×4 rectangle, so the two are similar → reject — The angles differ (60° and 90°); a numerical proportion does not give geometric similarity.

Result and limitations

For b≠0 and d≠0, a:b=x:d has exactly one solution, x=ad/b. The solution of 3:4=x:10 is 15/2 (check: 3·10=30=4·15/2); that of 4:3=x:10 is 40/3, so the order of a ratio matters. The first three data points fit y=(5/2)x, but the fourth gives 21/8≠5/2, so the table is not directly proportional. 0:0 is not a ratio, and cross products cannot make it legal.

• The parallelogram example in error control 2 uses the geometric fact that similar figures have equal corresponding angles; this guide does not prove it and uses it only to show that numerical proportion is not enough for similarity.

Verification and source binding

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

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

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