# Demonstrations for the theory of proveit.numbers.numerals.decimals¶

In [1]:
import proveit
from proveit import ExprRange, ExprTuple, var_range
from proveit.logic import Equals, InSet
from proveit.numbers import zero, one, two, three, four, five, six, seven, eight, nine
Natural, NaturalPos, subtract)
from proveit.numbers.numerals.decimals import DecimalSequence
from proveit.core_expr_types import Len
from proveit import A, a, b, c, d, e, f, g, h, i, j, k, m, n, x
from proveit.numbers.numerals.decimals import Digits
%begin demonstrations


Decimals are defined as numbers within the base-10 number system. That is, they use the numbers 0 through 9 for each digit. At the moment, only whole numbers are defined within Prove-It.

The digits 0 through 9 are individually defined literals that can be imported from proveit.numbers.

In [2]:
# each digit literal is defined as its linguistic counterpart. e.g. 1 is defined as "one"
zero


In order to create numbers larger than a single digit, create a DecimalSequence() object, or use the num() method.

In [3]:
# DecimalSequence() takes each digit as an argument
deci_sequence = DecimalSequence(one, zero, one)

deci_sequence:
In [4]:
# the num() method takes in a python integer as an argument
num_def = num(101)

num_def:
In [5]:
Equals(deci_sequence, num_def).prove()


The set Digits is defined as the natural numbers from 0 to 9.

In [6]:
from proveit.numbers.numerals.decimals import N_leq_9_enumSet
N_leq_9_enumSet

In [7]:
InSet(one, Digits).prove()


Prove-It is also able to perform basic arithmetic involving decimal sequences.

In [8]:
Add(num(11), one).evaluation()

In [9]:
Add(num(999), one).evaluation()

In [10]:
Add(num(10), one).evaluation()

In [11]:
Len(ExprTuple(a, b, c, d, e, f, g, h, i, k, m)).evaluation()

In [12]:
Equals(Len(ExprTuple(a, b , c, d, e, f, g, h, i, k, m)),
Len(var_range(a, one, num(11)))
).prove()

In [13]:
Equals(Len(ExprTuple(a, b , c, d, e, f, g, h, i, k, m)), num(11)).prove()

In [14]:
Equals(Len(ExprTuple(a, b, c, d, e, f, g, h, i, k, m, n)), num(12)).prove()

In [15]:
nines = num(999999999)

nines:
In [16]:
Add(nines, one).evaluation()

In [17]:
Add(num(99999), one).evaluation()

In [18]:
number = num(9999993)

number:
In [19]:
Len(DecimalSequence(three, eight, six, seven, four, ExprRange(i, nine, one, four), five, seven, two).digits).computation()

In [20]:
%end demonstrations