PROOF 04
Prove.
a ÷ (b/c) = a × (c/b)
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 c has a multiplicative inverse, b/c denotes b · c⁻¹.
Proof.
A fraction is not a new kind of number but a product.convention
∎
Definition D2
When x has a multiplicative inverse, a ÷ x denotes a · x⁻¹.
Proof.
Division is multiplication by the inverse. This definition asks only whether x 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 c ≠ 0, then b/c has a multiplicative inverse and (b/c)⁻¹ = c/b
Proof.
(1)(b/c)(c/b) = (b c⁻¹)(c b⁻¹)A4, D1
(2) = (b b⁻¹)(c c⁻¹)A1, A2
(3) = 1 × 1A4
(4) = 1A3
(5)c/b is a multiplicative inverse of b/c.(4)
(6)Such a number is unique.L1
(7)(b/c)⁻¹ = c/b(5), (6)
∎
Theorem T
If b ≠ 0 and c ≠ 0, then a ÷ (b/c) = a × (c/b)
Proof.
(1)b/c has a multiplicative inverse.L2
(2)Therefore a ÷ (b/c) is defined.D2, (1)
(3)a ÷ (b/c) = a · (b/c)⁻¹D2
(4)(b/c)⁻¹ = c/bL2
(5)a ÷ (b/c) = a × (c/b)(3), (4), E
∎
Remark
Can A4 be removed from this proof?
Check which axiom the invert-and-multiply rule hangs on.