In [1]:

```
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 [2]:

```
%begin axioms
```

In [3]:

```
# a mod b ≥ 0
mod_greater_eq_zero = Forall(
(a, b),
greater_eq(Mod(a, b), zero),
domains=[Real, RealPos])
```

In [4]:

```
# a mod b < b
mod_less_modulus = Forall(
(a, b),
Less(Mod(a, b), b),
domains=[Real, RealPos])
```

In [5]:

```
# a mod b is the remainder after taking out integer multiples of modulus b
mod_is_remainder = Forall(
(a, b),
Exists(q, Equals(a, Add(Mult(q,b),Mod(a,b))), domain=Integer),
domains=[Real, RealPos])
```

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 [6]:

```
mod_abs_def = Forall(
(a, b),
Equals(ModAbs(a, b), Min(Mod(a, b), Mod(Neg(a), b))),
domains=[Real, RealPos])
```

In [7]:

```
%end axioms
```