P. 465 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 46401-46500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sge0repnf 46401	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 46402*	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 46403	If the sum of nonnegative extended reals is not +∞ then no terms is +∞. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))    &   ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ)    ⇒   ⊢ (𝜑 → ¬ +∞ ∈ ran 𝐹)
Theorem	sge0supre 46404*	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 46406, but here we can use sup with respect to ℝ instead of ℝ*. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))    &   ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ)    ⇒   ⊢ (𝜑 → (Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ))
Theorem	sge0fsummpt 46405*	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 46406*	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 46407	A shorter sum of nonnegative extended reals is smaller than a longer one. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))    ⇒   ⊢ (𝜑 → (Σ^‘(𝐹 ↾ 𝑌)) ≤ (Σ^‘𝐹))
Theorem	sge0rnbnd 46408*	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 46409*	Sum of a pair of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐷 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐸 ∈ (0[,]+∞))    &   ⊢ (𝑘 = 𝐴 → 𝐶 = 𝐷)    &   ⊢ (𝑘 = 𝐵 → 𝐶 = 𝐸)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → (Σ^‘(𝑘 ∈ {𝐴, 𝐵} ↦ 𝐶)) = (𝐷 +𝑒 𝐸))
Theorem	sge0gerp 46410*	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 46411*	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 46412	If a sum of nonnegative extended reals is real, than any subsum is real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))    &   ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ)    ⇒   ⊢ (𝜑 → (Σ^‘(𝐹 ↾ 𝑌)) ∈ ℝ)
Theorem	sge0lefi 46413*	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 46414*	A shorter sum of nonnegative extended reals is smaller than a longer one. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐶 ↦ 𝐵)) ≤ (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)))
Theorem	sge0ltfirp 46415*	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 46416*	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 46409. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐷 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐸 ∈ (0[,]+∞))    &   ⊢ (𝑘 = 𝐴 → 𝐶 = 𝐷)    &   ⊢ (𝑘 = 𝐵 → 𝐶 = 𝐸)    ⇒   ⊢ (𝜑 → (Σ^‘(𝑘 ∈ {𝐴, 𝐵} ↦ 𝐶)) ≤ (𝐷 +𝑒 𝐸))
Theorem	sge0gerpmpt 46417*	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 46418	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 46419	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 46420*	If a sum of nonnegative extended reals is real, than any subsum is real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)) ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐶 ↦ 𝐵)) ∈ ℝ)
Theorem	sge0resplit 46421	Σ^ splits into two parts, when it's a real number. This is a special case of sge0split 46424. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝑈 = (𝐴 ∪ 𝐵)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ (𝜑 → 𝐹:𝑈⟶(0[,]+∞))    &   ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ)    ⇒   ⊢ (𝜑 → (Σ^‘𝐹) = ((Σ^‘(𝐹 ↾ 𝐴)) + (Σ^‘(𝐹 ↾ 𝐵))))
Theorem	sge0le 46422*	If all of the terms of sums compare, so do the sums. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))    &   ⊢ (𝜑 → 𝐺:𝑋⟶(0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ≤ (𝐺‘𝑥))    ⇒   ⊢ (𝜑 → (Σ^‘𝐹) ≤ (Σ^‘𝐺))
Theorem	sge0ltfirpmpt 46423*	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 46424	Split a sum of nonnegative extended reals into two parts. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝑈 = (𝐴 ∪ 𝐵)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ (𝜑 → 𝐹:𝑈⟶(0[,]+∞))    ⇒   ⊢ (𝜑 → (Σ^‘𝐹) = ((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 (Σ^‘(𝐹 ↾ 𝐵))))
Theorem	sge0lempt 46425*	If all of the terms of sums compare, so do the sums. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ 𝐶)    ⇒   ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)) ≤ (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐶)))
Theorem	sge0splitmpt 46426*	Split a sum of nonnegative extended reals into two parts. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → (Σ^‘(𝑥 ∈ (𝐴 ∪ 𝐵) ↦ 𝐶)) = ((Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐶)) +𝑒 (Σ^‘(𝑥 ∈ 𝐵 ↦ 𝐶))))
Theorem	sge0ss 46427*	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 46428*	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 46429*	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 46430*	Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ)    &   ⊢ (𝜑 → (Σ^‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) ∈ ℝ*)    &   ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐴 ↦ (Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ∈ ℝ*)    &   ⊢ (𝜑 → (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶):∪ 𝑥 ∈ 𝐴 𝐵⟶(0[,]+∞))    &   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)    ⇒   ⊢ (𝜑 → (Σ^‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^‘(𝑥 ∈ 𝐴 ↦ (Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
Theorem	sge0fodjrnlem 46431*	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 46432*	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 46433*	Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → (Σ^‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^‘(𝑥 ∈ 𝐴 ↦ (Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
Theorem	sge0iun 46434*	Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)    &   ⊢ 𝑋 = ∪ 𝑥 ∈ 𝐴 𝐵    &   ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))    &   ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)    ⇒   ⊢ (𝜑 → (Σ^‘𝐹) = (Σ^‘(𝑥 ∈ 𝐴 ↦ (Σ^‘(𝐹 ↾ 𝐵)))))
Theorem	sge0nemnf 46435	The generalized sum of nonnegative extended reals is not minus infinity. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶(0[,]+∞))    ⇒   ⊢ (𝜑 → (Σ^‘𝐹) ≠ -∞)
Theorem	sge0rpcpnf 46436*	The sum of an infinite number of a positive constant, is +∞ (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)) = +∞)
Theorem	sge0rernmpt 46437*	If the sum of nonnegative extended reals is not +∞ then no term is +∞. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)) ∈ ℝ)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞))
Theorem	sge0lefimpt 46438*	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 46439	Nonnegative integers are nonnegative reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ ℕ0 ⊆ (0[,)+∞)
Theorem	sge0clmpt 46440*	The generalized sum of nonnegative extended reals is a nonnegative extended real. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)) ∈ (0[,]+∞))
Theorem	sge0ltfirpmpt2 46441*	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 46442	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 46443*	The generalized sum of nonnegative extended reals is an extended real. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)) ∈ ℝ*)
Theorem	sge0xp 46444*	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 46445*	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 46446*	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 46447*	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 46448*	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 46449*	The extended addition of two generalized sums of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,)+∞))    &   ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) ∈ ℝ)    &   ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶)) ∈ ℝ)    ⇒   ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ (𝐵 +𝑒 𝐶))) = ((Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) +𝑒 (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶))))
Theorem	sge0xadd 46450*	The extended addition of two generalized sums of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ (𝐵 +𝑒 𝐶))) = ((Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) +𝑒 (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶))))
Theorem	sge0fsummptf 46451*	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 46452*	A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ (0[,]+∞))    &   ⊢ (𝑘 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (Σ^‘(𝑘 ∈ {𝐴} ↦ 𝐵)) = 𝐶)
Theorem	sge0ge0mpt 46453*	The sum of nonnegative extended reals is nonnegative. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → 0 ≤ (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)))
Theorem	sge0repnfmpt 46454*	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 46455*	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 46456*	Separate out a term in a generalized sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞))    &   ⊢ (𝑘 = 𝐵 → 𝐶 = 𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → (Σ^‘(𝑘 ∈ (𝐴 ∪ {𝐵}) ↦ 𝐶)) = ((Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶)) +𝑒 𝐷))
Theorem	sge0pnffsumgt 46457*	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 46458*	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 46459*	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 46460*	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 46461	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 46462*	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 46463*	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 46464	Extend class notation with the class of measures.
class Meas
Definition	df-mea 46465*	Define the class of measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Meas = {𝑥 ∣ (((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 ∈ SAlg) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥((𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤) → (𝑥‘∪ 𝑦) = (Σ^‘(𝑥 ↾ 𝑦))))}
Theorem	ismea 46466*	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 46467	The domain of a measure is a sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ 𝑆 = dom 𝑀    ⇒   ⊢ (𝜑 → 𝑆 ∈ SAlg)
Theorem	meaf 46468	A measure is a function that maps to nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ 𝑆 = dom 𝑀    ⇒   ⊢ (𝜑 → 𝑀:𝑆⟶(0[,]+∞))
Theorem	mea0 46469	The measure of the empty set is always 0 . (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑀 ∈ Meas)    ⇒   ⊢ (𝜑 → (𝑀‘∅) = 0)
Theorem	nnfoctbdjlem 46470*	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 46471*	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 46472*	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 46473	The measure of a set is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ 𝑆 = dom 𝑀    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) ∈ (0[,]+∞))
Theorem	iundjiunlem 46474*	The sets in the sequence 𝐹 are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ 𝑍 = (ℤ≥‘𝑁)    &   ⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)))    &   ⊢ (𝜑 → 𝐽 ∈ 𝑍)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑍)    &   ⊢ (𝜑 → 𝐽 < 𝐾)    ⇒   ⊢ (𝜑 → ((𝐹‘𝐽) ∩ (𝐹‘𝐾)) = ∅)
Theorem	iundjiun 46475*	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 46476	The measure of a set is an extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ 𝑆 = dom 𝑀    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) ∈ ℝ*)
Theorem	meadjun 46477	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 46478	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 46479	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 46480*	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 46481*	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 46482*	Sufficient condition to prove that 𝑀 is a measure. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝑀:𝑆⟶(0[,]+∞))    &   ⊢ (𝜑 → (𝑀‘∅) = 0)    &   ⊢ ((𝜑 ∧ 𝑒:ℕ⟶𝑆 ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛)) → (𝑀‘∪ 𝑛 ∈ ℕ (𝑒‘𝑛)) = (Σ^‘(𝑛 ∈ ℕ ↦ (𝑀‘(𝑒‘𝑛)))))    ⇒   ⊢ (𝜑 → 𝑀 ∈ Meas)
Theorem	meaiunlelem 46483*	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 46484*	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	psmeasurelem 46485*	𝑀 applied to a disjoint union of subsets of its domain is the sum of 𝑀 applied to such subset. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐻:𝑋⟶(0[,]+∞))    &   ⊢ 𝑀 = (𝑥 ∈ 𝒫 𝑋 ↦ (Σ^‘(𝐻 ↾ 𝑥)))    &   ⊢ (𝜑 → 𝑀:𝒫 𝑋⟶(0[,]+∞))    &   ⊢ (𝜑 → 𝑌 ⊆ 𝒫 𝑋)    &   ⊢ (𝜑 → Disj 𝑦 ∈ 𝑌 𝑦)    ⇒   ⊢ (𝜑 → (𝑀‘∪ 𝑌) = (Σ^‘(𝑀 ↾ 𝑌)))
Theorem	psmeasure 46486*	Point supported measure, Remark 112B (d) of [Fremlin1] p. 15. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐻:𝑋⟶(0[,]+∞))    &   ⊢ 𝑀 = (𝑥 ∈ 𝒫 𝑋 ↦ (Σ^‘(𝐻 ↾ 𝑥)))    ⇒   ⊢ (𝜑 → 𝑀 ∈ Meas)
Theorem	voliunsge0lem 46487*	The Lebesgue measure function is countably additive. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ 𝑆 = seq1( + , 𝐺)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝐸‘𝑛)))    &   ⊢ (𝜑 → 𝐸:ℕ⟶dom vol)    &   ⊢ (𝜑 → Disj 𝑛 ∈ ℕ (𝐸‘𝑛))    ⇒   ⊢ (𝜑 → (vol‘∪ 𝑛 ∈ ℕ (𝐸‘𝑛)) = (Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(𝐸‘𝑛)))))
Theorem	voliunsge0 46488*	The Lebesgue measure function is countably additive. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐸:ℕ⟶dom vol)    &   ⊢ (𝜑 → Disj 𝑛 ∈ ℕ (𝐸‘𝑛))    ⇒   ⊢ (𝜑 → (vol‘∪ 𝑛 ∈ ℕ (𝐸‘𝑛)) = (Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(𝐸‘𝑛)))))
Theorem	volmea 46489	The Lebesgue measure on the Reals is actually a measure. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → vol ∈ Meas)
Theorem	meage0 46490	If the measure of a measurable set is greater than or equal to 0. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ (𝜑 → 𝐴 ∈ dom 𝑀)    ⇒   ⊢ (𝜑 → 0 ≤ (𝑀‘𝐴))
Theorem	meadjunre 46491	The measure of the union of two disjoint sets, with finite measure, is the sum of the measures, Property 112C (a) of [Fremlin1] p. 15. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ 𝑆 = dom 𝑀    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ (𝜑 → (𝑀‘𝐴) ∈ ℝ)    &   ⊢ (𝜑 → (𝑀‘𝐵) ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝑀‘(𝐴 ∪ 𝐵)) = ((𝑀‘𝐴) + (𝑀‘𝐵)))
Theorem	meassre 46492	If the measure of a measurable set is real, then the measure of any of its measurable subsets is real. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ (𝜑 → 𝐴 ∈ dom 𝑀)    &   ⊢ (𝜑 → (𝑀‘𝐴) ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ dom 𝑀)    ⇒   ⊢ (𝜑 → (𝑀‘𝐵) ∈ ℝ)
Theorem	meale0eq0 46493	A measure that is less than or equal to 0 is 0. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ (𝜑 → 𝐴 ∈ dom 𝑀)    &   ⊢ (𝜑 → (𝑀‘𝐴) ≤ 0)    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) = 0)
Theorem	meadif 46494	The measure of the difference of two sets. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ (𝜑 → 𝐴 ∈ dom 𝑀)    &   ⊢ (𝜑 → (𝑀‘𝐴) ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ dom 𝑀)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (𝑀‘(𝐴 ∖ 𝐵)) = ((𝑀‘𝐴) − (𝑀‘𝐵)))
Theorem	meaiuninclem 46495*	Measures are continuous from below (bounded case): if 𝐸 is a sequence of increasing measurable sets (with uniformly bounded measure) then the measure of the union is the union of the measure. This is Proposition 112C (e) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑁)    &   ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1)))    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)    &   ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))    &   ⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)))    ⇒   ⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))
Theorem	meaiuninc 46496*	Measures are continuous from below (bounded case): if 𝐸 is a sequence of nondecreasing measurable sets (with bounded measure) then the measure of the union is the limit of the measures. This is Proposition 112C (e) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑁)    &   ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1)))    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)    &   ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))    ⇒   ⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))
Theorem	meaiuninc2 46497*	Measures are continuous from below (bounded case): if 𝐸 is a sequence of nondecreasing measurable sets (with bounded measure) then the measure of the union is the limit of the measures. This is Proposition 112C (e) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑁)    &   ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1)))    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ≤ 𝐵)    &   ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))    ⇒   ⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))
Theorem	meaiunincf 46498*	Measures are continuous from below (bounded case): if 𝐸 is a sequence of nondecreasing measurable sets (with bounded measure) then the measure of the union is the limit of the measures. This is Proposition 112C (e) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 13-Feb-2022.)
⊢ Ⅎ𝑛𝜑    &   ⊢ Ⅎ𝑛𝐸    &   ⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑁)    &   ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1)))    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)    &   ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))    ⇒   ⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))
Theorem	meaiuninc3v 46499*	Measures are continuous from below: if 𝐸 is a sequence of nondecreasing measurable sets (with bounded measure) then the measure of the union is the limit of the measures. This is the general case of Proposition 112C (e) of [Fremlin1] p. 16 . This theorem generalizes meaiuninc 46496 and meaiuninc2 46497 where the sequence is required to be bounded. (Contributed by Glauco Siliprandi, 13-Feb-2022.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑁)    &   ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1)))    &   ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))    ⇒   ⊢ (𝜑 → 𝑆~~>*(𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))
Theorem	meaiuninc3 46500*	Measures are continuous from below: if 𝐸 is a sequence of nondecreasing measurable sets (with bounded measure) then the measure of the union is the limit of the measures. This is the general case of Proposition 112C (e) of [Fremlin1] p. 16 . This theorem generalizes meaiuninc 46496 and meaiuninc2 46497 where the sequence is required to be bounded. (Contributed by Glauco Siliprandi, 13-Feb-2022.)
⊢ Ⅎ𝑛𝜑    &   ⊢ Ⅎ𝑛𝐸    &   ⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑁)    &   ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1)))    &   ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))    ⇒   ⊢ (𝜑 → 𝑆~~>*(𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))