Definition df-dp 31065

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 ℕ₀, 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

Step	Hyp	Ref	Expression
1		cdp 31064	. 2 class .
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cn0 12163	. . 3 class ℕ0
5		cr 10801	. . 3 class ℝ
6	2	cv 1538	. . . 4 class 𝑥
7	3	cv 1538	. . . 4 class 𝑦
8	6, 7	cdp2 31047	. . 3 class _𝑥𝑦
9	2, 3, 4, 5, 8	cmpo 7257	. 2 class (𝑥 ∈ ℕ0, 𝑦 ∈ ℝ ↦ _𝑥𝑦)
10	1, 9	wceq 1539	1 wff . = (𝑥 ∈ ℕ0, 𝑦 ∈ ℝ ↦ _𝑥𝑦)

This definition is referenced by:  dpval  31066