**Description: **Define the (decimal
point) operator. For example,
, and
;__ ;;;; ;;;
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 ,
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.) |