Home Metamath Proof ExplorerTheorem List (p. 306 of 453) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

 Color key: Metamath Proof Explorer (1-28699) Hilbert Space Explorer (28700-30222) Users' Mathboxes (30223-45272)

Theorem List for Metamath Proof Explorer - 30501-30600   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremdfrp2 30501 Alternate definition of the positive real numbers. (Contributed by Thierry Arnoux, 4-May-2020.)
+ = (0(,)+∞)

Theoremxrofsup 30502 The supremum is preserved by extended addition set operation. (Provided minus infinity is not involved as it does not behave well with addition.) (Contributed by Thierry Arnoux, 20-Mar-2017.)
(𝜑𝑋 ⊆ ℝ*)    &   (𝜑𝑌 ⊆ ℝ*)    &   (𝜑 → sup(𝑋, ℝ*, < ) ≠ -∞)    &   (𝜑 → sup(𝑌, ℝ*, < ) ≠ -∞)    &   (𝜑𝑍 = ( +𝑒 “ (𝑋 × 𝑌)))       (𝜑 → sup(𝑍, ℝ*, < ) = (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))

Theoremsupxrnemnf 30503 The supremum of a nonempty set of extended reals which does not contain minus infinity is not minus infinity. (Contributed by Thierry Arnoux, 21-Mar-2017.)
((𝐴 ⊆ ℝ*𝐴 ≠ ∅ ∧ ¬ -∞ ∈ 𝐴) → sup(𝐴, ℝ*, < ) ≠ -∞)

20.3.5.4  Extended nonnegative integers - misc additions

Theoremxnn0gt0 30504 Nonzero extended nonnegative integers are strictly greater than zero. (Contributed by Thierry Arnoux, 30-Jul-2023.)
((𝑁 ∈ ℕ0*𝑁 ≠ 0) → 0 < 𝑁)

Theoremxnn01gt 30505 An extended nonnegative integer is neither 0 nor 1 if and only if it is greater than 1. (Contributed by Thierry Arnoux, 21-Nov-2023.)
(𝑁 ∈ ℕ0* → (¬ 𝑁 ∈ {0, 1} ↔ 1 < 𝑁))

Theoremnn0xmulclb 30506 Finite multiplication in the extended nonnegative integers. (Contributed by Thierry Arnoux, 30-Jul-2023.)
(((𝐴 ∈ ℕ0*𝐵 ∈ ℕ0*) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ((𝐴 ·e 𝐵) ∈ ℕ0 ↔ (𝐴 ∈ ℕ0𝐵 ∈ ℕ0)))

20.3.5.5  Real number intervals - misc additions

Theoremjoiniooico 30507 Disjoint joining an open interval with a closed-below, open-above interval to form a closed-below, open-above interval. (Contributed by Thierry Arnoux, 26-Sep-2017.)
(((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐵𝐵𝐶)) → (((𝐴(,)𝐵) ∩ (𝐵[,)𝐶)) = ∅ ∧ ((𝐴(,)𝐵) ∪ (𝐵[,)𝐶)) = (𝐴(,)𝐶)))

Theoremubico 30508 A right-open interval does not contain its right endpoint. (Contributed by Thierry Arnoux, 5-Apr-2017.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) → ¬ 𝐵 ∈ (𝐴[,)𝐵))

Theoremxeqlelt 30509 Equality in terms of 'less than or equal to', 'less than'. (Contributed by Thierry Arnoux, 5-Jul-2017.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴 < 𝐵)))

Theoremeliccelico 30510 Relate elementhood to a closed interval with elementhood to the same closed-below, open-above interval or to its upper bound. (Contributed by Thierry Arnoux, 3-Jul-2017.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ (𝐴[,)𝐵) ∨ 𝐶 = 𝐵)))

Theoremelicoelioo 30511 Relate elementhood to a closed-below, open-above interval with elementhood to the same open interval or to its lower bound. (Contributed by Thierry Arnoux, 6-Jul-2017.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵) → (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 = 𝐴𝐶 ∈ (𝐴(,)𝐵))))

Theoremiocinioc2 30512 Intersection between two open-below, closed-above intervals sharing the same upper bound. (Contributed by Thierry Arnoux, 7-Aug-2017.)
(((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴𝐵) → ((𝐴(,]𝐶) ∩ (𝐵(,]𝐶)) = (𝐵(,]𝐶))

Theoremxrdifh 30513 Class difference of a half-open interval in the extended reals. (Contributed by Thierry Arnoux, 1-Aug-2017.)
𝐴 ∈ ℝ*       (ℝ* ∖ (𝐴[,]+∞)) = (-∞[,)𝐴)

Theoremiocinif 30514 Relate intersection of two open-below, closed-above intervals with the same upper bound with a conditional construct. (Contributed by Thierry Arnoux, 7-Aug-2017.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) → ((𝐴(,]𝐶) ∩ (𝐵(,]𝐶)) = if(𝐴 < 𝐵, (𝐵(,]𝐶), (𝐴(,]𝐶)))

Theoremdifioo 30515 The difference between two open intervals sharing the same lower bound. (Contributed by Thierry Arnoux, 26-Sep-2017.)
(((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ 𝐴 < 𝐵) → ((𝐴(,)𝐶) ∖ (𝐴(,)𝐵)) = (𝐵[,)𝐶))

Theoremdifico 30516 The difference between two closed-below, open-above intervals sharing the same upper bound. (Contributed by Thierry Arnoux, 13-Oct-2017.)
(((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐴𝐵𝐵𝐶)) → ((𝐴[,)𝐶) ∖ (𝐵[,)𝐶)) = (𝐴[,)𝐵))

20.3.5.6  Finite intervals of integers - misc additions

Theoremuzssico 30517 Upper integer sets are a subset of the corresponding closed-below, open-above intervals. (Contributed by Thierry Arnoux, 29-Dec-2021.)
(𝑀 ∈ ℤ → (ℤ𝑀) ⊆ (𝑀[,)+∞))

Theoremfz2ssnn0 30518 A finite set of sequential integers that is a subset of 0. (Contributed by Thierry Arnoux, 8-Dec-2021.)
(𝑀 ∈ ℕ0 → (𝑀...𝑁) ⊆ ℕ0)

Theoremnndiffz1 30519 Upper set of the positive integers. (Contributed by Thierry Arnoux, 22-Aug-2017.)
(𝑁 ∈ ℕ0 → (ℕ ∖ (1...𝑁)) = (ℤ‘(𝑁 + 1)))

Theoremssnnssfz 30520* For any finite subset of , find a superset in the form of a set of sequential integers. (Contributed by Thierry Arnoux, 13-Sep-2017.)
(𝐴 ∈ (𝒫 ℕ ∩ Fin) → ∃𝑛 ∈ ℕ 𝐴 ⊆ (1...𝑛))

Theoremfzne1 30521 Elementhood in a finite set of sequential integers, except its lower bound. (Contributed by Thierry Arnoux, 1-Jan-2024.)
((𝐾 ∈ (𝑀...𝑁) ∧ 𝐾𝑀) → 𝐾 ∈ ((𝑀 + 1)...𝑁))

Theoremfzm1ne1 30522 Elementhood of an integer and its predecessor in finite intervals of integers. (Contributed by Thierry Arnoux, 1-Jan-2024.)
((𝐾 ∈ (𝑀...𝑁) ∧ 𝐾𝑀) → (𝐾 − 1) ∈ (𝑀...(𝑁 − 1)))

Theoremfzspl 30523 Split the last element of a finite set of sequential integers. More generic than fzsuc 12949. (Contributed by Thierry Arnoux, 7-Nov-2016.)
(𝑁 ∈ (ℤ𝑀) → (𝑀...𝑁) = ((𝑀...(𝑁 − 1)) ∪ {𝑁}))

Theoremfzdif2 30524 Split the last element of a finite set of sequential integers. More generic than fzsuc 12949. (Contributed by Thierry Arnoux, 22-Aug-2020.)
(𝑁 ∈ (ℤ𝑀) → ((𝑀...𝑁) ∖ {𝑁}) = (𝑀...(𝑁 − 1)))

Theoremfzodif2 30525 Split the last element of a half-open range of sequential integers. (Contributed by Thierry Arnoux, 5-Dec-2021.)
(𝑁 ∈ (ℤ𝑀) → ((𝑀..^(𝑁 + 1)) ∖ {𝑁}) = (𝑀..^𝑁))

Theoremfzodif1 30526 Set difference of two half-open range of sequential integers sharing the same starting value. (Contributed by Thierry Arnoux, 2-Oct-2023.)
(𝐾 ∈ (𝑀...𝑁) → ((𝑀..^𝑁) ∖ (𝑀..^𝐾)) = (𝐾..^𝑁))

Theoremfzsplit3 30527 Split a finite interval of integers into two parts. (Contributed by Thierry Arnoux, 2-May-2017.)
(𝐾 ∈ (𝑀...𝑁) → (𝑀...𝑁) = ((𝑀...(𝐾 − 1)) ∪ (𝐾...𝑁)))

Theorembcm1n 30528 The proportion of one binomial coefficient to another with 𝑁 decreased by 1. (Contributed by Thierry Arnoux, 9-Nov-2016.)
((𝐾 ∈ (0...(𝑁 − 1)) ∧ 𝑁 ∈ ℕ) → (((𝑁 − 1)C𝐾) / (𝑁C𝐾)) = ((𝑁𝐾) / 𝑁))

20.3.5.7  Half-open integer ranges - misc additions

Theoremiundisjfi 30529* Rewrite a countable union as a disjoint union, finite version. Cf. iundisj 24150. (Contributed by Thierry Arnoux, 15-Feb-2017.)
𝑛𝐵    &   (𝑛 = 𝑘𝐴 = 𝐵)        𝑛 ∈ (1..^𝑁)𝐴 = 𝑛 ∈ (1..^𝑁)(𝐴 𝑘 ∈ (1..^𝑛)𝐵)

Theoremiundisj2fi 30530* A disjoint union is disjoint, finite version. Cf. iundisj2 24151. (Contributed by Thierry Arnoux, 16-Feb-2017.)
𝑛𝐵    &   (𝑛 = 𝑘𝐴 = 𝐵)       Disj 𝑛 ∈ (1..^𝑁)(𝐴 𝑘 ∈ (1..^𝑛)𝐵)

Theoremiundisjcnt 30531* Rewrite a countable union as a disjoint union. (Contributed by Thierry Arnoux, 16-Feb-2017.)
𝑛𝐵    &   (𝑛 = 𝑘𝐴 = 𝐵)    &   (𝜑 → (𝑁 = ℕ ∨ 𝑁 = (1..^𝑀)))       (𝜑 𝑛𝑁 𝐴 = 𝑛𝑁 (𝐴 𝑘 ∈ (1..^𝑛)𝐵))

Theoremiundisj2cnt 30532* A countable disjoint union is disjoint. Cf. iundisj2 24151. (Contributed by Thierry Arnoux, 16-Feb-2017.)
𝑛𝐵    &   (𝑛 = 𝑘𝐴 = 𝐵)    &   (𝜑 → (𝑁 = ℕ ∨ 𝑁 = (1..^𝑀)))       (𝜑Disj 𝑛𝑁 (𝐴 𝑘 ∈ (1..^𝑛)𝐵))

Theoremfzone1 30533 Elementhood in a half-open interval, except its lower bound. (Contributed by Thierry Arnoux, 1-Jan-2024.)
((𝐾 ∈ (𝑀..^𝑁) ∧ 𝐾𝑀) → 𝐾 ∈ ((𝑀 + 1)..^𝑁))

Theoremfzom1ne1 30534 Elementhood in a half-open interval, except the lower bound, shifted by one. (Contributed by Thierry Arnoux, 1-Jan-2024.)
((𝐾 ∈ (𝑀..^𝑁) ∧ 𝐾𝑀) → (𝐾 − 1) ∈ (𝑀..^(𝑁 − 1)))

Theoremf1ocnt 30535* Given a countable set 𝐴, number its elements by providing a one-to-one mapping either with or an integer range starting from 1. The domain of the function can then be used with iundisjcnt 30531 or iundisj2cnt 30532. (Contributed by Thierry Arnoux, 25-Jul-2020.)
(𝐴 ≼ ω → ∃𝑓(𝑓:dom 𝑓1-1-onto𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((♯‘𝐴) + 1)))))

Theoremfz1nnct 30536 NN and integer ranges starting from 1 are countable. (Contributed by Thierry Arnoux, 25-Jul-2020.)
((𝐴 = ℕ ∨ 𝐴 = (1..^𝑀)) → 𝐴 ≼ ω)

Theoremfz1nntr 30537 NN and integer ranges starting from 1 are a transitive family of set. (Contributed by Thierry Arnoux, 25-Jul-2020.)
(((𝐴 = ℕ ∨ 𝐴 = (1..^𝑀)) ∧ 𝑁𝐴) → (1..^𝑁) ⊆ 𝐴)

20.3.5.8  The ` # ` (set size) function - misc additions

Theoremhashunif 30538* The cardinality of a disjoint finite union of finite sets. Cf. hashuni 15172. (Contributed by Thierry Arnoux, 17-Feb-2017.)
𝑥𝜑    &   (𝜑𝐴 ∈ Fin)    &   (𝜑𝐴 ⊆ Fin)    &   (𝜑Disj 𝑥𝐴 𝑥)       (𝜑 → (♯‘ 𝐴) = Σ𝑥𝐴 (♯‘𝑥))

Theoremhashxpe 30539 The size of the Cartesian product of two finite sets is the product of their sizes. This is a version of hashxp 13791 valid for infinite sets, which uses extended real numbers. (Contributed by Thierry Arnoux, 27-May-2023.)
((𝐴𝑉𝐵𝑊) → (♯‘(𝐴 × 𝐵)) = ((♯‘𝐴) ·e (♯‘𝐵)))

Theoremhashgt1 30540 Restate "set contains at least two elements" in terms of elementhood. (Contributed by Thierry Arnoux, 21-Nov-2023.)
(𝐴𝑉 → (¬ 𝐴 ∈ (♯ “ {0, 1}) ↔ 1 < (♯‘𝐴)))

20.3.5.9  The greatest common divisor operator - misc. add

Theoremdvdszzq 30541 Divisibility for an integer quotient. (Contributed by Thierry Arnoux, 17-Sep-2023.)
𝑁 = (𝐴 / 𝐵)    &   (𝜑𝑃 ∈ ℙ)    &   (𝜑𝑁 ∈ ℤ)    &   (𝜑𝐵 ∈ ℤ)    &   (𝜑𝐵 ≠ 0)    &   (𝜑𝑃𝐴)    &   (𝜑 → ¬ 𝑃𝐵)       (𝜑𝑃𝑁)

Theoremprmdvdsbc 30542 Condition for a prime number to divide a binomial coefficient. (Contributed by Thierry Arnoux, 17-Sep-2023.)
((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑃 ∥ (𝑃C𝑁))

Theoremnumdenneg 30543 Numerator and denominator of the negative. (Contributed by Thierry Arnoux, 27-Oct-2017.)
(𝑄 ∈ ℚ → ((numer‘-𝑄) = -(numer‘𝑄) ∧ (denom‘-𝑄) = (denom‘𝑄)))

Theoremdivnumden2 30544 Calculate the reduced form of a quotient using gcd. This version extends divnumden 16077 for the negative integers. (Contributed by Thierry Arnoux, 25-Oct-2017.)
((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → ((numer‘(𝐴 / 𝐵)) = -(𝐴 / (𝐴 gcd 𝐵)) ∧ (denom‘(𝐴 / 𝐵)) = -(𝐵 / (𝐴 gcd 𝐵))))

20.3.5.10  Integers

Theoremnnindf 30545* Principle of Mathematical Induction, using a bound-variable hypothesis instead of distinct variables. (Contributed by Thierry Arnoux, 6-May-2018.)
𝑦𝜑    &   (𝑥 = 1 → (𝜑𝜓))    &   (𝑥 = 𝑦 → (𝜑𝜒))    &   (𝑥 = (𝑦 + 1) → (𝜑𝜃))    &   (𝑥 = 𝐴 → (𝜑𝜏))    &   𝜓    &   (𝑦 ∈ ℕ → (𝜒𝜃))       (𝐴 ∈ ℕ → 𝜏)

Theoremnn0min 30546* Extracting the minimum positive integer for which a property 𝜒 does not hold. This uses substitutions similar to nn0ind 12065. (Contributed by Thierry Arnoux, 6-May-2018.)
(𝑛 = 0 → (𝜓𝜒))    &   (𝑛 = 𝑚 → (𝜓𝜃))    &   (𝑛 = (𝑚 + 1) → (𝜓𝜏))    &   (𝜑 → ¬ 𝜒)    &   (𝜑 → ∃𝑛 ∈ ℕ 𝜓)       (𝜑 → ∃𝑚 ∈ ℕ0𝜃𝜏))

Theoremsubne0nn 30547 A nonnegative difference is positive if the two numbers are not equal. (Contributed by Thierry Arnoux, 17-Dec-2023.)
(𝜑𝑀 ∈ ℂ)    &   (𝜑𝑁 ∈ ℂ)    &   (𝜑 → (𝑀𝑁) ∈ ℕ0)    &   (𝜑𝑀𝑁)       (𝜑 → (𝑀𝑁) ∈ ℕ)

Theoremltesubnnd 30548 Subtracting an integer number from another number decreases it. See ltsubrpd 12451. (Contributed by Thierry Arnoux, 18-Apr-2017.)
(𝜑𝑀 ∈ ℤ)    &   (𝜑𝑁 ∈ ℕ)       (𝜑 → ((𝑀 + 1) − 𝑁) ≤ 𝑀)

Theoremfprodeq02 30549* If one of the factors is zero the product is zero. (Contributed by Thierry Arnoux, 11-Dec-2021.)
(𝑘 = 𝐾𝐵 = 𝐶)    &   (𝜑𝐴 ∈ Fin)    &   ((𝜑𝑘𝐴) → 𝐵 ∈ ℂ)    &   (𝜑𝐾𝐴)    &   (𝜑𝐶 = 0)       (𝜑 → ∏𝑘𝐴 𝐵 = 0)

Theorempr01ssre 30550 The range of the indicator function is a subset of . (Contributed by Thierry Arnoux, 14-Aug-2017.)
{0, 1} ⊆ ℝ

Theoremfprodex01 30551* A product of factors equal to zero or one is zero exactly when one of the factors is zero. (Contributed by Thierry Arnoux, 11-Dec-2021.)
(𝑘 = 𝑙𝐵 = 𝐶)    &   (𝜑𝐴 ∈ Fin)    &   ((𝜑𝑘𝐴) → 𝐵 ∈ {0, 1})       (𝜑 → ∏𝑘𝐴 𝐵 = if(∀𝑙𝐴 𝐶 = 1, 1, 0))

Theoremprodpr 30552* A product over a pair is the product of the elements. (Contributed by Thierry Arnoux, 1-Jan-2022.)
(𝑘 = 𝐴𝐷 = 𝐸)    &   (𝑘 = 𝐵𝐷 = 𝐹)    &   (𝜑𝐴𝑉)    &   (𝜑𝐵𝑊)    &   (𝜑𝐸 ∈ ℂ)    &   (𝜑𝐹 ∈ ℂ)    &   (𝜑𝐴𝐵)       (𝜑 → ∏𝑘 ∈ {𝐴, 𝐵}𝐷 = (𝐸 · 𝐹))

Theoremprodtp 30553* A product over a triple is the product of the elements. (Contributed by Thierry Arnoux, 1-Jan-2022.)
(𝑘 = 𝐴𝐷 = 𝐸)    &   (𝑘 = 𝐵𝐷 = 𝐹)    &   (𝜑𝐴𝑉)    &   (𝜑𝐵𝑊)    &   (𝜑𝐸 ∈ ℂ)    &   (𝜑𝐹 ∈ ℂ)    &   (𝜑𝐴𝐵)    &   (𝑘 = 𝐶𝐷 = 𝐺)    &   (𝜑𝐶𝑋)    &   (𝜑𝐺 ∈ ℂ)    &   (𝜑𝐴𝐶)    &   (𝜑𝐵𝐶)       (𝜑 → ∏𝑘 ∈ {𝐴, 𝐵, 𝐶}𝐷 = ((𝐸 · 𝐹) · 𝐺))

Theoremfsumub 30554* An upper bound for a term of a positive finite sum. (Contributed by Thierry Arnoux, 27-Dec-2021.)
(𝑘 = 𝐾𝐵 = 𝐷)    &   (𝜑𝐴 ∈ Fin)    &   (𝜑 → Σ𝑘𝐴 𝐵 = 𝐶)    &   ((𝜑𝑘𝐴) → 𝐵 ∈ ℝ+)    &   (𝜑𝐾𝐴)       (𝜑𝐷𝐶)

Theoremfsumiunle 30555* Upper bound for a sum of nonnegative terms over an indexed union. The inequality may be strict if the indexed union is non-disjoint, since in the right hand side, a summand may be counted several times. (Contributed by Thierry Arnoux, 1-Jan-2021.)
(𝜑𝐴 ∈ Fin)    &   ((𝜑𝑥𝐴) → 𝐵 ∈ Fin)    &   (((𝜑𝑥𝐴) ∧ 𝑘𝐵) → 𝐶 ∈ ℝ)    &   (((𝜑𝑥𝐴) ∧ 𝑘𝐵) → 0 ≤ 𝐶)       (𝜑 → Σ𝑘 𝑥𝐴 𝐵𝐶 ≤ Σ𝑥𝐴 Σ𝑘𝐵 𝐶)

20.3.5.11  Decimal numbers

Theoremdfdec100 30556 Split the hundreds from a decimal value. (Contributed by Thierry Arnoux, 25-Dec-2021.)
𝐴 ∈ ℕ0    &   𝐵 ∈ ℕ0    &   𝐶 ∈ ℝ       𝐴𝐵𝐶 = ((100 · 𝐴) + 𝐵𝐶)

20.3.6  Decimal expansion

Define a decimal expansion constructor. The decimal expansions built with this constructor are not meant to be used alone outside of this chapter. Rather, they are meant to be used exclusively as part of a decimal number with a decimal fraction, for example (3.14159).

That decimal point operator is defined in the next section. The bulk of these constructions have originally been proposed by David A. Wheeler on 12-May-2015, and discussed with Mario Carneiro in this thread: https://groups.google.com/g/metamath/c/2AW7T3d2YiQ.

Syntaxcdp2 30557 Constant used for decimal fraction constructor. See df-dp2 30558.
class 𝐴𝐵

Definitiondf-dp2 30558 Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12087. (Contributed by David A. Wheeler, 15-May-2015.) (Revised by AV, 9-Sep-2021.)
𝐴𝐵 = (𝐴 + (𝐵 / 10))

Theoremdp2eq1 30559 Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.)
(𝐴 = 𝐵𝐴𝐶 = 𝐵𝐶)

Theoremdp2eq2 30560 Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.)
(𝐴 = 𝐵𝐶𝐴 = 𝐶𝐵)

Theoremdp2eq1i 30561 Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.)
𝐴 = 𝐵       𝐴𝐶 = 𝐵𝐶

Theoremdp2eq2i 30562 Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.)
𝐴 = 𝐵       𝐶𝐴 = 𝐶𝐵

Theoremdp2eq12i 30563 Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.)
𝐴 = 𝐵    &   𝐶 = 𝐷       𝐴𝐶 = 𝐵𝐷

Theoremdp20u 30564 Add a zero in the tenths (lower) place. (Contributed by Thierry Arnoux, 16-Dec-2021.)
𝐴 ∈ ℕ0       𝐴0 = 𝐴

Theoremdp20h 30565 Add a zero in the unit places. (Contributed by Thierry Arnoux, 16-Dec-2021.)
𝐴 ∈ ℝ+       0𝐴 = (𝐴 / 10)

Theoremdp2cl 30566 Closure for the decimal fraction constructor if both values are reals. (Contributed by David A. Wheeler, 15-May-2015.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴𝐵 ∈ ℝ)

Theoremdp2clq 30567 Closure for a decimal fraction. (Contributed by Thierry Arnoux, 16-Dec-2021.)
𝐴 ∈ ℕ0    &   𝐵 ∈ ℚ       𝐴𝐵 ∈ ℚ

Theoremrpdp2cl 30568 Closure for a decimal fraction in the positive real numbers. (Contributed by Thierry Arnoux, 16-Dec-2021.)
𝐴 ∈ ℕ0    &   𝐵 ∈ ℝ+       𝐴𝐵 ∈ ℝ+

Theoremrpdp2cl2 30569 Closure for a decimal fraction with no decimal expansion in the positive real numbers. (Contributed by Thierry Arnoux, 25-Dec-2021.)
𝐴 ∈ ℕ       𝐴0 ∈ ℝ+

Theoremdp2lt10 30570 Decimal fraction builds real numbers less than 10. (Contributed by Thierry Arnoux, 16-Dec-2021.)
𝐴 ∈ ℕ0    &   𝐵 ∈ ℝ+    &   𝐴 < 10    &   𝐵 < 10       𝐴𝐵 < 10

Theoremdp2lt 30571 Comparing two decimal fractions (equal unit places). (Contributed by Thierry Arnoux, 16-Dec-2021.)
𝐴 ∈ ℕ0    &   𝐵 ∈ ℝ+    &   𝐶 ∈ ℝ+    &   𝐵 < 𝐶       𝐴𝐵 < 𝐴𝐶

Theoremdp2ltsuc 30572 Comparing a decimal fraction with the next integer. (Contributed by Thierry Arnoux, 25-Dec-2021.)
𝐴 ∈ ℕ0    &   𝐵 ∈ ℝ+    &   𝐵 < 10    &   (𝐴 + 1) = 𝐶       𝐴𝐵 < 𝐶

Theoremdp2ltc 30573 Comparing two decimal expansions (unequal higher places). (Contributed by Thierry Arnoux, 16-Dec-2021.)
𝐴 ∈ ℕ0    &   𝐵 ∈ ℝ+    &   𝐶 ∈ ℕ0    &   𝐷 ∈ ℝ+    &   𝐵 < 10    &   𝐴 < 𝐶       𝐴𝐵 < 𝐶𝐷

20.3.6.1  Decimal point

Define the decimal point operator and the decimal fraction constructor. This can model traditional decimal point notation, and serve as a convenient way to write some fractional numbers. See df-dp 30575 and df-dp2 30558 for more information; dpval2 30579 and dpfrac1 30578 provide a more convenient way to obtain a value. This is intentionally similar to df-dec 12087.

Syntaxcdp 30574 Decimal point operator. See df-dp 30575.
class .

Definitiondf-dp 30575* 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.)

. = (𝑥 ∈ ℕ0, 𝑦 ∈ ℝ ↦ 𝑥𝑦)

Theoremdpval 30576 Define the value of the decimal point operator. See df-dp 30575. (Contributed by David A. Wheeler, 15-May-2015.)
((𝐴 ∈ ℕ0𝐵 ∈ ℝ) → (𝐴.𝐵) = 𝐴𝐵)

Theoremdpcl 30577 Prove that the closure of the decimal point is as we have defined it. See df-dp 30575. (Contributed by David A. Wheeler, 15-May-2015.)
((𝐴 ∈ ℕ0𝐵 ∈ ℝ) → (𝐴.𝐵) ∈ ℝ)

Theoremdpfrac1 30578 Prove a simple equivalence involving the decimal point. See df-dp 30575 and dpcl 30577. (Contributed by David A. Wheeler, 15-May-2015.) (Revised by AV, 9-Sep-2021.)
((𝐴 ∈ ℕ0𝐵 ∈ ℝ) → (𝐴.𝐵) = (𝐴𝐵 / 10))

Theoremdpval2 30579 Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021.)
𝐴 ∈ ℕ0    &   𝐵 ∈ ℝ       (𝐴.𝐵) = (𝐴 + (𝐵 / 10))

Theoremdpval3 30580 Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021.)
𝐴 ∈ ℕ0    &   𝐵 ∈ ℝ       (𝐴.𝐵) = 𝐴𝐵

Theoremdpmul10 30581 Multiply by 10 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021.)
𝐴 ∈ ℕ0    &   𝐵 ∈ ℝ       ((𝐴.𝐵) · 10) = 𝐴𝐵

Theoremdecdiv10 30582 Divide a decimal number by 10. (Contributed by Thierry Arnoux, 25-Dec-2021.)
𝐴 ∈ ℕ0    &   𝐵 ∈ ℝ       (𝐴𝐵 / 10) = (𝐴.𝐵)

Theoremdpmul100 30583 Multiply by 100 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021.)
𝐴 ∈ ℕ0    &   𝐵 ∈ ℕ0    &   𝐶 ∈ ℝ       ((𝐴.𝐵𝐶) · 100) = 𝐴𝐵𝐶

Theoremdp3mul10 30584 Multiply by 10 a decimal expansion with 3 digits. (Contributed by Thierry Arnoux, 25-Dec-2021.)
𝐴 ∈ ℕ0    &   𝐵 ∈ ℕ0    &   𝐶 ∈ ℝ       ((𝐴.𝐵𝐶) · 10) = (𝐴𝐵.𝐶)

Theoremdpmul1000 30585 Multiply by 1000 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021.)
𝐴 ∈ ℕ0    &   𝐵 ∈ ℕ0    &   𝐶 ∈ ℕ0    &   𝐷 ∈ ℝ       ((𝐴.𝐵𝐶𝐷) · 1000) = 𝐴𝐵𝐶𝐷

Theoremdpval3rp 30586 Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021.)
𝐴 ∈ ℕ0    &   𝐵 ∈ ℝ+       (𝐴.𝐵) = 𝐴𝐵

Theoremdp0u 30587 Add a zero in the tenths place. (Contributed by Thierry Arnoux, 16-Dec-2021.)
𝐴 ∈ ℕ0       (𝐴.0) = 𝐴

Theoremdp0h 30588 Remove a zero in the units places. (Contributed by Thierry Arnoux, 16-Dec-2021.)
𝐴 ∈ ℝ+       (0.𝐴) = (𝐴 / 10)

Theoremrpdpcl 30589 Closure of the decimal point in the positive real numbers. (Contributed by Thierry Arnoux, 16-Dec-2021.)
𝐴 ∈ ℕ0    &   𝐵 ∈ ℝ+       (𝐴.𝐵) ∈ ℝ+

Theoremdplt 30590 Comparing two decimal expansions (equal higher places). (Contributed by Thierry Arnoux, 16-Dec-2021.)
𝐴 ∈ ℕ0    &   𝐵 ∈ ℝ+    &   𝐶 ∈ ℝ+    &   𝐵 < 𝐶       (𝐴.𝐵) < (𝐴.𝐶)

Theoremdplti 30591 Comparing a decimal expansions with the next higher integer. (Contributed by Thierry Arnoux, 16-Dec-2021.)
𝐴 ∈ ℕ0    &   𝐵 ∈ ℝ+    &   𝐶 ∈ ℕ0    &   𝐵 < 10    &   (𝐴 + 1) = 𝐶       (𝐴.𝐵) < 𝐶

Theoremdpgti 30592 Comparing a decimal expansions with the next lower integer. (Contributed by Thierry Arnoux, 16-Dec-2021.)
𝐴 ∈ ℕ0    &   𝐵 ∈ ℝ+       𝐴 < (𝐴.𝐵)

Theoremdpltc 30593 Comparing two decimal integers (unequal higher places). (Contributed by Thierry Arnoux, 16-Dec-2021.)
𝐴 ∈ ℕ0    &   𝐵 ∈ ℝ+    &   𝐶 ∈ ℕ0    &   𝐷 ∈ ℝ+    &   𝐴 < 𝐶    &   𝐵 < 10       (𝐴.𝐵) < (𝐶.𝐷)

Theoremdpexpp1 30594 Add one zero to the mantisse, and a one to the exponent in a scientific notation. (Contributed by Thierry Arnoux, 16-Dec-2021.)
𝐴 ∈ ℕ0    &   𝐵 ∈ ℝ+    &   (𝑃 + 1) = 𝑄    &   𝑃 ∈ ℤ    &   𝑄 ∈ ℤ       ((𝐴.𝐵) · (10↑𝑃)) = ((0.𝐴𝐵) · (10↑𝑄))

Theorem0dp2dp 30595 Multiply by 10 a decimal expansion which starts with a zero. (Contributed by Thierry Arnoux, 16-Dec-2021.)
𝐴 ∈ ℕ0    &   𝐵 ∈ ℝ+       ((0.𝐴𝐵) · 10) = (𝐴.𝐵)

Theoremdpadd2 30596 Addition with one decimal, no carry. (Contributed by Thierry Arnoux, 29-Dec-2021.)
𝐴 ∈ ℕ0    &   𝐵 ∈ ℝ+    &   𝐶 ∈ ℕ0    &   𝐷 ∈ ℝ+    &   𝐸 ∈ ℕ0    &   𝐹 ∈ ℝ+    &   𝐺 ∈ ℕ0    &   𝐻 ∈ ℕ0    &   (𝐺 + 𝐻) = 𝐼    &   ((𝐴.𝐵) + (𝐶.𝐷)) = (𝐸.𝐹)       ((𝐺.𝐴𝐵) + (𝐻.𝐶𝐷)) = (𝐼.𝐸𝐹)

𝐴 ∈ ℕ0    &   𝐵 ∈ ℕ0    &   𝐶 ∈ ℕ0    &   𝐷 ∈ ℕ0    &   𝐸 ∈ ℕ0    &   𝐹 ∈ ℕ0    &   (𝐴𝐵 + 𝐶𝐷) = 𝐸𝐹       ((𝐴.𝐵) + (𝐶.𝐷)) = (𝐸.𝐹)