Definition df-dp 29596

Description: Define the period (decimal point) operator. For example, ( 1 period 5 ) = ( 3 / 2 ), and -u (; 3 2 period_ 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 period B ) is just as convenient.) (Contributed by David A. Wheeler, 15-May-2015.)

Assertion

Ref	Expression
df-dp	|- period = ( x e. NN0 , y e. RR |-> _ x y )

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-dp

Step	Hyp	Ref	Expression
1		cdp 29595	. 2 class period
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cn0 11292	. . 3 class NN0
5		cr 9935	. . 3 class RR
6	2	cv 1482	. . . 4 class x
7	3	cv 1482	. . . 4 class y
8	6, 7	cdp2 29577	. . 3 class _ x y
9	2, 3, 4, 5, 8	cmpt2 6652	. 2 class ( x e. NN0 , y e. RR |-> _ x y )
10	1, 9	wceq 1483	1 wff period = ( x e. NN0 , y e. RR |-> _ x y )

This definition is referenced by:  dpval  29597