Definition D1
b − a denotes b + (−a).
Proof.
Subtraction is not a new operation but addition of the inverse.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), A3
(3)0 < b − a(2), A6, D1
(4)Conversely, suppose 0 < b − a.assumption
(5)0 + a < (b + (−a)) + a(4), A3, D1
(6)(b + (−a)) + a = b + ((−a) + a) = bA7, A8, A6, A5
(7)0 + a = aA8, A5
(8)a < b(5), (6), (7)
∎
Lemma L2
For all a, a × 0 = 0
Proof.
(1)0 + 0 = 0A5
(2)a(0 + 0) = a × 0(1), E
(3)a×0 + a×0 = a×0(2), A9
(4)(a×0 + a×0) + (−(a×0)) = a×0 + (−(a×0))(3), E
(5)left side = a×0 + (a×0 + (−(a×0))) = a×0 + 0 = a×0A7, A6, A5
(6)right side = 0A6
(7)a × 0 = 0(4), (5), (6)
∎
Lemma L3
If x + y = 0 and x + z = 0, then y = z
Proof.
(1)y = y + 0A5
(2) = y + (x + z)assumption
(3) = (y + x) + zA7
(4) = (x + y) + zA8
(5) = 0 + zassumption
(6) = z + 0 = zA8, A5
∎
Lemma L4
(b − a)(−c) = ac − bc
Proof.
(1)Set P = b − a.D1
(2)P(−c) + Pc = P((−c) + c)A9
(3)(−c) + c = 0A8, A6
(4)P((−c) + c) = P × 0 = 0(3), E, L2
(5)P(−c) + Pc = 0(2), (4)
(6)Pc = c(b + (−a)) = cb + c(−a)(1), A10, A9
(7)c(−a) + ca = c((−a) + a) = c × 0 = 0A9, A8, A6, L2, E
(8)ca + (−(ca)) = 0A6
(9)c(−a) = −(ca)(7), (8), A8, L3
(10)Pc = bc + (−(ac))(6), (9), A10
(11)(bc + (−(ac))) + (ac + (−(bc))) = 0A7, A8, A6, A5
(12)Pc + P(−c) = 0 and Pc + (ac − bc) = 0(5), (10), (11), A8, D1
(13)P(−c) = ac − bc, that is, (b − a)(−c) = ac − bc(1), (12), L3
∎
Theorem T
If a < b and c < 0, then bc < ac, that is, ac > bc
Proof.
(1)Suppose a < b and c < 0.assumption
(2)c + (−c) < 0 + (−c)(1), A3
(3)0 < −c(2), A6, A8, A5
(4)0 < b − a(1), L1
(5)0 < (b − a)(−c)(3), (4), A4
(6)(b − a)(−c) = ac − bcL4
(7)0 < ac − bc(5), (6), E
(8)bc < ac(7), L1
∎
Corollary C
For c < 0, a < b holds if and only if bc < ac.
Proof.
(1)If a < b, then bc < ac.T
(2)Conversely, suppose bc < ac.assumption
(3)If a = b, then ac = bc, which violates (2) and trichotomy.E, A1, (2)
(4)If b < a, then by T, ac < bc.T
(5)Then from bc < ac and ac < bc, bc < bc.(2), (4), A2
(6)Trichotomy does not permit bc < bc.A1
(7)One of a < b, a = b, b < a holds.A1
(8)Therefore a < b.(3), (6), (7)
∎