Description: Define the . (decimal point) operator. For example, ( 1 . 5 ) = ( 3 / 2 ) , and -u ( ; 3 2 . 7 1 8 ) = -u ( ; ; ; ; 3 2 7 1 8 / ; ; ; 1 0 0 0 ) 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 RR , not QQ ; this should simplify some proofs. The LHS is NN0 , 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 -u ( A . B ) is just as convenient.) (Contributed by David A. Wheeler, 15-May-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-dp | |- . = ( x e. NN0 , y e. RR |-> _ x y ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cdp | |- . |
|
| 1 | vx | |- x |
|
| 2 | cn0 | |- NN0 |
|
| 3 | vy | |- y |
|
| 4 | cr | |- RR |
|
| 5 | 1 | cv | |- x |
| 6 | 3 | cv | |- y |
| 7 | 5 6 | cdp2 | |- _ x y |
| 8 | 1 3 2 4 7 | cmpo | |- ( x e. NN0 , y e. RR |-> _ x y ) |
| 9 | 0 8 | wceq | |- . = ( x e. NN0 , y e. RR |-> _ x y ) |