 Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-dp Structured version   Visualization version   GIF version

Definition df-dp 29905
 Description: Define the . (decimal point) operator. For example, (1.5) = (3 / 2), and -(;32._7_18) = -(;;;;32718 / ;;;1000) 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 ℝ, not ℚ; this should simplify some proofs. The LHS is ℕ0, 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 . = (𝑥 ∈ ℕ0, 𝑦 ∈ ℝ ↦ 𝑥𝑦)
Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-dp
StepHypRef Expression
1 cdp 29904 . 2 class .
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cn0 11484 . . 3 class 0
5 cr 10127 . . 3 class
62cv 1631 . . . 4 class 𝑥
73cv 1631 . . . 4 class 𝑦
86, 7cdp2 29886 . . 3 class 𝑥𝑦
92, 3, 4, 5, 8cmpt2 6815 . 2 class (𝑥 ∈ ℕ0, 𝑦 ∈ ℝ ↦ 𝑥𝑦)
101, 9wceq 1632 1 wff . = (𝑥 ∈ ℕ0, 𝑦 ∈ ℝ ↦ 𝑥𝑦)
 Colors of variables: wff setvar class This definition is referenced by:  dpval  29906
 Copyright terms: Public domain W3C validator