| Metamath
Proof Explorer Theorem List (p. 329 of 494) | < 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: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | iundisj2cnt 32801* | A countable disjoint union is disjoint. Cf. iundisj2 25584. (Contributed by Thierry Arnoux, 16-Feb-2017.) |
| ⊢ Ⅎ𝑛𝐵 & ⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝑁 = ℕ ∨ 𝑁 = (1..^𝑀))) ⇒ ⊢ (𝜑 → Disj 𝑛 ∈ 𝑁 (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) | ||
| Theorem | fzone1 32802 | Elementhood in a half-open interval, except its lower bound. (Contributed by Thierry Arnoux, 1-Jan-2024.) |
| ⊢ ((𝐾 ∈ (𝑀..^𝑁) ∧ 𝐾 ≠ 𝑀) → 𝐾 ∈ ((𝑀 + 1)..^𝑁)) | ||
| Theorem | fzom1ne1 32803 | Elementhood in a half-open interval, except the lower bound, shifted by one. (Contributed by Thierry Arnoux, 1-Jan-2024.) |
| ⊢ ((𝐾 ∈ (𝑀..^𝑁) ∧ 𝐾 ≠ 𝑀) → (𝐾 − 1) ∈ (𝑀..^(𝑁 − 1))) | ||
| Theorem | f1ocnt 32804* | 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 32800 or iundisj2cnt 32801. (Contributed by Thierry Arnoux, 25-Jul-2020.) |
| ⊢ (𝐴 ≼ ω → ∃𝑓(𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((♯‘𝐴) + 1))))) | ||
| Theorem | fz1nnct 32805 | NN and integer ranges starting from 1 are countable. (Contributed by Thierry Arnoux, 25-Jul-2020.) |
| ⊢ ((𝐴 = ℕ ∨ 𝐴 = (1..^𝑀)) → 𝐴 ≼ ω) | ||
| Theorem | fz1nntr 32806 | NN and integer ranges starting from 1 are a transitive family of set. (Contributed by Thierry Arnoux, 25-Jul-2020.) |
| ⊢ (((𝐴 = ℕ ∨ 𝐴 = (1..^𝑀)) ∧ 𝑁 ∈ 𝐴) → (1..^𝑁) ⊆ 𝐴) | ||
| Theorem | fzo0opth 32807 | Equality for a half open integer range starting at zero is the same as equality of its upper bound, analogous to fzopth 13601 and fzoopth 13801. (Contributed by Thierry Arnoux, 27-May-2025.) |
| ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((0..^𝑀) = (0..^𝑁) ↔ 𝑀 = 𝑁)) | ||
| Theorem | nn0difffzod 32808 | A nonnegative integer that is not in the half-open range from 0 to 𝑁 is at least 𝑁. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
| ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ (ℕ0 ∖ (0..^𝑁))) ⇒ ⊢ (𝜑 → ¬ 𝑀 < 𝑁) | ||
| Theorem | suppssnn0 32809* | Show that the support of a function is contained in an half-open nonnegative integer range. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
| ⊢ (𝜑 → 𝐹 Fn ℕ0) & ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑁 ≤ 𝑘) → (𝐹‘𝑘) = 𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ (0..^𝑁)) | ||
| Theorem | hashunif 32810* | The cardinality of a disjoint finite union of finite sets. Cf. hashuni 15862. (Contributed by Thierry Arnoux, 17-Feb-2017.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ Fin) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝑥) ⇒ ⊢ (𝜑 → (♯‘∪ 𝐴) = Σ𝑥 ∈ 𝐴 (♯‘𝑥)) | ||
| Theorem | hashxpe 32811 | The size of the Cartesian product of two finite sets is the product of their sizes. This is a version of hashxp 14473 valid for infinite sets, which uses extended real numbers. (Contributed by Thierry Arnoux, 27-May-2023.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (♯‘(𝐴 × 𝐵)) = ((♯‘𝐴) ·e (♯‘𝐵))) | ||
| Theorem | hashgt1 32812 | Restate "set contains at least two elements" in terms of elementhood. (Contributed by Thierry Arnoux, 21-Nov-2023.) |
| ⊢ (𝐴 ∈ 𝑉 → (¬ 𝐴 ∈ (◡♯ “ {0, 1}) ↔ 1 < (♯‘𝐴))) | ||
| Theorem | hashpss 32813 | The size of a proper subset is less than the size of its finite superset. (Contributed by Thierry Arnoux, 13-Oct-2025.) |
| ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊊ 𝐴) → (♯‘𝐵) < (♯‘𝐴)) | ||
| Theorem | znumd 32814 | Numerator of an integer. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ (𝜑 → 𝑍 ∈ ℤ) ⇒ ⊢ (𝜑 → (numer‘𝑍) = 𝑍) | ||
| Theorem | zdend 32815 | Denominator of an integer. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ (𝜑 → 𝑍 ∈ ℤ) ⇒ ⊢ (𝜑 → (denom‘𝑍) = 1) | ||
| Theorem | numdenneg 32816 | Numerator and denominator of the negative. (Contributed by Thierry Arnoux, 27-Oct-2017.) |
| ⊢ (𝑄 ∈ ℚ → ((numer‘-𝑄) = -(numer‘𝑄) ∧ (denom‘-𝑄) = (denom‘𝑄))) | ||
| Theorem | divnumden2 32817 | Calculate the reduced form of a quotient using gcd. This version extends divnumden 16785 for the negative integers. (Contributed by Thierry Arnoux, 25-Oct-2017.) |
| ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → ((numer‘(𝐴 / 𝐵)) = -(𝐴 / (𝐴 gcd 𝐵)) ∧ (denom‘(𝐴 / 𝐵)) = -(𝐵 / (𝐴 gcd 𝐵)))) | ||
| Theorem | expgt0b 32818 | A real number 𝐴 raised to an odd integer power is positive iff it is positive. (Contributed by SN, 4-Mar-2023.) Use the more standard ¬ 2 ∥ 𝑁 (Revised by Thierry Arnoux, 14-Jun-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → ¬ 2 ∥ 𝑁) ⇒ ⊢ (𝜑 → (0 < 𝐴 ↔ 0 < (𝐴↑𝑁))) | ||
| Theorem | nn0split01 32819 | Split 0 and 1 from the nonnegative integers. (Contributed by Thierry Arnoux, 8-Jun-2025.) |
| ⊢ ℕ0 = ({0, 1} ∪ (ℤ≥‘2)) | ||
| Theorem | nn0disj01 32820 | The pair {0, 1} does not overlap the rest of the nonnegative integers. (Contributed by Thierry Arnoux, 8-Jun-2025.) |
| ⊢ ({0, 1} ∩ (ℤ≥‘2)) = ∅ | ||
| Theorem | nnindf 32821* | Principle of Mathematical Induction, using a bound-variable hypothesis instead of distinct variables. (Contributed by Thierry Arnoux, 6-May-2018.) |
| ⊢ Ⅎ𝑦𝜑 & ⊢ (𝑥 = 1 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑦 ∈ ℕ → (𝜒 → 𝜃)) ⇒ ⊢ (𝐴 ∈ ℕ → 𝜏) | ||
| Theorem | nn0min 32822* | Extracting the minimum positive integer for which a property 𝜒 does not hold. This uses substitutions similar to nn0ind 12713. (Contributed by Thierry Arnoux, 6-May-2018.) |
| ⊢ (𝑛 = 0 → (𝜓 ↔ 𝜒)) & ⊢ (𝑛 = 𝑚 → (𝜓 ↔ 𝜃)) & ⊢ (𝑛 = (𝑚 + 1) → (𝜓 ↔ 𝜏)) & ⊢ (𝜑 → ¬ 𝜒) & ⊢ (𝜑 → ∃𝑛 ∈ ℕ 𝜓) ⇒ ⊢ (𝜑 → ∃𝑚 ∈ ℕ0 (¬ 𝜃 ∧ 𝜏)) | ||
| Theorem | subne0nn 32823 | A nonnegative difference is positive if the two numbers are not equal. (Contributed by Thierry Arnoux, 17-Dec-2023.) |
| ⊢ (𝜑 → 𝑀 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℂ) & ⊢ (𝜑 → (𝑀 − 𝑁) ∈ ℕ0) & ⊢ (𝜑 → 𝑀 ≠ 𝑁) ⇒ ⊢ (𝜑 → (𝑀 − 𝑁) ∈ ℕ) | ||
| Theorem | ltesubnnd 32824 | Subtracting an integer number from another number decreases it. See ltsubrpd 13109. (Contributed by Thierry Arnoux, 18-Apr-2017.) |
| ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → ((𝑀 + 1) − 𝑁) ≤ 𝑀) | ||
| Theorem | fprodeq02 32825* | If one of the factors is zero the product is zero. (Contributed by Thierry Arnoux, 11-Dec-2021.) |
| ⊢ (𝑘 = 𝐾 → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐾 ∈ 𝐴) & ⊢ (𝜑 → 𝐶 = 0) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = 0) | ||
| Theorem | pr01ssre 32826 | The range of the indicator function is a subset of ℝ. (Contributed by Thierry Arnoux, 14-Aug-2017.) |
| ⊢ {0, 1} ⊆ ℝ | ||
| Theorem | fprodex01 32827* | 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 32828* | A product over a pair is the product of the elements. (Contributed by Thierry Arnoux, 1-Jan-2022.) |
| ⊢ (𝑘 = 𝐴 → 𝐷 = 𝐸) & ⊢ (𝑘 = 𝐵 → 𝐷 = 𝐹) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐸 ∈ ℂ) & ⊢ (𝜑 → 𝐹 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ {𝐴, 𝐵}𝐷 = (𝐸 · 𝐹)) | ||
| Theorem | prodtp 32829* | A product over a triple is the product of the elements. (Contributed by Thierry Arnoux, 1-Jan-2022.) |
| ⊢ (𝑘 = 𝐴 → 𝐷 = 𝐸) & ⊢ (𝑘 = 𝐵 → 𝐷 = 𝐹) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐸 ∈ ℂ) & ⊢ (𝜑 → 𝐹 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝑘 = 𝐶 → 𝐷 = 𝐺) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐺 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐶) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ {𝐴, 𝐵, 𝐶}𝐷 = ((𝐸 · 𝐹) · 𝐺)) | ||
| Theorem | fsumub 32830* | An upper bound for a term of a positive finite sum. (Contributed by Thierry Arnoux, 27-Dec-2021.) |
| ⊢ (𝑘 = 𝐾 → 𝐵 = 𝐷) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = 𝐶) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐾 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐷 ≤ 𝐶) | ||
| Theorem | fsumiunle 32831* | 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 32832 | Split the hundreds from a decimal value. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ ;;𝐴𝐵𝐶 = ((;;100 · 𝐴) + ;𝐵𝐶) | ||
| Theorem | nexple 32833 | A lower bound for an exponentiation. (Contributed by Thierry Arnoux, 19-Aug-2017.) |
| ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵) → 𝐴 ≤ (𝐵↑𝐴)) | ||
| Theorem | 2exple2exp 32834* | If a nonnegative integer 𝑋 is a multiple of a power of two, but less than the next power of two, it is itself a power of two. (Contributed by Thierry Arnoux, 19-Oct-2025.) |
| ⊢ (𝜑 → 𝑋 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ (𝜑 → (2↑𝐾) ∥ 𝑋) & ⊢ (𝜑 → 𝑋 ≤ (2↑(𝐾 + 1))) ⇒ ⊢ (𝜑 → ∃𝑛 ∈ ℕ0 𝑋 = (2↑𝑛)) | ||
| Syntax | cind 32835 | Extend class notation with the indicator function generator. |
| class 𝟭 | ||
| Definition | df-ind 32836* | Define the indicator function generator. (Contributed by Thierry Arnoux, 20-Jan-2017.) |
| ⊢ 𝟭 = (𝑜 ∈ V ↦ (𝑎 ∈ 𝒫 𝑜 ↦ (𝑥 ∈ 𝑜 ↦ if(𝑥 ∈ 𝑎, 1, 0)))) | ||
| Theorem | indv 32837* | Value of the indicator function generator with domain 𝑂. (Contributed by Thierry Arnoux, 23-Aug-2017.) |
| ⊢ (𝑂 ∈ 𝑉 → (𝟭‘𝑂) = (𝑎 ∈ 𝒫 𝑂 ↦ (𝑥 ∈ 𝑂 ↦ if(𝑥 ∈ 𝑎, 1, 0)))) | ||
| Theorem | indval 32838* | Value of the indicator function generator for a set 𝐴 and a domain 𝑂. (Contributed by Thierry Arnoux, 2-Feb-2017.) |
| ⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂) → ((𝟭‘𝑂)‘𝐴) = (𝑥 ∈ 𝑂 ↦ if(𝑥 ∈ 𝐴, 1, 0))) | ||
| Theorem | indval2 32839 | Alternate value of the indicator function generator. (Contributed by Thierry Arnoux, 2-Feb-2017.) |
| ⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂) → ((𝟭‘𝑂)‘𝐴) = ((𝐴 × {1}) ∪ ((𝑂 ∖ 𝐴) × {0}))) | ||
| Theorem | indf 32840 | An indicator function as a function with domain and codomain. (Contributed by Thierry Arnoux, 13-Aug-2017.) |
| ⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂) → ((𝟭‘𝑂)‘𝐴):𝑂⟶{0, 1}) | ||
| Theorem | indfval 32841 | Value of the indicator function. (Contributed by Thierry Arnoux, 13-Aug-2017.) |
| ⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝑂) → (((𝟭‘𝑂)‘𝐴)‘𝑋) = if(𝑋 ∈ 𝐴, 1, 0)) | ||
| Theorem | ind1 32842 | Value of the indicator function where it is 1. (Contributed by Thierry Arnoux, 14-Aug-2017.) |
| ⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝐴) → (((𝟭‘𝑂)‘𝐴)‘𝑋) = 1) | ||
| Theorem | ind0 32843 | Value of the indicator function where it is 0. (Contributed by Thierry Arnoux, 14-Aug-2017.) |
| ⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ (𝑂 ∖ 𝐴)) → (((𝟭‘𝑂)‘𝐴)‘𝑋) = 0) | ||
| Theorem | ind1a 32844 | Value of the indicator function where it is 1. (Contributed by Thierry Arnoux, 22-Aug-2017.) |
| ⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝑂) → ((((𝟭‘𝑂)‘𝐴)‘𝑋) = 1 ↔ 𝑋 ∈ 𝐴)) | ||
| Theorem | indpi1 32845 | Preimage of the singleton {1} by the indicator function. See i1f1lem 25724. (Contributed by Thierry Arnoux, 21-Aug-2017.) |
| ⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂) → (◡((𝟭‘𝑂)‘𝐴) “ {1}) = 𝐴) | ||
| Theorem | indsum 32846* | Finite sum of a product with the indicator function / Cartesian product with the indicator function. (Contributed by Thierry Arnoux, 14-Aug-2017.) |
| ⊢ (𝜑 → 𝑂 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ 𝑂) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑂) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑥 ∈ 𝑂 ((((𝟭‘𝑂)‘𝐴)‘𝑥) · 𝐵) = Σ𝑥 ∈ 𝐴 𝐵) | ||
| Theorem | indsumin 32847* | Finite sum of a product with the indicator function / Cartesian product with the indicator function. (Contributed by Thierry Arnoux, 11-Dec-2021.) |
| ⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ 𝑂) & ⊢ (𝜑 → 𝐵 ⊆ 𝑂) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 ((((𝟭‘𝑂)‘𝐵)‘𝑘) · 𝐶) = Σ𝑘 ∈ (𝐴 ∩ 𝐵)𝐶) | ||
| Theorem | prodindf 32848* | The product of indicators is one if and only if all values are in the set. (Contributed by Thierry Arnoux, 11-Dec-2021.) |
| ⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ⊆ 𝑂) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑂) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 (((𝟭‘𝑂)‘𝐵)‘(𝐹‘𝑘)) = if(ran 𝐹 ⊆ 𝐵, 1, 0)) | ||
| Theorem | indf1o 32849 | The bijection between a power set and the set of indicator functions. (Contributed by Thierry Arnoux, 14-Aug-2017.) |
| ⊢ (𝑂 ∈ 𝑉 → (𝟭‘𝑂):𝒫 𝑂–1-1-onto→({0, 1} ↑m 𝑂)) | ||
| Theorem | indpreima 32850 | A function with range {0, 1} as an indicator of the preimage of {1}. (Contributed by Thierry Arnoux, 23-Aug-2017.) |
| ⊢ ((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) → 𝐹 = ((𝟭‘𝑂)‘(◡𝐹 “ {1}))) | ||
| Theorem | indf1ofs 32851* | The bijection between finite subsets and the indicator functions with finite support. (Contributed by Thierry Arnoux, 22-Aug-2017.) |
| ⊢ (𝑂 ∈ 𝑉 → ((𝟭‘𝑂) ↾ Fin):(𝒫 𝑂 ∩ Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑m 𝑂) ∣ (◡𝑓 “ {1}) ∈ Fin}) | ||
| Theorem | indsupp 32852 | The support of the indicator function. (Contributed by Thierry Arnoux, 13-Oct-2025.) |
| ⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂) → (((𝟭‘𝑂)‘𝐴) supp 0) = 𝐴) | ||
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 32853 | Constant used for decimal fraction constructor. See df-dp2 32854. |
| class _𝐴𝐵 | ||
| Definition | df-dp2 32854 | Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12734. (Contributed by David A. Wheeler, 15-May-2015.) (Revised by AV, 9-Sep-2021.) |
| ⊢ _𝐴𝐵 = (𝐴 + (𝐵 / ;10)) | ||
| Theorem | dp2eq1 32855 | Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.) |
| ⊢ (𝐴 = 𝐵 → _𝐴𝐶 = _𝐵𝐶) | ||
| Theorem | dp2eq2 32856 | Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.) |
| ⊢ (𝐴 = 𝐵 → _𝐶𝐴 = _𝐶𝐵) | ||
| Theorem | dp2eq1i 32857 | Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ _𝐴𝐶 = _𝐵𝐶 | ||
| Theorem | dp2eq2i 32858 | Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ _𝐶𝐴 = _𝐶𝐵 | ||
| Theorem | dp2eq12i 32859 | Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.) |
| ⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ _𝐴𝐶 = _𝐵𝐷 | ||
| Theorem | dp20u 32860 | Add a zero in the tenths (lower) place. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
| ⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ _𝐴0 = 𝐴 | ||
| Theorem | dp20h 32861 | Add a zero in the unit places. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
| ⊢ 𝐴 ∈ ℝ+ ⇒ ⊢ _0𝐴 = (𝐴 / ;10) | ||
| Theorem | dp2cl 32862 | Closure for the decimal fraction constructor if both values are reals. (Contributed by David A. Wheeler, 15-May-2015.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → _𝐴𝐵 ∈ ℝ) | ||
| Theorem | dp2clq 32863 | Closure for a decimal fraction. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℚ ⇒ ⊢ _𝐴𝐵 ∈ ℚ | ||
| Theorem | rpdp2cl 32864 | Closure for a decimal fraction in the positive real numbers. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ ⇒ ⊢ _𝐴𝐵 ∈ ℝ+ | ||
| Theorem | rpdp2cl2 32865 | Closure for a decimal fraction with no decimal expansion in the positive real numbers. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
| ⊢ 𝐴 ∈ ℕ ⇒ ⊢ _𝐴0 ∈ ℝ+ | ||
| Theorem | dp2lt10 32866 | Decimal fraction builds real numbers less than 10. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ & ⊢ 𝐴 < ;10 & ⊢ 𝐵 < ;10 ⇒ ⊢ _𝐴𝐵 < ;10 | ||
| Theorem | dp2lt 32867 | Comparing two decimal fractions (equal unit places). (Contributed by Thierry Arnoux, 16-Dec-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ & ⊢ 𝐶 ∈ ℝ+ & ⊢ 𝐵 < 𝐶 ⇒ ⊢ _𝐴𝐵 < _𝐴𝐶 | ||
| Theorem | dp2ltsuc 32868 | Comparing a decimal fraction with the next integer. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ & ⊢ 𝐵 < ;10 & ⊢ (𝐴 + 1) = 𝐶 ⇒ ⊢ _𝐴𝐵 < 𝐶 | ||
| Theorem | dp2ltc 32869 | 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 32871 and df-dp2 32854 for more information; dpval2 32875 and dpfrac1 32874 provide a more convenient way to obtain a value. This is intentionally similar to df-dec 12734. | ||
| Syntax | cdp 32870 | Decimal point operator. See df-dp 32871. |
| class . | ||
| Definition | df-dp 32871* |
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 32872 | Define the value of the decimal point operator. See df-dp 32871. (Contributed by David A. Wheeler, 15-May-2015.) |
| ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ) → (𝐴.𝐵) = _𝐴𝐵) | ||
| Theorem | dpcl 32873 | Prove that the closure of the decimal point is ℝ as we have defined it. See df-dp 32871. (Contributed by David A. Wheeler, 15-May-2015.) |
| ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ) → (𝐴.𝐵) ∈ ℝ) | ||
| Theorem | dpfrac1 32874 | Prove a simple equivalence involving the decimal point. See df-dp 32871 and dpcl 32873. (Contributed by David A. Wheeler, 15-May-2015.) (Revised by AV, 9-Sep-2021.) |
| ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ) → (𝐴.𝐵) = (;𝐴𝐵 / ;10)) | ||
| Theorem | dpval2 32875 | Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴.𝐵) = (𝐴 + (𝐵 / ;10)) | ||
| Theorem | dpval3 32876 | Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴.𝐵) = _𝐴𝐵 | ||
| Theorem | dpmul10 32877 | Multiply by 10 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((𝐴.𝐵) · ;10) = ;𝐴𝐵 | ||
| Theorem | decdiv10 32878 | Divide a decimal number by 10. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (;𝐴𝐵 / ;10) = (𝐴.𝐵) | ||
| Theorem | dpmul100 32879 | Multiply by 100 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ ((𝐴._𝐵𝐶) · ;;100) = ;;𝐴𝐵𝐶 | ||
| Theorem | dp3mul10 32880 | Multiply by 10 a decimal expansion with 3 digits. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ ((𝐴._𝐵𝐶) · ;10) = (;𝐴𝐵.𝐶) | ||
| Theorem | dpmul1000 32881 | Multiply by 1000 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℝ ⇒ ⊢ ((𝐴._𝐵_𝐶𝐷) · ;;;1000) = ;;;𝐴𝐵𝐶𝐷 | ||
| Theorem | dpval3rp 32882 | Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ ⇒ ⊢ (𝐴.𝐵) = _𝐴𝐵 | ||
| Theorem | dp0u 32883 | Add a zero in the tenths place. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
| ⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ (𝐴.0) = 𝐴 | ||
| Theorem | dp0h 32884 | Remove a zero in the units places. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
| ⊢ 𝐴 ∈ ℝ+ ⇒ ⊢ (0.𝐴) = (𝐴 / ;10) | ||
| Theorem | rpdpcl 32885 | Closure of the decimal point in the positive real numbers. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ ⇒ ⊢ (𝐴.𝐵) ∈ ℝ+ | ||
| Theorem | dplt 32886 | Comparing two decimal expansions (equal higher places). (Contributed by Thierry Arnoux, 16-Dec-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ & ⊢ 𝐶 ∈ ℝ+ & ⊢ 𝐵 < 𝐶 ⇒ ⊢ (𝐴.𝐵) < (𝐴.𝐶) | ||
| Theorem | dplti 32887 | Comparing a decimal expansions with the next higher integer. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐵 < ;10 & ⊢ (𝐴 + 1) = 𝐶 ⇒ ⊢ (𝐴.𝐵) < 𝐶 | ||
| Theorem | dpgti 32888 | Comparing a decimal expansions with the next lower integer. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ ⇒ ⊢ 𝐴 < (𝐴.𝐵) | ||
| Theorem | dpltc 32889 | Comparing two decimal integers (unequal higher places). (Contributed by Thierry Arnoux, 16-Dec-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℝ+ & ⊢ 𝐴 < 𝐶 & ⊢ 𝐵 < ;10 ⇒ ⊢ (𝐴.𝐵) < (𝐶.𝐷) | ||
| Theorem | dpexpp1 32890 | 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 32891 | Multiply by 10 a decimal expansion which starts with a zero. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ ⇒ ⊢ ((0._𝐴𝐵) · ;10) = (𝐴.𝐵) | ||
| Theorem | dpadd2 32892 | Addition with one decimal, no carry. (Contributed by Thierry Arnoux, 29-Dec-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℝ+ & ⊢ 𝐸 ∈ ℕ0 & ⊢ 𝐹 ∈ ℝ+ & ⊢ 𝐺 ∈ ℕ0 & ⊢ 𝐻 ∈ ℕ0 & ⊢ (𝐺 + 𝐻) = 𝐼 & ⊢ ((𝐴.𝐵) + (𝐶.𝐷)) = (𝐸.𝐹) ⇒ ⊢ ((𝐺._𝐴𝐵) + (𝐻._𝐶𝐷)) = (𝐼._𝐸𝐹) | ||
| Theorem | dpadd 32893 | Addition with one decimal. (Contributed by Thierry Arnoux, 27-Dec-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐸 ∈ ℕ0 & ⊢ 𝐹 ∈ ℕ0 & ⊢ (;𝐴𝐵 + ;𝐶𝐷) = ;𝐸𝐹 ⇒ ⊢ ((𝐴.𝐵) + (𝐶.𝐷)) = (𝐸.𝐹) | ||
| Theorem | dpadd3 32894 | Addition with two decimals. (Contributed by Thierry Arnoux, 27-Dec-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐸 ∈ ℕ0 & ⊢ 𝐺 ∈ ℕ0 & ⊢ 𝐹 ∈ ℕ0 & ⊢ 𝐻 ∈ ℕ0 & ⊢ 𝐼 ∈ ℕ0 & ⊢ (;;𝐴𝐵𝐶 + ;;𝐷𝐸𝐹) = ;;𝐺𝐻𝐼 ⇒ ⊢ ((𝐴._𝐵𝐶) + (𝐷._𝐸𝐹)) = (𝐺._𝐻𝐼) | ||
| Theorem | dpmul 32895 | Multiplication with one decimal point. (Contributed by Thierry Arnoux, 26-Dec-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐸 ∈ ℕ0 & ⊢ 𝐺 ∈ ℕ0 & ⊢ 𝐽 ∈ ℕ0 & ⊢ 𝐾 ∈ ℕ0 & ⊢ (𝐴 · 𝐶) = 𝐹 & ⊢ (𝐴 · 𝐷) = 𝑀 & ⊢ (𝐵 · 𝐶) = 𝐿 & ⊢ (𝐵 · 𝐷) = ;𝐸𝐾 & ⊢ ((𝐿 + 𝑀) + 𝐸) = ;𝐺𝐽 & ⊢ (𝐹 + 𝐺) = 𝐼 ⇒ ⊢ ((𝐴.𝐵) · (𝐶.𝐷)) = (𝐼._𝐽𝐾) | ||
| Theorem | dpmul4 32896 | 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 32897 | Example theorem demonstrating decimal expansions. (Contributed by Thierry Arnoux, 27-Dec-2021.) |
| ⊢ (3 / 2) = (1.5) | ||
| Theorem | 1mhdrd 32898 | Example theorem demonstrating decimal expansions. (Contributed by Thierry Arnoux, 27-Dec-2021.) |
| ⊢ ((0._99) + (0._01)) = 1 | ||
| Syntax | cxdiv 32899 | Extend class notation to include division of extended reals. |
| class /𝑒 | ||
| Definition | df-xdiv 32900* | Define division over extended real numbers. (Contributed by Thierry Arnoux, 17-Dec-2016.) |
| ⊢ /𝑒 = (𝑥 ∈ ℝ*, 𝑦 ∈ (ℝ ∖ {0}) ↦ (℩𝑧 ∈ ℝ* (𝑦 ·e 𝑧) = 𝑥)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |