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

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

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$.¶

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

mod_greater_eq_zero:
In [4]:
# a mod b < b
mod_less_modulus = Forall(
(a, b),
Less(Mod(a, b), b),
domains=[Real, RealPos])

mod_less_modulus:
In [5]:
# a mod b is the remainder after taking out integer multiples of modulus b
mod_is_remainder = Forall(
(a, b),
domains=[Real, RealPos])

mod_is_remainder:

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])

mod_abs_def:
In [7]:
%end axioms

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