**Description: **Define the . (decimal point) operator. For example,
(1.5) = (3 / 2), and
-(;32._7_18) =
-(;;;;32718 / ;;;1000)
Unary minus, if applied, should normally be applied in front of the
parentheses.
Metamath intentionally does not have a built-in construct for numbers,
so it can show that numbers are something you can build based on set
theory. However, that means that Metamath has no built-in way to parse
and handle decimal numbers as traditionally written, e.g.,
"2.54". Here
we create a system for modeling traditional decimal point notation; it
is not syntactically identical, but it is sufficiently similar so it is
a reasonable model of decimal point notation. It should also serve as a
convenient way to write some fractional numbers.
The RHS is ℝ, not ℚ; this should simplify some proofs. The
LHS is ℕ_{0}, since that is what
is used in practice. The definition
intentionally does not allow negative numbers on the LHS; if it did,
nonzero fractions would produce the wrong results. (It would be
possible to define the decimal point to do this, but using it would be
more complicated, and the expression -(𝐴.𝐵) is just as
convenient.) (Contributed by David A. Wheeler,
15-May-2015.) |