logo

Theory of proveit.numbers

Covers all generic number concepts: sets of numbers (integers, reals, and complexes), number relations (<, $\leq$, >, $\geq$), and numeric operations (+, -, $\times$, /, mod, exp), and operations over numeric functions ($\sum$, $\prod$, $\partial$, $\nabla$, $\int$).

In [1]:
import proveit
%theory # toggles between interactive and static modes

Local content of this theory

common expressions axioms theorems demonstrations

Sub-theories

number_setsdefining standard number sets: integers, reals, complexes, and important subsets of these
roundingrounding of real numbers, such as round, floor, and ceiling
absolute_valueabsolute value of reals (and subsets) and norm of complex numbers
numeralsnumber representions: binary, decimal, hexidecimal
additionadding numbers (repetitive counting)
negationnegating numbers (subtraction from zero)
orderingordering relations of numbers: <, ≤ >, ≥
multiplicationmultiplying numbers (repetitive addition)
divisiondividing numbers (inverse of multiplication)
divisibilitydivisibility operations such as x|y to indicate x is a factor of y
modularmodular arithmetic (i.e., remainders of division)
exponentiationexponentiating numbers (repetitive multiplication)
logarithmslogarithms (inverse of exponentiation)
summationadd function evaluation instances: ∑
productmultiply function evaluation instances: ∏
differentiationrates of change; calculus: ∂, ∇, etc.
integrationsummation over infinitesimals, inverse of differentiation: ∫
functionscomplex- and real-valued functions of one or more variables

All axioms contained within this theory

This theory contains no axioms directly.

proveit.numbers.number_sets

proveit.numbers.rounding

proveit.numbers.absolute_value

proveit.numbers.numerals

proveit.numbers.addition

proveit.numbers.negation

proveit.numbers.ordering

proveit.numbers.multiplication

proveit.numbers.division

This sub-theory contains no axioms.

proveit.numbers.divisibility

proveit.numbers.modular

proveit.numbers.exponentiation

proveit.numbers.logarithms

This sub-theory contains no axioms.

proveit.numbers.summation

proveit.numbers.product

This sub-theory contains no axioms.

proveit.numbers.differentiation

This sub-theory contains no axioms.

proveit.numbers.integration

This sub-theory contains no axioms.

proveit.numbers.functions