PROOF 70
Prove.
Reducing a fraction leaves its value unchanged
On the rational numbers ℚ.
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 means a · b⁻¹.
Proof.
A fraction is not a symbol stacking two numbers vertically 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 k ≠ 0 and b ≠ 0, then kb has a multiplicative inverse and (kb)⁻¹ = k⁻¹b⁻¹
Proof.
(1)Since k ≠ 0, k⁻¹ exists; since b ≠ 0, b⁻¹ exists.assumption, A4
(2)(kb)(k⁻¹b⁻¹) = (k k⁻¹)(b b⁻¹)A1, A2
(3) = 1 × 1A4
(4) = 1A3
(5)k⁻¹b⁻¹ is a multiplicative inverse of kb.(4)
(6)There is only one such number.L1
(7)(kb)⁻¹ = k⁻¹b⁻¹(5), (6)
∎
Theorem T
If k ≠ 0 and b ≠ 0, then (ka)/(kb) = a/b
Proof.
(1)kb has a multiplicative inverse.L2
(2)(ka)/(kb) = (ka)(kb)⁻¹(1), D1
(3) = (ka)(k⁻¹b⁻¹)L2, E
(4) = ((ka)k⁻¹)b⁻¹A1
(5) = ((ak)k⁻¹)b⁻¹A2
(6) = (a(k k⁻¹))b⁻¹A1
(7) = (a × 1)b⁻¹A4
(8) = a · b⁻¹A3
(9) = a/bD1
(10)k ≠ 0 was used in (1) and (7). If k = 0, then k⁻¹ does not exist and the proof fails from (2) onward.(1), (7), A4
∎
Remark
Can A4 be removed from this proof?
Reducing looks like erasing the same number from top and bottom. Check what remains in the erased place.