Users' Mathboxes Mathbox for David A. Wheeler < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-dp Unicode version

Definition df-dp 28238
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 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  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
StepHypRef Expression
1 cdp 28236 . 2  class  period
2 vx . . 3  set  x
3 vy . . 3  set  y
4 cn0 9965 . . 3  class  NN0
5 cr 8736 . . 3  class  RR
62cv 1622 . . . 4  class  x
73cv 1622 . . . 4  class  y
86, 7cdp2 28235 . . 3  class _ x y
92, 3, 4, 5, 8cmpt2 5860 . 2  class  ( x  e.  NN0 ,  y  e.  RR  |-> _ x y )
101, 9wceq 1623 1  wff  period  =  ( x  e.  NN0 , 
y  e.  RR  |-> _ x y )
Colors of variables: wff set class
This definition is referenced by:  dpval  28240
  Copyright terms: Public domain W3C validator