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

Definition df-dp 28448
 Description: Define the (decimal point) operator. For example, , and ;__ ;;;; ;;; 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 , not ; this should simplify some proofs. The LHS is , 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 is just as convenient.) (Contributed by David A. Wheeler, 15-May-2015.)
Assertion
Ref Expression
df-dp _
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-dp
StepHypRef Expression
1 cdp 28446 . 2
2 vx . . 3
3 vy . . 3
4 cn0 10213 . . 3
5 cr 8981 . . 3
62cv 1651 . . . 4
73cv 1651 . . . 4
86, 7cdp2 28445 . . 3 _
92, 3, 4, 5, 8cmpt2 6075 . 2 _
101, 9wceq 1652 1 _
 Colors of variables: wff set class This definition is referenced by:  dpval  28450
 Copyright terms: Public domain W3C validator