Metamath Proof Explorer


Definition df-dp

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 )

Detailed syntax breakdown

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 )