P. 475 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 47401-47500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pwsal 47401	The power set of a given set is a sigma-algebra (the so called discrete sigma-algebra). (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ SAlg)
Theorem	salunicl 47402	SAlg sigma-algebra is closed under countable union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝑇 ∈ 𝒫 𝑆)    &   ⊢ (𝜑 → 𝑇 ≼ ω)    ⇒   ⊢ (𝜑 → ∪ 𝑇 ∈ 𝑆)
Theorem	saluncl 47403	The union of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ((𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆) → (𝐸 ∪ 𝐹) ∈ 𝑆)
Theorem	prsal 47404	The pair of the empty set and the whole base is a sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝑋 ∈ 𝑉 → {∅, 𝑋} ∈ SAlg)
Theorem	saldifcl 47405	The complement of an element of a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ((𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆) → (∪ 𝑆 ∖ 𝐸) ∈ 𝑆)
Theorem	0sal 47406	The empty set belongs to every sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝑆 ∈ SAlg → ∅ ∈ 𝑆)
Theorem	salgenval 47407*	The sigma-algebra generated by a set. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝑋 ∈ 𝑉 → (SalGen‘𝑋) = ∩ {𝑠 ∈ SAlg ∣ (∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)})
Theorem	saliunclf 47408	SAlg sigma-algebra is closed under countable indexed union. (Contributed by Glauco Siliprandi, 24-Jan-2025.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝑆    &   ⊢ Ⅎ𝑘𝐾    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐾 ≼ ω)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐾) → 𝐸 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ∪ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆)
Theorem	saliuncl 47409*	SAlg sigma-algebra is closed under countable indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐾 ≼ ω)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐾) → 𝐸 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ∪ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆)
Theorem	salincl 47410	The intersection of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ((𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆) → (𝐸 ∩ 𝐹) ∈ 𝑆)
Theorem	saluni 47411	A set is an element of any sigma-algebra on it. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝑆 ∈ SAlg → ∪ 𝑆 ∈ 𝑆)
Theorem	saliinclf 47412	SAlg sigma-algebra is closed under countable indexed intersection. (Contributed by Glauco Siliprandi, 24-Jan-2025.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝑆    &   ⊢ Ⅎ𝑘𝐾    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐾 ≼ ω)    &   ⊢ (𝜑 → 𝐾 ≠ ∅)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐾) → 𝐸 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ∩ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆)
Theorem	saliincl 47413*	SAlg sigma-algebra is closed under countable indexed intersection. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐾 ≼ ω)    &   ⊢ (𝜑 → 𝐾 ≠ ∅)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐾) → 𝐸 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ∩ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆)
Theorem	saldifcl2 47414	The difference of two elements of a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ((𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆) → (𝐸 ∖ 𝐹) ∈ 𝑆)
Theorem	intsaluni 47415*	The union of an arbitrary intersection of sigma-algebras on the same set 𝑋, is 𝑋. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐺 ⊆ SAlg)    &   ⊢ (𝜑 → 𝐺 ≠ ∅)    &   ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∪ 𝑠 = 𝑋)    ⇒   ⊢ (𝜑 → ∪ ∩ 𝐺 = 𝑋)
Theorem	intsal 47416*	The arbitrary intersection of sigma-algebra (on the same set 𝑋) is a sigma-algebra ( on the same set 𝑋, see intsaluni 47415). (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐺 ⊆ SAlg)    &   ⊢ (𝜑 → 𝐺 ≠ ∅)    &   ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∪ 𝑠 = 𝑋)    ⇒   ⊢ (𝜑 → ∩ 𝐺 ∈ SAlg)
Theorem	salgenn0 47417*	The set used in the definition of the generated sigma-algebra, is not empty. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝑋 ∈ 𝑉 → {𝑠 ∈ SAlg ∣ (∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} ≠ ∅)
Theorem	salgencl 47418	SalGen actually generates a sigma-algebra. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝑋 ∈ 𝑉 → (SalGen‘𝑋) ∈ SAlg)
Theorem	issald 47419*	Sufficient condition to prove that 𝑆 is sigma-algebra. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → ∅ ∈ 𝑆)    &   ⊢ 𝑋 = ∪ 𝑆    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝑋 ∖ 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω) → ∪ 𝑦 ∈ 𝑆)    ⇒   ⊢ (𝜑 → 𝑆 ∈ SAlg)
Theorem	salexct 47420*	An example of nontrivial sigma-algebra: the collection of all subsets which either are countable or have countable complement. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ 𝑆 = {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω)}    ⇒   ⊢ (𝜑 → 𝑆 ∈ SAlg)
Theorem	sssalgen 47421	A set is a subset of the sigma-algebra it generates. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ 𝑆 = (SalGen‘𝑋)    ⇒   ⊢ (𝑋 ∈ 𝑉 → 𝑋 ⊆ 𝑆)
Theorem	salgenss 47422	The sigma-algebra generated by a set is the smallest sigma-algebra, on the same base set, that includes the set. Proposition 111G (b) of [Fremlin1] p. 13. Notice that the condition "on the same base set" is needed, see the counterexample salgensscntex 47430, where a sigma-algebra is shown that includes a set, but does not include the sigma-algebra generated (the key is that its base set is larger than the base set of the generating set). (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ 𝐺 = (SalGen‘𝑋)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑆)    &   ⊢ (𝜑 → ∪ 𝑆 = ∪ 𝑋)    ⇒   ⊢ (𝜑 → 𝐺 ⊆ 𝑆)
Theorem	salgenuni 47423	The base set of the sigma-algebra generated by a set is the union of the set itself. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ 𝑆 = (SalGen‘𝑋)    &   ⊢ 𝑈 = ∪ 𝑋    ⇒   ⊢ (𝜑 → ∪ 𝑆 = 𝑈)
Theorem	issalgend 47424*	One side of dfsalgen2 47427. If a sigma-algebra on ∪ 𝑋 includes 𝑋 and it is included in all the sigma-algebras with such two properties, then it is the sigma-algebra generated by 𝑋. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → ∪ 𝑆 = ∪ 𝑋)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑆)    &   ⊢ ((𝜑 ∧ (𝑦 ∈ SAlg ∧ ∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦)) → 𝑆 ⊆ 𝑦)    ⇒   ⊢ (𝜑 → (SalGen‘𝑋) = 𝑆)
Theorem	salexct2 47425*	An example of a subset that does not belong to a nontrivial sigma-algebra, see salexct 47420. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ 𝐴 = (0[,]2)    &   ⊢ 𝑆 = {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω)}    &   ⊢ 𝐵 = (0[,]1)    ⇒   ⊢ ¬ 𝐵 ∈ 𝑆
Theorem	unisalgen 47426	The union of a set belongs to the sigma-algebra generated by the set. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ 𝑆 = (SalGen‘𝑋)    &   ⊢ 𝑈 = ∪ 𝑋    ⇒   ⊢ (𝜑 → 𝑈 ∈ 𝑆)
Theorem	dfsalgen2 47427*	Alternate characterization of the sigma-algebra generated by a set. It is the smallest sigma-algebra, on the same base set, that includes the set. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((SalGen‘𝑋) = 𝑆 ↔ ((𝑆 ∈ SAlg ∧ ∪ 𝑆 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑆) ∧ ∀𝑦 ∈ SAlg ((∪ 𝑦 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑦) → 𝑆 ⊆ 𝑦))))
Theorem	salexct3 47428*	An example of a sigma-algebra that's not closed under uncountable union. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ 𝐴 = (0[,]2)    &   ⊢ 𝑆 = {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω)}    &   ⊢ 𝑋 = ran (𝑦 ∈ (0[,]1) ↦ {𝑦})    ⇒   ⊢ (𝑆 ∈ SAlg ∧ 𝑋 ⊆ 𝑆 ∧ ¬ ∪ 𝑋 ∈ 𝑆)
Theorem	salgencntex 47429*	This counterexample shows that df-salgen 47399 needs to require that all containing sigma-algebra have the same base set. Otherwise, the intersection could lead to a set that is not a sigma-algebra. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ 𝐴 = (0[,]2)    &   ⊢ 𝑆 = {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω)}    &   ⊢ 𝐵 = (0[,]1)    &   ⊢ 𝑇 = 𝒫 𝐵    &   ⊢ 𝐶 = (𝑆 ∩ 𝑇)    &   ⊢ 𝑍 = ∩ {𝑠 ∈ SAlg ∣ 𝐶 ⊆ 𝑠}    ⇒   ⊢ ¬ 𝑍 ∈ SAlg
Theorem	salgensscntex 47430*	This counterexample shows that the sigma-algebra generated by a set is not the smallest sigma-algebra containing the set, if we consider also sigma-algebras with a larger base set. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ 𝐴 = (0[,]2)    &   ⊢ 𝑆 = {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω)}    &   ⊢ 𝑋 = ran (𝑦 ∈ (0[,]1) ↦ {𝑦})    &   ⊢ 𝐺 = (SalGen‘𝑋)    ⇒   ⊢ (𝑋 ⊆ 𝑆 ∧ 𝑆 ∈ SAlg ∧ ¬ 𝐺 ⊆ 𝑆)
Theorem	issalnnd 47431*	Sufficient condition to prove that 𝑆 is sigma-algebra. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → ∅ ∈ 𝑆)    &   ⊢ 𝑋 = ∪ 𝑆    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝑋 ∖ 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑒:ℕ⟶𝑆) → ∪ 𝑛 ∈ ℕ (𝑒‘𝑛) ∈ 𝑆)    ⇒   ⊢ (𝜑 → 𝑆 ∈ SAlg)
Theorem	dmvolsal 47432	Lebesgue measurable sets form a sigma-algebra. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ dom vol ∈ SAlg
Theorem	saldifcld 47433	The complement of an element of a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (∪ 𝑆 ∖ 𝐸) ∈ 𝑆)
Theorem	saluncld 47434	The union of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐸 ∪ 𝐹) ∈ 𝑆)
Theorem	salgencld 47435	SalGen actually generates a sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ 𝑆 = (SalGen‘𝑋)    ⇒   ⊢ (𝜑 → 𝑆 ∈ SAlg)
Theorem	0sald 47436	The empty set belongs to every sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    ⇒   ⊢ (𝜑 → ∅ ∈ 𝑆)
Theorem	iooborel 47437	An open interval is a Borel set. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐵 = (SalGen‘𝐽)    ⇒   ⊢ (𝐴(,)𝐶) ∈ 𝐵
Theorem	salincld 47438	The intersection of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐸 ∩ 𝐹) ∈ 𝑆)
Theorem	salunid 47439	A set is an element of any sigma-algebra on it. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    ⇒   ⊢ (𝜑 → ∪ 𝑆 ∈ 𝑆)
Theorem	unisalgen2 47440	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 47441	The Borel sigma-algebra on the Reals. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐵 = (SalGen‘𝐽)    ⇒   ⊢ 𝐵 ∈ SAlg
Theorem	iocborel 47442	A left-open, right-closed interval is a Borel set. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐵 = (SalGen‘𝐽)    ⇒   ⊢ (𝜑 → (𝐴(,]𝐶) ∈ 𝐵)
Theorem	subsaliuncllem 47443*	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 47444*	A subspace sigma-algebra is closed under countable union. This is Lemma 121A (iii) of [Fremlin1] p. 35. The proof uses fnrndomnum 10618 rather than fnrndomg 10619, and so does not require ax-ac 10538. (Contributed by Glauco Siliprandi, 26-Jun-2021.) (Revised by Vincent Gonzalez, 30-Aug-2026.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ 𝑇 = (𝑆 ↾t 𝐷)    &   ⊢ (𝜑 → 𝐹:ℕ⟶𝑇)    ⇒   ⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) ∈ 𝑇)
Theorem	subsalsal 47445	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 47446	A set belongs to the subspace sigma-algebra it induces. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝑆)    ⇒   ⊢ (𝜑 → 𝐴 ∈ (𝑆 ↾t 𝐴))
Theorem	salrestss 47447	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.47.19.2  Sum of nonnegative extended reals
Syntax	csumge0 47448	Extend class notation to include the sum of nonnegative extended reals.
class Σ^
Definition	df-sumge0 47449*	Define the arbitrary sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) $.
⊢ Σ^ = (𝑥 ∈ V ↦ if(+∞ ∈ ran 𝑥, +∞, sup(ran (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)), ℝ*, < )))
Theorem	sge0rnre 47450*	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 47451	If 𝐹 maps to nonnegative reals, then 𝐹 maps to nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐹:𝑋⟶(0[,)+∞))    ⇒   ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))
Theorem	sge0val 47452*	The value of the sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) → (Σ^‘𝐹) = if(+∞ ∈ ran 𝐹, +∞, sup(ran (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝐹‘𝑤)), ℝ*, < )))
Theorem	fge0npnf 47453	If 𝐹 maps to nonnegative reals, then +∞ is not in its range. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐹:𝑋⟶(0[,)+∞))    ⇒   ⊢ (𝜑 → ¬ +∞ ∈ ran 𝐹)
Theorem	sge0rnn0 47454*	The range used in the definition of Σ^ is not empty. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ≠ ∅
Theorem	sge0vald 47455*	The value of the sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))    ⇒   ⊢ (𝜑 → (Σ^‘𝐹) = if(+∞ ∈ ran 𝐹, +∞, sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, < )))
Theorem	fge0iccico 47456	A range of nonnegative extended reals without plus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))    &   ⊢ (𝜑 → ¬ +∞ ∈ ran 𝐹)    ⇒   ⊢ (𝜑 → 𝐹:𝑋⟶(0[,)+∞))
Theorem	gsumge0cl 47457	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 47458*	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 47459	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 47460	A range of nonnegative extended reals without plus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))    &   ⊢ (𝜑 → ¬ +∞ ∈ ran 𝐹)    ⇒   ⊢ (𝜑 → 𝐹:𝑋⟶ℝ)
Theorem	sge0z 47461*	Any nonnegative extended sum of zero is zero. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 0)) = 0)
Theorem	sge00 47462	The sum of nonnegative extended reals is zero when applied to the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (Σ^‘∅) = 0
Theorem	fsumlesge0 47463*	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 47464*	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 47465	A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:{𝐴}⟶(0[,]+∞))    ⇒   ⊢ (𝜑 → (Σ^‘𝐹) = (𝐹‘𝐴))
Theorem	sge0tsms 47466	Σ^ 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 47467	The arbitrary sum of nonnegative extended reals is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))    ⇒   ⊢ (𝜑 → (Σ^‘𝐹) ∈ (0[,]+∞))
Theorem	sge0f1o 47468*	Re-index a nonnegative extended sum using a bijection. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑛𝜑    &   ⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷)))
Theorem	sge0snmpt 47469*	A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ (0[,]+∞))    &   ⊢ (𝑘 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (Σ^‘(𝑘 ∈ {𝐴} ↦ 𝐵)) = 𝐶)
Theorem	sge0ge0 47470	The sum of nonnegative extended reals is nonnegative. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))    ⇒   ⊢ (𝜑 → 0 ≤ (Σ^‘𝐹))
Theorem	sge0xrcl 47471	The arbitrary sum of nonnegative extended reals is an extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))    ⇒   ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ*)
Theorem	sge0repnf 47472	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 47473*	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 47474	If the sum of nonnegative extended reals is not +∞ then no terms is +∞. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))    &   ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ)    ⇒   ⊢ (𝜑 → ¬ +∞ ∈ ran 𝐹)
Theorem	sge0supre 47475*	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 47477, but here we can use sup with respect to ℝ instead of ℝ*. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))    &   ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ)    ⇒   ⊢ (𝜑 → (Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ))
Theorem	sge0fsummpt 47476*	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 47477*	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 47478	A shorter sum of nonnegative extended reals is smaller than a longer one. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))    ⇒   ⊢ (𝜑 → (Σ^‘(𝐹 ↾ 𝑌)) ≤ (Σ^‘𝐹))
Theorem	sge0rnbnd 47479*	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 47480*	Sum of a pair of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐷 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐸 ∈ (0[,]+∞))    &   ⊢ (𝑘 = 𝐴 → 𝐶 = 𝐷)    &   ⊢ (𝑘 = 𝐵 → 𝐶 = 𝐸)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → (Σ^‘(𝑘 ∈ {𝐴, 𝐵} ↦ 𝐶)) = (𝐷 +e 𝐸))
Theorem	sge0gerp 47481*	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)𝐴 ≤ ((Σ^‘(𝐹 ↾ 𝑧)) +e 𝑥))    ⇒   ⊢ (𝜑 → 𝐴 ≤ (Σ^‘𝐹))
Theorem	sge0pnffigt 47482*	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 47483	If a sum of nonnegative extended reals is real, than any subsum is real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))    &   ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ)    ⇒   ⊢ (𝜑 → (Σ^‘(𝐹 ↾ 𝑌)) ∈ ℝ)
Theorem	sge0lefi 47484*	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 47485*	A shorter sum of nonnegative extended reals is smaller than a longer one. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐶 ↦ 𝐵)) ≤ (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)))
Theorem	sge0ltfirp 47486*	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 47487*	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 47480. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐷 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐸 ∈ (0[,]+∞))    &   ⊢ (𝑘 = 𝐴 → 𝐶 = 𝐷)    &   ⊢ (𝑘 = 𝐵 → 𝐶 = 𝐸)    ⇒   ⊢ (𝜑 → (Σ^‘(𝑘 ∈ {𝐴, 𝐵} ↦ 𝐶)) ≤ (𝐷 +e 𝐸))
Theorem	sge0gerpmpt 47488*	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)𝐶 ≤ ((Σ^‘(𝑥 ∈ 𝑧 ↦ 𝐵)) +e 𝑦))    ⇒   ⊢ (𝜑 → 𝐶 ≤ (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)))
Theorem	sge0resrnlem 47489	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 47490	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 47491*	If a sum of nonnegative extended reals is real, than any subsum is real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)) ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐶 ↦ 𝐵)) ∈ ℝ)
Theorem	sge0resplit 47492	Σ^ splits into two parts, when it's a real number. This is a special case of sge0split 47495. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝑈 = (𝐴 ∪ 𝐵)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ (𝜑 → 𝐹:𝑈⟶(0[,]+∞))    &   ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ)    ⇒   ⊢ (𝜑 → (Σ^‘𝐹) = ((Σ^‘(𝐹 ↾ 𝐴)) + (Σ^‘(𝐹 ↾ 𝐵))))
Theorem	sge0le 47493*	If all of the terms of sums compare, so do the sums. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))    &   ⊢ (𝜑 → 𝐺:𝑋⟶(0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ≤ (𝐺‘𝑥))    ⇒   ⊢ (𝜑 → (Σ^‘𝐹) ≤ (Σ^‘𝐺))
Theorem	sge0ltfirpmpt 47494*	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 47495	Split a sum of nonnegative extended reals into two parts. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝑈 = (𝐴 ∪ 𝐵)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ (𝜑 → 𝐹:𝑈⟶(0[,]+∞))    ⇒   ⊢ (𝜑 → (Σ^‘𝐹) = ((Σ^‘(𝐹 ↾ 𝐴)) +e (Σ^‘(𝐹 ↾ 𝐵))))
Theorem	sge0lempt 47496*	If all of the terms of sums compare, so do the sums. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ 𝐶)    ⇒   ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)) ≤ (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐶)))
Theorem	sge0splitmpt 47497*	Split a sum of nonnegative extended reals into two parts. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → (Σ^‘(𝑥 ∈ (𝐴 ∪ 𝐵) ↦ 𝐶)) = ((Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐶)) +e (Σ^‘(𝑥 ∈ 𝐵 ↦ 𝐶))))
Theorem	sge0ss 47498*	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 47499*	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 47500*	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)) ↦ 𝐴)) = ((Σ^‘(𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)) +e 𝐵))