 # Axioms for the theory of proveit.numbers.modular¶

In :
import proveit
# Prepare this notebook for defining the axioms of a theory:
%axioms_notebook # Keep this at the top following 'import proveit'.
from proveit import a, b, q
from proveit.logic import Equals, Exists, Forall
from proveit.numbers import Add, greater_eq, Less, Min, Mod, ModAbs, Mult, Neg
from proveit.numbers import zero, Integer, NaturalPos, Real, RealPos

In :
%begin axioms

Defining axioms for theory 'proveit.numbers.modular'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions


#### For positive real-valued modulus $b$, $\text{mod}(a, b)$ is the non-negative remainder $r$ when $a$ is divided by $b$ in the usual way, giving $0 \le r < b$. This means that there exists a unique integer $q$ such that $a = qb + r$.¶

ModAbs captures the concept of the arc-distance between points on a circle. If $b$ is the circumference of the circle and $a$ maps to a point on the circle by traversing an arc-distance of $a$ from the origin then $|a|_{\textrm{mod}~b}$ is the arc-distance of that point from the origin (the shortest distance to traverse between the two points in either direction).

In :
%end axioms

These axioms may now be imported from the theory package: proveit.numbers.modular