P. 467 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 46601-46700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	salrestss 46601	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 𝐸) ⊆ 𝑆)
21.43.19.2  Sum of nonnegative extended reals
Syntax	csumge0 46602	Extend class notation to include the sum of nonnegative extended reals.
class Σ^
Definition	df-sumge0 46603*	Define the arbitrary sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) $.
⊢ Σ^ = (𝑥 ∈ V ↦ if(+∞ ∈ ran 𝑥, +∞, sup(ran (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)), ℝ*, < )))
Theorem	sge0rnre 46604*	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 46605	If 𝐹 maps to nonnegative reals, then 𝐹 maps to nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐹:𝑋⟶(0[,)+∞))    ⇒   ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))
Theorem	sge0val 46606*	The value of the sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) → (Σ^‘𝐹) = if(+∞ ∈ ran 𝐹, +∞, sup(ran (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝐹‘𝑤)), ℝ*, < )))
Theorem	fge0npnf 46607	If 𝐹 maps to nonnegative reals, then +∞ is not in its range. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐹:𝑋⟶(0[,)+∞))    ⇒   ⊢ (𝜑 → ¬ +∞ ∈ ran 𝐹)
Theorem	sge0rnn0 46608*	The range used in the definition of Σ^ is not empty. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ≠ ∅
Theorem	sge0vald 46609*	The value of the sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))    ⇒   ⊢ (𝜑 → (Σ^‘𝐹) = if(+∞ ∈ ran 𝐹, +∞, sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, < )))
Theorem	fge0iccico 46610	A range of nonnegative extended reals without plus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))    &   ⊢ (𝜑 → ¬ +∞ ∈ ran 𝐹)    ⇒   ⊢ (𝜑 → 𝐹:𝑋⟶(0[,)+∞))
Theorem	gsumge0cl 46611	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 46612*	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 46613	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 46614	A range of nonnegative extended reals without plus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))    &   ⊢ (𝜑 → ¬ +∞ ∈ ran 𝐹)    ⇒   ⊢ (𝜑 → 𝐹:𝑋⟶ℝ)
Theorem	sge0z 46615*	Any nonnegative extended sum of zero is zero. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 0)) = 0)
Theorem	sge00 46616	The sum of nonnegative extended reals is zero when applied to the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (Σ^‘∅) = 0
Theorem	fsumlesge0 46617*	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 46618*	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 46619	A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:{𝐴}⟶(0[,]+∞))    ⇒   ⊢ (𝜑 → (Σ^‘𝐹) = (𝐹‘𝐴))
Theorem	sge0tsms 46620	Σ^ 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 46621	The arbitrary sum of nonnegative extended reals is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))    ⇒   ⊢ (𝜑 → (Σ^‘𝐹) ∈ (0[,]+∞))
Theorem	sge0f1o 46622*	Re-index a nonnegative extended sum using a bijection. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑛𝜑    &   ⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷)))
Theorem	sge0snmpt 46623*	A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ (0[,]+∞))    &   ⊢ (𝑘 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (Σ^‘(𝑘 ∈ {𝐴} ↦ 𝐵)) = 𝐶)
Theorem	sge0ge0 46624	The sum of nonnegative extended reals is nonnegative. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))    ⇒   ⊢ (𝜑 → 0 ≤ (Σ^‘𝐹))
Theorem	sge0xrcl 46625	The arbitrary sum of nonnegative extended reals is an extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))    ⇒   ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ*)
Theorem	sge0repnf 46626	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 46627*	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 46628	If the sum of nonnegative extended reals is not +∞ then no terms is +∞. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))    &   ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ)    ⇒   ⊢ (𝜑 → ¬ +∞ ∈ ran 𝐹)
Theorem	sge0supre 46629*	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 46631, but here we can use sup with respect to ℝ instead of ℝ*. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))    &   ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ)    ⇒   ⊢ (𝜑 → (Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ))
Theorem	sge0fsummpt 46630*	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 46631*	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 46632	A shorter sum of nonnegative extended reals is smaller than a longer one. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))    ⇒   ⊢ (𝜑 → (Σ^‘(𝐹 ↾ 𝑌)) ≤ (Σ^‘𝐹))
Theorem	sge0rnbnd 46633*	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 46634*	Sum of a pair of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐷 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐸 ∈ (0[,]+∞))    &   ⊢ (𝑘 = 𝐴 → 𝐶 = 𝐷)    &   ⊢ (𝑘 = 𝐵 → 𝐶 = 𝐸)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → (Σ^‘(𝑘 ∈ {𝐴, 𝐵} ↦ 𝐶)) = (𝐷 +𝑒 𝐸))
Theorem	sge0gerp 46635*	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 46636*	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 46637	If a sum of nonnegative extended reals is real, than any subsum is real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))    &   ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ)    ⇒   ⊢ (𝜑 → (Σ^‘(𝐹 ↾ 𝑌)) ∈ ℝ)
Theorem	sge0lefi 46638*	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 46639*	A shorter sum of nonnegative extended reals is smaller than a longer one. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐶 ↦ 𝐵)) ≤ (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)))
Theorem	sge0ltfirp 46640*	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 46641*	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 46634. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐷 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐸 ∈ (0[,]+∞))    &   ⊢ (𝑘 = 𝐴 → 𝐶 = 𝐷)    &   ⊢ (𝑘 = 𝐵 → 𝐶 = 𝐸)    ⇒   ⊢ (𝜑 → (Σ^‘(𝑘 ∈ {𝐴, 𝐵} ↦ 𝐶)) ≤ (𝐷 +𝑒 𝐸))
Theorem	sge0gerpmpt 46642*	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 46643	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 46644	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 46645*	If a sum of nonnegative extended reals is real, than any subsum is real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)) ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐶 ↦ 𝐵)) ∈ ℝ)
Theorem	sge0resplit 46646	Σ^ splits into two parts, when it's a real number. This is a special case of sge0split 46649. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝑈 = (𝐴 ∪ 𝐵)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ (𝜑 → 𝐹:𝑈⟶(0[,]+∞))    &   ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ)    ⇒   ⊢ (𝜑 → (Σ^‘𝐹) = ((Σ^‘(𝐹 ↾ 𝐴)) + (Σ^‘(𝐹 ↾ 𝐵))))
Theorem	sge0le 46647*	If all of the terms of sums compare, so do the sums. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))    &   ⊢ (𝜑 → 𝐺:𝑋⟶(0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ≤ (𝐺‘𝑥))    ⇒   ⊢ (𝜑 → (Σ^‘𝐹) ≤ (Σ^‘𝐺))
Theorem	sge0ltfirpmpt 46648*	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 46649	Split a sum of nonnegative extended reals into two parts. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝑈 = (𝐴 ∪ 𝐵)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ (𝜑 → 𝐹:𝑈⟶(0[,]+∞))    ⇒   ⊢ (𝜑 → (Σ^‘𝐹) = ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 (Σ^‘(𝐹 ↾ 𝐵))))
Theorem	sge0lempt 46650*	If all of the terms of sums compare, so do the sums. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ 𝐶)    ⇒   ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)) ≤ (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐶)))
Theorem	sge0splitmpt 46651*	Split a sum of nonnegative extended reals into two parts. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → (Σ^‘(𝑥 ∈ (𝐴 ∪ 𝐵) ↦ 𝐶)) = ((Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐶)) +𝑒 (Σ^‘(𝑥 ∈ 𝐵 ↦ 𝐶))))
Theorem	sge0ss 46652*	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 46653*	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 46654*	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 46655*	Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ)    &   ⊢ (𝜑 → (Σ^‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) ∈ ℝ*)    &   ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐴 ↦ (Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ∈ ℝ*)    &   ⊢ (𝜑 → (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶):∪ 𝑥 ∈ 𝐴 𝐵⟶(0[,]+∞))    &   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)    ⇒   ⊢ (𝜑 → (Σ^‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^‘(𝑥 ∈ 𝐴 ↦ (Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
Theorem	sge0fodjrnlem 46656*	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 46657*	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 46658*	Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → (Σ^‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^‘(𝑥 ∈ 𝐴 ↦ (Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
Theorem	sge0iun 46659*	Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)    &   ⊢ 𝑋 = ∪ 𝑥 ∈ 𝐴 𝐵    &   ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))    &   ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)    ⇒   ⊢ (𝜑 → (Σ^‘𝐹) = (Σ^‘(𝑥 ∈ 𝐴 ↦ (Σ^‘(𝐹 ↾ 𝐵)))))
Theorem	sge0nemnf 46660	The generalized sum of nonnegative extended reals is not minus infinity. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶(0[,]+∞))    ⇒   ⊢ (𝜑 → (Σ^‘𝐹) ≠ -∞)
Theorem	sge0rpcpnf 46661*	The sum of an infinite number of a positive constant, is +∞ (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)) = +∞)
Theorem	sge0rernmpt 46662*	If the sum of nonnegative extended reals is not +∞ then no term is +∞. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)) ∈ ℝ)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞))
Theorem	sge0lefimpt 46663*	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 46664	Nonnegative integers are nonnegative reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ ℕ0 ⊆ (0[,)+∞)
Theorem	sge0clmpt 46665*	The generalized sum of nonnegative extended reals is a nonnegative extended real. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)) ∈ (0[,]+∞))
Theorem	sge0ltfirpmpt2 46666*	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 46667	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 46668*	The generalized sum of nonnegative extended reals is an extended real. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)) ∈ ℝ*)
Theorem	sge0xp 46669*	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 46670*	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 46671*	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 46672*	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 46673*	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 46674*	The extended addition of two generalized sums of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,)+∞))    &   ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) ∈ ℝ)    &   ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶)) ∈ ℝ)    ⇒   ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ (𝐵 +𝑒 𝐶))) = ((Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) +𝑒 (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶))))
Theorem	sge0xadd 46675*	The extended addition of two generalized sums of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ (𝐵 +𝑒 𝐶))) = ((Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) +𝑒 (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶))))
Theorem	sge0fsummptf 46676*	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 46677*	A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ (0[,]+∞))    &   ⊢ (𝑘 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (Σ^‘(𝑘 ∈ {𝐴} ↦ 𝐵)) = 𝐶)
Theorem	sge0ge0mpt 46678*	The sum of nonnegative extended reals is nonnegative. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → 0 ≤ (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)))
Theorem	sge0repnfmpt 46679*	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 46680*	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 46681*	Separate out a term in a generalized sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))    &   ⊢ (𝑘 = 𝐵 → 𝐶 = 𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → (Σ^‘(𝑘 ∈ (𝐴 ∪ {𝐵}) ↦ 𝐶)) = ((Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶)) +𝑒 𝐷))
Theorem	sge0pnffsumgt 46682*	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 46683*	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 46684*	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 46685*	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 46686	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 46687*	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 46688*	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 (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐵), ℝ, < ))
21.43.19.3  Measures Proofs for most of the theorems in section 112 of [Fremlin1]
Syntax	cmea 46689	Extend class notation with the class of measures.
class Meas
Definition	df-mea 46690*	Define the class of measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Meas = {𝑥 ∣ (((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 ∈ SAlg) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥((𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤) → (𝑥‘∪ 𝑦) = (Σ^‘(𝑥 ↾ 𝑦))))}
Theorem	ismea 46691*	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 46692	The domain of a measure is a sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ 𝑆 = dom 𝑀    ⇒   ⊢ (𝜑 → 𝑆 ∈ SAlg)
Theorem	meaf 46693	A measure is a function that maps to nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ 𝑆 = dom 𝑀    ⇒   ⊢ (𝜑 → 𝑀:𝑆⟶(0[,]+∞))
Theorem	mea0 46694	The measure of the empty set is always 0 . (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑀 ∈ Meas)    ⇒   ⊢ (𝜑 → (𝑀‘∅) = 0)
Theorem	nnfoctbdjlem 46695*	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 46696*	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 46697*	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 46698	The measure of a set is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ 𝑆 = dom 𝑀    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) ∈ (0[,]+∞))
Theorem	iundjiunlem 46699*	The sets in the sequence 𝐹 are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ 𝑍 = (ℤ≥‘𝑁)    &   ⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)))    &   ⊢ (𝜑 → 𝐽 ∈ 𝑍)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑍)    &   ⊢ (𝜑 → 𝐽 < 𝐾)    ⇒   ⊢ (𝜑 → ((𝐹‘𝐽) ∩ (𝐹‘𝐾)) = ∅)
Theorem	iundjiun 46700*	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 𝑛 ∈ 𝑍 (𝐹‘𝑛)))