fsumlesge0

Description: 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)

	Ref	Expression
Hypotheses	fsumlesge0.x	$⊢ φ \to X \in V$
	fsumlesge0.f	$⊢ φ \to F : X ⟶ [0, +∞)$
	fsumlesge0.y	$⊢ φ \to Y \subseteq X$
	fsumlesge0.fi	$⊢ φ \to Y \in Fin$
Assertion	fsumlesge0	$⊢ φ \to \sum_{x \in Y} F (x) \leq sum^(F)$

Proof

Step	Hyp	Ref	Expression
1		fsumlesge0.x	$⊢ φ \to X \in V$
2		fsumlesge0.f	$⊢ φ \to F : X ⟶ [0, +∞)$
3		fsumlesge0.y	$⊢ φ \to Y \subseteq X$
4		fsumlesge0.fi	$⊢ φ \to Y \in Fin$
5	2	sge0rnre	$⊢ φ \to ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{z \in y} F (z)) \subseteq ℝ$
6		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
7	6	a1i	$⊢ φ \to ℝ \subseteq ℝ^{*}$
8	5 7	sstrd	$⊢ φ \to ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{z \in y} F (z)) \subseteq ℝ^{*}$
9	1 3	ssexd	$⊢ φ \to Y \in V$
10		elpwg	$⊢ Y \in V \to (Y \in 𝒫 X \leftrightarrow Y \subseteq X)$
11	9 10	syl	$⊢ φ \to (Y \in 𝒫 X \leftrightarrow Y \subseteq X)$
12	3 11	mpbird	$⊢ φ \to Y \in 𝒫 X$
13	12 4	elind	$⊢ φ \to Y \in (𝒫 X \cap Fin)$
14		fveq2	$⊢ x = z \to F (x) = F (z)$
15	14	cbvsumv	$⊢ \sum_{x \in Y} F (x) = \sum_{z \in Y} F (z)$
16	15	a1i	$⊢ φ \to \sum_{x \in Y} F (x) = \sum_{z \in Y} F (z)$
17		sumeq1	$⊢ y = Y \to \sum_{z \in y} F (z) = \sum_{z \in Y} F (z)$
18	17	rspceeqv	$⊢ (Y \in (𝒫 X \cap Fin) \land \sum_{x \in Y} F (x) = \sum_{z \in Y} F (z)) \to \exists y \in (𝒫 X \cap Fin) \sum_{x \in Y} F (x) = \sum_{z \in y} F (z)$
19	13 16 18	syl2anc	$⊢ φ \to \exists y \in (𝒫 X \cap Fin) \sum_{x \in Y} F (x) = \sum_{z \in y} F (z)$
20		sumex	$⊢ \sum_{x \in Y} F (x) \in V$
21	20	a1i	$⊢ φ \to \sum_{x \in Y} F (x) \in V$
22		eqid	$⊢ (y \in (𝒫 X \cap Fin) ⟼ \sum_{z \in y} F (z)) = (y \in (𝒫 X \cap Fin) ⟼ \sum_{z \in y} F (z))$
23	22	elrnmpt	$⊢ \sum_{x \in Y} F (x) \in V \to (\sum_{x \in Y} F (x) \in ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{z \in y} F (z)) \leftrightarrow \exists y \in (𝒫 X \cap Fin) \sum_{x \in Y} F (x) = \sum_{z \in y} F (z))$
24	21 23	syl	$⊢ φ \to (\sum_{x \in Y} F (x) \in ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{z \in y} F (z)) \leftrightarrow \exists y \in (𝒫 X \cap Fin) \sum_{x \in Y} F (x) = \sum_{z \in y} F (z))$
25	19 24	mpbird	$⊢ φ \to \sum_{x \in Y} F (x) \in ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{z \in y} F (z))$
26		supxrub	$⊢ (ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{z \in y} F (z)) \subseteq ℝ^{} \land \sum_{x \in Y} F (x) \in ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{z \in y} F (z))) \to \sum_{x \in Y} F (x) \leq sup (ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{z \in y} F (z)) ℝ^{} <)$
27	8 25 26	syl2anc	$⊢ φ \to \sum_{x \in Y} F (x) \leq sup (ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{z \in y} F (z)) ℝ^{*} <)$
28	1 2	sge0reval	$⊢ φ \to sum^(F) = sup (ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{z \in y} F (z)) ℝ^{*} <)$
29	28	eqcomd	$⊢ φ \to sup (ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{z \in y} F (z)) ℝ^{*} <) = sum^(F)$
30	27 29	breqtrd	$⊢ φ \to \sum_{x \in Y} F (x) \leq sum^(F)$

Metamath Proof Explorer

Theorem fsumlesge0

Proof