Definition D1
b − a means b + (−a).
Proof.
Subtraction is not a new operation but the addition of an inverse.convention
∎
Definition D2
When b has a multiplicative inverse, a/b means a · b⁻¹.
Proof.
Before asking which is larger, fix what is being compared. The objects of comparison are two products.convention
∎
Lemma L1
a < b holds if and only if 0 < b − a.
Proof.
(1)Suppose a < b.assumption
(2)a + (−a) < b + (−a)(1), A2
(3)0 < b − a(2), A7, D1
(4)Conversely, suppose 0 < b − a.assumption
(5)0 + a < (b + (−a)) + a(4), A2, D1
(6)(b + (−a)) + a = b + ((−a) + a) = bA4, A5, A7, A6
(7)0 + a = aA5, A6
(8)a < b(5), (6), (7)
∎
Lemma L2
(x − y)z = xz − yz
Proof.
(1)((x − y) + y)z = (x − y)z + yzA12
(2)(x − y) + y = x + ((−y) + y) = xD1, A4, A5, A7, A6
(3)(x − y)z + yz = xz(1), (2), E
(4)((x − y)z + yz) + (−(yz)) = xz + (−(yz))(3), E
(5)left side = (x − y)z + (yz + (−(yz))) = (x − y)zA4, A7, A6
(6)(x − y)z = xz − yz(4), (5), D1
∎
Lemma L3
For every a, a × 0 = 0
Proof.
(1)0 + 0 = 0A6
(2)(0 + 0)a = 0 × a(1), E
(3)0×a + 0×a = 0×a(2), A12
(4)(0×a + 0×a) + (−(0×a)) = 0×a + (−(0×a))(3), E
(5)left side = 0×a + (0×a + (−(0×a))) = 0×aA4, A7, A6
(6)right side = 0A7
(7)0 × a = 0, that is, a × 0 = 0(4), (5), (6), A9
∎
Lemma L4
If b ≠ 0 and d ≠ 0, then (a/b)(bd) = ad and (c/d)(bd) = bc
Proof.
(1)(a/b)(bd) = (a · b⁻¹)(bd)D2
(2) = a((b⁻¹b)d)A8
(3) = a(1 × d) = adA9, A11, A10
(4)(c/d)(bd) = (c · d⁻¹)(db)D2, A9
(5) = c((d⁻¹d)b)A8
(6) = c(1 × b) = cb = bcA9, A11, A10
∎
Theorem T
If 0 < b and 0 < d, then a/b < c/d holds if and only if ad < bc.
Proof.
(1)Suppose 0 < b and 0 < d.assumption
(2)b ≠ 0 and d ≠ 0.(1), A1
(3)0 < bd(1), A3
(4)Suppose a/b < c/d.assumption
(5)0 < (c/d) − (a/b)(4), L1
(6)0 < ((c/d) − (a/b))(bd)(3), (5), A3
(7)((c/d) − (a/b))(bd) = (c/d)(bd) − (a/b)(bd)L2
(8) = bc − ad(2), L4, E
(9)0 < bc − ad(6), (7), (8), E
(10)ad < bc(9), L1
(11)Conversely, suppose ad < bc.assumption
(12)If c/d < a/b, applying (4)–(10) with a/b and c/d exchanged gives bc < ad.(10)
(13)Then ad < bc and bc < ad hold together, which violates trichotomy.(11), (12), A1
(14)If a/b = c/d, multiplying both sides by bd gives ad = bc.(2), L4, E
(15)Then ad < bc and ad = bc hold together, which violates trichotomy.(11), (14), A1
(16)a/b < c/d(13), (15), A1
∎
Corollary C
If 0 < b and d < 0, then a/b < c/d holds if and only if bc < ad.
Proof.
(1)Suppose 0 < b and d < 0.assumption
(2)b ≠ 0 and d ≠ 0.(1), A1
(3)0 × d > b × d and 0 × d = 0, so bd < 0(1), P, L3, A9
(4)Suppose a/b < c/d.assumption
(5)(a/b)(bd) > (c/d)(bd)(3), (4), P
(6)ad > bc, that is, bc < ad(2), (5), L4, E
(7)Conversely, suppose bc < ad.assumption
(8)If c/d < a/b, applying (4)–(6) with the roles exchanged gives ad < bc.(6)
(9)If a/b = c/d, multiplying both sides by bd gives ad = bc.(2), L4, E
(10)Both (8) and (9) violate (7) and trichotomy.(7), (8), (9), A1
(11)a/b < c/d(10), A1
(12)T and C use the same product bd. The only difference is the sign of bd, and the direction of the conclusion follows it.T, (3), (6)
∎