Home | Metamath
Proof Explorer Theorem List (p. 305 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-28622) |
Hilbert Space Explorer
(28623-30145) |
Users' Mathboxes
(30146-44834) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lt2addrd 30401* | If the right-hand side of a 'less than' relationship is an addition, then we can express the left-hand side as an addition, too, where each term is respectively less than each term of the original right side. (Contributed by Thierry Arnoux, 15-Mar-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < (𝐵 + 𝐶)) ⇒ ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ (𝐴 = (𝑏 + 𝑐) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶)) | ||
Theorem | xrlelttric 30402 | Trichotomy law for extended reals. (Contributed by Thierry Arnoux, 12-Sep-2017.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ∨ 𝐵 < 𝐴)) | ||
Theorem | xaddeq0 30403 | Two extended reals which add up to zero are each other's negatives. (Contributed by Thierry Arnoux, 13-Jun-2017.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((𝐴 +𝑒 𝐵) = 0 ↔ 𝐴 = -𝑒𝐵)) | ||
Theorem | xrinfm 30404 | The extended real numbers are unbounded below. (Contributed by Thierry Arnoux, 18-Feb-2018.) (Revised by AV, 28-Sep-2020.) |
⊢ inf(ℝ*, ℝ*, < ) = -∞ | ||
Theorem | le2halvesd 30405 | A sum is less than the whole if each term is less than half. (Contributed by Thierry Arnoux, 29-Nov-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ (𝐶 / 2)) & ⊢ (𝜑 → 𝐵 ≤ (𝐶 / 2)) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ≤ 𝐶) | ||
Theorem | xraddge02 30406 | A number is less than or equal to itself plus a nonnegative number. (Contributed by Thierry Arnoux, 28-Dec-2016.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (0 ≤ 𝐵 → 𝐴 ≤ (𝐴 +𝑒 𝐵))) | ||
Theorem | xrge0addge 30407 | A number is less than or equal to itself plus a nonnegative number. (Contributed by Thierry Arnoux, 19-Jul-2020.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ (0[,]+∞)) → 𝐴 ≤ (𝐴 +𝑒 𝐵)) | ||
Theorem | xlt2addrd 30408* | If the right-hand side of a 'less than' relationship is an addition, then we can express the left-hand side as an addition, too, where each term is respectively less than each term of the original right side. (Contributed by Thierry Arnoux, 15-Mar-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ≠ -∞) & ⊢ (𝜑 → 𝐶 ≠ -∞) & ⊢ (𝜑 → 𝐴 < (𝐵 +𝑒 𝐶)) ⇒ ⊢ (𝜑 → ∃𝑏 ∈ ℝ* ∃𝑐 ∈ ℝ* (𝐴 = (𝑏 +𝑒 𝑐) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶)) | ||
Theorem | xrsupssd 30409 | Inequality deduction for supremum of an extended real subset. (Contributed by Thierry Arnoux, 21-Mar-2017.) |
⊢ (𝜑 → 𝐵 ⊆ 𝐶) & ⊢ (𝜑 → 𝐶 ⊆ ℝ*) ⇒ ⊢ (𝜑 → sup(𝐵, ℝ*, < ) ≤ sup(𝐶, ℝ*, < )) | ||
Theorem | xrge0infss 30410* | Any subset of nonnegative extended reals has an infimum. (Contributed by Thierry Arnoux, 16-Sep-2019.) (Revised by AV, 4-Oct-2020.) |
⊢ (𝐴 ⊆ (0[,]+∞) → ∃𝑥 ∈ (0[,]+∞)(∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ (0[,]+∞)(𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) | ||
Theorem | xrge0infssd 30411 | Inequality deduction for infimum of a nonnegative extended real subset. (Contributed by Thierry Arnoux, 16-Sep-2019.) (Revised by AV, 4-Oct-2020.) |
⊢ (𝜑 → 𝐶 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 ⊆ (0[,]+∞)) ⇒ ⊢ (𝜑 → inf(𝐵, (0[,]+∞), < ) ≤ inf(𝐶, (0[,]+∞), < )) | ||
Theorem | xrge0addcld 30412 | Nonnegative extended reals are closed under addition. (Contributed by Thierry Arnoux, 16-Sep-2019.) |
⊢ (𝜑 → 𝐴 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐵 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → (𝐴 +𝑒 𝐵) ∈ (0[,]+∞)) | ||
Theorem | xrge0subcld 30413 | Condition for closure of nonnegative extended reals under subtraction. (Contributed by Thierry Arnoux, 27-May-2020.) |
⊢ (𝜑 → 𝐴 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐵 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐵 ≤ 𝐴) ⇒ ⊢ (𝜑 → (𝐴 +𝑒 -𝑒𝐵) ∈ (0[,]+∞)) | ||
Theorem | infxrge0lb 30414 | A member of a set of nonnegative extended reals is greater than or equal to the set's infimum. (Contributed by Thierry Arnoux, 19-Jul-2020.) (Revised by AV, 4-Oct-2020.) |
⊢ (𝜑 → 𝐴 ⊆ (0[,]+∞)) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → inf(𝐴, (0[,]+∞), < ) ≤ 𝐵) | ||
Theorem | infxrge0glb 30415* | The infimum of a set of nonnegative extended reals is the greatest lower bound. (Contributed by Thierry Arnoux, 19-Jul-2020.) (Revised by AV, 4-Oct-2020.) |
⊢ (𝜑 → 𝐴 ⊆ (0[,]+∞)) & ⊢ (𝜑 → 𝐵 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → (inf(𝐴, (0[,]+∞), < ) < 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑥 < 𝐵)) | ||
Theorem | infxrge0gelb 30416* | The infimum of a set of nonnegative extended reals is greater than or equal to a lower bound. (Contributed by Thierry Arnoux, 19-Jul-2020.) (Revised by AV, 4-Oct-2020.) |
⊢ (𝜑 → 𝐴 ⊆ (0[,]+∞)) & ⊢ (𝜑 → 𝐵 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → (𝐵 ≤ inf(𝐴, (0[,]+∞), < ) ↔ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑥)) | ||
Theorem | dfrp2 30417 | Alternate definition of the positive real numbers. (Contributed by Thierry Arnoux, 4-May-2020.) |
⊢ ℝ+ = (0(,)+∞) | ||
Theorem | xrofsup 30418 | 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(𝑌, ℝ*, < ))) | ||
Theorem | supxrnemnf 30419 | 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(𝐴, ℝ*, < ) ≠ -∞) | ||
Theorem | xnn0gt0 30420 | Nonzero extended nonnegative integers are strictly greater than zero. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
⊢ ((𝑁 ∈ ℕ0* ∧ 𝑁 ≠ 0) → 0 < 𝑁) | ||
Theorem | xnn01gt 30421 | 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 < 𝑁)) | ||
Theorem | nn0xmulclb 30422 | Finite multiplication in the extended nonnegative integers. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
⊢ (((𝐴 ∈ ℕ0* ∧ 𝐵 ∈ ℕ0*) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ((𝐴 ·e 𝐵) ∈ ℕ0 ↔ (𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0))) | ||
Theorem | joiniooico 30423 | 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.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶)) → (((𝐴(,)𝐵) ∩ (𝐵[,)𝐶)) = ∅ ∧ ((𝐴(,)𝐵) ∪ (𝐵[,)𝐶)) = (𝐴(,)𝐶))) | ||
Theorem | ubico 30424 | A right-open interval does not contain its right endpoint. (Contributed by Thierry Arnoux, 5-Apr-2017.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) → ¬ 𝐵 ∈ (𝐴[,)𝐵)) | ||
Theorem | xeqlelt 30425 | Equality in terms of 'less than or equal to', 'less than'. (Contributed by Thierry Arnoux, 5-Jul-2017.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ ¬ 𝐴 < 𝐵))) | ||
Theorem | eliccelico 30426 | 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.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ (𝐴[,)𝐵) ∨ 𝐶 = 𝐵))) | ||
Theorem | elicoelioo 30427 | 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.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 = 𝐴 ∨ 𝐶 ∈ (𝐴(,)𝐵)))) | ||
Theorem | iocinioc2 30428 | Intersection between two open-below, closed-above intervals sharing the same upper bound. (Contributed by Thierry Arnoux, 7-Aug-2017.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → ((𝐴(,]𝐶) ∩ (𝐵(,]𝐶)) = (𝐵(,]𝐶)) | ||
Theorem | xrdifh 30429 | Class difference of a half-open interval in the extended reals. (Contributed by Thierry Arnoux, 1-Aug-2017.) |
⊢ 𝐴 ∈ ℝ* ⇒ ⊢ (ℝ* ∖ (𝐴[,]+∞)) = (-∞[,)𝐴) | ||
Theorem | iocinif 30430 | 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(𝐴 < 𝐵, (𝐵(,]𝐶), (𝐴(,]𝐶))) | ||
Theorem | difioo 30431 | The difference between two open intervals sharing the same lower bound. (Contributed by Thierry Arnoux, 26-Sep-2017.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 < 𝐵) → ((𝐴(,)𝐶) ∖ (𝐴(,)𝐵)) = (𝐵[,)𝐶)) | ||
Theorem | difico 30432 | The difference between two closed-below, open-above intervals sharing the same upper bound. (Contributed by Thierry Arnoux, 13-Oct-2017.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶)) → ((𝐴[,)𝐶) ∖ (𝐵[,)𝐶)) = (𝐴[,)𝐵)) | ||
Theorem | uzssico 30433 | Upper integer sets are a subset of the corresponding closed-below, open-above intervals. (Contributed by Thierry Arnoux, 29-Dec-2021.) |
⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ⊆ (𝑀[,)+∞)) | ||
Theorem | fz2ssnn0 30434 | A finite set of sequential integers that is a subset of ℕ0. (Contributed by Thierry Arnoux, 8-Dec-2021.) |
⊢ (𝑀 ∈ ℕ0 → (𝑀...𝑁) ⊆ ℕ0) | ||
Theorem | nndiffz1 30435 | Upper set of the positive integers. (Contributed by Thierry Arnoux, 22-Aug-2017.) |
⊢ (𝑁 ∈ ℕ0 → (ℕ ∖ (1...𝑁)) = (ℤ≥‘(𝑁 + 1))) | ||
Theorem | ssnnssfz 30436* | 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 30437 | Elementhood in a finite set of sequential integers, except its lower bound. (Contributed by Thierry Arnoux, 1-Jan-2024.) |
⊢ ((𝐾 ∈ (𝑀...𝑁) ∧ 𝐾 ≠ 𝑀) → 𝐾 ∈ ((𝑀 + 1)...𝑁)) | ||
Theorem | fzm1ne1 30438 | Elementhood of an integer and its predecessor in finite intervals of integers. (Contributed by Thierry Arnoux, 1-Jan-2024.) |
⊢ ((𝐾 ∈ (𝑀...𝑁) ∧ 𝐾 ≠ 𝑀) → (𝐾 − 1) ∈ (𝑀...(𝑁 − 1))) | ||
Theorem | fzspl 30439 | Split the last element of a finite set of sequential integers. (more generic than fzsuc 12942) (Contributed by Thierry Arnoux, 7-Nov-2016.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) = ((𝑀...(𝑁 − 1)) ∪ {𝑁})) | ||
Theorem | fzdif2 30440 | Split the last element of a finite set of sequential integers. (more generic than fzsuc 12942) (Contributed by Thierry Arnoux, 22-Aug-2020.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((𝑀...𝑁) ∖ {𝑁}) = (𝑀...(𝑁 − 1))) | ||
Theorem | fzodif2 30441 | Split the last element of a half-open range of sequential integers. (Contributed by Thierry Arnoux, 5-Dec-2021.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((𝑀..^(𝑁 + 1)) ∖ {𝑁}) = (𝑀..^𝑁)) | ||
Theorem | fzodif1 30442 | Set difference of two half-open range of sequential integers sharing the same starting value. (Contributed by Thierry Arnoux, 2-Oct-2023.) |
⊢ (𝐾 ∈ (𝑀...𝑁) → ((𝑀..^𝑁) ∖ (𝑀..^𝐾)) = (𝐾..^𝑁)) | ||
Theorem | fzsplit3 30443 | Split a finite interval of integers into two parts. (Contributed by Thierry Arnoux, 2-May-2017.) |
⊢ (𝐾 ∈ (𝑀...𝑁) → (𝑀...𝑁) = ((𝑀...(𝐾 − 1)) ∪ (𝐾...𝑁))) | ||
Theorem | bcm1n 30444 | 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 30445* | Rewrite a countable union as a disjoint union, finite version. Cf. iundisj 24076. (Contributed by Thierry Arnoux, 15-Feb-2017.) |
⊢ Ⅎ𝑛𝐵 & ⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵) ⇒ ⊢ ∪ 𝑛 ∈ (1..^𝑁)𝐴 = ∪ 𝑛 ∈ (1..^𝑁)(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) | ||
Theorem | iundisj2fi 30446* | A disjoint union is disjoint, finite version. Cf. iundisj2 24077. (Contributed by Thierry Arnoux, 16-Feb-2017.) |
⊢ Ⅎ𝑛𝐵 & ⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵) ⇒ ⊢ Disj 𝑛 ∈ (1..^𝑁)(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) | ||
Theorem | iundisjcnt 30447* | Rewrite a countable union as a disjoint union. (Contributed by Thierry Arnoux, 16-Feb-2017.) |
⊢ Ⅎ𝑛𝐵 & ⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝑁 = ℕ ∨ 𝑁 = (1..^𝑀))) ⇒ ⊢ (𝜑 → ∪ 𝑛 ∈ 𝑁 𝐴 = ∪ 𝑛 ∈ 𝑁 (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) | ||
Theorem | iundisj2cnt 30448* | A countable disjoint union is disjoint. Cf. iundisj2 24077. (Contributed by Thierry Arnoux, 16-Feb-2017.) |
⊢ Ⅎ𝑛𝐵 & ⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝑁 = ℕ ∨ 𝑁 = (1..^𝑀))) ⇒ ⊢ (𝜑 → Disj 𝑛 ∈ 𝑁 (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)) | ||
Theorem | fzone1 30449 | Elementhood in a half-open interval, except its lower bound. (Contributed by Thierry Arnoux, 1-Jan-2024.) |
⊢ ((𝐾 ∈ (𝑀..^𝑁) ∧ 𝐾 ≠ 𝑀) → 𝐾 ∈ ((𝑀 + 1)..^𝑁)) | ||
Theorem | fzom1ne1 30450 | Elementhood in a half-open interval, except the lower bound, shifted by one. (Contributed by Thierry Arnoux, 1-Jan-2024.) |
⊢ ((𝐾 ∈ (𝑀..^𝑁) ∧ 𝐾 ≠ 𝑀) → (𝐾 − 1) ∈ (𝑀..^(𝑁 − 1))) | ||
Theorem | f1ocnt 30451* | 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 30447 or iundisj2cnt 30448. (Contributed by Thierry Arnoux, 25-Jul-2020.) |
⊢ (𝐴 ≼ ω → ∃𝑓(𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((♯‘𝐴) + 1))))) | ||
Theorem | fz1nnct 30452 | NN and integer ranges starting from 1 are countable. (Contributed by Thierry Arnoux, 25-Jul-2020.) |
⊢ ((𝐴 = ℕ ∨ 𝐴 = (1..^𝑀)) → 𝐴 ≼ ω) | ||
Theorem | fz1nntr 30453 | NN and integer ranges starting from 1 are a transitive family of set. (Contributed by Thierry Arnoux, 25-Jul-2020.) |
⊢ (((𝐴 = ℕ ∨ 𝐴 = (1..^𝑀)) ∧ 𝑁 ∈ 𝐴) → (1..^𝑁) ⊆ 𝐴) | ||
Theorem | hashunif 30454* | The cardinality of a disjoint finite union of finite sets. Cf. hashuni 15169. (Contributed by Thierry Arnoux, 17-Feb-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ Fin) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝑥) ⇒ ⊢ (𝜑 → (♯‘∪ 𝐴) = Σ𝑥 ∈ 𝐴 (♯‘𝑥)) | ||
Theorem | hashxpe 30455 | The size of the Cartesian product of two finite sets is the product of their sizes. This is a version of hashxp 13783 valid for infinite sets, which uses extended real numbers. (Contributed by Thierry Arnoux, 27-May-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (♯‘(𝐴 × 𝐵)) = ((♯‘𝐴) ·e (♯‘𝐵))) | ||
Theorem | hashgt1 30456 | Restate "set contains at least two elements" in terms of elementhood. (Contributed by Thierry Arnoux, 21-Nov-2023.) |
⊢ (𝐴 ∈ 𝑉 → (¬ 𝐴 ∈ (◡♯ “ {0, 1}) ↔ 1 < (♯‘𝐴))) | ||
Theorem | dvdszzq 30457 | Divisibility for an integer quotient. (Contributed by Thierry Arnoux, 17-Sep-2023.) |
⊢ 𝑁 = (𝐴 / 𝐵) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝑃 ∥ 𝐴) & ⊢ (𝜑 → ¬ 𝑃 ∥ 𝐵) ⇒ ⊢ (𝜑 → 𝑃 ∥ 𝑁) | ||
Theorem | prmdvdsbc 30458 | Condition for a prime number to divide a binomial coefficient. (Contributed by Thierry Arnoux, 17-Sep-2023.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑃 ∥ (𝑃C𝑁)) | ||
Theorem | numdenneg 30459 | Numerator and denominator of the negative. (Contributed by Thierry Arnoux, 27-Oct-2017.) |
⊢ (𝑄 ∈ ℚ → ((numer‘-𝑄) = -(numer‘𝑄) ∧ (denom‘-𝑄) = (denom‘𝑄))) | ||
Theorem | divnumden2 30460 | Calculate the reduced form of a quotient using gcd. This version extends divnumden 16076 for the negative integers. (Contributed by Thierry Arnoux, 25-Oct-2017.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → ((numer‘(𝐴 / 𝐵)) = -(𝐴 / (𝐴 gcd 𝐵)) ∧ (denom‘(𝐴 / 𝐵)) = -(𝐵 / (𝐴 gcd 𝐵)))) | ||
Theorem | nnindf 30461* | Principle of Mathematical Induction, using a bound-variable hypothesis instead of distinct variables. (Contributed by Thierry Arnoux, 6-May-2018.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝑥 = 1 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑦 ∈ ℕ → (𝜒 → 𝜃)) ⇒ ⊢ (𝐴 ∈ ℕ → 𝜏) | ||
Theorem | nnindd 30462* | Principle of Mathematical Induction (inference schema) on integers, a deduction version. (Contributed by Thierry Arnoux, 19-Jul-2020.) |
⊢ (𝑥 = 1 → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃)) & ⊢ (𝑥 = (𝑦 + 1) → (𝜓 ↔ 𝜏)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜂)) & ⊢ (𝜑 → 𝜒) & ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → 𝜂) | ||
Theorem | nn0min 30463* | 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 (¬ 𝜃 ∧ 𝜏)) | ||
Theorem | subne0nn 30464 | A nonnegative difference is positive if the two numbers are not equal. (Contributed by Thierry Arnoux, 17-Dec-2023.) |
⊢ (𝜑 → 𝑀 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℂ) & ⊢ (𝜑 → (𝑀 − 𝑁) ∈ ℕ0) & ⊢ (𝜑 → 𝑀 ≠ 𝑁) ⇒ ⊢ (𝜑 → (𝑀 − 𝑁) ∈ ℕ) | ||
Theorem | ltesubnnd 30465 | Subtracting an integer number from another number decreases it. See ltsubrpd 12451. (Contributed by Thierry Arnoux, 18-Apr-2017.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → ((𝑀 + 1) − 𝑁) ≤ 𝑀) | ||
Theorem | fprodeq02 30466* | If one of the factors is zero the product is zero. (Contributed by Thierry Arnoux, 11-Dec-2021.) |
⊢ (𝑘 = 𝐾 → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐾 ∈ 𝐴) & ⊢ (𝜑 → 𝐶 = 0) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = 0) | ||
Theorem | pr01ssre 30467 | The range of the indicator function is a subset of ℝ. (Contributed by Thierry Arnoux, 14-Aug-2017.) |
⊢ {0, 1} ⊆ ℝ | ||
Theorem | fprodex01 30468* | 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 30469* | A product over a pair is the product of the elements. (Contributed by Thierry Arnoux, 1-Jan-2022.) |
⊢ (𝑘 = 𝐴 → 𝐷 = 𝐸) & ⊢ (𝑘 = 𝐵 → 𝐷 = 𝐹) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐸 ∈ ℂ) & ⊢ (𝜑 → 𝐹 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ {𝐴, 𝐵}𝐷 = (𝐸 · 𝐹)) | ||
Theorem | prodtp 30470* | A product over a triple is the product of the elements. (Contributed by Thierry Arnoux, 1-Jan-2022.) |
⊢ (𝑘 = 𝐴 → 𝐷 = 𝐸) & ⊢ (𝑘 = 𝐵 → 𝐷 = 𝐹) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐸 ∈ ℂ) & ⊢ (𝜑 → 𝐹 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝑘 = 𝐶 → 𝐷 = 𝐺) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐺 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐶) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ {𝐴, 𝐵, 𝐶}𝐷 = ((𝐸 · 𝐹) · 𝐺)) | ||
Theorem | fsumub 30471* | An upper bound for a term of a positive finite sum. (Contributed by Thierry Arnoux, 27-Dec-2021.) |
⊢ (𝑘 = 𝐾 → 𝐵 = 𝐷) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = 𝐶) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐾 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐷 ≤ 𝐶) | ||
Theorem | fsumiunle 30472* | 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 30473 | 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 30474 | Constant used for decimal fraction constructor. See df-dp2 30475. |
class _𝐴𝐵 | ||
Definition | df-dp2 30475 | 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)) | ||
Theorem | dp2eq1 30476 | Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.) |
⊢ (𝐴 = 𝐵 → _𝐴𝐶 = _𝐵𝐶) | ||
Theorem | dp2eq2 30477 | Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.) |
⊢ (𝐴 = 𝐵 → _𝐶𝐴 = _𝐶𝐵) | ||
Theorem | dp2eq1i 30478 | Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ _𝐴𝐶 = _𝐵𝐶 | ||
Theorem | dp2eq2i 30479 | Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ _𝐶𝐴 = _𝐶𝐵 | ||
Theorem | dp2eq12i 30480 | Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ _𝐴𝐶 = _𝐵𝐷 | ||
Theorem | dp20u 30481 | Add a zero in the tenths (lower) place. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ _𝐴0 = 𝐴 | ||
Theorem | dp20h 30482 | Add a zero in the unit places. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℝ+ ⇒ ⊢ _0𝐴 = (𝐴 / ;10) | ||
Theorem | dp2cl 30483 | Closure for the decimal fraction constructor if both values are reals. (Contributed by David A. Wheeler, 15-May-2015.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → _𝐴𝐵 ∈ ℝ) | ||
Theorem | dp2clq 30484 | Closure for a decimal fraction. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℚ ⇒ ⊢ _𝐴𝐵 ∈ ℚ | ||
Theorem | rpdp2cl 30485 | Closure for a decimal fraction in the positive real numbers. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ ⇒ ⊢ _𝐴𝐵 ∈ ℝ+ | ||
Theorem | rpdp2cl2 30486 | Closure for a decimal fraction with no decimal expansion in the positive real numbers. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
⊢ 𝐴 ∈ ℕ ⇒ ⊢ _𝐴0 ∈ ℝ+ | ||
Theorem | dp2lt10 30487 | Decimal fraction builds real numbers less than 10. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ & ⊢ 𝐴 < ;10 & ⊢ 𝐵 < ;10 ⇒ ⊢ _𝐴𝐵 < ;10 | ||
Theorem | dp2lt 30488 | Comparing two decimal fractions (equal unit places). (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ & ⊢ 𝐶 ∈ ℝ+ & ⊢ 𝐵 < 𝐶 ⇒ ⊢ _𝐴𝐵 < _𝐴𝐶 | ||
Theorem | dp2ltsuc 30489 | Comparing a decimal fraction with the next integer. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ+ & ⊢ 𝐵 < ;10 & ⊢ (𝐴 + 1) = 𝐶 ⇒ ⊢ _𝐴𝐵 < 𝐶 | ||
Theorem | dp2ltc 30490 | 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 30492 and df-dp2 30475 for more information; dpval2 30496 and dpfrac1 30495 provide a more convenient way to obtain a value. This is intentionally similar to df-dec 12087. | ||
Syntax | cdp 30491 | Decimal point operator. See df-dp 30492. |
class . | ||
Definition | df-dp 30492* |
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 30493 | Define the value of the decimal point operator. See df-dp 30492. (Contributed by David A. Wheeler, 15-May-2015.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ) → (𝐴.𝐵) = _𝐴𝐵) | ||
Theorem | dpcl 30494 | Prove that the closure of the decimal point is ℝ as we have defined it. See df-dp 30492. (Contributed by David A. Wheeler, 15-May-2015.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ) → (𝐴.𝐵) ∈ ℝ) | ||
Theorem | dpfrac1 30495 | Prove a simple equivalence involving the decimal point. See df-dp 30492 and dpcl 30494. (Contributed by David A. Wheeler, 15-May-2015.) (Revised by AV, 9-Sep-2021.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ) → (𝐴.𝐵) = (;𝐴𝐵 / ;10)) | ||
Theorem | dpval2 30496 | Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴.𝐵) = (𝐴 + (𝐵 / ;10)) | ||
Theorem | dpval3 30497 | Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴.𝐵) = _𝐴𝐵 | ||
Theorem | dpmul10 30498 | Multiply by 10 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((𝐴.𝐵) · ;10) = ;𝐴𝐵 | ||
Theorem | decdiv10 30499 | Divide a decimal number by 10. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (;𝐴𝐵 / ;10) = (𝐴.𝐵) | ||
Theorem | dpmul100 30500 | Multiply by 100 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℝ ⇒ ⊢ ((𝐴._𝐵𝐶) · ;;100) = ;;𝐴𝐵𝐶 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |