Home | Metamath
Proof Explorer Theorem List (p. 306 of 449) | < 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-28689) |
Hilbert Space Explorer
(28690-30212) |
Users' Mathboxes
(30213-44899) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | uzssico 30501 | Upper integer sets are a subset of the corresponding closed-below, open-above intervals. (Contributed by Thierry Arnoux, 29-Dec-2021.) |
⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ⊆ (𝑀[,)+∞)) | ||
Theorem | fz2ssnn0 30502 | A finite set of sequential integers that is a subset of ℕ0. (Contributed by Thierry Arnoux, 8-Dec-2021.) |
⊢ (𝑀 ∈ ℕ0 → (𝑀...𝑁) ⊆ ℕ0) | ||
Theorem | nndiffz1 30503 | Upper set of the positive integers. (Contributed by Thierry Arnoux, 22-Aug-2017.) |
⊢ (𝑁 ∈ ℕ0 → (ℕ ∖ (1...𝑁)) = (ℤ≥‘(𝑁 + 1))) | ||
Theorem | ssnnssfz 30504* | 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...𝑛)) | ||
Theorem | fzne1 30505 | Elementhood in a finite set of sequential integers, except its lower bound. (Contributed by Thierry Arnoux, 1-Jan-2024.) |
⊢ ((𝐾 ∈ (𝑀...𝑁) ∧ 𝐾 ≠ 𝑀) → 𝐾 ∈ ((𝑀 + 1)...𝑁)) | ||
Theorem | fzm1ne1 30506 | Elementhood of an integer and its predecessor in finite intervals of integers. (Contributed by Thierry Arnoux, 1-Jan-2024.) |
⊢ ((𝐾 ∈ (𝑀...𝑁) ∧ 𝐾 ≠ 𝑀) → (𝐾 − 1) ∈ (𝑀...(𝑁 − 1))) | ||
Theorem | fzspl 30507 | Split the last element of a finite set of sequential integers. (more generic than fzsuc 12948) (Contributed by Thierry Arnoux, 7-Nov-2016.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) = ((𝑀...(𝑁 − 1)) ∪ {𝑁})) | ||
Theorem | fzdif2 30508 | Split the last element of a finite set of sequential integers. (more generic than fzsuc 12948) (Contributed by Thierry Arnoux, 22-Aug-2020.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((𝑀...𝑁) ∖ {𝑁}) = (𝑀...(𝑁 − 1))) | ||
Theorem | fzodif2 30509 | Split the last element of a half-open range of sequential integers. (Contributed by Thierry Arnoux, 5-Dec-2021.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((𝑀..^(𝑁 + 1)) ∖ {𝑁}) = (𝑀..^𝑁)) | ||
Theorem | fzodif1 30510 | Set difference of two half-open range of sequential integers sharing the same starting value. (Contributed by Thierry Arnoux, 2-Oct-2023.) |
⊢ (𝐾 ∈ (𝑀...𝑁) → ((𝑀..^𝑁) ∖ (𝑀..^𝐾)) = (𝐾..^𝑁)) | ||
Theorem | fzsplit3 30511 | Split a finite interval of integers into two parts. (Contributed by Thierry Arnoux, 2-May-2017.) |
⊢ (𝐾 ∈ (𝑀...𝑁) → (𝑀...𝑁) = ((𝑀...(𝐾 − 1)) ∪ (𝐾...𝑁))) | ||
Theorem | bcm1n 30512 | The proportion of one binomial coefficient to another with 𝑁 decreased by 1. (Contributed by Thierry Arnoux, 9-Nov-2016.) |
⊢ ((𝐾 ∈ (0...(𝑁 − 1)) ∧ 𝑁 ∈ ℕ) → (((𝑁 − 1)C𝐾) / (𝑁C𝐾)) = ((𝑁 − 𝐾) / 𝑁)) | ||
Theorem | iundisjfi 30513* | Rewrite a countable union as a disjoint union, finite version. Cf. iundisj 24143. (Contributed by Thierry Arnoux, 15-Feb-2017.) |
⊢ Ⅎ𝑛𝐵 & ⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵) ⇒ ⊢ ∪ 𝑛 ∈ (1..^𝑁)𝐴 = ∪ 𝑛 ∈ (1..^𝑁)(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) | ||
Theorem | iundisj2fi 30514* | A disjoint union is disjoint, finite version. Cf. iundisj2 24144. (Contributed by Thierry Arnoux, 16-Feb-2017.) |
⊢ Ⅎ𝑛𝐵 & ⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵) ⇒ ⊢ Disj 𝑛 ∈ (1..^𝑁)(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) | ||
Theorem | iundisjcnt 30515* | Rewrite a countable union as a disjoint union. (Contributed by Thierry Arnoux, 16-Feb-2017.) |
⊢ Ⅎ𝑛𝐵 & ⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝑁 = ℕ ∨ 𝑁 = (1..^𝑀))) ⇒ ⊢ (𝜑 → ∪ 𝑛 ∈ 𝑁 𝐴 = ∪ 𝑛 ∈ 𝑁 (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) | ||
Theorem | iundisj2cnt 30516* | A countable disjoint union is disjoint. Cf. iundisj2 24144. (Contributed by Thierry Arnoux, 16-Feb-2017.) |
⊢ Ⅎ𝑛𝐵 & ⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝑁 = ℕ ∨ 𝑁 = (1..^𝑀))) ⇒ ⊢ (𝜑 → Disj 𝑛 ∈ 𝑁 (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) | ||
Theorem | fzone1 30517 | Elementhood in a half-open interval, except its lower bound. (Contributed by Thierry Arnoux, 1-Jan-2024.) |
⊢ ((𝐾 ∈ (𝑀..^𝑁) ∧ 𝐾 ≠ 𝑀) → 𝐾 ∈ ((𝑀 + 1)..^𝑁)) | ||
Theorem | fzom1ne1 30518 | Elementhood in a half-open interval, except the lower bound, shifted by one. (Contributed by Thierry Arnoux, 1-Jan-2024.) |
⊢ ((𝐾 ∈ (𝑀..^𝑁) ∧ 𝐾 ≠ 𝑀) → (𝐾 − 1) ∈ (𝑀..^(𝑁 − 1))) | ||
Theorem | f1ocnt 30519* | 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 30515 or iundisj2cnt 30516. (Contributed by Thierry Arnoux, 25-Jul-2020.) |
⊢ (𝐴 ≼ ω → ∃𝑓(𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((♯‘𝐴) + 1))))) | ||
Theorem | fz1nnct 30520 | NN and integer ranges starting from 1 are countable. (Contributed by Thierry Arnoux, 25-Jul-2020.) |
⊢ ((𝐴 = ℕ ∨ 𝐴 = (1..^𝑀)) → 𝐴 ≼ ω) | ||
Theorem | fz1nntr 30521 | NN and integer ranges starting from 1 are a transitive family of set. (Contributed by Thierry Arnoux, 25-Jul-2020.) |
⊢ (((𝐴 = ℕ ∨ 𝐴 = (1..^𝑀)) ∧ 𝑁 ∈ 𝐴) → (1..^𝑁) ⊆ 𝐴) | ||
Theorem | hashunif 30522* | The cardinality of a disjoint finite union of finite sets. Cf. hashuni 15175. (Contributed by Thierry Arnoux, 17-Feb-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ Fin) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝑥) ⇒ ⊢ (𝜑 → (♯‘∪ 𝐴) = Σ𝑥 ∈ 𝐴 (♯‘𝑥)) | ||
Theorem | hashxpe 30523 | The size of the Cartesian product of two finite sets is the product of their sizes. This is a version of hashxp 13789 valid for infinite sets, which uses extended real numbers. (Contributed by Thierry Arnoux, 27-May-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (♯‘(𝐴 × 𝐵)) = ((♯‘𝐴) ·e (♯‘𝐵))) | ||
Theorem | hashgt1 30524 | Restate "set contains at least two elements" in terms of elementhood. (Contributed by Thierry Arnoux, 21-Nov-2023.) |
⊢ (𝐴 ∈ 𝑉 → (¬ 𝐴 ∈ (◡♯ “ {0, 1}) ↔ 1 < (♯‘𝐴))) | ||
Theorem | dvdszzq 30525 | Divisibility for an integer quotient. (Contributed by Thierry Arnoux, 17-Sep-2023.) |
⊢ 𝑁 = (𝐴 / 𝐵) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝑃 ∥ 𝐴) & ⊢ (𝜑 → ¬ 𝑃 ∥ 𝐵) ⇒ ⊢ (𝜑 → 𝑃 ∥ 𝑁) | ||
Theorem | prmdvdsbc 30526 | Condition for a prime number to divide a binomial coefficient. (Contributed by Thierry Arnoux, 17-Sep-2023.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑃 ∥ (𝑃C𝑁)) | ||
Theorem | numdenneg 30527 | Numerator and denominator of the negative. (Contributed by Thierry Arnoux, 27-Oct-2017.) |
⊢ (𝑄 ∈ ℚ → ((numer‘-𝑄) = -(numer‘𝑄) ∧ (denom‘-𝑄) = (denom‘𝑄))) | ||
Theorem | divnumden2 30528 | Calculate the reduced form of a quotient using gcd. This version extends divnumden 16082 for the negative integers. (Contributed by Thierry Arnoux, 25-Oct-2017.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → ((numer‘(𝐴 / 𝐵)) = -(𝐴 / (𝐴 gcd 𝐵)) ∧ (denom‘(𝐴 / 𝐵)) = -(𝐵 / (𝐴 gcd 𝐵)))) | ||
Theorem | nnindf 30529* | Principle of Mathematical Induction, using a bound-variable hypothesis instead of distinct variables. (Contributed by Thierry Arnoux, 6-May-2018.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝑥 = 1 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑦 ∈ ℕ → (𝜒 → 𝜃)) ⇒ ⊢ (𝐴 ∈ ℕ → 𝜏) | ||
Theorem | nnindd 30530* | Principle of Mathematical Induction (inference schema) on integers, a deduction version. (Contributed by Thierry Arnoux, 19-Jul-2020.) |
⊢ (𝑥 = 1 → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃)) & ⊢ (𝑥 = (𝑦 + 1) → (𝜓 ↔ 𝜏)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜂)) & ⊢ (𝜑 → 𝜒) & ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → 𝜂) | ||
Theorem | nn0min 30531* | Extracting the minimum positive integer for which a property 𝜒 does not hold. This uses substitutions similar to nn0ind 12071. (Contributed by Thierry Arnoux, 6-May-2018.) |
⊢ (𝑛 = 0 → (𝜓 ↔ 𝜒)) & ⊢ (𝑛 = 𝑚 → (𝜓 ↔ 𝜃)) & ⊢ (𝑛 = (𝑚 + 1) → (𝜓 ↔ 𝜏)) & ⊢ (𝜑 → ¬ 𝜒) & ⊢ (𝜑 → ∃𝑛 ∈ ℕ 𝜓) ⇒ ⊢ (𝜑 → ∃𝑚 ∈ ℕ0 (¬ 𝜃 ∧ 𝜏)) | ||
Theorem | subne0nn 30532 | A nonnegative difference is positive if the two numbers are not equal. (Contributed by Thierry Arnoux, 17-Dec-2023.) |
⊢ (𝜑 → 𝑀 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℂ) & ⊢ (𝜑 → (𝑀 − 𝑁) ∈ ℕ0) & ⊢ (𝜑 → 𝑀 ≠ 𝑁) ⇒ ⊢ (𝜑 → (𝑀 − 𝑁) ∈ ℕ) | ||
Theorem | ltesubnnd 30533 | Subtracting an integer number from another number decreases it. See ltsubrpd 12457. (Contributed by Thierry Arnoux, 18-Apr-2017.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → ((𝑀 + 1) − 𝑁) ≤ 𝑀) | ||
Theorem | fprodeq02 30534* | If one of the factors is zero the product is zero. (Contributed by Thierry Arnoux, 11-Dec-2021.) |
⊢ (𝑘 = 𝐾 → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐾 ∈ 𝐴) & ⊢ (𝜑 → 𝐶 = 0) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = 0) | ||
Theorem | pr01ssre 30535 | The range of the indicator function is a subset of ℝ. (Contributed by Thierry Arnoux, 14-Aug-2017.) |
⊢ {0, 1} ⊆ ℝ | ||
Theorem | fprodex01 30536* | 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)) | ||
Theorem | prodpr 30537* | A product over a pair is the product of the elements. (Contributed by Thierry Arnoux, 1-Jan-2022.) |
⊢ (𝑘 = 𝐴 → 𝐷 = 𝐸) & ⊢ (𝑘 = 𝐵 → 𝐷 = 𝐹) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐸 ∈ ℂ) & ⊢ (𝜑 → 𝐹 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ {𝐴, 𝐵}𝐷 = (𝐸 · 𝐹)) | ||
Theorem | prodtp 30538* | A product over a triple is the product of the elements. (Contributed by Thierry Arnoux, 1-Jan-2022.) |
⊢ (𝑘 = 𝐴 → 𝐷 = 𝐸) & ⊢ (𝑘 = 𝐵 → 𝐷 = 𝐹) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐸 ∈ ℂ) & ⊢ (𝜑 → 𝐹 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝑘 = 𝐶 → 𝐷 = 𝐺) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐺 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐶) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ {𝐴, 𝐵, 𝐶}𝐷 = ((𝐸 · 𝐹) · 𝐺)) | ||
Theorem | fsumub 30539* | An upper bound for a term of a positive finite sum. (Contributed by Thierry Arnoux, 27-Dec-2021.) |
⊢ (𝑘 = 𝐾 → 𝐵 = 𝐷) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = 𝐶) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐾 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐷 ≤ 𝐶) | ||
Theorem | fsumiunle 30540* | 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 ≤ 𝐶) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝐶 ≤ Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶) | ||
Theorem | dfdec100 30541 | Split the hundreds from a decimal value. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ ;;𝐴𝐵𝐶 = ((;;100 · 𝐴) + ;𝐵𝐶) | ||
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._1_4_1_59). 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. | ||
Syntax | cdp2 30542 | Constant used for decimal fraction constructor. See df-dp2 30543. |
class _𝐴𝐵 | ||
Definition | df-dp2 30543 | Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12093. (Contributed by David A. Wheeler, 15-May-2015.) (Revised by AV, 9-Sep-2021.) |
⊢ _𝐴𝐵 = (𝐴 + (𝐵 / ;10)) | ||
Theorem | dp2eq1 30544 | Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.) |
⊢ (𝐴 = 𝐵 → _𝐴𝐶 = _𝐵𝐶) | ||
Theorem | dp2eq2 30545 | Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.) |
⊢ (𝐴 = 𝐵 → _𝐶𝐴 = _𝐶𝐵) | ||
Theorem | dp2eq1i 30546 | Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ _𝐴𝐶 = _𝐵𝐶 | ||
Theorem | dp2eq2i 30547 | Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ _𝐶𝐴 = _𝐶𝐵 | ||
Theorem | dp2eq12i 30548 | Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ _𝐴𝐶 = _𝐵𝐷 | ||
Theorem | dp20u 30549 | Add a zero in the tenths (lower) place. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ _𝐴0 = 𝐴 | ||
Theorem | dp20h 30550 | Add a zero in the unit places. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℝ+ ⇒ ⊢ _0𝐴 = (𝐴 / ;10) | ||
Theorem | dp2cl 30551 | Closure for the decimal fraction constructor if both values are reals. (Contributed by David A. Wheeler, 15-May-2015.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → _𝐴𝐵 ∈ ℝ) | ||
Theorem | dp2clq 30552 | Closure for a decimal fraction. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℚ ⇒ ⊢ _𝐴𝐵 ∈ ℚ | ||
Theorem | rpdp2cl 30553 | Closure for a decimal fraction in the positive real numbers. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ ⇒ ⊢ _𝐴𝐵 ∈ ℝ+ | ||
Theorem | rpdp2cl2 30554 | Closure for a decimal fraction with no decimal expansion in the positive real numbers. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
⊢ 𝐴 ∈ ℕ ⇒ ⊢ _𝐴0 ∈ ℝ+ | ||
Theorem | dp2lt10 30555 | Decimal fraction builds real numbers less than 10. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ & ⊢ 𝐴 < ;10 & ⊢ 𝐵 < ;10 ⇒ ⊢ _𝐴𝐵 < ;10 | ||
Theorem | dp2lt 30556 | Comparing two decimal fractions (equal unit places). (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ & ⊢ 𝐶 ∈ ℝ+ & ⊢ 𝐵 < 𝐶 ⇒ ⊢ _𝐴𝐵 < _𝐴𝐶 | ||
Theorem | dp2ltsuc 30557 | Comparing a decimal fraction with the next integer. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ & ⊢ 𝐵 < ;10 & ⊢ (𝐴 + 1) = 𝐶 ⇒ ⊢ _𝐴𝐵 < 𝐶 | ||
Theorem | dp2ltc 30558 | Comparing two decimal expansions (unequal higher places). (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℝ+ & ⊢ 𝐵 < ;10 & ⊢ 𝐴 < 𝐶 ⇒ ⊢ _𝐴𝐵 < _𝐶𝐷 | ||
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 30560 and df-dp2 30543 for more information; dpval2 30564 and dpfrac1 30563 provide a more convenient way to obtain a value. This is intentionally similar to df-dec 12093. | ||
Syntax | cdp 30559 | Decimal point operator. See df-dp 30560. |
class . | ||
Definition | df-dp 30560* |
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.) |
⊢ . = (𝑥 ∈ ℕ0, 𝑦 ∈ ℝ ↦ _𝑥𝑦) | ||
Theorem | dpval 30561 | Define the value of the decimal point operator. See df-dp 30560. (Contributed by David A. Wheeler, 15-May-2015.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ) → (𝐴.𝐵) = _𝐴𝐵) | ||
Theorem | dpcl 30562 | Prove that the closure of the decimal point is ℝ as we have defined it. See df-dp 30560. (Contributed by David A. Wheeler, 15-May-2015.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ) → (𝐴.𝐵) ∈ ℝ) | ||
Theorem | dpfrac1 30563 | Prove a simple equivalence involving the decimal point. See df-dp 30560 and dpcl 30562. (Contributed by David A. Wheeler, 15-May-2015.) (Revised by AV, 9-Sep-2021.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ) → (𝐴.𝐵) = (;𝐴𝐵 / ;10)) | ||
Theorem | dpval2 30564 | Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴.𝐵) = (𝐴 + (𝐵 / ;10)) | ||
Theorem | dpval3 30565 | Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴.𝐵) = _𝐴𝐵 | ||
Theorem | dpmul10 30566 | Multiply by 10 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((𝐴.𝐵) · ;10) = ;𝐴𝐵 | ||
Theorem | decdiv10 30567 | Divide a decimal number by 10. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (;𝐴𝐵 / ;10) = (𝐴.𝐵) | ||
Theorem | dpmul100 30568 | Multiply by 100 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ ((𝐴._𝐵𝐶) · ;;100) = ;;𝐴𝐵𝐶 | ||
Theorem | dp3mul10 30569 | Multiply by 10 a decimal expansion with 3 digits. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ ((𝐴._𝐵𝐶) · ;10) = (;𝐴𝐵.𝐶) | ||
Theorem | dpmul1000 30570 | Multiply by 1000 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℝ ⇒ ⊢ ((𝐴._𝐵_𝐶𝐷) · ;;;1000) = ;;;𝐴𝐵𝐶𝐷 | ||
Theorem | dpval3rp 30571 | Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ ⇒ ⊢ (𝐴.𝐵) = _𝐴𝐵 | ||
Theorem | dp0u 30572 | Add a zero in the tenths place. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ (𝐴.0) = 𝐴 | ||
Theorem | dp0h 30573 | Remove a zero in the units places. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℝ+ ⇒ ⊢ (0.𝐴) = (𝐴 / ;10) | ||
Theorem | rpdpcl 30574 | Closure of the decimal point in the positive real numbers. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ ⇒ ⊢ (𝐴.𝐵) ∈ ℝ+ | ||
Theorem | dplt 30575 | Comparing two decimal expansions (equal higher places). (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ & ⊢ 𝐶 ∈ ℝ+ & ⊢ 𝐵 < 𝐶 ⇒ ⊢ (𝐴.𝐵) < (𝐴.𝐶) | ||
Theorem | dplti 30576 | Comparing a decimal expansions with the next higher integer. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐵 < ;10 & ⊢ (𝐴 + 1) = 𝐶 ⇒ ⊢ (𝐴.𝐵) < 𝐶 | ||
Theorem | dpgti 30577 | Comparing a decimal expansions with the next lower integer. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ ⇒ ⊢ 𝐴 < (𝐴.𝐵) | ||
Theorem | dpltc 30578 | Comparing two decimal integers (unequal higher places). (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℝ+ & ⊢ 𝐴 < 𝐶 & ⊢ 𝐵 < ;10 ⇒ ⊢ (𝐴.𝐵) < (𝐶.𝐷) | ||
Theorem | dpexpp1 30579 | 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↑𝑄)) | ||
Theorem | 0dp2dp 30580 | Multiply by 10 a decimal expansion which starts with a zero. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ ⇒ ⊢ ((0._𝐴𝐵) · ;10) = (𝐴.𝐵) | ||
Theorem | dpadd2 30581 | Addition with one decimal, no carry. (Contributed by Thierry Arnoux, 29-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℝ+ & ⊢ 𝐸 ∈ ℕ0 & ⊢ 𝐹 ∈ ℝ+ & ⊢ 𝐺 ∈ ℕ0 & ⊢ 𝐻 ∈ ℕ0 & ⊢ (𝐺 + 𝐻) = 𝐼 & ⊢ ((𝐴.𝐵) + (𝐶.𝐷)) = (𝐸.𝐹) ⇒ ⊢ ((𝐺._𝐴𝐵) + (𝐻._𝐶𝐷)) = (𝐼._𝐸𝐹) | ||
Theorem | dpadd 30582 | Addition with one decimal. (Contributed by Thierry Arnoux, 27-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐸 ∈ ℕ0 & ⊢ 𝐹 ∈ ℕ0 & ⊢ (;𝐴𝐵 + ;𝐶𝐷) = ;𝐸𝐹 ⇒ ⊢ ((𝐴.𝐵) + (𝐶.𝐷)) = (𝐸.𝐹) | ||
Theorem | dpadd3 30583 | Addition with two decimals. (Contributed by Thierry Arnoux, 27-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐸 ∈ ℕ0 & ⊢ 𝐺 ∈ ℕ0 & ⊢ 𝐹 ∈ ℕ0 & ⊢ 𝐻 ∈ ℕ0 & ⊢ 𝐼 ∈ ℕ0 & ⊢ (;;𝐴𝐵𝐶 + ;;𝐷𝐸𝐹) = ;;𝐺𝐻𝐼 ⇒ ⊢ ((𝐴._𝐵𝐶) + (𝐷._𝐸𝐹)) = (𝐺._𝐻𝐼) | ||
Theorem | dpmul 30584 | Multiplication with one decimal point. (Contributed by Thierry Arnoux, 26-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐸 ∈ ℕ0 & ⊢ 𝐺 ∈ ℕ0 & ⊢ 𝐽 ∈ ℕ0 & ⊢ 𝐾 ∈ ℕ0 & ⊢ (𝐴 · 𝐶) = 𝐹 & ⊢ (𝐴 · 𝐷) = 𝑀 & ⊢ (𝐵 · 𝐶) = 𝐿 & ⊢ (𝐵 · 𝐷) = ;𝐸𝐾 & ⊢ ((𝐿 + 𝑀) + 𝐸) = ;𝐺𝐽 & ⊢ (𝐹 + 𝐺) = 𝐼 ⇒ ⊢ ((𝐴.𝐵) · (𝐶.𝐷)) = (𝐼._𝐽𝐾) | ||
Theorem | dpmul4 30585 | An upper bound to multiplication of decimal numbers with 4 digits. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐸 ∈ ℕ0 & ⊢ 𝐺 ∈ ℕ0 & ⊢ 𝐽 ∈ ℕ0 & ⊢ 𝐾 ∈ ℕ0 & ⊢ 𝐹 ∈ ℕ0 & ⊢ 𝐻 ∈ ℕ0 & ⊢ 𝐼 ∈ ℕ0 & ⊢ 𝐿 ∈ ℕ0 & ⊢ 𝑀 ∈ ℕ0 & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑂 ∈ ℕ0 & ⊢ 𝑃 ∈ ℕ0 & ⊢ 𝑄 ∈ ℕ0 & ⊢ 𝑅 ∈ ℕ0 & ⊢ 𝑆 ∈ ℕ0 & ⊢ 𝑇 ∈ ℕ0 & ⊢ 𝑈 ∈ ℕ0 & ⊢ 𝑊 ∈ ℕ0 & ⊢ 𝑋 ∈ ℕ0 & ⊢ 𝑌 ∈ ℕ0 & ⊢ 𝑍 ∈ ℕ0 & ⊢ 𝑈 < ;10 & ⊢ 𝑃 < ;10 & ⊢ 𝑄 < ;10 & ⊢ (;;𝐿𝑀𝑁 + 𝑂) = ;;;𝑅𝑆𝑇𝑈 & ⊢ ((𝐴.𝐵) · (𝐸.𝐹)) = (𝐼._𝐽𝐾) & ⊢ ((𝐶.𝐷) · (𝐺.𝐻)) = (𝑂._𝑃𝑄) & ⊢ (;;;𝐼𝐽𝐾1 + ;;𝑅𝑆𝑇) = ;;;𝑊𝑋𝑌𝑍 & ⊢ (((𝐴.𝐵) + (𝐶.𝐷)) · ((𝐸.𝐹) + (𝐺.𝐻))) = (((𝐼._𝐽𝐾) + (𝐿._𝑀𝑁)) + (𝑂._𝑃𝑄)) ⇒ ⊢ ((𝐴._𝐵_𝐶𝐷) · (𝐸._𝐹_𝐺𝐻)) < (𝑊._𝑋_𝑌𝑍) | ||
Theorem | threehalves 30586 | Example theorem demonstrating decimal expansions. (Contributed by Thierry Arnoux, 27-Dec-2021.) |
⊢ (3 / 2) = (1.5) | ||
Theorem | 1mhdrd 30587 | Example theorem demonstrating decimal expansions. (Contributed by Thierry Arnoux, 27-Dec-2021.) |
⊢ ((0._99) + (0._01)) = 1 | ||
Syntax | cxdiv 30588 | Extend class notation to include division of extended reals. |
class /𝑒 | ||
Definition | df-xdiv 30589* | Define division over extended real numbers. (Contributed by Thierry Arnoux, 17-Dec-2016.) |
⊢ /𝑒 = (𝑥 ∈ ℝ*, 𝑦 ∈ (ℝ ∖ {0}) ↦ (℩𝑧 ∈ ℝ* (𝑦 ·e 𝑧) = 𝑥)) | ||
Theorem | xdivval 30590* | Value of division: the (unique) element 𝑥 such that (𝐵 · 𝑥) = 𝐴. This is meaningful only when 𝐵 is nonzero. (Contributed by Thierry Arnoux, 17-Dec-2016.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 /𝑒 𝐵) = (℩𝑥 ∈ ℝ* (𝐵 ·e 𝑥) = 𝐴)) | ||
Theorem | xrecex 30591* | Existence of reciprocal of nonzero real number. (Contributed by Thierry Arnoux, 17-Dec-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → ∃𝑥 ∈ ℝ (𝐴 ·e 𝑥) = 1) | ||
Theorem | xmulcand 30592 | Cancellation law for extended multiplication. (Contributed by Thierry Arnoux, 17-Dec-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐶 ·e 𝐴) = (𝐶 ·e 𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | xreceu 30593* | Existential uniqueness of reciprocals. Theorem I.8 of [Apostol] p. 18. (Contributed by Thierry Arnoux, 17-Dec-2016.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → ∃!𝑥 ∈ ℝ* (𝐵 ·e 𝑥) = 𝐴) | ||
Theorem | xdivcld 30594 | Closure law for the extended division. (Contributed by Thierry Arnoux, 15-Mar-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 /𝑒 𝐵) ∈ ℝ*) | ||
Theorem | xdivcl 30595 | Closure law for the extended division. (Contributed by Thierry Arnoux, 15-Mar-2017.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 /𝑒 𝐵) ∈ ℝ*) | ||
Theorem | xdivmul 30596 | Relationship between division and multiplication. (Contributed by Thierry Arnoux, 24-Dec-2016.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ (𝐶 ∈ ℝ ∧ 𝐶 ≠ 0)) → ((𝐴 /𝑒 𝐶) = 𝐵 ↔ (𝐶 ·e 𝐵) = 𝐴)) | ||
Theorem | rexdiv 30597 | The extended real division operation when both arguments are real. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 /𝑒 𝐵) = (𝐴 / 𝐵)) | ||
Theorem | xdivrec 30598 | Relationship between division and reciprocal. (Contributed by Thierry Arnoux, 5-Jul-2017.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 /𝑒 𝐵) = (𝐴 ·e (1 /𝑒 𝐵))) | ||
Theorem | xdivid 30599 | A number divided by itself is one. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (𝐴 /𝑒 𝐴) = 1) | ||
Theorem | xdiv0 30600 | Division into zero is zero. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (0 /𝑒 𝐴) = 0) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |