Users' Mathboxes 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 30492
Description: Define the . (decimal point) operator. For example, (1.5) = (3 / 2), and -(32.718) = -(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 30491 . 2 class .
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cn0 11885 . . 3 class 0
5 cr 10524 . . 3 class
62cv 1527 . . . 4 class 𝑥
73cv 1527 . . . 4 class 𝑦
86, 7cdp2 30474 . . 3 class 𝑥𝑦
92, 3, 4, 5, 8cmpo 7147 . 2 class (𝑥 ∈ ℕ0, 𝑦 ∈ ℝ ↦ 𝑥𝑦)
101, 9wceq 1528 1 wff . = (𝑥 ∈ ℕ0, 𝑦 ∈ ℝ ↦ 𝑥𝑦)
Colors of variables: wff setvar class
This definition is referenced by:  dpval  30493
  Copyright terms: Public domain W3C validator