Integers, Divisibility & Proof Tools

Intuition, Vocabulary and Foundations

Integers model signed counts, positions, balances, and discrete changes. Think of the division algorithm as packing objects into equal-sized boxes: dividing $a=23$ objects into boxes of size $d=5$ produces $q=4$ full boxes and a remainder $r=3$. Formally, for every integer $a$ and positive integer $d$, there are unique integers $q,r$ such that

$$ a=dq+r,\qquad 0\le r\lt d. $$

The equation is equally important for negative inputs. For example, $-23=5(-5)+2$, so Euclidean division gives $q=-5$ and $r=2$, not $q=-4$ and $r=-3$. The remainder bound selects one canonical answer from infinitely many algebraic decompositions.

An integer $d$ divides $n$, written $d\mid n$, when some integer $k$ satisfies $n=dk$. Thus $4\mid20$, but $4\nmid22$. This definition uses multiplication rather than a programming-language division operator: $0\mid n$ holds only when $n=0$, while every nonzero integer divides $0$.

The floor and ceiling functions select neighboring integers: $\lfloor x\rfloor\le x\lt\lfloor x\rfloor+1$ and $\lceil x\rceil-1\lt x\le\lceil x\rceil$. For integers $a$ and nonzero $b$, floor division is $\lfloor a/b\rfloor$, whereas ceiling division is $\lceil a/b\rceil$. Parity is divisibility by $2$, and the valuation $v_p(n)$ counts how many copies of $p>1$ divide a nonzero $n$; for example, $v_2(40)=3$.

These definitions support reusable proof tools. A direct divisibility proof exhibits a witness. Induction proves a base case and a step that preserves truth, while contradiction assumes the negation and derives an impossibility. In algorithm proofs, the same reasoning appears as an invariant: a statement that is true initially, preserved by every transition, and strong enough to imply the result at termination.

Step-by-Step Derivations and Algorithms

For $a\in\mathbb Z$ and $d>0$, choose $q=\lfloor a/d\rfloor$ and define $r=a-dq$. From $q\le a/d\lt q+1$, multiplication by positive $d$ gives $dq\le a\lt d(q+1)$, hence $0\le r\lt d$. This constructs a valid quotient and remainder for positive and negative dividends.

For uniqueness, suppose $a=dq+r=dq'+r'$ with both remainders in $[0,d)$. Then $d(q-q')=r'-r$. The right side has absolute value below $d$, while the left side is a multiple of $d$; both must be zero. Therefore $r=r'$ and $q=q'$.

Divisibility lemmas expose witnesses. If $d\mid a$ and $d\mid b$, write $a=dx$ and $b=dy$. For any integers $u,v$,

$$ ua+vb=d(ux+vy), $$

so $d\mid ua+vb$. This closure under linear combinations later powers Euclid's algorithm and Bézout identities. Transitivity is similar: $b=ax$ and $c=by$ imply $c=a(xy)$.

Floor division can be derived from truncation without floating point. A truncating quotient is already the floor when division is exact or the operands have the same sign. If signs differ and a nonzero remainder remains, subtract one. Ceiling division then follows from $\lceil a/b\rceil=-\lfloor-a/b\rfloor$. A valuation algorithm repeatedly divides by $p$; each successful division proves one more factor, and the first nonzero remainder proves maximality.

flowchart TD
    A["Integer model and sign conventions"] --> B["Division algorithm: a = dq + r"]
    B --> C["Canonical quotient and remainder"]
    B --> D["Divisibility witnesses"]
    C --> E["Floor and ceiling helpers"]
    D --> F["Linear-combination lemmas"]
    D --> G["Parity and valuations"]
    F --> H["Induction, contradiction, and invariants"]
    E --> I["Reliable integer algorithms"]
    G --> I
    H --> I

Implementation, Complexity and Engineering

Integer APIs must document their semantics. Python's // computes mathematical floor division, but several languages truncate toward zero; remainder signs also differ. Code that assumes a / b and a % b mean Euclidean division may pass positive-only tests and fail immediately for negative operands.

The implementation below avoids floating point. floor_div begins with a truncating quotient constructed from magnitudes and corrects it when opposite signs leave a remainder. euclidean_divmod guarantees $0\le r\lt\lvert b\rvert$, including for a negative divisor. ceil_div, divides, and valuation build on explicit contracts.

Python integers grow automatically. In a fixed-width language, however, MIN_INT / -1, negating MIN_INT, reconstructing q*b, or using (a+b-1)/b may overflow. Production code should use checked operations, wider intermediates, or primitives whose supported domain is explicit.

from __future__ import annotations


def trunc_div(a: int, b: int) -> int:
    """Return a / b truncated toward zero, without floating point."""
    if b == 0:
        raise ZeroDivisionError("integer division by zero")
    magnitude = abs(a) // abs(b)
    return -magnitude if (a < 0) != (b < 0) else magnitude


def floor_div(a: int, b: int) -> int:
    """Return floor(a / b) for integers a and nonzero b."""
    q = trunc_div(a, b)
    remainder = a - b * q
    if remainder != 0 and (a < 0) != (b < 0):
        q -= 1
    return q


def ceil_div(a: int, b: int) -> int:
    """Return ceil(a / b) for integers a and nonzero b."""
    return -floor_div(-a, b)


def euclidean_divmod(a: int, b: int) -> tuple[int, int]:
    """Return q, r satisfying a = b*q + r and 0 <= r < abs(b)."""
    if b == 0:
        raise ZeroDivisionError("Euclidean division requires b != 0")
    q, r = divmod(a, abs(b))
    if b < 0:
        q = -q
    assert a == b * q + r
    assert 0 <= r < abs(b)
    return q, r


def divides(d: int, n: int) -> bool:
    """Return whether an integer k exists with n = d*k."""
    return n == 0 if d == 0 else n % d == 0


def valuation(n: int, p: int) -> int:
    """Return the largest e such that p**e divides nonzero n."""
    if p <= 1:
        raise ValueError("p must be greater than 1")
    if n == 0:
        raise ValueError("v_p(0) is not finite")
    n = abs(n)
    exponent = 0
    while n % p == 0:
        n //= p
        exponent += 1
    return exponent


def run_tests() -> None:
    cases = [
        (23, 5, 4, 5),
        (-23, 5, -5, -4),
        (23, -5, -5, -4),
        (-23, -5, 4, 5),
        (20, 5, 4, 4),
        (0, 7, 0, 0),
    ]
    for a, b, expected_floor, expected_ceil in cases:
        assert floor_div(a, b) == expected_floor
        assert ceil_div(a, b) == expected_ceil
        q, r = euclidean_divmod(a, b)
        assert a == b * q + r
        assert 0 <= r < abs(b)

    assert divides(6, 42) and not divides(6, 43)
    assert divides(-7, 0) and divides(0, 0) and not divides(0, 5)
    assert valuation(40, 2) == 3
    assert valuation(-108, 3) == 3
    assert valuation(35, 2) == 0

    for operation in (lambda: floor_div(8, 0), lambda: valuation(0, 2)):
        try:
            operation()
        except (ZeroDivisionError, ValueError):
            pass
        else:
            raise AssertionError("invalid input was not rejected")


if __name__ == "__main__":
    run_tests()
    print("all arithmetic-helper tests passed")

Applications, Case Studies and Exercises

These foundations recur whenever software partitions resources, maps signed coordinates into buckets, reasons about periodic schedules, or proves an arithmetic loop correct. The same specification-first discipline scales from a classroom quotient helper to storage sharding and modular arithmetic.