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	Could not format assertion : No typesetting found for |- . = ( x e. NN0 , y e. RR |-> _ x y ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdp	$$class.$$
1		vx	$$setvarx$$
2		cn0	$$class{\mathbb{N}}_0$$
3		vy	$$setvary$$
4		cr	$$classℝ$$
5	1	cv	$$setvarx$$
6	3	cv	$$setvary$$
7	5 6	cdp2	Could not format _ x y : No typesetting found for class _ x y with typecode class
8	1 3 2 4 7	cmpo	Could not format ( x e. NN0 , y e. RR |-> _ x y ) : No typesetting found for class ( x e. NN0 , y e. RR |-> _ x y ) with typecode class
9	0 8	wceq	Could not format . = ( x e. NN0 , y e. RR |-> _ x y ) : No typesetting found for wff . = ( x e. NN0 , y e. RR |-> _ x y ) with typecode wff