Home | Metamath
Proof Explorer Theorem List (p. 428 of 450) | < 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-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44955) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fge0iccico 42701 | A range of nonnegative extended reals without plus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → ¬ +∞ ∈ ran 𝐹) ⇒ ⊢ (𝜑 → 𝐹:𝑋⟶(0[,)+∞)) | ||
Theorem | gsumge0cl 42702 | 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 42703* | 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 42704 | 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 42705 | A range of nonnegative extended reals without plus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → ¬ +∞ ∈ ran 𝐹) ⇒ ⊢ (𝜑 → 𝐹:𝑋⟶ℝ) | ||
Theorem | sge0z 42706* | Any nonnegative extended sum of zero is zero. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 0)) = 0) | ||
Theorem | sge00 42707 | The sum of nonnegative extended reals is zero when applied to the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (Σ^‘∅) = 0 | ||
Theorem | fsumlesge0 42708* | 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 42709* | 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 42710 | A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:{𝐴}⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) = (𝐹‘𝐴)) | ||
Theorem | sge0tsms 42711 | Σ^ 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 42712 | The arbitrary sum of nonnegative extended reals is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) ∈ (0[,]+∞)) | ||
Theorem | sge0f1o 42713* | Re-index a nonnegative extended sum using a bijection. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑛𝜑 & ⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷))) | ||
Theorem | sge0snmpt 42714* | A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ (0[,]+∞)) & ⊢ (𝑘 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ {𝐴} ↦ 𝐵)) = 𝐶) | ||
Theorem | sge0ge0 42715 | The sum of nonnegative extended reals is nonnegative. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → 0 ≤ (Σ^‘𝐹)) | ||
Theorem | sge0xrcl 42716 | The arbitrary sum of nonnegative extended reals is an extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ*) | ||
Theorem | sge0repnf 42717 | 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 42718* | 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 42719 | If the sum of nonnegative extended reals is not +∞ then no terms is +∞. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ) ⇒ ⊢ (𝜑 → ¬ +∞ ∈ ran 𝐹) | ||
Theorem | sge0supre 42720* | 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 42722, but here we can use sup with respect to ℝ instead of ℝ* (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < )) | ||
Theorem | sge0fsummpt 42721* | 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 42722* | 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 42723 | A shorter sum of nonnegative extended reals is smaller than a longer one. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘(𝐹 ↾ 𝑌)) ≤ (Σ^‘𝐹)) | ||
Theorem | sge0rnbnd 42724* | 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 42725* | Sum of a pair of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐷 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐸 ∈ (0[,]+∞)) & ⊢ (𝑘 = 𝐴 → 𝐶 = 𝐷) & ⊢ (𝑘 = 𝐵 → 𝐶 = 𝐸) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ {𝐴, 𝐵} ↦ 𝐶)) = (𝐷 +𝑒 𝐸)) | ||
Theorem | sge0gerp 42726* | 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 42727* | 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 42728 | If a sum of nonnegative extended reals is real, than any subsum is real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ) ⇒ ⊢ (𝜑 → (Σ^‘(𝐹 ↾ 𝑌)) ∈ ℝ) | ||
Theorem | sge0lefi 42729* | 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 42730* | A shorter sum of nonnegative extended reals is smaller than a longer one. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐶 ↦ 𝐵)) ≤ (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵))) | ||
Theorem | sge0ltfirp 42731* | 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 42732* | 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 42725. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐷 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐸 ∈ (0[,]+∞)) & ⊢ (𝑘 = 𝐴 → 𝐶 = 𝐷) & ⊢ (𝑘 = 𝐵 → 𝐶 = 𝐸) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ {𝐴, 𝐵} ↦ 𝐶)) ≤ (𝐷 +𝑒 𝐸)) | ||
Theorem | sge0gerpmpt 42733* | 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 42734 | 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 42735 | 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 42736* | If a sum of nonnegative extended reals is real, than any subsum is real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) & ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)) ∈ ℝ) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐶 ↦ 𝐵)) ∈ ℝ) | ||
Theorem | sge0resplit 42737 | Σ^ splits into two parts, when it's a real number. This is a special case of sge0split 42740. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ 𝑈 = (𝐴 ∪ 𝐵) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) & ⊢ (𝜑 → 𝐹:𝑈⟶(0[,]+∞)) & ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) = ((Σ^‘(𝐹 ↾ 𝐴)) + (Σ^‘(𝐹 ↾ 𝐵)))) | ||
Theorem | sge0le 42738* | If all of the terms of sums compare, so do the sums. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → 𝐺:𝑋⟶(0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ≤ (𝐺‘𝑥)) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) ≤ (Σ^‘𝐺)) | ||
Theorem | sge0ltfirpmpt 42739* | 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 42740 | Split a sum of nonnegative extended reals into two parts. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ 𝑈 = (𝐴 ∪ 𝐵) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) & ⊢ (𝜑 → 𝐹:𝑈⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) = ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 (Σ^‘(𝐹 ↾ 𝐵)))) | ||
Theorem | sge0lempt 42741* | If all of the terms of sums compare, so do the sums. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)) ≤ (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐶))) | ||
Theorem | sge0splitmpt 42742* | Split a sum of nonnegative extended reals into two parts. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘(𝑥 ∈ (𝐴 ∪ 𝐵) ↦ 𝐶)) = ((Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐶)) +𝑒 (Σ^‘(𝑥 ∈ 𝐵 ↦ 𝐶)))) | ||
Theorem | sge0ss 42743* | 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 42744* | 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 42745* | 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 42746* | Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ) & ⊢ (𝜑 → (Σ^‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) ∈ ℝ*) & ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐴 ↦ (Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ∈ ℝ*) & ⊢ (𝜑 → (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶):∪ 𝑥 ∈ 𝐴 𝐵⟶(0[,]+∞)) & ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^‘(𝑥 ∈ 𝐴 ↦ (Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))))) | ||
Theorem | sge0fodjrnlem 42747* | 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 42748* | 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 42749* | Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^‘(𝑥 ∈ 𝐴 ↦ (Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))))) | ||
Theorem | sge0iun 42750* | Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) & ⊢ 𝑋 = ∪ 𝑥 ∈ 𝐴 𝐵 & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) = (Σ^‘(𝑥 ∈ 𝐴 ↦ (Σ^‘(𝐹 ↾ 𝐵))))) | ||
Theorem | sge0nemnf 42751 | The generalized sum of nonnegative extended reals is not minus infinity. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) ≠ -∞) | ||
Theorem | sge0rpcpnf 42752* | The sum of an infinite number of a positive constant, is +∞ (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)) = +∞) | ||
Theorem | sge0rernmpt 42753* | If the sum of nonnegative extended reals is not +∞ then no term is +∞. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) & ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)) ∈ ℝ) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞)) | ||
Theorem | sge0lefimpt 42754* | 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 42755 | Nonnegative integers are nonnegative reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ ℕ0 ⊆ (0[,)+∞) | ||
Theorem | sge0clmpt 42756* | The generalized sum of nonnegative extended reals is a nonnegative extended real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)) ∈ (0[,]+∞)) | ||
Theorem | sge0ltfirpmpt2 42757* | 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 42758 | 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 42759* | The generalized sum of nonnegative extended reals is an extended real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)) ∈ ℝ*) | ||
Theorem | sge0xp 42760* | 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 42761* | 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 42762* | 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 42763* | 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 42764* | 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 42765* | The extended addition of two generalized sums of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,)+∞)) & ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) ∈ ℝ) & ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶)) ∈ ℝ) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ (𝐵 +𝑒 𝐶))) = ((Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) +𝑒 (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶)))) | ||
Theorem | sge0xadd 42766* | The extended addition of two generalized sums of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ (𝐵 +𝑒 𝐶))) = ((Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) +𝑒 (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶)))) | ||
Theorem | sge0fsummptf 42767* | 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 42768* | A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ (0[,]+∞)) & ⊢ (𝑘 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ {𝐴} ↦ 𝐵)) = 𝐶) | ||
Theorem | sge0ge0mpt 42769* | The sum of nonnegative extended reals is nonnegative. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → 0 ≤ (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵))) | ||
Theorem | sge0repnfmpt 42770* | 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 42771* | 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 42772* | Separate out a term in a generalized sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → ¬ 𝐵 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞)) & ⊢ (𝑘 = 𝐵 → 𝐶 = 𝐷) & ⊢ (𝜑 → 𝐷 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ (𝐴 ∪ {𝐵}) ↦ 𝐶)) = ((Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶)) +𝑒 𝐷)) | ||
Theorem | sge0pnffsumgt 42773* | 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 42774* | 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 42775* | 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 42776* | 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[,]+∞)) & ⊢ (𝜑 → ∃𝑘 ∈ 𝐴 𝐵 = +∞) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = +∞) | ||
Theorem | sge0seq 42777 | A series of nonnegative reals agrees with the generalized sum of nonnegative reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹:𝑍⟶(0[,)+∞)) & ⊢ 𝐺 = seq𝑀( + , 𝐹) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) = sup(ran 𝐺, ℝ*, < )) | ||
Theorem | sge0reuz 42778* | Value of the generalized sum of nonnegative reals, when the domain is a set of upper integers. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ (0[,)+∞)) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝑍 ↦ 𝐵)) = sup(ran (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵), ℝ*, < )) | ||
Theorem | sge0reuzb 42779* | Value of the generalized sum of uniformly bounded nonnegative reals, when the domain is a set of upper integers. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ (0[,)+∞)) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 Σ𝑘 ∈ (𝑀...𝑛)𝐵 ≤ 𝑥) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝑍 ↦ 𝐵)) = sup(ran (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵), ℝ, < )) | ||
Proofs for most of the theorems in section 112 of [Fremlin1] | ||
Syntax | cmea 42780 | Extend class notation with the class of measures. |
class Meas | ||
Definition | df-mea 42781* | Define the class of measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Meas = {𝑥 ∣ (((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 ∈ SAlg) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥((𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤) → (𝑥‘∪ 𝑦) = (Σ^‘(𝑥 ↾ 𝑦))))} | ||
Theorem | ismea 42782* | Express the predicate "𝑀 is a measure." Definition 112A of [Fremlin1] p. 14. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝑀 ∈ Meas ↔ (((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧ ∀𝑥 ∈ 𝒫 dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = (Σ^‘(𝑀 ↾ 𝑥))))) | ||
Theorem | dmmeasal 42783 | The domain of a measure is a sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ 𝑆 = dom 𝑀 ⇒ ⊢ (𝜑 → 𝑆 ∈ SAlg) | ||
Theorem | meaf 42784 | A measure is a function that maps to nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ 𝑆 = dom 𝑀 ⇒ ⊢ (𝜑 → 𝑀:𝑆⟶(0[,]+∞)) | ||
Theorem | mea0 42785 | The measure of the empty set is always 0 . (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑀 ∈ Meas) ⇒ ⊢ (𝜑 → (𝑀‘∅) = 0) | ||
Theorem | nnfoctbdjlem 42786* | There exists a mapping from ℕ onto any (nonempty) countable set of disjoint sets, such that elements in the range of the map are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ) & ⊢ (𝜑 → 𝐺:𝐴–1-1-onto→𝑋) & ⊢ (𝜑 → Disj 𝑦 ∈ 𝑋 𝑦) & ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1)))) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:ℕ–onto→(𝑋 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛))) | ||
Theorem | nnfoctbdj 42787* | There exists a mapping from ℕ onto any (nonempty) countable set of disjoint sets, such that elements in the range of the map are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ≼ ω) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → Disj 𝑦 ∈ 𝑋 𝑦) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:ℕ–onto→(𝑋 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛))) | ||
Theorem | meadjuni 42788* | The measure of the disjoint union of a countable set is the extended sum of the measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ 𝑆 = dom 𝑀 & ⊢ (𝜑 → 𝑋 ⊆ 𝑆) & ⊢ (𝜑 → 𝑋 ≼ ω) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝑋 𝑥) ⇒ ⊢ (𝜑 → (𝑀‘∪ 𝑋) = (Σ^‘(𝑀 ↾ 𝑋))) | ||
Theorem | meacl 42789 | The measure of a set is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ 𝑆 = dom 𝑀 & ⊢ (𝜑 → 𝐴 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑀‘𝐴) ∈ (0[,]+∞)) | ||
Theorem | iundjiunlem 42790* | The sets in the sequence 𝐹 are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) & ⊢ (𝜑 → 𝐽 ∈ 𝑍) & ⊢ (𝜑 → 𝐾 ∈ 𝑍) & ⊢ (𝜑 → 𝐽 < 𝐾) ⇒ ⊢ (𝜑 → ((𝐹‘𝐽) ∩ (𝐹‘𝐾)) = ∅) | ||
Theorem | iundjiun 42791* | Given a sequence 𝐸 of sets, a sequence 𝐹 of disjoint sets is built, such that the indexed union stays the same. As in the proof of Property 112C (d) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑛𝜑 & ⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝐸:𝑍⟶𝑉) & ⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) ⇒ ⊢ (𝜑 → ((∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) ∧ ∪ 𝑛 ∈ 𝑍 (𝐹‘𝑛) = ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ∧ Disj 𝑛 ∈ 𝑍 (𝐹‘𝑛))) | ||
Theorem | meaxrcl 42792 | The measure of a set is an extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ 𝑆 = dom 𝑀 & ⊢ (𝜑 → 𝐴 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑀‘𝐴) ∈ ℝ*) | ||
Theorem | meadjun 42793 | The measure of the union of two disjoint sets is the sum of the measures, Property 112C (a) of [Fremlin1] p. 15. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ 𝑆 = dom 𝑀 & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) ⇒ ⊢ (𝜑 → (𝑀‘(𝐴 ∪ 𝐵)) = ((𝑀‘𝐴) +𝑒 (𝑀‘𝐵))) | ||
Theorem | meassle 42794 | The measure of a set is greater than or equal to the measure of a subset, Property 112C (b) of [Fremlin1] p. 15. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ 𝑆 = dom 𝑀 & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝑀‘𝐴) ≤ (𝑀‘𝐵)) | ||
Theorem | meaunle 42795 | The measure of the union of two sets is less than or equal to the sum of the measures, Property 112C (c) of [Fremlin1] p. 15. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ 𝑆 = dom 𝑀 & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑀‘(𝐴 ∪ 𝐵)) ≤ ((𝑀‘𝐴) +𝑒 (𝑀‘𝐵))) | ||
Theorem | meadjiunlem 42796* | The sum of nonnegative extended reals, restricted to the range of another function. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ 𝑆 = dom 𝑀 & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐺:𝑋⟶𝑆) & ⊢ 𝑌 = {𝑖 ∈ 𝑋 ∣ (𝐺‘𝑖) ≠ ∅} & ⊢ (𝜑 → Disj 𝑖 ∈ 𝑋 (𝐺‘𝑖)) ⇒ ⊢ (𝜑 → (Σ^‘(𝑀 ↾ ran 𝐺)) = (Σ^‘(𝑀 ∘ 𝐺))) | ||
Theorem | meadjiun 42797* | The measure of the disjoint union of a countable set is the extended sum of the measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ 𝑆 = dom 𝑀 & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐴 ≼ ω) & ⊢ (𝜑 → Disj 𝑘 ∈ 𝐴 𝐵) ⇒ ⊢ (𝜑 → (𝑀‘∪ 𝑘 ∈ 𝐴 𝐵) = (Σ^‘(𝑘 ∈ 𝐴 ↦ (𝑀‘𝐵)))) | ||
Theorem | ismeannd 42798* | Sufficient condition to prove that 𝑀 is a measure. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝑀:𝑆⟶(0[,]+∞)) & ⊢ (𝜑 → (𝑀‘∅) = 0) & ⊢ ((𝜑 ∧ 𝑒:ℕ⟶𝑆 ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛)) → (𝑀‘∪ 𝑛 ∈ ℕ (𝑒‘𝑛)) = (Σ^‘(𝑛 ∈ ℕ ↦ (𝑀‘(𝑒‘𝑛))))) ⇒ ⊢ (𝜑 → 𝑀 ∈ Meas) | ||
Theorem | meaiunlelem 42799* | The measure of the union of countable sets is less than or equal to the sum of the measures, Property 112C (d) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑛𝜑 & ⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ 𝑆 = dom 𝑀 & ⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝐸:𝑍⟶𝑆) & ⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) ⇒ ⊢ (𝜑 → (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ≤ (Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))))) | ||
Theorem | meaiunle 42800* | The measure of the union of countable sets is less than or equal to the sum of the measures, Property 112C (d) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑛𝜑 & ⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ 𝑆 = dom 𝑀 & ⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝐸:𝑍⟶𝑆) ⇒ ⊢ (𝜑 → (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ≤ (Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |