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 handle
decimal numbers as traditionally written, e.g., "2.54", and
its parsing
system intentionally does not include the complexities necessary to
define such a parsing system. 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.) |