nLab decimal rational number

Contents

Context

Arithmetic

Algebra

Contents

Idea

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

Definition

As a subset of the rational numbers

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

As the localisation of the integers at 10

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

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 AA with a function ι×A\iota \in \mathbb{Z} \times \mathbb{N} \to A, such that

a.b.c.d.(a10 d=c10 b)(ι(a,b)=ι(c,d))\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: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: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 AA and BB is a function f:ABf:A \to B such that

a.b.f(ι A(a,b))=ι B(a,b)\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 SwDFSwDF whose objects Ob(SwDF)Ob(SwDF) are sets with decimal fractions and whose morphisms Mor(A,B)Mor(A,B) for sets with decimal fractions AOb(SwDF)A \in Ob(SwDF), BOb(SwDF)B \in Ob(SwDF) are homomorphisms of sets with decimal fractions. The set of decimal fractions, denoted [1/10]\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 [1/10]\mathbb{Z}[1/10], could be defined as the higher inductive type generated by:

  • A function ()/10 ():×[1/10](-)/10^{(-)}:\mathbb{Z} \times \mathbb{N} \rightarrow \mathbb{Z}[1/10]. The integer a: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: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: a: b: c: d:(a10 d=c10 b)(a/10 b=c/10 d)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
    τ 0: a:[1/10] b:[1/10]isProp(a=b)\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[1/10]p \in \mathbb{Z}[1/10] and q[1/10]q \in \mathbb{Z}[1/10], p=qp = q or ¬(p=q)\neg(p = q).

Definition

(Inequality)

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

pq¬(p=q)p \neq q \coloneqq \neg(p = q)
Proposition

(Tight apartness relation)

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

Commutative ring structure

Definition

(Addition)

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

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

for aa \in \mathbb{Z}, bb \in \mathbb{N}, cc \in \mathbb{Z}, dd \in \mathbb{N}.

Proposition

(Associativity of addition)

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

Proof

By definition of the set of decimal fractions, there exist numbers aa \in \mathbb{Z}, bb \in \mathbb{N}, cc \in \mathbb{Z}, dd \in \mathbb{N}, ee \in \mathbb{Z}, ff \in \mathbb{N} such that a/10 b=pa/10^b = p, c/10 d=qc/10^d = q, and e/10 f=qe/10^f = q. Thus,

p+q=a/10 b+c/10 d=(a10 d+c10 b)/10 (b+d)p + q = a/10^b + c/10^d = (a \cdot 10^d + c \cdot 10^b)/10^{(b + d)}
(p+q)+r=(a10 d+c10 b)/10 (b+d)+e/10 f=((a10 d+c10 b)10 f+e10 (b+d))/10 (b+d)+f(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=(c10 f+e10 d)/10 (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+(c10 f+e10 d)/10 (d+f)=(a10 (d+f)+(c10 f+e10 d)10 b)/10 b+(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

((a10 d+c10 b)10 f+e10 (b+d))/10 (b+d)+f=(a10 d10 f+c10 b10 f)+e10 (b+d))/10 (b+d)+f((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}
(a10 (d+f)+(c10 f+e10 d)10 b)/10 b+(d+f)=(a10 (d+f)+(c10 f10 b+e10 d10 b)/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,

(a10 d10 f+c10 b10 f)+e10 (b+d))/10 (b+d)+f=(a10 d+f+c10 b+f)+e10 (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^{b + f}) + e \cdot 10^{(b + d)})/10^{(b + d) + f}
(a10 (d+f)+(c10 f10 b+e10 d10 b)/10 b+(d+f)=(a10 d+f+(c10 b+f+e10 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,

(a10 d+f+c10 b+f)+e10 (b+d))/10 (b+d)+f=(a10 d+f+(c10 b+f+e10 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^{b + f} + e \cdot 10^{b + d})/10^{b + (d + f)}

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

Proposition

(Commutativity of addition)

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

Proof

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

p+q=a/10 b+c/10 d=(a10 d+c10 b)/10 (b+d)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=(c10 b+a10 d)/10 (d+b)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,

(a10 d+c10 b)/10 (b+d)=(c10 b+a10 d)/10 (d+b)(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+pp + q = q + p.

Definition

(Zero)

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

Proposition

(Zero is a left identity of addition)

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

Proof

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

0+p=0/10 0+a/10 b=(010 b+a10 0)/10 (0+b)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 00 with respect to multiplication in the integers,

(010 b+a10 0)/10 (0+b)=(a10 0)/10 (0+b)(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,

(a10 0)/10 (0+b)=(a1)/10 (0+b)(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,

(a1)/10 (0+b)=a/10 (0+b)(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 ba/10^{(0 + b)} = a/10^{b}

Thus, 0+p=p0 + p = p.

Proposition

(Zero is a right identity of addition)

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

Proof

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

p+0=a/10 b+0/10 0=(a10 0+010 b)/10 (b+0)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 00 with respect to multiplication in the integers,

(a10 0+010 b)/10 (b+0)=(a10 0)/10 (b+0)(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,

(a10 0)/10 (b+0)=(a1)/10 (b+0)(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,

(a1)/10 (b+0)=a/10 (b+0)(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 ba/10^{(b + 0)} = a/10^{b}

Thus, p+0=pp + 0 = p.

Definition

(Negation)

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

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

for aa \in \mathbb{Z}, bb \in \mathbb{N}.

Proposition

(Negation is a left inverse of addition)

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

Proof

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

p+p=(a)/10 b+a/10 0=((a)10 b+a10 b)/10 (b+b)-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)10 b+a10 b)/10 (b+b)=((a10 b)+a10 b)/10 (b+b)((-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,

((a10 b)+a10 b)/10 (b+b)/10 (b+b)=0/10 (b+b)(-(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

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

this means that

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

Thus, p+p=0-p + p = 0.

Proposition

(Negation is a right inverse of addition)

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

Proof

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

p+p=a/10 b+(a)/10 0=(a10 b+(a)10 b)/10 (b+b)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,

(a10 b+(a)10 b)/10 (b+b)=(a10 b+(a10 b))/10 (b+b)(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,

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

and by definition of equality of decimal fractions, since

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

this means that

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

Thus, p+p=0p + -p = 0.

Definition

(Subtraction)

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

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

for aa \in \mathbb{Z}, bb \in \mathbb{N}, cc \in \mathbb{Z}, dd \in \mathbb{N}.

Proposition

(Abelian group)

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

Definition

(Multiplication)

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

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

for aa \in \mathbb{Z}, bb \in \mathbb{N}, cc \in \mathbb{Z}, dd \in \mathbb{N}.

Proposition

(Left distributivity of multiplication over addition)

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

Proof

By definition of the set of decimal fractions, there exist numbers aa \in \mathbb{Z}, bb \in \mathbb{N}, cc \in \mathbb{Z}, dd \in \mathbb{N}, ee \in \mathbb{Z}, ff \in \mathbb{N} such that a/10 b=pa/10^b = p, c/10 d=qc/10^d = q, and e/10 f=qe/10^f = q. Thus,

q+r=c/10 d+e/10 f=(c10 f+e10 d)/10 (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(c10 f+e10 d)/10 (d+f)=(a(c10 f+e10 d))/10 b+(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)}
pq=a/10 bc/10 d=(ac)/10 (b+d)p \cdot q = a/10^b \cdot c/10^d = (a \cdot c)/10^{(b + d)}
pr=a/10 be/10 f=(ae)/10 (b+f)p \cdot r = a/10^b \cdot e/10^f = (a \cdot e)/10^{(b + f)}
pq+pr=(ac)/10 (b+d)+(ae)/10 (b+f)=((ac)10 (b+f)+(ae)10 (b+d))/10 (b+d)+(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(c10 f+e10 d))/10 b+(d+f)=(a(c10 f)+a(e10 d))/10 b+(d+f)(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(c10 f)+a(e10 d))/10 b+(d+f)=((ac)10 f+(ae)10 d)/10 b+(d+f)(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,

((ac)10 f+(ae)10 d)10 (b+d)+(b+f)=((ac)10 f)10 (b+d)+(b+f)+((ae)10 d)10 (b+d)+(b+f)((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)}
((ac)10 (b+f)+(ae)10 (b+d))10 b+(d+f)=((ac)10 (b+f))10 b+(d+f)+((ae)10 (b+d))10 b+(d+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,

((ac)10 f)10 (b+d)+(b+f)+((ae)10 d)10 (b+d)+(b+f)=(ac)(10 f10 (b+d)+(b+f))+(ae)(10 d10 (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^f \cdot 10^{(b + d) + (b + f)}) + (a \cdot e) \cdot (10^d \cdot 10^{(b + d) + (b + f)})
((ac)10 (b+f))10 b+(d+f)+((ae)10 (b+d))10 b+(d+f)=(ac)(10 (b+f)10 b+(d+f))+(ae)(10 (b+d)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)} = (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,

(ac)(10 f10 (b+d)+(b+f))+(ae)(10 d10 (b+d)+(b+f))=(ac)10 f+((b+d)+(b+f))+(ae)(10 d+((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^{f + ((b + d) + (b + f))} + (a \cdot e) \cdot (10^{d + ((b + d) + (b + f))}
(ac)(10 (b+f)10 b+(d+f))+(ae)(10 (b+d)10 b+(d+f))=(ac)10 (b+f)+(b+(d+f))+(ae)10 (b+d)+(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)}) = (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,

(ac)10 f+((b+d)+(b+f))+(ae)(10 d+((b+d)+(b+f))=(ac)10 (f+(b+d))+(b+f)+(ae)(10 d+((b+f)+(b+d))(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))}
(ac)10 (f+(b+d))+(b+f)+(ae)(10 d+((b+f)+(b+d))=(ac)10 (b+f)+((b+d)+f)+(ae)(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)}
(ac)10 (b+f)+((b+d)+f)+(ae)(10 (d+(b+f))+(b+d)=(ac)10 (b+f)+(b+(d+f))+(ae)(10 (b+d)+((b+f)+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)}
(ac)10 (b+f)+(b+(d+f))+(ae)(10 (b+d)+((b+f)+d)=(ac)10 (b+f)+(b+(d+f))+(ae)(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))}
(ac)10 (b+f)+(b+(d+f))+(ae)(10 (b+d)+(b+(f+d))=(ac)10 (b+f)+(b+(d+f))+(ae)(10 (b+d)+(b+(d+f))(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,

((ac)10 f+(ae)10 d)10 (b+d)+(b+f)=((ac)10 (b+f)+(ae)10 (b+d))10 b+(d+f)((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

((ac)10 f+(ae)10 d)10 (b+d)+(b+f)=((ac)10 (b+f)+(ae)10 (b+d))10 b+(d+f)((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

((ac)10 f)+(ae)10 d))/10 b+(d+f)=((ac)10 (b+f)+(ae)10 (b+d))/10 (b+d)+(b+f)((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(q+r)=pq+prp \cdot (q + r) = p \cdot q + p \cdot r.

Proposition

(Right distributivity of multiplication over addition)

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

Proof

By definition of the set of decimal fractions, there exist numbers aa \in \mathbb{Z}, bb \in \mathbb{N}, cc \in \mathbb{Z}, dd \in \mathbb{N}, ee \in \mathbb{Z}, ff \in \mathbb{N} such that a/10 b=pa/10^b = p, c/10 d=qc/10^d = q, and e/10 f=qe/10^f = q. Thus,

p+q=a/10 b+c/10 d=(a10 d+c10 b)/10 (b+d)p + q = a/10^b + c/10^d = (a \cdot 10^d + c \cdot 10^b)/10^{(b + d)}
(p+q)r=(a10 d+c10 b)/10 (b+d)e/10 f=((a10 d+c10 b)e)/10 (b+d)+f)(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)}
pr=a/10 be/10 f=(ae)/10 (b+f)p \cdot r = a/10^b \cdot e/10^f = (a \cdot e)/10^{(b + f)}
qr=c/10 dc/10 d=(ce)/10 (d+f)q \cdot r = c/10^d \cdot c/10^d = (c \cdot e)/10^{(d + f)}
pr+qr=(ae)/10 (b+f)+(ce)/10 (d+f)=((ae)10 (d+f)+(ce)10 (b+f))/10 (b+f)+(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,

((a10 d+c10 b)e)/10 (b+d)+f)=((a10 d)e+(c10 b)e)/10 (b+d)+f)((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,

((a10 d)e+(c10 b)e)/10 (b+d)+f)=(a(10 de)+c(10 be))/10 (b+d)+f)((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(10 de)+c(10 be))/10 (b+d)+f)=(a(e10 d)+c(e10 b))/10 (b+d)+f)(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(e10 d)+c(e10 b))/10 (b+d)+f)=((ae)10 d+(ce)10 b)/10 (b+d)+f)(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,

((ae)10 d+(ce)10 b)10 (b+f)+(d+f)=((ae)10 d)10 (b+f)+(d+f)+((ce)10 b)10 (b+f)+(d+f)((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)}
((ae)10 (d+f)+(ce)10 (b+f))10 (b+d)+f)=((ae)10 (d+f))10 (b+d)+f)+((ce)10 (b+f))10 (b+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,

((ae)10 d)10 (b+f)+(d+f)+((ce)10 b)10 (b+f)+(d+f)=(ae)(10 d10 (b+f)+(d+f))+(ce)(10 b10 (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 \cdot 10^{(b + f) + (d + f)}) + (c \cdot e) \cdot (10^b \cdot 10^{(b + f) + (d + f)})
((ae)10 (d+f))10 (b+d)+f)+(ce)10 (b+f))10 (b+d)+f)=(ae)(10 (d+f)10 (b+d)+f))+(ce)(10 (b+f)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)} = (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,

(ae)(10 d10 (b+f)+(d+f))+(ce)(10 b10 (b+f)+(d+f))=(ae)10 d+((b+f)+(d+f))+(ce)(10 b+((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 + ((b + f) + (d + f))} + (c \cdot e) \cdot (10^{b + ((b + f) + (d + f))}
(ae)(10 (d+f)10 (b+d)+f))+(ce)(10 (b+f)10 (b+d)+f))=(ae)10 (d+f)+((b+d)+f)+(ce)10 (b+f)+((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)}) = (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,

(ae)10 d+((b+f)+(d+f))+(ce)(10 b+((b+f)+(d+f))=(ae)10 (d+(b+f))+(d+f)+(ce)(10 b+((d+f)+(b+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 + (b + f)) + (d + f)} + (c \cdot e) \cdot (10^{b + ((d + f) + (b + f))}
(ae)10 (d+(b+f))+(d+f)+(ce)(10 b+((d+f)+(b+f))=(ae)10 (d+f)+(d+(b+f))+(ce)(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)}
(ae)10 (d+(b+f))+(d+f)+(ce)(10 b+((d+f)+(b+f))=(ae)10 (d+f)+((d+b)+f)+(ce)(10 (b+f)+(b+(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 + f) + ((d + b) + f)} + (c \cdot e) \cdot (10^{(b + f) + (b + (d + f))}
(ae)10 (d+f)+((d+b)+f)+(ce)(10 (b+f)+(b+(d+f))=(ae)10 (d+f)+((b+d)+f)+(ce)(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,

((ae)10 d+(ce)10 b)10 (b+f)+(d+f)=((ae)10 (d+f)+(ce)10 (b+f))10 (b+d)+f)((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

((ae)10 d+(ce)10 b)10 (b+f)+(d+f)=((ae)10 (d+f)+(ce)10 (b+f))10 (b+d)+f)((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

((ae)10 d+(ce)10 b)/10 (b+d)+f)=((ae)10 (d+f)+(ce)10 (b+f))/10 (b+f)+(d+f)((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)r=pr+qr(p + q) \cdot r = p \cdot r + q \cdot r.

Proposition

(Associativity of multiplication)

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

Proof

By definition of the set of decimal fractions, there exist numbers aa \in \mathbb{Z}, bb \in \mathbb{N}, cc \in \mathbb{Z}, dd \in \mathbb{N}, ee \in \mathbb{Z}, ff \in \mathbb{N} such that a/10 b=pa/10^b = p, c/10 d=qc/10^d = q, and e/10 f=qe/10^f = q. Thus,

pq=a/10 bc/10 d=(ac)/10 (b+d)p \cdot q = a/10^b \cdot c/10^d = (a \cdot c)/10^{(b + d)}
(pq)r=(ac)/10 (b+d)+e/10 f=((ac)e)/10 (b+d)+f(p \cdot q) \cdot r = (a \cdot c)/10^{(b + d)} + e/10^f = ((a \cdot c) \cdot e)/10^{(b + d) + f}
qr=c/10 de/10 f=(ce)/10 (d+f)q \cdot r = c/10^d \cdot e/10^f = (c \cdot e)/10^{(d + f)}
p(qr)=a/10 b+(ce)/10 (d+f)=(a(ce))/10 b+(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,

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

Thus, (pq)r=p(qr)(p \cdot q) \cdot r = p \cdot (q \cdot r).

Proposition

(Commutativity of multiplication)

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

Proof

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

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

and

qp=c/10 da/10 b=(ca)/10 (d+b)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,

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

Thus, pq=qpp \cdot q = q \cdot p.

Definition

(One)

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

Proposition

(One is a left identity of multiplication)

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

Proof

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

1p=1/10 0a/10 b=(1a)/10 (0+b)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,

(1a)/10 (0+b)=a/10 (0+b)(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 ba/10^{(0 + b)} = a/10^{b}

Thus, 1p=p1 \cdot p = p.

Proposition

(One is a right identity of multiplication)

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

Proof

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

p1=a/10 b1/10 0=(a1)/10 (b+0)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,

(a1)/10 (b+0)=a/10 (b+0)(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 ba/10^{(b + 0)} = a/10^{b}

Thus, p1=pp \cdot 1 = p.

Proposition

(Commutative ring)

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

Definition

(Exponentiation)

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

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

for aa \in \mathbb{Z}, bb \in \mathbb{N}, nn \in \mathbb{N}.

Proposition

(10 is a unit)

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

Proposition

(Powers of 10 are isomorphic to the integers)

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

Order

Definition

(Positive numbers)

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

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

(Decidability of positive numbers)

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

Proof

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

Definition

(Less than)

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

p<qisPositive(qp)p \lt q \coloneqq \mathrm{isPositive}(q - p)
Proposition

(Decidability of less than)

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

Proof

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

Definition

(Negative numbers)

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

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

(Decidability of negative numbers)

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

Proof

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

Definition

(Greater than)

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

p<qisNegative(qp)p \lt q \coloneqq \mathrm{isNegative}(q - p)
Proposition

(Decidability of greater than)

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

Proof

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

Definition

(Non-negative numbers)

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

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

(Decidability of non-negative numbers)

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

Proof

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

Definition

(Less than or equal to)

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

pqisNonNegative(qp)p \leq q \coloneqq \mathrm{isNonNegative}(q - p)
Proposition

(Decidability of less than or equal to)

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

Proof

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

Definition

(Non-positive numbers)

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

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

(Decidability of non-positive numbers)

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

Proof

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

Definition

(Greater than or equal to)

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

pqisNonPositive(qp)p \leq q \coloneqq \mathrm{isNonPositive}(q - p)
Proposition

(Decidability of greater than or equal to)

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

Proof

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

Definition

(Non-zero numbers)

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

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

(ordered integral domain)

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

Definition

(Ramp)

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

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

for aa \in \mathbb{Z}, bb \in \mathbb{N}.

Definition

(Minimum)

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

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

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

Definition

(Maximum)

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

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

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

Definition

(Absolute value)

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

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

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

Proposition

(total order)

The decimal fractions ([1/10],0,+,,1,,<,>,,,min,max,ramp)(\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[1/10]p \in \mathbb{Z}[1/10], if (0<p)(0 \lt p), then there exists an integer bb \in \mathbb{Z} such that 1a10 b1 \leq a \cdot 10^b and a10 b<10a \cdot 10^b \lt 10.

Algebraic closure

The algebraic closure [1/10]¯\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 [1/10]\mathbb{Z}[1/10] that make [1/10]\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)|xy|d(x,y) \coloneqq {|x - y|}; the completion is the field of real numbers.

    (This topology is totally disconnected.)

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

Approximate division

Let ()÷():× 0(-)\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

()/():× 0([1/10])(-)/(-): \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/ba/b

(a/b) n(a10 n÷b)/10 n(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.

References

Last revised on June 15, 2022 at 14:49:12. See the history of this page for a list of all contributions to it.