Below zero
On a January morning in Ulaanbaatar, the thermometer may read . The shore of the Dead Sea lies more than 400 metres below sea level, and the city of Baku sits about 28 metres below it. A shop that owes a supplier 300 dirhams has a balance of .
Whenever a quantity can go below a starting point, the counting numbers are not enough. We need numbers that point the other way.
The number line, in both directions
Picture the counting numbers marching to the right from . The integers add their mirror images marching to the left:
Adding a positive number moves right; adding a negative number moves left. Every integer has an opposite on the other side of zero, the same distance away.
संख्या रेखा पर चलना
ऋणात्मक संख्या जोड़ने का अर्थ है बाईं ओर चलना। हर पूर्णांक का एक विपरीत होता है, जो आपको शून्य पर घर वापस ले आता है।
3 + (−5) = −2
क्या आप वह संख्या खोज सकते हैं जो आपको ठीक 0 पर वापस ले आए?
Definitions and properties
परिभाषा— additive inverse
For an integer , its opposite or additive inverse is the integer with .
Subtraction is defined as adding the opposite: . So .
The integers obey a short list of rules. For all integers :
| Property | Addition | Multiplication |
|---|---|---|
| Commutative | ||
| Associative | ||
| Identity | ||
| Inverse | — (see below!) |
and the two operations are linked by the distributive law: .
That empty box in the multiplication column is not a mistake. It will lead us somewhere wonderful.
टिप्पणी
With only the counting numbers there is no number with . Inventing the integers is exactly what makes additive inverses exist for every number.
/-- In the natural numbers there is no additive inverse of `1`: no `n` with `1 + n = 0`.
This is why we extend the natural numbers to the integers. -/
theorem nat_no_additive_inverse : ¬ ∃ n : Nat, 1 + n = 0 := by
intro ⟨n, h⟩
-- `1 + n` is the successor `n + 1`, and a successor is never `0`.
rw [Nat.add_comm] at h
exact Nat.succ_ne_zero n h/-- Every integer cancels with its negative: `a + (-a) = 0`.
This applies core Lean's `Int.add_right_neg`. -/
theorem add_neg_cancel (a : Int) : a + -a = 0 := Int.add_right_neg aWorked examples
उदाहरण— Adding and subtracting
- : start at , move to the right.
- .
- : subtracting a negative is adding its opposite.
उदाहरण— Multiplying
- .
- by commutativity.
- — and the next section explains why it must be.
Why negative times negative is positive
Many people learn "a negative times a negative is a positive" as a rule to memorise. In fact it is forced by the properties in the table. If we want distributivity to keep working for negative numbers, there is no other choice.
First, two small facts.
प्रमेय— Lemma 1
For every integer : .
उपपत्ति
Since , distributivity gives . Adding to both sides leaves .
∎
प्रमेय— Lemma 2
For all integers : .
उपपत्ति
By distributivity and Lemma 1, . So is a number that adds to to give — that is, it is the opposite of . (An integer has only one opposite: if , adding to both sides gives .)
∎
प्रमेय— sign rule
For all integers : .
उपपत्ति
Distributivity and Lemma 1 give
So is the opposite of . By Lemma 2, , and the opposite of is . Therefore .
∎
The same proof, checked by Lean
Here is the same argument written in Lean. Each step of the calc block matches a line of the human proof.
/-- `a · 0 = 0`, derived from distributivity and cancellation:
`a·0 + a·0 = a·(0 + 0) = a·0 = a·0 + 0`, and cancelling `a·0` leaves `a·0 = 0`. -/
theorem mul_zero_from_distrib (a : Int) : a * 0 = 0 := by
have h : a * 0 + a * 0 = a * 0 + 0 :=
calc a * 0 + a * 0 = a * (0 + 0) := (Int.mul_add a 0 0).symm
_ = a * 0 := by rw [Int.add_zero]
_ = a * 0 + 0 := (Int.add_zero (a * 0)).symm
exact Int.add_left_cancel h/-- `(-a) · b = -(a · b)`, from distributivity:
`(-a)·b + a·b = (-a + a)·b = 0·b = 0`, so `(-a)·b` is the additive inverse of `a·b`. -/
theorem neg_mul_from_distrib (a b : Int) : -a * b = -(a * b) := by
have h : -a * b + a * b = 0 :=
calc -a * b + a * b = (-a + a) * b := (Int.add_mul (-a) a b).symm
_ = 0 * b := by rw [Int.add_left_neg]
_ = b * 0 := Int.mul_comm 0 b
_ = 0 := mul_zero_from_distrib b
exact eq_neg_of_add_eq_zero h/-- "Negative times negative is positive", proved the way a student would:
1. `(-a)(-b) + (-a)b = (-a)(-b + b) = (-a)·0 = 0` (distributivity, then `-b + b = 0`);
2. `(-a)b = -(ab)` (`neg_mul_from_distrib`);
3. so `(-a)(-b) + -(ab) = 0`, which forces `(-a)(-b) = ab`. -/
theorem neg_mul_neg_from_axioms (a b : Int) : -a * -b = a * b := by
-- Step 1.
have step1 : -a * -b + -a * b = 0 :=
calc -a * -b + -a * b = -a * (-b + b) := (Int.mul_add (-a) (-b) b).symm
_ = -a * 0 := by rw [Int.add_left_neg]
_ = 0 := mul_zero_from_distrib (-a)
-- Step 2.
have step2 : -a * b = -(a * b) := neg_mul_from_distrib a b
-- Step 3: substitute step 2 into step 1, then cancel.
rw [step2] at step1
exact eq_of_add_neg_eq_zero step1/-- "Negative times negative is positive": `(-a) · (-b) = a · b`.
This version just applies core Lean's theorem `Int.neg_mul_neg`. Compare
`neg_mul_neg_from_axioms`, which proves the same statement from the ring axioms. -/
theorem neg_mul_neg_library (a b : Int) : -a * -b = a * b := Int.neg_mul_neg a bCalculating, checking and being fooled
"""Why is a negative times a negative positive? Three kinds of evidence.
1. Experimental: check (-a)(-b) = ab on a grid of integers.
2. Symbolic: let SymPy manipulate the letters a and b themselves.
3. Explanation: the lesson's proof from the distributive law, whose steps we
display (SymPy cannot tell you *why* - it already has the rules built in).
Runs in the browser (Pyodide) with the ``sympy`` package loaded.
"""
import textwrap
import sympy
def grid(radius):
"""Return all integer pairs (a, b) with -radius <= a, b <= radius."""
if radius < 0:
raise ValueError("radius must be non-negative")
values = range(-radius, radius + 1)
return [(a, b) for a in values for b in values]
def check_on_grid(rule, pairs):
"""Apply ``rule(a, b) -> bool`` to every pair; return (cases, list of failing pairs)."""
failures = [(a, b) for a, b in pairs if not rule(a, b)]
return len(pairs), failures
def neg_times_neg(a, b):
"""The rule (-a)(-b) = ab for one pair of numbers."""
return (-a) * (-b) == a * b
def neg_times_pos(a, b):
"""The rule (-a)b = -(ab) for one pair of numbers."""
return (-a) * b == -(a * b)
def symbolic_difference(lhs, rhs):
"""Return ``sympy.expand(lhs - rhs)``; it is 0 exactly when SymPy proves lhs = rhs as polynomials."""
return sympy.expand(lhs - rhs)
def symbolic_examples():
"""Return a list of (description, SymPy result) rows used in the printout."""
a, b = sympy.symbols("a b")
A, B = sympy.symbols("A B", commutative=False)
return [
("(-a)*(-b)", (-a) * (-b)),
("(-a)*(-b) - a*b, expanded", symbolic_difference((-a) * (-b), a * b)),
("(-a)*b + a*b, expanded", symbolic_difference((-a) * b, -(a * b))),
("(a - b)*(a + b), expanded", sympy.expand((a - b) * (a + b))),
("how SymPy stores -a", sympy.srepr(-a)),
("(-A)*(-B), non-commuting A, B", (-A) * (-B)),
("A*B - B*A, non-commuting A, B", sympy.expand(A * B - B * A)),
]
#: Steps of the proof in the lesson. Each uses one ring law.
PROOF_STEPS = [
("0 = (-a) * 0", "x * 0 = 0, itself proved from distributivity"),
(" = (-a) * (b + (-b))", "b + (-b) = 0"),
(" = (-a)b + (-a)(-b)", "distributive law"),
(" = -(ab) + (-a)(-b)", "(-a)b = -(ab), proved the same way"),
("so (-a)(-b) = ab", "add ab to both sides"),
]
def main():
print(f"1. Experiment: exact integer arithmetic on a grid (SymPy {sympy.__version__} used below)")
pairs = grid(10)
for label, rule in [("(-a)(-b) = ab ", neg_times_neg), ("(-a)b = -(ab) ", neg_times_pos)]:
cases, failures = check_on_grid(rule, pairs)
print(f" {label} for all a, b in -10..10: {cases} cases, {len(failures)} failures")
print(" A grid can never reach every integer: this is evidence, not proof.")
print()
print("2. Symbolic algebra: SymPy works with the letters themselves")
for description, result in symbolic_examples():
print(f" {description:<34} -> {result}")
print(textwrap.fill(
"SymPy turns (-a)*(-b) into a*b the moment it is typed: it stores -a as "
"(-1)*a and multiplies the coefficients (-1)*(-1) = 1. A zero difference "
"means the identity holds for all values in any commutative ring - "
"provided SymPy's built-in rules are implemented correctly. The last two "
"rows show the sign rule does not even need commutativity.",
width=78, initial_indent=" ", subsequent_indent=" ",
))
print()
print("3. Why it is true (the lesson's proof, using only the ring laws):")
for step, reason in PROOF_STEPS:
print(f" {step:<24} [{reason}]")
print()
print(textwrap.fill(
"Epistemic status: part 1 is experimental evidence for 441 cases; part 2 "
"is a symbolic verification that is only as trustworthy as SymPy's "
"implementation of the ring axioms; only the proof in part 3 explains "
"why (-a)(-b) = ab in every ring.",
width=78,
))
if __name__ == "__main__":
main()A grid check is experimental evidence: it can't cover every integer. Symbolic expansion is stronger — but it relies on the rules the algebra system was programmed with, which are exactly the properties our proof used. The proof explains why.
Evidence can also be misleading. The formula gives a prime number for — forty successes in a row. Is it always prime?
"""Euler's prime-generating polynomial: forty successes, then a failure.
p(n) = n^2 + n + 41 is prime for n = 0, 1, 2, ..., 39 - forty cases in a row.
It is tempting to conclude "always prime". n = 40 breaks the pattern:
p(40) = 1681 = 41 * 41. Evidence, however plentiful, is not proof.
Runs unchanged in the browser (Pyodide) using only the standard library.
"""
import textwrap
def euler(n):
"""Euler's polynomial n^2 + n + 41."""
return n * n + n + 41
def is_prime(n):
"""Exact primality test by trial division (fine for the small numbers used here)."""
if n < 2:
return False
if n % 2 == 0:
return n == 2
d = 3
while d * d <= n:
if n % d == 0:
return False
d += 2
return True
def smallest_factor(n):
"""The smallest prime factor of an integer n >= 2."""
if n < 2:
raise ValueError("n must be at least 2")
if n % 2 == 0:
return 2
d = 3
while d * d <= n:
if n % d == 0:
return d
d += 2
return n
def first_failure(poly, start=0, stop=10_000):
"""Return the first n in start..stop-1 where poly(n) is not prime, or None."""
for n in range(start, stop):
if not is_prime(poly(n)):
return n
return None
def prime_count(poly, stop):
"""How many of poly(0), ..., poly(stop - 1) are prime."""
return sum(is_prime(poly(n)) for n in range(stop))
def main():
print("Euler's polynomial p(n) = n^2 + n + 41. Is p(n) always prime?")
print()
values = [euler(n) for n in range(40)]
for row in range(0, 40, 8):
cells = " ".join(f"{v:>5}" for v in values[row:row + 8])
print(f" n = {row:>2}..{row + 7:<2}: {cells}")
streak = sum(is_prime(v) for v in values)
print(f"All {streak} of these 40 values are prime (checked exactly by trial division).")
print()
n = first_failure(euler)
v = euler(n)
f = smallest_factor(v)
print(f"First failure: n = {n}, p({n}) = {v} = {f} * {v // f}.")
print(f"Why n = 40 had to fail: p(40) = 40*40 + 40 + 41 = 40*41 + 41 = 41*41.")
print(f"And p(41) = 41*41 + 41 + 41 = 41 * 43 = {euler(41)} fails too.")
print()
for stop in (100, 1000):
print(f"Primes among p(0), ..., p({stop - 1}): {prime_count(euler, stop)} of {stop}")
print("Still remarkably many - but a pattern that is 'usually true' is not a theorem.")
print()
print(textwrap.fill(
"Epistemic status: forty confirming cases were experimental evidence, "
"and they were not a proof - the single counterexample at n = 40 proves "
"that n^2+n+41 is not always prime. (No non-constant polynomial with "
"integer coefficients gives primes for every n; that is a theorem, not "
"something this program checked.)",
width=78,
))
if __name__ == "__main__":
main()The empty box: multiplicative inverses
Every integer has an additive partner with . What about multiplication? Is there an integer with ?
For , yes: . For , yes: . But for ?
प्रमेय— no half in the integers
There is no integer with .
उपपत्ति
For any integer , the number is even. But is odd. So .
∎
/-- There is no integer `x` with `2 · x = 1`, so `2` has no multiplicative inverse in `Int`.
Reason: `2 · x` always leaves remainder `0` when divided by `2`, but `1` leaves remainder `1`. -/
theorem no_int_half : ¬ ∃ x : Int, 2 * x = 1 := by
intro ⟨x, h⟩
have hrem : (2 * x) % 2 = 1 % 2 := by rw [h]
rw [Int.mul_emod_right] at hrem
-- `hrem : 0 = 1 % 2`, i.e. `0 = 1`, which is false.
exact absurd hrem (by decide)In fact, only and have multiplicative partners among the integers:
/-- The only integers with a multiplicative inverse are `1` and `-1`:
if `a · b = 1` then `a = 1` or `a = -1`.
Proof: take absolute values. `|a| · |b| = |a · b| = 1` in the natural numbers, which forces
`|a| = 1`; an integer with absolute value `1` is `1` or `-1`. -/
theorem int_units (a b : Int) (h : a * b = 1) : a = 1 ∨ a = -1 := by
have habs : a.natAbs * b.natAbs = 1 := by
rw [← Int.natAbs_mul, h]
rfl
have ha : a.natAbs = 1 := Nat.eq_one_of_mul_eq_one_right habs
-- Every integer is `+|a|` or `-|a|`.
cases Int.natAbs_eq a with
| inl hpos => left; rw [hpos, ha]; rfl
| inr hneg => right; rw [hneg, ha]; rfl"""Searching for inverses among the integers, and among the rationals.
For each integer n we search a window of integers m for an *additive inverse*
(n + m = 0) and a *multiplicative inverse* (n * m = 1). Additive inverses are
always found; multiplicative ones only for n = 1 and n = -1. Then we move to
the rational numbers, using ``fractions.Fraction`` for exact arithmetic, where
every non-zero number has a multiplicative inverse.
Runs unchanged in the browser (Pyodide) using only the standard library.
"""
from fractions import Fraction
import textwrap
def window(radius):
"""Return the integers -radius..radius (inclusive) as a range."""
if radius < 0:
raise ValueError("radius must be non-negative")
return range(-radius, radius + 1)
def find_additive_inverse(n, candidates):
"""Return the first m in ``candidates`` with n + m == 0, or None if none is found."""
for m in candidates:
if n + m == 0:
return m
return None
def find_multiplicative_inverse(n, candidates):
"""Return the first m in ``candidates`` with n * m == 1, or None if none is found.
``None`` only means "not found among the candidates": on its own a search
cannot prove that no inverse exists further away.
"""
for m in candidates:
if n * m == 1:
return m
return None
def rational_inverse(q):
"""Return the exact multiplicative inverse 1/q of a rational q, or None when q == 0."""
q = Fraction(q)
if q == 0:
return None
return 1 / q
def search_summary(n_radius, m_radius):
"""Search every n in -n_radius..n_radius over candidates m in -m_radius..m_radius.
Returns ``(additive_found, multiplicative_found)``: the lists of n for which
an additive / multiplicative inverse was found.
"""
candidates = window(m_radius)
additive = [n for n in window(n_radius) if find_additive_inverse(n, candidates) is not None]
multiplicative = [n for n in window(n_radius) if find_multiplicative_inverse(n, candidates) is not None]
return additive, multiplicative
def main():
candidates = window(50)
print("For each n, search m in -50..50 for n + m = 0 and for n * m = 1.")
print("Then, in the rationals Q, compute 1/n exactly with fractions.Fraction.")
print()
print(f"{'n':>4} | {'n + m = 0':>9} | {'n * m = 1':>9} | {'1/n in Q':>8} | n * (1/n)")
print("-" * 52)
for n in window(6):
add = find_additive_inverse(n, candidates)
mul = find_multiplicative_inverse(n, candidates)
inv = rational_inverse(n)
mul_s = "none" if mul is None else str(mul)
inv_s = "none" if inv is None else str(inv)
check = "-" if inv is None else str(n * inv)
print(f"{n:>4} | {add:>9} | {mul_s:>9} | {inv_s:>8} | {check}")
print()
radius = 30
additive, multiplicative = search_summary(radius, radius)
total = 2 * radius + 1
print(f"Wider search, n and m both in -{radius}..{radius}:")
print(f" additive inverse found for {len(additive)} of {total} integers")
print(f" multiplicative inverse found for {len(multiplicative)} of {total}: n = {multiplicative}")
q = Fraction(-7, 12)
print(f" in Q, e.g. q = {q}: 1/q = {rational_inverse(q)} and q * (1/q) = {q * rational_inverse(q)} exactly")
print()
print("Why the integer search can stop: if |n| >= 2 and m != 0 then |n * m| >= 2,")
print("and if m = 0 then n * m = 0. So n * m = 1 is impossible however far we look.")
print()
print(textwrap.fill(
"Epistemic status: the searches are experiments over finite windows (a "
"failed search alone proves nothing about numbers outside the window); "
"the rational arithmetic is exact. The two-line size argument above, "
"not the search, proves that only 1 and -1 have integer inverses.",
width=78,
))
if __name__ == "__main__":
main()Exercises
1. Integers
आरंभिकमानवीयCompute .
2. Integers
आरंभिकमानवीयCompute .
3. Integers
मुख्यमानवीयCompute .
4. Integers
मुख्यमानवीयCompute .
5. Integers
मुख्यमानवीयIn the proof that , we wrote . Which property justifies this step?
6. Integers
मुख्यमानवीयFor which integers is there an integer with ? (Choose all that apply.)
7. Integers
आरंभिकमानवीयAt dawn in Ulaanbaatar the temperature is . By noon it has risen by degrees. What is the noon temperature, in ?
8. Integers
चुनौतीसंगणनात्मकWrite find_mult_partner(a, limit) that searches the integers with and returns the first with a * b == 1, or None if there is none. Then think: why does searching further never help when ?
Common misconceptions
भ्रांति
"Two negatives make a positive" — for addition too. The sign rule is about multiplication. For addition, : two steps to the left take you further left.
भ्रांति
" is always negative." means the opposite of . If , then , which is positive.
भ्रांति
"Subtraction is commutative." but . Rewriting subtraction as adding the opposite, , shows exactly where the asymmetry comes from.
भ्रांति
"The sign rule is just a convention." It is a consequence: as the proof shows, any number system with these properties must have .
Wonder Trails
The empty box in the table — and the arithmetic of clocks — lead to some of the most important ideas in mathematics. All of these are optional.
विस्मय पथ · वैकल्पिक · कभी अंक नहीं दिए जातेInverses and structureEvery integer can be added to another integer to get . So why can almost no integer be multiplied by another integer to get ?पथ पर चलें विस्मय पथ · वैकल्पिक · कभी अंक नहीं दिए जातेClock arithmeticIt's 9 o'clock. What time will it be in 5 hours — and in 29 hours? Can a clock teach us a whole new kind of arithmetic?पथ पर चलें विस्मय पथ · वैकल्पिक · कभी अंक नहीं दिए जातेRemainder familiesSort every integer — positive, negative and zero — into families by its remainder after dividing by 3. If you add a member of one family to a member of another, does the family of the answer depend on which members you chose?पथ पर चलेंSet-theoretic connection
The counting numbers form a subset of the integers: . At university you may see a way to build the integers out of the counting numbers: an integer is represented by a pair of counting numbers, thought of as "", where two pairs count as the same integer when . This uses an equivalence relation — an idea you can preview on the Remainder families trail.
A glimpse of structure
"Add " is a transformation of the whole number line: it slides every integer three places right. It can always be undone, by "add ". Doing "add " and then "add " is the same as "add ", and "add " does nothing at all. A collection of reversible transformations that combine like this is called a group — and the integers under addition are one of the most important examples. The Inverses and structure trail starts here.
History and global context
- In China, The Nine Chapters on the Mathematical Art — compiled roughly two thousand years ago — solved problems using positive and negative quantities. In Liu Hui's 3rd-century commentary, counting rods of two colours, red and black, distinguish the two kinds.
- In India, Brahmagupta's Brāhmasphuṭasiddhānta (628 CE) gave rules for calculating with "fortunes" and "debts" — positive and negative numbers — and with zero, including the rule that a debt times a debt is a fortune.
- Mathematicians writing in Arabic and Persian, and later in Europe, used these ideas cautiously. As late as 1545, Gerolamo Cardano called negative solutions "fictitious". Full acceptance of negative numbers as numbers came gradually over the following centuries.
Further reading
- Richard Courant and Herbert Robbins, What Is Mathematics? (1941), chapter 2 on number systems.
- Edmund Landau, Foundations of Analysis (1930), for a rigorous construction of the integers from the natural numbers.
वैकल्पिक ईसाई चिंतन · debts and forgiveness
ईसाई परंपरा से एक चिंतन, जो The Lumenary की प्रेरणा है। यह गणित का हिस्सा नहीं है, और आप इसे बेझिझक छोड़ सकते हैं।
Brahmagupta called negative numbers debts. In the prayer Jesus taught, Christians ask God to "forgive us our debts, as we also have forgiven our debtors" (Matthew 6:12). Adding the opposite cancels a debt, and the account returns to zero — but in real life someone must bear the cost. Christians understand forgiveness as exactly that kind of costly gift. Mathematics, of course, needs none of this to be true; it is offered only as a reflection.