Description: Define the . (decimal point) operator. For example, ( 1 . 5 ) = ( 3 / 2 ) , and -u ( ; 3 2 . 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 . B ) is just as convenient.) (Contributed by David A. Wheeler, 15-May-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-dp | ⊢ . = ( 𝑥 ∈ ℕ0 , 𝑦 ∈ ℝ ↦ _ 𝑥 𝑦 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cdp | ⊢ . | |
| 1 | vx | ⊢ 𝑥 | |
| 2 | cn0 | ⊢ ℕ0 | |
| 3 | vy | ⊢ 𝑦 | |
| 4 | cr | ⊢ ℝ | |
| 5 | 1 | cv | ⊢ 𝑥 |
| 6 | 3 | cv | ⊢ 𝑦 |
| 7 | 5 6 | cdp2 | ⊢ _ 𝑥 𝑦 |
| 8 | 1 3 2 4 7 | cmpo | ⊢ ( 𝑥 ∈ ℕ0 , 𝑦 ∈ ℝ ↦ _ 𝑥 𝑦 ) |
| 9 | 0 8 | wceq | ⊢ . = ( 𝑥 ∈ ℕ0 , 𝑦 ∈ ℝ ↦ _ 𝑥 𝑦 ) |