![]() |
Metamath
Proof Explorer Theorem List (p. 464 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dmvolsal 46301 | Lebesgue measurable sets form a sigma-algebra. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ dom vol ∈ SAlg | ||
Theorem | saldifcld 46302 | The complement of an element of a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐸 ∈ 𝑆) ⇒ ⊢ (𝜑 → (∪ 𝑆 ∖ 𝐸) ∈ 𝑆) | ||
Theorem | saluncld 46303 | The union of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐸 ∈ 𝑆) & ⊢ (𝜑 → 𝐹 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐸 ∪ 𝐹) ∈ 𝑆) | ||
Theorem | salgencld 46304 | SalGen actually generates a sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ 𝑆 = (SalGen‘𝑋) ⇒ ⊢ (𝜑 → 𝑆 ∈ SAlg) | ||
Theorem | 0sald 46305 | The empty set belongs to every sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝑆 ∈ SAlg) ⇒ ⊢ (𝜑 → ∅ ∈ 𝑆) | ||
Theorem | iooborel 46306 | An open interval is a Borel set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐵 = (SalGen‘𝐽) ⇒ ⊢ (𝐴(,)𝐶) ∈ 𝐵 | ||
Theorem | salincld 46307 | The intersection of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐸 ∈ 𝑆) & ⊢ (𝜑 → 𝐹 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐸 ∩ 𝐹) ∈ 𝑆) | ||
Theorem | salunid 46308 | A set is an element of any sigma-algebra on it. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝑆 ∈ SAlg) ⇒ ⊢ (𝜑 → ∪ 𝑆 ∈ 𝑆) | ||
Theorem | unisalgen2 46309 | The union of a set belongs is equal to the union of the sigma-algebra generated by the set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ 𝑆 = (SalGen‘𝐴) ⇒ ⊢ (𝜑 → ∪ 𝑆 = ∪ 𝐴) | ||
Theorem | bor1sal 46310 | The Borel sigma-algebra on the Reals. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐵 = (SalGen‘𝐽) ⇒ ⊢ 𝐵 ∈ SAlg | ||
Theorem | iocborel 46311 | A left-open, right-closed interval is a Borel set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐵 = (SalGen‘𝐽) ⇒ ⊢ (𝜑 → (𝐴(,]𝐶) ∈ 𝐵) | ||
Theorem | subsaliuncllem 46312* | A subspace sigma-algebra is closed under countable union. This is Lemma 121A (iii) of [Fremlin1] p. 35. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) & ⊢ 𝐸 = (𝐻 ∘ 𝐺) & ⊢ (𝜑 → 𝐻 Fn ran 𝐺) & ⊢ (𝜑 → ∀𝑦 ∈ ran 𝐺(𝐻‘𝑦) ∈ 𝑦) ⇒ ⊢ (𝜑 → ∃𝑒 ∈ (𝑆 ↑m ℕ)∀𝑛 ∈ ℕ (𝐹‘𝑛) = ((𝑒‘𝑛) ∩ 𝐷)) | ||
Theorem | subsaliuncl 46313* | A subspace sigma-algebra is closed under countable union. This is Lemma 121A (iii) of [Fremlin1] p. 35. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ 𝑇 = (𝑆 ↾t 𝐷) & ⊢ (𝜑 → 𝐹:ℕ⟶𝑇) ⇒ ⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) ∈ 𝑇) | ||
Theorem | subsalsal 46314 | A subspace sigma-algebra is a sigma algebra. This is Lemma 121A of [Fremlin1] p. 35. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ 𝑇 = (𝑆 ↾t 𝐷) ⇒ ⊢ (𝜑 → 𝑇 ∈ SAlg) | ||
Theorem | subsaluni 46315 | A set belongs to the subspace sigma-algebra it induces. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝑆) ⇒ ⊢ (𝜑 → 𝐴 ∈ (𝑆 ↾t 𝐴)) | ||
Theorem | salrestss 46316 | A sigma-algebra restricted to one of its elements is a subset of the original sigma-algebra. (Contributed by Glauco Siliprandi, 21-Dec-2024.) |
⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐸 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑆 ↾t 𝐸) ⊆ 𝑆) | ||
Syntax | csumge0 46317 | Extend class notation to include the sum of nonnegative extended reals. |
class Σ^ | ||
Definition | df-sumge0 46318* | Define the arbitrary sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) $. |
⊢ Σ^ = (𝑥 ∈ V ↦ if(+∞ ∈ ran 𝑥, +∞, sup(ran (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)), ℝ*, < ))) | ||
Theorem | sge0rnre 46319* | When Σ^ is applied to nonnegative real numbers the range used in its definition is a subset of the reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐹:𝑋⟶(0[,)+∞)) ⇒ ⊢ (𝜑 → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ⊆ ℝ) | ||
Theorem | fge0icoicc 46320 | If 𝐹 maps to nonnegative reals, then 𝐹 maps to nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐹:𝑋⟶(0[,)+∞)) ⇒ ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) | ||
Theorem | sge0val 46321* | The value of the sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) → (Σ^‘𝐹) = if(+∞ ∈ ran 𝐹, +∞, sup(ran (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝐹‘𝑤)), ℝ*, < ))) | ||
Theorem | fge0npnf 46322 | If 𝐹 maps to nonnegative reals, then +∞ is not in its range. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐹:𝑋⟶(0[,)+∞)) ⇒ ⊢ (𝜑 → ¬ +∞ ∈ ran 𝐹) | ||
Theorem | sge0rnn0 46323* | The range used in the definition of Σ^ is not empty. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ≠ ∅ | ||
Theorem | sge0vald 46324* | The value of the sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) = if(+∞ ∈ ran 𝐹, +∞, sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, < ))) | ||
Theorem | fge0iccico 46325 | A range of nonnegative extended reals without plus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → ¬ +∞ ∈ ran 𝐹) ⇒ ⊢ (𝜑 → 𝐹:𝑋⟶(0[,)+∞)) | ||
Theorem | gsumge0cl 46326 | Closure of group sum, for finitely supported nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ 𝐺 = (ℝ*𝑠 ↾s (0[,]+∞)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → 𝐹 finSupp 0) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) ∈ (0[,]+∞)) | ||
Theorem | sge0reval 46327* | Value of the sum of nonnegative extended reals, when all terms in the sum are reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,)+∞)) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, < )) | ||
Theorem | sge0pnfval 46328 | If a term in the sum of nonnegative extended reals is +∞, then the value of the sum is +∞. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → +∞ ∈ ran 𝐹) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) = +∞) | ||
Theorem | fge0iccre 46329 | A range of nonnegative extended reals without plus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → ¬ +∞ ∈ ran 𝐹) ⇒ ⊢ (𝜑 → 𝐹:𝑋⟶ℝ) | ||
Theorem | sge0z 46330* | Any nonnegative extended sum of zero is zero. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 0)) = 0) | ||
Theorem | sge00 46331 | The sum of nonnegative extended reals is zero when applied to the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (Σ^‘∅) = 0 | ||
Theorem | fsumlesge0 46332* | Every finite subsum of nonnegative reals is less than or equal to the extended sum over the whole (possibly infinite) domain. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,)+∞)) & ⊢ (𝜑 → 𝑌 ⊆ 𝑋) & ⊢ (𝜑 → 𝑌 ∈ Fin) ⇒ ⊢ (𝜑 → Σ𝑥 ∈ 𝑌 (𝐹‘𝑥) ≤ (Σ^‘𝐹)) | ||
Theorem | sge0revalmpt 46333* | Value of the sum of nonnegative extended reals, when all terms in the sum are reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞)) ⇒ ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)) = sup(ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑥 ∈ 𝑦 𝐵), ℝ*, < )) | ||
Theorem | sge0sn 46334 | A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:{𝐴}⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) = (𝐹‘𝐴)) | ||
Theorem | sge0tsms 46335 | Σ^ applied to a nonnegative function (its meaningful domain) is the same as the infinite group sum (that's always convergent, in this case). (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ 𝐺 = (ℝ*𝑠 ↾s (0[,]+∞)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) ∈ (𝐺 tsums 𝐹)) | ||
Theorem | sge0cl 46336 | The arbitrary sum of nonnegative extended reals is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) ∈ (0[,]+∞)) | ||
Theorem | sge0f1o 46337* | Re-index a nonnegative extended sum using a bijection. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑛𝜑 & ⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷))) | ||
Theorem | sge0snmpt 46338* | A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ (0[,]+∞)) & ⊢ (𝑘 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ {𝐴} ↦ 𝐵)) = 𝐶) | ||
Theorem | sge0ge0 46339 | The sum of nonnegative extended reals is nonnegative. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → 0 ≤ (Σ^‘𝐹)) | ||
Theorem | sge0xrcl 46340 | The arbitrary sum of nonnegative extended reals is an extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ*) | ||
Theorem | sge0repnf 46341 | The of nonnegative extended reals is a real number if and only if it is not +∞. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → ((Σ^‘𝐹) ∈ ℝ ↔ ¬ (Σ^‘𝐹) = +∞)) | ||
Theorem | sge0fsum 46342* | The arbitrary sum of a finite set of nonnegative extended real numbers is equal to the sum of those numbers, when none of them is +∞ (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,)+∞)) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) = Σ𝑥 ∈ 𝑋 (𝐹‘𝑥)) | ||
Theorem | sge0rern 46343 | If the sum of nonnegative extended reals is not +∞ then no terms is +∞. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ) ⇒ ⊢ (𝜑 → ¬ +∞ ∈ ran 𝐹) | ||
Theorem | sge0supre 46344* | If the arbitrary sum of nonnegative extended reals is real, then it is the supremum (in the real numbers) of finite subsums. Similar to sge0sup 46346, but here we can use sup with respect to ℝ instead of ℝ*. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < )) | ||
Theorem | sge0fsummpt 46345* | The arbitrary sum of a finite set of nonnegative extended real numbers is equal to the sum of those numbers, when none of them is +∞ (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞)) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵) | ||
Theorem | sge0sup 46346* | The arbitrary sum of nonnegative extended reals is the supremum of finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (Σ^‘(𝐹 ↾ 𝑥))), ℝ*, < )) | ||
Theorem | sge0less 46347 | A shorter sum of nonnegative extended reals is smaller than a longer one. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘(𝐹 ↾ 𝑌)) ≤ (Σ^‘𝐹)) | ||
Theorem | sge0rnbnd 46348* | The range used in the definition of Σ^ is bounded, when the whole sum is a real number. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))𝑤 ≤ 𝑧) | ||
Theorem | sge0pr 46349* | Sum of a pair of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐷 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐸 ∈ (0[,]+∞)) & ⊢ (𝑘 = 𝐴 → 𝐶 = 𝐷) & ⊢ (𝑘 = 𝐵 → 𝐶 = 𝐸) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ {𝐴, 𝐵} ↦ 𝐶)) = (𝐷 +𝑒 𝐸)) | ||
Theorem | sge0gerp 46350* | The arbitrary sum of nonnegative extended reals is greater than or equal to a given extended real number if this number can be approximated from below by finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ∃𝑧 ∈ (𝒫 𝑋 ∩ Fin)𝐴 ≤ ((Σ^‘(𝐹 ↾ 𝑧)) +𝑒 𝑥)) ⇒ ⊢ (𝜑 → 𝐴 ≤ (Σ^‘𝐹)) | ||
Theorem | sge0pnffigt 46351* | If the sum of nonnegative extended reals is +∞, then any real number can be dominated by finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → (Σ^‘𝐹) = +∞) & ⊢ (𝜑 → 𝑌 ∈ ℝ) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)𝑌 < (Σ^‘(𝐹 ↾ 𝑥))) | ||
Theorem | sge0ssre 46352 | If a sum of nonnegative extended reals is real, than any subsum is real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ) ⇒ ⊢ (𝜑 → (Σ^‘(𝐹 ↾ 𝑌)) ∈ ℝ) | ||
Theorem | sge0lefi 46353* | A sum of nonnegative extended reals is smaller than a given extended real if and only if every finite subsum is smaller than it. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → 𝐴 ∈ ℝ*) ⇒ ⊢ (𝜑 → ((Σ^‘𝐹) ≤ 𝐴 ↔ ∀𝑥 ∈ (𝒫 𝑋 ∩ Fin)(Σ^‘(𝐹 ↾ 𝑥)) ≤ 𝐴)) | ||
Theorem | sge0lessmpt 46354* | A shorter sum of nonnegative extended reals is smaller than a longer one. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐶 ↦ 𝐵)) ≤ (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵))) | ||
Theorem | sge0ltfirp 46355* | If the sum of nonnegative extended reals is real, then it can be approximated from below by finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → 𝑌 ∈ ℝ+) & ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)(Σ^‘𝐹) < ((Σ^‘(𝐹 ↾ 𝑥)) + 𝑌)) | ||
Theorem | sge0prle 46356* | The sum of a pair of nonnegative extended reals is less than or equal their extended addition. When it is a distinct pair, than equality holds, see sge0pr 46349. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐷 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐸 ∈ (0[,]+∞)) & ⊢ (𝑘 = 𝐴 → 𝐶 = 𝐷) & ⊢ (𝑘 = 𝐵 → 𝐶 = 𝐸) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ {𝐴, 𝐵} ↦ 𝐶)) ≤ (𝐷 +𝑒 𝐸)) | ||
Theorem | sge0gerpmpt 46357* | The arbitrary sum of nonnegative extended reals is greater than or equal to a given extended real number if this number can be approximated from below by finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)𝐶 ≤ ((Σ^‘(𝑥 ∈ 𝑧 ↦ 𝐵)) +𝑒 𝑦)) ⇒ ⊢ (𝜑 → 𝐶 ≤ (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵))) | ||
Theorem | sge0resrnlem 46358 | The sum of nonnegative extended reals restricted to the range of a function is less than or equal to the sum of the composition of the two functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐵⟶(0[,]+∞)) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝒫 𝐴) & ⊢ (𝜑 → (𝐺 ↾ 𝑋):𝑋–1-1-onto→ran 𝐺) ⇒ ⊢ (𝜑 → (Σ^‘(𝐹 ↾ ran 𝐺)) ≤ (Σ^‘(𝐹 ∘ 𝐺))) | ||
Theorem | sge0resrn 46359 | The sum of nonnegative extended reals restricted to the range of a function is less than or equal to the sum of the composition of the two functions (well-order hypothesis allows to avoid using the axiom of choice). (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐵⟶(0[,]+∞)) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐵) & ⊢ (𝜑 → 𝑅 We 𝐴) ⇒ ⊢ (𝜑 → (Σ^‘(𝐹 ↾ ran 𝐺)) ≤ (Σ^‘(𝐹 ∘ 𝐺))) | ||
Theorem | sge0ssrempt 46360* | If a sum of nonnegative extended reals is real, than any subsum is real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) & ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)) ∈ ℝ) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐶 ↦ 𝐵)) ∈ ℝ) | ||
Theorem | sge0resplit 46361 | Σ^ splits into two parts, when it's a real number. This is a special case of sge0split 46364. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ 𝑈 = (𝐴 ∪ 𝐵) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) & ⊢ (𝜑 → 𝐹:𝑈⟶(0[,]+∞)) & ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) = ((Σ^‘(𝐹 ↾ 𝐴)) + (Σ^‘(𝐹 ↾ 𝐵)))) | ||
Theorem | sge0le 46362* | If all of the terms of sums compare, so do the sums. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → 𝐺:𝑋⟶(0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ≤ (𝐺‘𝑥)) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) ≤ (Σ^‘𝐺)) | ||
Theorem | sge0ltfirpmpt 46363* | If the extended sum of nonnegative reals is not +∞, then it can be approximated from below by finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝑌 ∈ ℝ+) & ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)) ∈ ℝ) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)(Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)) < ((Σ^‘(𝑥 ∈ 𝑦 ↦ 𝐵)) + 𝑌)) | ||
Theorem | sge0split 46364 | Split a sum of nonnegative extended reals into two parts. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ 𝑈 = (𝐴 ∪ 𝐵) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) & ⊢ (𝜑 → 𝐹:𝑈⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) = ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 (Σ^‘(𝐹 ↾ 𝐵)))) | ||
Theorem | sge0lempt 46365* | If all of the terms of sums compare, so do the sums. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)) ≤ (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐶))) | ||
Theorem | sge0splitmpt 46366* | Split a sum of nonnegative extended reals into two parts. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘(𝑥 ∈ (𝐴 ∪ 𝐵) ↦ 𝐶)) = ((Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐶)) +𝑒 (Σ^‘(𝑥 ∈ 𝐵 ↦ 𝐶)))) | ||
Theorem | sge0ss 46367* | Change the index set to a subset in a sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 0) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶)) = (Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))) | ||
Theorem | sge0iunmptlemfi 46368* | Sum of nonnegative extended reals over a disjoint indexed union (in this lemma, for a finite index set). (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^‘(𝑥 ∈ 𝐴 ↦ (Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))))) | ||
Theorem | sge0p1 46369* | The addition of the next term in a finite sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 + 1))) → 𝐴 ∈ (0[,]+∞)) & ⊢ (𝑘 = (𝑁 + 1) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ (𝑀...(𝑁 + 1)) ↦ 𝐴)) = ((Σ^‘(𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)) +𝑒 𝐵)) | ||
Theorem | sge0iunmptlemre 46370* | Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ) & ⊢ (𝜑 → (Σ^‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) ∈ ℝ*) & ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐴 ↦ (Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ∈ ℝ*) & ⊢ (𝜑 → (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶):∪ 𝑥 ∈ 𝐴 𝐵⟶(0[,]+∞)) & ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^‘(𝑥 ∈ 𝐴 ↦ (Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))))) | ||
Theorem | sge0fodjrnlem 46371* | Re-index a nonnegative extended sum using an onto function with disjoint range, when the empty set is assigned 0 in the sum (this is true, for example, both for measures and outer measures). (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑛𝜑 & ⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐶–onto→𝐴) & ⊢ (𝜑 → Disj 𝑛 ∈ 𝐶 (𝐹‘𝑛)) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑘 = ∅) → 𝐵 = 0) & ⊢ 𝑍 = (◡𝐹 “ {∅}) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷))) | ||
Theorem | sge0fodjrn 46372* | Re-index a nonnegative extended sum using an onto function with disjoint range, when the empty set is assigned 0 in the sum (this is true, for example, both for measures and outer measures). (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑛𝜑 & ⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐶–onto→𝐴) & ⊢ (𝜑 → Disj 𝑛 ∈ 𝐶 (𝐹‘𝑛)) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑘 = ∅) → 𝐵 = 0) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷))) | ||
Theorem | sge0iunmpt 46373* | Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^‘(𝑥 ∈ 𝐴 ↦ (Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))))) | ||
Theorem | sge0iun 46374* | Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) & ⊢ 𝑋 = ∪ 𝑥 ∈ 𝐴 𝐵 & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) = (Σ^‘(𝑥 ∈ 𝐴 ↦ (Σ^‘(𝐹 ↾ 𝐵))))) | ||
Theorem | sge0nemnf 46375 | The generalized sum of nonnegative extended reals is not minus infinity. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) ≠ -∞) | ||
Theorem | sge0rpcpnf 46376* | The sum of an infinite number of a positive constant, is +∞ (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)) = +∞) | ||
Theorem | sge0rernmpt 46377* | If the sum of nonnegative extended reals is not +∞ then no term is +∞. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) & ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)) ∈ ℝ) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞)) | ||
Theorem | sge0lefimpt 46378* | A sum of nonnegative extended reals is smaller than a given extended real if and only if every finite subsum is smaller than it. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) ⇒ ⊢ (𝜑 → ((Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)) ≤ 𝐶 ↔ ∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(Σ^‘(𝑥 ∈ 𝑦 ↦ 𝐵)) ≤ 𝐶)) | ||
Theorem | nn0ssge0 46379 | Nonnegative integers are nonnegative reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ ℕ0 ⊆ (0[,)+∞) | ||
Theorem | sge0clmpt 46380* | The generalized sum of nonnegative extended reals is a nonnegative extended real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)) ∈ (0[,]+∞)) | ||
Theorem | sge0ltfirpmpt2 46381* | If the extended sum of nonnegative reals is not +∞, then it can be approximated from below by finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝑌 ∈ ℝ+) & ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)) ∈ ℝ) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)(Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)) < (Σ𝑥 ∈ 𝑦 𝐵 + 𝑌)) | ||
Theorem | sge0isum 46382 | If a series of nonnegative reals is convergent, then it agrees with the generalized sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹:𝑍⟶(0[,)+∞)) & ⊢ 𝐺 = seq𝑀( + , 𝐹) & ⊢ (𝜑 → 𝐺 ⇝ 𝐵) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) = 𝐵) | ||
Theorem | sge0xrclmpt 46383* | The generalized sum of nonnegative extended reals is an extended real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)) ∈ ℝ*) | ||
Theorem | sge0xp 46384* | Combine two generalized sums of nonnegative extended reals into a single generalized sum over the cartesian product. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝑧 = 〈𝑗, 𝑘〉 → 𝐷 = 𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘(𝑗 ∈ 𝐴 ↦ (Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) = (Σ^‘(𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐷))) | ||
Theorem | sge0isummpt 46385* | If a series of nonnegative reals is convergent, then it agrees with the generalized sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ (0[,)+∞)) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → seq𝑀( + , (𝑘 ∈ 𝑍 ↦ 𝐴)) ⇝ 𝐵) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝑍 ↦ 𝐴)) = 𝐵) | ||
Theorem | sge0ad2en 46386* | The value of the infinite geometric series 2↑-1 + 2↑-2 +... , multiplied by a constant. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐴 ∈ (0[,)+∞)) ⇒ ⊢ (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (𝐴 / (2↑𝑛)))) = 𝐴) | ||
Theorem | sge0isummpt2 46387* | If a series of nonnegative reals is convergent, then it agrees with the generalized sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ (0[,)+∞)) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → seq𝑀( + , (𝑘 ∈ 𝑍 ↦ 𝐴)) ⇝ 𝐵) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝑍 ↦ 𝐴)) = Σ𝑘 ∈ 𝑍 𝐴) | ||
Theorem | sge0xaddlem1 46388* | The extended addition of two generalized sums of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,)+∞)) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ (𝜑 → 𝑈 ⊆ 𝐴) & ⊢ (𝜑 → 𝑈 ∈ Fin) & ⊢ (𝜑 → 𝑊 ⊆ 𝐴) & ⊢ (𝜑 → 𝑊 ∈ Fin) & ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) < (Σ𝑘 ∈ 𝑈 𝐵 + (𝐸 / 2))) & ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶)) < (Σ𝑘 ∈ 𝑊 𝐶 + (𝐸 / 2))) & ⊢ (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈ (0[,]+∞)) & ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) ∈ ℝ) & ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶)) ∈ ℝ) ⇒ ⊢ (𝜑 → ((Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) + (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶))) ≤ (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) +𝑒 𝐸)) | ||
Theorem | sge0xaddlem2 46389* | The extended addition of two generalized sums of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,)+∞)) & ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) ∈ ℝ) & ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶)) ∈ ℝ) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ (𝐵 +𝑒 𝐶))) = ((Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) +𝑒 (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶)))) | ||
Theorem | sge0xadd 46390* | The extended addition of two generalized sums of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ (𝐵 +𝑒 𝐶))) = ((Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) +𝑒 (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶)))) | ||
Theorem | sge0fsummptf 46391* | The generalized sum of a finite set of nonnegative extended real numbers is equal to the sum of those numbers, when none of them is +∞ (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞)) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵) | ||
Theorem | sge0snmptf 46392* | A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ (0[,]+∞)) & ⊢ (𝑘 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ {𝐴} ↦ 𝐵)) = 𝐶) | ||
Theorem | sge0ge0mpt 46393* | The sum of nonnegative extended reals is nonnegative. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → 0 ≤ (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵))) | ||
Theorem | sge0repnfmpt 46394* | The of nonnegative extended reals is a real number if and only if it is not +∞. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → ((Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) ∈ ℝ ↔ ¬ (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = +∞)) | ||
Theorem | sge0pnffigtmpt 46395* | If the generalized sum of nonnegative reals is +∞, then any real number can be dominated by finite subsums. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) & ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = +∞) & ⊢ (𝜑 → 𝑌 ∈ ℝ) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑌 < (Σ^‘(𝑘 ∈ 𝑥 ↦ 𝐵))) | ||
Theorem | sge0splitsn 46396* | Separate out a term in a generalized sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → ¬ 𝐵 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞)) & ⊢ (𝑘 = 𝐵 → 𝐶 = 𝐷) & ⊢ (𝜑 → 𝐷 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ (𝐴 ∪ {𝐵}) ↦ 𝐶)) = ((Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶)) +𝑒 𝐷)) | ||
Theorem | sge0pnffsumgt 46397* | If the sum of nonnegative extended reals is +∞, then any real number can be dominated by finite subsums. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞)) & ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = +∞) & ⊢ (𝜑 → 𝑌 ∈ ℝ) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑌 < Σ𝑘 ∈ 𝑥 𝐵) | ||
Theorem | sge0gtfsumgt 46398* | If the generalized sum of nonnegative reals is larger than a given number, then that number can be dominated by a finite subsum. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞)) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐶 < (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵))) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)𝐶 < Σ𝑘 ∈ 𝑦 𝐵) | ||
Theorem | sge0uzfsumgt 46399* | If a real number is smaller than a generalized sum of nonnegative reals, then it is smaller than some finite subsum. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝐾) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ (0[,)+∞)) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐶 < (Σ^‘(𝑘 ∈ 𝑍 ↦ 𝐵))) ⇒ ⊢ (𝜑 → ∃𝑚 ∈ 𝑍 𝐶 < Σ𝑘 ∈ (𝐾...𝑚)𝐵) | ||
Theorem | sge0pnfmpt 46400* | If a term in the sum of nonnegative extended reals is +∞, then the value of the sum is +∞. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) & ⊢ (𝜑 → ∃𝑘 ∈ 𝐴 𝐵 = +∞) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = +∞) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |