PROOF 03
Prove.
a/b + c/d = (ad+bc)/bd
On the rationals ℚ.
A way to read this proof
First separate what is assumed from what is to be proved. At each step, ask which definition or earlier result permits the move. If it is unclear, return to that premise rather than skipping to the conclusion.
Definition D1
When b has a multiplicative inverse, a/b denotes a · b⁻¹.
Proof.
A fraction is not a new kind of number but a product. This definition asks only whether b has an inverse.convention
∎
Lemma L1
If xy = 1 and xz = 1, then y = z
Proof.
(1)y = y × 1A3
(2) = y(xz)assumption
(3) = (yx)zA1
(4) = (xy)zA2
(5) = 1 × zassumption
(6) = z × 1A2
(7) = zA3
∎
Lemma L2
If b ≠ 0 and d ≠ 0, then (bd)⁻¹ = b⁻¹d⁻¹
Proof.
(1)(bd)(b⁻¹d⁻¹) = (b b⁻¹)(d d⁻¹)A4, A1, A2
(2) = 1 × 1A4
(3) = 1A3
(4)b⁻¹d⁻¹ is a multiplicative inverse of bd.(3)
(5)Such a number is unique.L1
(6)(bd)⁻¹ = b⁻¹d⁻¹(4), (5)
∎
Theorem T
If b ≠ 0 and d ≠ 0, then a/b + c/d = (ad + bc)/bd
Proof.
(1)a/b + c/d = a·b⁻¹ + c·d⁻¹A4, D1, E
(2) = (a·b⁻¹)×1 + (c·d⁻¹)×1A3
(3) = a b⁻¹(d d⁻¹) + c d⁻¹(b b⁻¹)A4, E
(4) = (ad)(b⁻¹d⁻¹) + (cb)(d⁻¹b⁻¹)A1, A2
(5) = (ad)(b⁻¹d⁻¹) + (cb)(b⁻¹d⁻¹)A2
(6) = (ad + cb)(b⁻¹d⁻¹)A5
(7) = (ad + bc)(bd)⁻¹A2, L2
(8) = (ad + bc)/bdD1
∎
Remark
Can A4 be removed from this proof?
That every nonzero number has an inverse is a property of the rationals. Remove it and see which lines lose their justification.