nLab decimal rational number

Idea

A decimal rational number or decimal fraction is a rational number $r \in \mathbb{Q}$ such that the decimal expansion of $r$ has finitely many digits.

Definition

As a subset of the rational numbers

A decimal rational number or decimal fraction is a rational number $r \in \mathbb{Q}$ such that there exists $n \in \mathbb{N}$ and $a \in \mathbb{Z}$ such that $r = \frac{a}{10^n}$.

As the localisation of the integers at 10

The commutative ring of decimal rational numbers $\mathbb{Z}[1/10]$ is the localization of the integers $\mathbb{Z}$ away from $10$.

As an initial object of a category

For lack of a better name, let us define a set with decimal fractions to be a set $A$ with a function $\iota \in \mathbb{Z} \times \mathbb{N} \to A$, such that

$$\forall a \in \mathbb{Z}. \forall b \in \mathbb{N}. \forall c \in \mathbb{Z}. \forall d \in \mathbb{N}. (a \cdot 10^d = c \cdot 10^b) \implies (\iota(a, b) = \iota(c, d))$$

The integer $a:\mathbb{Z}$ represents the integer if one ignores the decimal separator in the decimal numeral representation of the decimal fraction, and the natural number $b:\mathbb{N}$ represents the number of digits to the left of the final digit where the decimal separator ought to be placed after in the decimal numeral representation of the decimal fraction. The axiom above is used to state that equivalent decimals are equal: i.e. 1.00 = 1.000 with decimal numeral representations.

A homomorphism of sets with decimal fractions between two decimal fraction algebras $A$ and $B$ is a function $f:A \to B$ such that

$$\forall a \in \mathbb{Z}. \forall b \in \mathbb{N}. f(\iota_A(a, b)) = \iota_B(a, b)$$

The category of sets with decimal fractions is the category $SwDF$ whose objects $Ob(SwDF)$ are sets with decimal fractions and whose morphisms $Mor(A,B)$ for sets with decimal fractions $A \in Ob(SwDF)$, $B \in Ob(SwDF)$ are homomorphisms of sets with decimal fractions. The set of decimal fractions, denoted $\mathbb{Z}[1/10]$, is defined as the initial object in the category of sets with decimal fractions.

As a higher inductive type

In homotopy type theory, the type of decimal numbers, denoted $\mathbb{Z}[1/10]$, could be defined as the higher inductive type generated by:

• A function $(-)/10^{(-)}:\mathbb{Z} \times \mathbb{N} \rightarrow \mathbb{Z}[1/10]$. The integer $a:\mathbb{Z}$ represents the integer if one ignores the decimal separator in the decimal numeral representation of the decimal number, and the natural number $b:\mathbb{N}$ represents the number of digits to the left of the final digit where the decimal separator ought to be placed after in the decimal numeral representation of the decimal number.
• A dependent product of functions between identities representing that equivalent decimals are equal:
  $$equivdec : \prod_{a:\mathbb{Z}} \prod_{b:\mathbb{N}} \prod_{c:\mathbb{Z}} \prod_{d:\mathbb{N}} (a \cdot 10^d = c \cdot 10^b) \to (a/10^b = c/10^d)$$

  (i.e. 1.00 = 1.000 with decimal numeral representations)

• A set-truncator
  $$\tau_0: \prod_{a:\mathbb{Z}[1/10]} \prod_{b:\mathbb{Z}[1/10]} isProp(a=b)$$

Properties

Decidability

Proposition

(Decidability of equality)

For every decimal fraction $p \in \mathbb{Z}[1/10]$ and $q \in \mathbb{Z}[1/10]$, $p = q$ or $\neg(p = q)$.

Definition

(Inequality)

For every decimal fraction $p \in \mathbb{Z}[1/10]$ and $q \in \mathbb{Z}[1/10]$, there is a proposition $p \neq q$ called inequality and defined as

$$p \neq q \coloneqq \neg(p = q)$$

Proposition

(Tight apartness relation)

Inequality $\neq$ is a tight apartness relation: For every decimal fraction $p \in \mathbb{Z}[1/10]$ and $q \in \mathbb{Z}[1/10]$, if $\neg(p \neq q)$, then $p = q$.

Commutative ring structure

Definition

(Addition)

There exists a binary operation $(-)+(-):\mathbb{Z}[1/10] \times \mathbb{Z}[1/10] \to \mathbb{Z}[1/10]$ called addition defined as

$$a/10^b + c/10^d \coloneqq (a \cdot 10^d + c \cdot 10^b)/10^{(b + d)}$$

for $a \in \mathbb{Z}$, $b \in \mathbb{N}$, $c \in \mathbb{Z}$, $d \in \mathbb{N}$.

Proposition

(Associativity of addition)

For every decimal fraction $p \in \mathbb{Z}[1/10]$, $q \in \mathbb{Z}[1/10]$, and $r \in \mathbb{Z}[1/10]$, $(p + q) + r = p + (q + r)$.

Proof

By definition of the set of decimal fractions, there exist numbers $a \in \mathbb{Z}$, $b \in \mathbb{N}$, $c \in \mathbb{Z}$, $d \in \mathbb{N}$, $e \in \mathbb{Z}$, $f \in \mathbb{N}$ such that $a/10^b = p$, $c/10^d = q$, and $e/10^f = q$. Thus,

$$p + q = a/10^b + c/10^d = (a \cdot 10^d + c \cdot 10^b)/10^{(b + d)}$$

$$(p + q) + r = (a \cdot 10^d + c \cdot 10^b)/10^{(b + d)} + e/10^f = ((a \cdot 10^d + c \cdot 10^b) \cdot 10^f + e \cdot 10^{(b + d)})/10^{(b + d) + f}$$

$$q + r = c/10^d + e/10^f = (c \cdot 10^f + e \cdot 10^d)/10^{(d + f)}$$

$$p + (q + r) = a/10^b + (c \cdot 10^f + e \cdot 10^d)/10^{(d + f)} = (a \cdot 10^{(d + f)} + (c \cdot 10^f + e \cdot 10^d) \cdot 10^b)/10^{b + (d + f)}$$

by definition of addition. By the distributive property of multiplication of integers

$$((a \cdot 10^d + c \cdot 10^b) \cdot 10^f + e \cdot 10^{(b + d)})/10^{(b + d) + f} = (a \cdot 10^d \cdot 10^f + c \cdot 10^b \cdot 10^f) + e \cdot 10^{(b + d)})/10^{(b + d) + f}$$

$$(a \cdot 10^{(d + f)} + (c \cdot 10^f + e \cdot 10^d) \cdot 10^b)/10^{b + (d + f)} = (a \cdot 10^{(d + f)} + (c \cdot 10^f \cdot 10^b + e \cdot 10^d \cdot 10^b)/10^{b + (d + f)}$$

and by the fact that exponentiation is an $\mathbb{N}$-action with respect to multiplication and by the commutative property of addition of natural numbers,

$$(a \cdot 10^d \cdot 10^f + c \cdot 10^b \cdot 10^f) + e \cdot 10^{(b + d)})/10^{(b + d) + f} = (a \cdot 10^{d + f} + c \cdot 10^{b + f}) + e \cdot 10^{(b + d)})/10^{(b + d) + f}$$

$$(a \cdot 10^{(d + f)} + (c \cdot 10^f \cdot 10^b + e \cdot 10^d \cdot 10^b)/10^{b + (d + f)} = (a \cdot 10^{d + f} + (c \cdot 10^{b + f} + e \cdot 10^{b + d})/10^{b + (d + f)}$$

Finally, by the associative property of addition of integers and natural numbers,

$$(a \cdot 10^{d + f} + c \cdot 10^{b + f}) + e \cdot 10^{(b + d)})/10^{(b + d) + f} = (a \cdot 10^{d + f} + (c \cdot 10^{b + f} + e \cdot 10^{b + d})/10^{b + (d + f)}$$

Thus, $(p + q) + r = p + (q + r)$.

Proposition

(Commutativity of addition)

For every decimal fraction $p \in \mathbb{Z}[1/10]$ and $q \in \mathbb{Z}[1/10]$, $p + q = q + p$.

Proof

By definition of the set of decimal fractions, there exist numbers $a \in \mathbb{Z}$, $b \in \mathbb{N}$, $c \in \mathbb{Z}$, $d \in \mathbb{N}$ such that $a/10^b = p$ and $c/10^d = q$. Thus,

$$p + q = a/10^b + c/10^d = (a \cdot 10^d + c \cdot 10^b)/10^{(b + d)}$$

and

$$q + p = c/10^d + a/10^b = (c \cdot 10^b + a \cdot 10^d)/10^{(d + b)}$$

by definition of addition. By the commutativity of addition in the integers and the natural numbers,

$$(a \cdot 10^d + c \cdot 10^b)/10^{(b + d)} = (c \cdot 10^b + a \cdot 10^d)/10^{(d + b)}$$

Thus, $p + q = q + p$.

Definition

(Zero)

There exists an element $0 \in \mathbb{Z}[1/10]$ called zero and defined as $0 \coloneqq 0/10^0$.

Proposition

(Zero is a left identity of addition)

For every decimal fraction $p \in \mathbb{Z}[1/10]$, $0 + p = p$.

Proof

By definition of the set of decimal fractions, there exist numbers $a \in \mathbb{Z}$, $b \in \mathbb{N}$ such that $a/10^b = p$. Thus,

$$0 + p = 0/10^0 + a/10^b = (0 \cdot 10^b + a \cdot 10^0)/10^{(0 + b)}$$

by definition of addition. By the absorption property of $0$ with respect to multiplication in the integers,

$$(0 \cdot 10^b + a \cdot 10^0)/10^{(0 + b)} = (a \cdot 10^0)/10^{(0 + b)}$$

by the fact that exponentiation is an $\mathbb{N}$-action with respect to multiplication in the integers,

$$(a \cdot 10^0)/10^{(0 + b)} = (a \cdot 1)/10^{(0 + b)}$$

by the fact that 1 is a right identity element with respect to multiplication in the integers,

$$(a \cdot 1)/10^{(0 + b)} = a/10^{(0 + b)}$$

and by the fact that 0 is a left identity element with respect to addition in the natural numbers,

$$a/10^{(0 + b)} = a/10^{b}$$

Thus, $0 + p = p$.

Proposition

(Zero is a right identity of addition)

For every decimal fraction $p \in \mathbb{Z}[1/10]$, $p + 0 = p$.

Proof

By definition of the set of decimal fractions, there exist numbers $a \in \mathbb{Z}$, $b \in \mathbb{N}$ such that $a/10^b = p$. Thus,

$$p + 0 = a/10^b + 0/10^0 = (a \cdot 10^0 + 0 \cdot 10^b)/10^{(b + 0)}$$

by definition of addition. By the absorption property of $0$ with respect to multiplication in the integers,

$$(a \cdot 10^0 + 0 \cdot 10^b)/10^{(b + 0)} = (a \cdot 10^0)/10^{(b + 0)}$$

by the fact that exponentiation is an $\mathbb{N}$-action with respect to multiplication in the integers,

$$(a \cdot 10^0)/10^{(b + 0)} = (a \cdot 1)/10^{(b + 0)}$$

by the fact that 1 is a right identity element with respect to multiplication in the integers,

$$(a \cdot 1)/10^{(b + 0)} = a/10^{(b + 0)}$$

and by that 0 is a left identity element with respect to addition in the natural numbers,

$$a/10^{(b + 0)} = a/10^{b}$$

Thus, $p + 0 = p$.

Definition

(Negation)

There exists a function $-(-):\mathbb{Z}[1/10] \to \mathbb{Z}[1/10]$ called negation and defined as

$$-(a/10^b) \coloneqq (-a)/10^b$$

for $a \in \mathbb{Z}$, $b \in \mathbb{N}$.

Proposition

(Negation is a left inverse of addition)

For every decimal fraction $p \in \mathbb{Z}[1/10]$, $-p + p = 0$.

Proof

By definition of the set of decimal fractions, there exist numbers $a \in \mathbb{Z}$, $b \in \mathbb{N}$ such that $a/10^b = p$. Thus,

$$-p + p = (-a)/10^b + a/10^0 = ((-a) \cdot 10^b + a \cdot 10^b)/10^{(b + b)}$$

by definition of addition. By the fact that multiplication is a bilinear function in the integers,

$$((-a) \cdot 10^b + a \cdot 10^b)/10^{(b + b)} = (-(a \cdot 10^b) + a \cdot 10^b)/10^{(b + b)}$$

and by the fact that negation is a left inverse of addition in the integers,

$$(-(a \cdot 10^b) + a \cdot 10^b)/10^{(b + b)}/10^{(b + b)} = 0/10^{(b + b)}$$

and by definition of equality of decimal fractions, since

$$0 \cdot 10^{(b + b)} = 0 \cdot 10^0$$

this means that

$$0/10^{(b + b)} = 0/10^0$$

Thus, $-p + p = 0$.

Proposition

(Negation is a right inverse of addition)

For every decimal fraction $p \in \mathbb{Z}[1/10]$, $p + (-p) = 0$.

Proof

By definition of the set of decimal fractions, there exist numbers $a \in \mathbb{Z}$, $b \in \mathbb{N}$ such that $a/10^b = p$. Thus,

$$p + -p = a/10^b + (-a)/10^0 = (a \cdot 10^b + (-a) \cdot 10^b)/10^{(b + b)}$$

by definition of addition. By the fact that multiplication is a bilinear function in the integers,

$$(a \cdot 10^b + (-a) \cdot 10^b)/10^{(b + b)} = (a \cdot 10^b + -(a \cdot 10^b))/10^{(b + b)}$$

and by the fact that negation is a right inverse of addition in the integers,

$$(a \cdot 10^b + -(a \cdot 10^b))/10^{(b + b)} = 0/10^{(b + b)}$$

and by definition of equality of decimal fractions, since

$$0 \cdot 10^{(b + b)} = 0 \cdot 10^0$$

this means that

$$0/10^{(b + b)} = 0/10^0$$

Thus, $p + -p = 0$.

Definition

(Subtraction)

There exists a binary operation $(-)-(-):\mathbb{Z}[1/10] \times \mathbb{Z}[1/10] \to \mathbb{Z}[1/10]$ called subtraction defined as

$$a/10^b - c/10^d \coloneqq (a \cdot 10^d - c \cdot 10^b)/10^{(b + d)}$$

for $a \in \mathbb{Z}$, $b \in \mathbb{N}$, $c \in \mathbb{Z}$, $d \in \mathbb{N}$.

Proposition

(Abelian group)

The decimal fractions $(\mathbb{Z}[1/10], 0, +, -)$ form an abelian group.

Definition

(Multiplication)

There exists a binary operation $(-)\cdot (-):\mathbb{Z}[1/10] \times \mathbb{Z}[1/10] \to \mathbb{Z}[1/10]$ called multiplication defined as

$$a/10^b \cdot c/10^d \coloneqq (a \cdot c)/10^{(b + d)}$$

for $a \in \mathbb{Z}$, $b \in \mathbb{N}$, $c \in \mathbb{Z}$, $d \in \mathbb{N}$.

Proposition

(Left distributivity of multiplication over addition)

For every decimal fraction $p \in \mathbb{Z}[1/10]$, $q \in \mathbb{Z}[1/10]$, and $r \in \mathbb{Z}[1/10]$, $p \cdot (q + r) = p \cdot q + p \cdot r$.

Proof

By definition of the set of decimal fractions, there exist numbers $a \in \mathbb{Z}$, $b \in \mathbb{N}$, $c \in \mathbb{Z}$, $d \in \mathbb{N}$, $e \in \mathbb{Z}$, $f \in \mathbb{N}$ such that $a/10^b = p$, $c/10^d = q$, and $e/10^f = q$. Thus,

$$q + r = c/10^d + e/10^f = (c \cdot 10^f + e \cdot 10^d)/10^{(d + f)}$$

$$p \cdot (q + r) = a/10^b \cdot (c \cdot 10^f + e \cdot 10^d)/10^{(d + f)} = (a \cdot (c \cdot 10^f + e \cdot 10^d))/10^{b + (d + f)}$$

$$p \cdot q = a/10^b \cdot c/10^d = (a \cdot c)/10^{(b + d)}$$

$$p \cdot r = a/10^b \cdot e/10^f = (a \cdot e)/10^{(b + f)}$$

$$p \cdot q + p \cdot r = (a \cdot c)/10^{(b + d)} + (a \cdot e)/10^{(b + f)} = ((a \cdot c) \cdot 10^{(b + f)} + (a \cdot e) \cdot 10^{(b + d)})/10^{(b + d) + (b + f)}$$

by definition of addition and multiplication. By left distributivity of multiplication over addition of integers,

$$(a \cdot (c \cdot 10^f + e \cdot 10^d))/10^{b + (d + f)} = (a \cdot (c \cdot 10^f) + a \cdot (e \cdot 10^d))/10^{b + (d + f)}$$

and by associativity of multiplication of integers,

$$(a \cdot (c \cdot 10^f) + a \cdot (e \cdot 10^d))/10^{b + (d + f)} = ((a \cdot c) \cdot 10^f + (a \cdot e) \cdot 10^d)/10^{b + (d + f)}$$

Now we consider the following integer expressions: by the right distributive property of multiplication over addition in integers,

$$((a \cdot c) \cdot 10^f + (a \cdot e) \cdot 10^d) \cdot 10^{(b + d) + (b + f)} = ((a \cdot c) \cdot 10^f) \cdot 10^{(b + d) + (b + f)} + ((a \cdot e) \cdot 10^d) \cdot 10^{(b + d) + (b + f)}$$

$$((a \cdot c) \cdot 10^{(b + f)} + (a \cdot e) \cdot 10^{(b + d)}) \cdot 10^{b + (d + f)} = ((a \cdot c) \cdot 10^{(b + f)}) \cdot 10^{b + (d + f)} + ((a \cdot e) \cdot 10^{(b + d)}) \cdot 10^{b + (d + f)}$$

and by the associative property of multiplication in integers,

$$((a \cdot c) \cdot 10^f) \cdot 10^{(b + d) + (b + f)} + ((a \cdot e) \cdot 10^d) \cdot 10^{(b + d) + (b + f)} = (a \cdot c) \cdot (10^f \cdot 10^{(b + d) + (b + f)}) + (a \cdot e) \cdot (10^d \cdot 10^{(b + d) + (b + f)})$$

$$((a \cdot c) \cdot 10^{(b + f)}) \cdot 10^{b + (d + f)} + ((a \cdot e) \cdot 10^{(b + d)}) \cdot 10^{b + (d + f)} = (a \cdot c) \cdot (10^{(b + f)} \cdot 10^{b + (d + f)}) + (a \cdot e) \cdot (10^{(b + d)} \cdot 10^{b + (d + f)})$$

By the fact that exponentiation is an $\mathbb{N}$-action over multiplication on the integers,

$$(a \cdot c) \cdot (10^f \cdot 10^{(b + d) + (b + f)}) + (a \cdot e) \cdot (10^d \cdot 10^{(b + d) + (b + f)}) = (a \cdot c) \cdot 10^{f + ((b + d) + (b + f))} + (a \cdot e) \cdot (10^{d + ((b + d) + (b + f))}$$

$$(a \cdot c) \cdot (10^{(b + f)} \cdot 10^{b + (d + f)}) + (a \cdot e) \cdot (10^{(b + d)} \cdot 10^{b + (d + f)}) = (a \cdot c) \cdot 10^{(b + f) + (b + (d + f))} + (a \cdot e) \cdot 10^{(b + d) + (b + (d + f))}$$

and by the associativity and commutativity of addition on the natural numbers,

$$(a \cdot c) \cdot 10^{f + ((b + d) + (b + f))} + (a \cdot e) \cdot (10^{d + ((b + d) + (b + f))} = (a \cdot c) \cdot 10^{(f + (b + d)) + (b + f)} + (a \cdot e) \cdot (10^{d + ((b + f) + (b + d))}$$

$$(a \cdot c) \cdot 10^{(f + (b + d)) + (b + f)} + (a \cdot e) \cdot (10^{d + ((b + f) + (b + d))} = (a \cdot c) \cdot 10^{(b + f) + ((b + d) + f)} + (a \cdot e) \cdot (10^{(d + (b + f)) + (b + d)}$$

$$(a \cdot c) \cdot 10^{(b + f) + ((b + d) + f)} + (a \cdot e) \cdot (10^{(d + (b + f)) + (b + d)} = (a \cdot c) \cdot 10^{(b + f) + (b + (d + f))} + (a \cdot e) \cdot (10^{(b + d) + ((b + f) + d)}$$

$$(a \cdot c) \cdot 10^{(b + f) + (b + (d + f))} + (a \cdot e) \cdot (10^{(b + d) + ((b + f) + d)} = (a \cdot c) \cdot 10^{(b + f) + (b + (d + f))} + (a \cdot e) \cdot (10^{(b + d) + (b + (f + d))}$$

$$(a \cdot c) \cdot 10^{(b + f) + (b + (d + f))} + (a \cdot e) \cdot (10^{(b + d) + (b + (f + d))} = (a \cdot c) \cdot 10^{(b + f) + (b + (d + f))} + (a \cdot e) \cdot (10^{(b + d) + (b + (d + f))}$$

Thus,

$$((a \cdot c) \cdot 10^f + (a \cdot e) \cdot 10^d) \cdot 10^{(b + d) + (b + f)} = ((a \cdot c) \cdot 10^{(b + f)} + (a \cdot e) \cdot 10^{(b + d)}) \cdot 10^{b + (d + f)}$$

By definition of equality of decimal fractions, since

$$((a \cdot c) \cdot 10^f + (a \cdot e) \cdot 10^d) \cdot 10^{(b + d) + (b + f)} = ((a \cdot c) \cdot 10^{(b + f)} + (a \cdot e) \cdot 10^{(b + d)}) \cdot 10^{b + (d + f)}$$

then

$$((a \cdot c) \cdot 10^f) + (a \cdot e) \cdot 10^d))/10^{b + (d + f)} = ((a \cdot c) \cdot 10^{(b + f)} + (a \cdot e) \cdot 10^{(b + d)})/10^{(b + d) + (b + f)}$$

Thus, $p \cdot (q + r) = p \cdot q + p \cdot r$.

Proposition

(Right distributivity of multiplication over addition)

For every decimal fraction $p \in \mathbb{Z}[1/10]$, $q \in \mathbb{Z}[1/10]$, and $r \in \mathbb{Z}[1/10]$, $(p + q) \cdot r = p \cdot r + q \cdot r$.

Proof

By definition of the set of decimal fractions, there exist numbers $a \in \mathbb{Z}$, $b \in \mathbb{N}$, $c \in \mathbb{Z}$, $d \in \mathbb{N}$, $e \in \mathbb{Z}$, $f \in \mathbb{N}$ such that $a/10^b = p$, $c/10^d = q$, and $e/10^f = q$. Thus,

$$p + q = a/10^b + c/10^d = (a \cdot 10^d + c \cdot 10^b)/10^{(b + d)}$$

$$(p + q) \cdot r = (a \cdot 10^d + c \cdot 10^b)/10^{(b + d)} \cdot e/10^f = ((a \cdot 10^d + c \cdot 10^b) \cdot e)/10^{(b + d) + f)}$$

$$p \cdot r = a/10^b \cdot e/10^f = (a \cdot e)/10^{(b + f)}$$

$$q \cdot r = c/10^d \cdot c/10^d = (c \cdot e)/10^{(d + f)}$$

$$p \cdot r + q \cdot r = (a \cdot e)/10^{(b + f)} + (c \cdot e)/10^{(d + f)} = ((a \cdot e) \cdot 10^{(d + f)} + (c \cdot e) \cdot 10^{(b + f)})/10^{(b + f) + (d + f)}$$

by definition of addition and multiplication. By right distributivity of multiplication over addition of integers,

$$((a \cdot 10^d + c \cdot 10^b) \cdot e)/10^{(b + d) + f)} = ((a \cdot 10^d) \cdot e + (c \cdot 10^b) \cdot e)/10^{(b + d) + f)}$$

and by associativity of multiplication of integers,

$$((a \cdot 10^d) \cdot e + (c \cdot 10^b) \cdot e)/10^{(b + d) + f)} = (a \cdot (10^d \cdot e) + c \cdot (10^b \cdot e))/10^{(b + d) + f)}$$

and by commutativity of multiplication of integers,

$$(a \cdot (10^d \cdot e) + c \cdot (10^b \cdot e))/10^{(b + d) + f)} = (a \cdot (e \cdot 10^d) + c \cdot (e \cdot 10^b))/10^{(b + d) + f)}$$

and by associativity of multiplication of integers,

$$(a \cdot (e \cdot 10^d) + c \cdot (e \cdot 10^b))/10^{(b + d) + f)} = ((a \cdot e) \cdot 10^d + (c \cdot e) \cdot 10^b)/10^{(b + d) + f)}$$

Now we consider the following integer expressions: by the right distributive property of multiplication over addition in integers,

$$((a \cdot e) \cdot 10^d + (c \cdot e) \cdot 10^b) \cdot 10^{(b + f) + (d + f)} = ((a \cdot e) \cdot 10^d) \cdot 10^{(b + f) + (d + f)} + ((c \cdot e) \cdot 10^b) \cdot 10^{(b + f) + (d + f)}$$

$$((a \cdot e) \cdot 10^{(d + f)} + (c \cdot e) \cdot 10^{(b + f)}) \cdot 10^{(b + d) + f)} = ((a \cdot e) \cdot 10^{(d + f)}) \cdot 10^{(b + d) + f)} + ((c \cdot e) \cdot 10^{(b + f)}) \cdot 10^{(b + d) + f)}$$

and by the associative property of multiplication in integers,

$$((a \cdot e) \cdot 10^d) \cdot 10^{(b + f) + (d + f)} + ((c \cdot e) \cdot 10^b) \cdot 10^{(b + f) + (d + f)} = (a \cdot e) \cdot (10^d \cdot 10^{(b + f) + (d + f)}) + (c \cdot e) \cdot (10^b \cdot 10^{(b + f) + (d + f)})$$

$$((a \cdot e) \cdot 10^{(d + f)}) \cdot 10^{(b + d) + f)} + (c \cdot e) \cdot 10^{(b + f)}) \cdot 10^{(b + d) + f)} = (a \cdot e) \cdot (10^{(d + f)} \cdot 10^{(b + d) + f)}) + (c \cdot e) \cdot (10^{(b + f)} \cdot 10^{(b + d) + f)})$$

By the fact that exponentiation is an $\mathbb{N}$-action over multiplication on the integers,

$$(a \cdot e) \cdot (10^d \cdot 10^{(b + f) + (d + f)}) + (c \cdot e) \cdot (10^b \cdot 10^{(b + f) + (d + f)}) = (a \cdot e) \cdot 10^{d + ((b + f) + (d + f))} + (c \cdot e) \cdot (10^{b + ((b + f) + (d + f))}$$

$$(a \cdot e) \cdot (10^{(d + f)} \cdot 10^{(b + d) + f)}) + (c \cdot e) \cdot (10^{(b + f)} \cdot 10^{(b + d) + f)}) = (a \cdot e) \cdot 10^{(d + f) + ((b + d) + f)} + (c \cdot e) \cdot 10^{(b + f) + ((b + d) + f)}$$

and by the associativity and commutativity of addition on the natural numbers,

$$(a \cdot e) \cdot 10^{d + ((b + f) + (d + f))} + (c \cdot e) \cdot (10^{b + ((b + f) + (d + f))} = (a \cdot e) \cdot 10^{(d + (b + f)) + (d + f)} + (c \cdot e) \cdot (10^{b + ((d + f) + (b + f))}$$

$$(a \cdot e) \cdot 10^{(d + (b + f)) + (d + f)} + (c \cdot e) \cdot (10^{b + ((d + f) + (b + f))} = (a \cdot e) \cdot 10^{(d + f) + (d + (b + f))} + (c \cdot e) \cdot (10^{(b + (d + f)) + (b + f)}$$

$$(a \cdot e) \cdot 10^{(d + (b + f)) + (d + f)} + (c \cdot e) \cdot (10^{b + ((d + f) + (b + f))} = (a \cdot e) \cdot 10^{(d + f) + ((d + b) + f)} + (c \cdot e) \cdot (10^{(b + f) + (b + (d + f))}$$

$$(a \cdot e) \cdot 10^{(d + f) + ((d + b) + f)} + (c \cdot e) \cdot (10^{(b + f) + (b + (d + f))} = (a \cdot e) \cdot 10^{(d + f) + ((b +d) + f)} + (c \cdot e) \cdot (10^{(b + f) + ((b + d) + f)}$$

Thus,

$$((a \cdot e) \cdot 10^d + (c \cdot e) \cdot 10^b) \cdot 10^{(b + f) + (d + f)} = ((a \cdot e) \cdot 10^{(d + f)} + (c \cdot e) \cdot 10^{(b + f)}) \cdot 10^{(b + d) + f)}$$

By definition of equality of decimal fractions, since

$$((a \cdot e) \cdot 10^d + (c \cdot e) \cdot 10^b) \cdot 10^{(b + f) + (d + f)} = ((a \cdot e) \cdot 10^{(d + f)} + (c \cdot e) \cdot 10^{(b + f)}) \cdot 10^{(b + d) + f)}$$

then

$$((a \cdot e) \cdot 10^d + (c \cdot e) \cdot 10^b)/10^{(b + d) + f)} = ((a \cdot e) \cdot 10^{(d + f)} + (c \cdot e) \cdot 10^{(b + f)})/10^{(b + f) + (d + f)}$$

Thus, $(p + q) \cdot r = p \cdot r + q \cdot r$.

Proposition

(Associativity of multiplication)

For every decimal fraction $p \in \mathbb{Z}[1/10]$, $q \in \mathbb{Z}[1/10]$, and $r \in \mathbb{Z}[1/10]$, $(p \cdot q) \cdot r = p \cdot (q \cdot r)$.

Proof

By definition of the set of decimal fractions, there exist numbers $a \in \mathbb{Z}$, $b \in \mathbb{N}$, $c \in \mathbb{Z}$, $d \in \mathbb{N}$, $e \in \mathbb{Z}$, $f \in \mathbb{N}$ such that $a/10^b = p$, $c/10^d = q$, and $e/10^f = q$. Thus,

$$p \cdot q = a/10^b \cdot c/10^d = (a \cdot c)/10^{(b + d)}$$

$$(p \cdot q) \cdot r = (a \cdot c)/10^{(b + d)} + e/10^f = ((a \cdot c) \cdot e)/10^{(b + d) + f}$$

$$q \cdot r = c/10^d \cdot e/10^f = (c \cdot e)/10^{(d + f)}$$

$$p \cdot (q \cdot r) = a/10^b + (c \cdot e)/10^{(d + f)} = (a \cdot (c \cdot e))/10^{b + (d + f)}$$

by definition of addition. By the associative property of multiplication of integers and addition of natural numbers,

$$((a \cdot c) \cdot e)/10^{(b + d) + f} = (a \cdot (c \cdot e))/10^{b + (d + f)}$$

Thus, $(p \cdot q) \cdot r = p \cdot (q \cdot r)$.

Proposition

(Commutativity of multiplication)

For every decimal fraction $p \in \mathbb{Z}[1/10]$ and $q \in \mathbb{Z}[1/10]$, $p \cdot q = q \cdot p$.

Proof

By definition of the set of decimal fractions, there exist numbers $a \in \mathbb{Z}$, $b \in \mathbb{N}$, $c \in \mathbb{Z}$, $d \in \mathbb{N}$ such that $a/10^b = p$ and $c/10^d = q$. Thus,

$$p \cdot q = a/10^b \cdot c/10^d = (a \cdot c)/10^{(b + d)}$$

and

$$q \cdot p = c/10^d \cdot a/10^b = (c \cdot a)/10^{(d + b)}$$

by definition of addition. By the commutativity of multiplication in the integers and the commutativity of addition in the natural numbers,

$$(a \cdot c)/10^{(b + d)} = (c \cdot a)/10^{(d + b)}$$

Thus, $p \cdot q = q \cdot p$.

Definition

(One)

There exists an element $1 \in \mathbb{Z}[1/10]$ called one and defined as $1 \coloneqq 1/10^0$.

Proposition

(One is a left identity of multiplication)

For every decimal fraction $p \in \mathbb{Z}[1/10]$, $1 \cdot p = p$.

Proof

By definition of the set of decimal fractions, there exist numbers $a \in \mathbb{Z}$, $b \in \mathbb{N}$ such that $a/10^b = p$. Thus,

$$1 \cdot p = 1/10^0 \cdot a/10^b = (1 \cdot a)/10^{(0 + b)}$$

by the fact that 1 is a left identity element with respect to multiplication in the integers,

$$(1 \cdot a)/10^{(0 + b)} = a/10^{(0 + b)}$$

and by the fact that 0 is a left identity element with respect to addition in the natural numbers,

$$a/10^{(0 + b)} = a/10^{b}$$

Thus, $1 \cdot p = p$.

Proposition

(One is a right identity of multiplication)

For every decimal fraction $p \in \mathbb{Z}[1/10]$, $p \cdot 1 = p$.

Proof

By definition of the set of decimal fractions, there exist numbers $a \in \mathbb{Z}$, $b \in \mathbb{N}$ such that $a/10^b = p$. Thus,

$$p \cdot 1 = a/10^b \cdot 1/10^0 = (a \cdot 1)/10^{(b + 0)}$$

by the fact that 1 is a right identity element with respect to multiplication in the integers,

$$(a \cdot 1)/10^{(b + 0)} = a/10^{(b + 0)}$$

and by the fact that 0 is a right identity element with respect to addition in the natural numbers,

$$a/10^{(b + 0)} = a/10^{b}$$

Thus, $p \cdot 1 = p$.

Proposition

(Commutative ring)

The decimal fractions $(\mathbb{Z}[1/10], 0, +, -, 1, \cdot)$ form a commutative ring.

Definition

(Exponentiation)

There exists a binary operation $(-)^{(-)}:\mathbb{Z}[1/10] \times \mathbb{N} \to \mathbb{Z}[1/10]$ called exponentiation defined as

$$(a/10^b)^n \coloneqq (a^n)/10^{(b \cdot n)}$$

for $a \in \mathbb{Z}$, $b \in \mathbb{N}$, $n \in \mathbb{N}$.

Proposition

(10 is a unit)

There is an element $1/10 \in \mathbb{Z}[1/10]$ such that $1/10 \cdot 10 = 1$ and $10 \cdot 1/10 = 1$

Proposition

(Powers of 10 are isomorphic to the integers)

There is an injection $10^{(-)}: \mathbb{Z} \hookrightarrow \mathbb{Z}[1/10]$.

Order

Definition

(Positive numbers)

Given $a \in \mathbb{Z}$ and $b \in \mathbb{N}$, a decimal fraction $a/10^b \in \mathbb{Z}[1/10]$ is positive if $a \gt 0$: i.e. the predicate $\mathrm{isPositive}(a/10^b)$ is defined as

$$\mathrm{isPositive}(a/10^b) \coloneqq a \gt 0$$

Proposition

(Decidability of positive numbers)

Given $a \in \mathbb{Z}$, $b \in \mathbb{N}$, the predicate $\mathrm{isPositive}(a/10^b)$ is a decidable proposition.

Proof

By definition, $\mathrm{isPositive}(a/10^b)$ is the same as $a \gt 0$. Because the relation $a \gt 0$ is decidable for every integer $a \in \mathbb{Z}$, $\mathrm{isPositive}(a/10^b)$ is decidable for every integer $a \in \mathbb{Z}$ and natural number $b \in \mathbb{N}$.

Definition

(Less than)

For every decimal fraction $p \in \mathbb{Z}[1/10]$ and $q \in \mathbb{Z}[1/10]$, there is a proposition $p \lt q$ called less than and defined as

$$p \lt q \coloneqq \mathrm{isPositive}(q - p)$$

Proposition

(Decidability of less than)

Given $p \in \mathbb{Z}[1/10]$ and $q \in \mathbb{Z}[1/10]$, the predicate $p \lt q$ is a decidable proposition.

Proof

By definition, $p \lt q$ is the same as $\mathrm{isPositive}(q - p)$. Because the relation $\mathrm{isPositive}(p)$ is decidable for every decimal fraction $p \in \mathbb{Z}[1/10]$, $\mathrm{isPositive}(q - p)$ and $p \lt q$ is decidable for every decimal fraction $p \in \mathbb{Z}[1/10]$ and $q \in \mathbb{Z}[1/10]$.

Definition

(Negative numbers)

Given $a \in \mathbb{Z}$ and $b \in \mathbb{N}$, a decimal fraction $a/10^b \in \mathbb{Z}[1/10]$ is negative if $a \lt 0$; i.e. the predicate $\mathrm{isNegative}(a/10^b)$ is defined as

$$\mathrm{isNegative}(a/10^b) \coloneqq a \lt 0$$

Proposition

(Decidability of negative numbers)

Given $a \in \mathbb{Z}$, $b \in \mathbb{N}$, the predicate $\mathrm{isNegative}(a/10^b)$ is a decidable proposition.

Proof

By definition, $\mathrm{isNegative}(a/10^b)$ is the same as $a \lt 0$. Because the relation $a \lt 0$ is decidable for every integer $a \in \mathbb{Z}$, $\mathrm{isNegative}(a/10^b)$ is decidable for every integer $a \in \mathbb{Z}$ and natural number $b \in \mathbb{N}$

Definition

(Greater than)

For every decimal fraction $p \in \mathbb{Z}[1/10]$ and $q \in \mathbb{Z}[1/10]$, there is a proposition $p \gt q$ called greater than and defined as

$$p \lt q \coloneqq \mathrm{isNegative}(q - p)$$

Proposition

(Decidability of greater than)

Given $p \in \mathbb{Z}[1/10]$ and $q \in \mathbb{Z}[1/10]$, the predicate $p \gt q$ is a decidable proposition.

Proof

By definition, $p \gt q$ is the same as $\mathrm{isNegative}(q - p)$. Because the relation $\mathrm{isNegative}(p)$ is decidable for every decimal fraction $p \in \mathbb{Z}[1/10]$, $\mathrm{isNegative}(q - p)$ and $p \gt q$ is decidable for every decimal fraction $p \in \mathbb{Z}[1/10]$ and $q \in \mathbb{Z}[1/10]$.

Definition

(Non-negative numbers)

Given $a \in \mathbb{Z}$ and $b \in \mathbb{N}$, a decimal fraction $a/10^b \in \mathbb{Z}[1/10]$ is non-negative if $a \geq 0$; i.e. the predicate $\mathrm{isNonNegative}(a/10^b)$ is defined as

$$\mathrm{isNonNegative}(a/10^b) \coloneqq a \geq 0$$

Proposition

(Decidability of non-negative numbers)

Given $a \in \mathbb{Z}$, $b \in \mathbb{N}$, the predicate $\mathrm{isNonNegative}(a/10^b)$ is a decidable proposition.

Proof

By definition, $\mathrm{isNonNegative}(a/10^b)$ is the same as $a \geq 0$. Because the relation $a \geq 0$ is decidable for every integer $a \in \mathbb{Z}$, $\mathrm{isNonNegative}(a/10^b)$ is decidable for every integer $a \in \mathbb{Z}$ and natural number $b \in \mathbb{N}$

Definition

(Less than or equal to)

For every decimal fraction $p \in \mathbb{Z}[1/10]$ and $q \in \mathbb{Z}[1/10]$, there is a proposition $p \leq q$ called less than or equal to and defined as

$$p \leq q \coloneqq \mathrm{isNonNegative}(q - p)$$

Proposition

(Decidability of less than or equal to)

Given $p \in \mathbb{Z}[1/10]$ and $q \in \mathbb{Z}[1/10]$, the predicate $p \leq q$ is a decidable proposition.

Proof

By definition, $p \leq q$ is the same as $\mathrm{isNonNegative}(q - p)$. Because the relation $\mathrm{isNonNegative}(p)$ is decidable for every decimal fraction $p \in \mathbb{Z}[1/10]$, $\mathrm{isNonNegative}(q - p)$ and $p \leq q$ is decidable for every decimal fraction $p \in \mathbb{Z}[1/10]$ and $q \in \mathbb{Z}[1/10]$.

Definition

(Non-positive numbers)

Given $a \in \mathbb{Z}$ and $b \in \mathbb{N}$, a decimal fraction $a/10^b \in \mathbb{Z}[1/10]$ is non-positive if $a \leq 0$; i.e. the predicate $\mathrm{isNonPositive}(a/10^b)$ is defined as

$$\mathrm{isNonPositive}(a/10^b) \coloneqq a \leq 0$$

Proposition

(Decidability of non-positive numbers)

Given $a \in \mathbb{Z}$, $b \in \mathbb{N}$, the predicate $\mathrm{isNonPositive}(a/10^b)$ is a decidable proposition.

Proof

By definition, $\mathrm{isNonNegative}(a/10^b)$ is the same as $a \leq 0$. Because the relation $a \leq 0$ is decidable for every integer $a \in \mathbb{Z}$, $\mathrm{isNonPositive}(a/10^b)$ is decidable for every integer $a \in \mathbb{Z}$ and natural number $b \in \mathbb{N}$

Definition

(Greater than or equal to)

For every decimal fraction $p \in \mathbb{Z}[1/10]$ and $q \in \mathbb{Z}[1/10]$, there is a proposition $p \geq q$ called greater than or equal to and defined as

$$p \leq q \coloneqq \mathrm{isNonPositive}(q - p)$$

Proposition

(Decidability of greater than or equal to)

Given $p \in \mathbb{Z}[1/10]$ and $q \in \mathbb{Z}[1/10]$, the predicate $p \geq q$ is a decidable proposition.

Proof

By definition, $p \geq q$ is the same as $\mathrm{isNonPositive}(q - p)$. Because the relation $\mathrm{isNonPositive}(p)$ is decidable for every decimal fraction $p \in \mathbb{Z}[1/10]$, $\mathrm{isNonPositive}(q - p)$ and $p \geq q$ is decidable for every decimal fraction $p \in \mathbb{Z}[1/10]$ and $q \in \mathbb{Z}[1/10]$.

Definition

(Non-zero numbers)

Given $a \in \mathbb{Z}$ and $b \in \mathbb{N}$, a decimal fraction $a/10^b \in \mathbb{Z}[1/10]$ is non-zero if $a \neq 0$; i.e. the predicate $\mathrm{isNonZero}(a/10^b)$ is defined as

$$\mathrm{isNonZero}(a/10^b) \coloneqq a \neq 0$$

Proposition

(ordered integral domain)

The decimal fractions $(\mathbb{Z}[1/10], 0, +, -, 1, \cdot, \lt)$ form an ordered integral domain.

Definition

(Ramp)

There exists a function $\mathrm{ramp}:\mathbb{Z}[1/10] \to \mathbb{Z}[1/10]$ called ramp and defined as

$$\mathrm{ramp}(a/10^b) \coloneqq \mathrm{ramp}(a)/10^b$$

for $a \in \mathbb{Z}$, $b \in \mathbb{N}$.

Definition

(Minimum)

There exists a binary operation $\min:\mathbb{Z}[1/10] \times \mathbb{Z}[1/10] \to \mathbb{Z}[1/10]$ called minimum defined as

$$\min(p,q) \coloneqq p - \mathrm{ramp}(p - q)$$

for $p \in \mathbb{Z}[1/10]$, $q \in \mathbb{Z}[1/10]$.

Definition

(Maximum)

There exists a binary operation $\max:\mathbb{Z}[1/10] \times \mathbb{Z}[1/10] \to \mathbb{Z}[1/10]$ called maximum defined as

$$max(p, q) \coloneqq p + \mathrm{ramp}(q - p)$$

for $p \in \mathbb{Z}[1/10]$, $q \in \mathbb{Z}[1/10]$.

Definition

(Absolute value)

There exists a function $\vert(-)\vert:\mathbb{Z}[1/10] \to \mathbb{Z}[1/10]$ called absolute value and defined as

$$\vert p \vert \coloneqq max(p, -p)$$

for $p \in \mathbb{Z}[1/10]$.

Proposition

(total order)

The decimal fractions $(\mathbb{Z}[1/10], 0, +, -, 1, \cdot, \lt, \gt, \leq, \geq, \min, \max, \mathrm{ramp})$ are a totally ordered ring.

Scientific notation

Proposition

(scientific notation)

For all decimal fractions $p \in \mathbb{Z}[1/10]$, if $(0 \lt p)$, then there exists an integer $b \in \mathbb{Z}$ such that $1 \leq a \cdot 10^b$ and $a \cdot 10^b \lt 10$.

Algebraic closure

The algebraic closure $\overline{\mathbb{Z}[1/10]}$ of the rational numbers is called the field of algebraic numbers, and is thus isomorphic to \overline{\mathbb{Q}}, the algebraic closure of the rational numbers.

Topologies

There are several interesting topologies on $\mathbb{Z}[1/10]$ that make $\mathbb{Z}[1/10]$ into a topological group under addition, allowing us to define interesting fields by taking the completion with respect to this topology:

1. The discrete topology is the most obvious, which is already complete.

2. The absolute-value topology is defined by the metric $d(x,y) \coloneqq {|x - y|}$; the completion is the field of real numbers.

   (This topology is totally disconnected.)

3. For prime numbers $2$ and $5$, the $2$-adic topology and $5$-adic topology are defined by the ultrametric $d(x,y) \coloneqq 1/n$ where $n$ is the highest exponent on $2$ and $5$ respectively in the prime factorization of ${|x - y|}$; the completions of each metric are the fields of $2$-adic numbers and $5$-adic numbers respectively.

Approximate division

Let $(-)\div(-):\mathbb{Z} \times \mathbb{Z}_{\neq 0} \to \mathbb{Z}$ be a Euclidean division function on the integers. Then there is a function called approximate division

$$(-)/(-): \mathbb{Z} \times \mathbb{Z}_{\neq 0} \to (\mathbb{N} \to \mathbb{Z}[1/10])$$

to a sequence of decimal fractions called the infinite decimal representation of the rational number $a/b$

$$(a/b)_n \coloneqq (a \cdot 10^n \div b)/10^n$$

This sequence in general does not converge in the decimal rational numbers; the initial archimedean integral domain in which every infinite decimal representation of a rational number converges is the rational numbers.

Related entries

• dyadic rational number

• decimal interval coalgebra

References

• Wikipedia, Decimal