sge0cl

Description: The arbitrary sum of nonnegative extended reals is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0cl.x	$⊢ φ \to X \in V$
	sge0cl.f	$⊢ φ \to F : X ⟶ [0, +∞]$
Assertion	sge0cl	$⊢ φ \to sum^(F) \in [0, +∞]$

Proof

Step	Hyp	Ref	Expression
1		sge0cl.x	$⊢ φ \to X \in V$
2		sge0cl.f	$⊢ φ \to F : X ⟶ [0, +∞]$
3		fveq2	$⊢ F = \emptyset \to sum^(F) = sum^(\emptyset)$
4		sge00	$⊢ sum^(\emptyset) = 0$
5	4	a1i	$⊢ F = \emptyset \to sum^(\emptyset) = 0$
6	3 5	eqtrd	$⊢ F = \emptyset \to sum^(F) = 0$
7		0e0iccpnf	$⊢ 0 \in [0, +∞]$
8	7	a1i	$⊢ F = \emptyset \to 0 \in [0, +∞]$
9	6 8	eqeltrd	$⊢ F = \emptyset \to sum^(F) \in [0, +∞]$
10	9	adantl	$⊢ (φ \land F = \emptyset) \to sum^(F) \in [0, +∞]$
11	1	adantr	$⊢ (φ \land +∞ \in ran F) \to X \in V$
12	2	adantr	$⊢ (φ \land +∞ \in ran F) \to F : X ⟶ [0, +∞]$
13		simpr	$⊢ (φ \land +∞ \in ran F) \to +∞ \in ran F$
14	11 12 13	sge0pnfval	$⊢ (φ \land +∞ \in ran F) \to sum^(F) = +∞$
15		pnfel0pnf	$⊢ +∞ \in [0, +∞]$
16	15	a1i	$⊢ (φ \land +∞ \in ran F) \to +∞ \in [0, +∞]$
17	14 16	eqeltrd	$⊢ (φ \land +∞ \in ran F) \to sum^(F) \in [0, +∞]$
18	17	adantlr	$⊢ ((φ \land \neg F = \emptyset) \land +∞ \in ran F) \to sum^(F) \in [0, +∞]$
19		simpll	$⊢ ((φ \land \neg F = \emptyset) \land \neg +∞ \in ran F) \to φ$
20		neqne	$⊢ \neg F = \emptyset \to F \neq \emptyset$
21	20	ad2antlr	$⊢ ((φ \land \neg F = \emptyset) \land \neg +∞ \in ran F) \to F \neq \emptyset$
22		simpr	$⊢ ((φ \land \neg F = \emptyset) \land \neg +∞ \in ran F) \to \neg +∞ \in ran F$
23		0xr	$⊢ 0 \in ℝ^{*}$
24	23	a1i	$⊢ ((φ \land F \neq \emptyset) \land \neg +∞ \in ran F) \to 0 \in ℝ^{*}$
25		pnfxr	$⊢ +∞ \in ℝ^{*}$
26	25	a1i	$⊢ ((φ \land F \neq \emptyset) \land \neg +∞ \in ran F) \to +∞ \in ℝ^{*}$
27	1	adantr	$⊢ (φ \land \neg +∞ \in ran F) \to X \in V$
28	2	adantr	$⊢ (φ \land \neg +∞ \in ran F) \to F : X ⟶ [0, +∞]$
29		simpr	$⊢ (φ \land \neg +∞ \in ran F) \to \neg +∞ \in ran F$
30	28 29	fge0iccico	$⊢ (φ \land \neg +∞ \in ran F) \to F : X ⟶ [0, +∞)$
31	27 30	sge0reval	$⊢ (φ \land \neg +∞ \in ran F) \to sum^(F) = sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ^{*} <)$
32		elinel2	$⊢ x \in (𝒫 X \cap Fin) \to x \in Fin$
33	32	adantl	$⊢ ((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \to x \in Fin$
34	2	ad2antrr	$⊢ ((φ \land x \in (𝒫 X \cap Fin)) \land y \in x) \to F : X ⟶ [0, +∞]$
35		elinel1	$⊢ x \in (𝒫 X \cap Fin) \to x \in 𝒫 X$
36		elpwi	$⊢ x \in 𝒫 X \to x \subseteq X$
37	35 36	syl	$⊢ x \in (𝒫 X \cap Fin) \to x \subseteq X$
38	37	adantl	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to x \subseteq X$
39	38	adantr	$⊢ ((φ \land x \in (𝒫 X \cap Fin)) \land y \in x) \to x \subseteq X$
40		simpr	$⊢ ((φ \land x \in (𝒫 X \cap Fin)) \land y \in x) \to y \in x$
41	39 40	sseldd	$⊢ ((φ \land x \in (𝒫 X \cap Fin)) \land y \in x) \to y \in X$
42	34 41	ffvelrnd	$⊢ ((φ \land x \in (𝒫 X \cap Fin)) \land y \in x) \to F (y) \in [0, +∞]$
43	42	adantllr	$⊢ (((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \land y \in x) \to F (y) \in [0, +∞]$
44		nne	$⊢ \neg F (y) \neq +∞ \leftrightarrow F (y) = +∞$
45	44	biimpi	$⊢ \neg F (y) \neq +∞ \to F (y) = +∞$
46	45	eqcomd	$⊢ \neg F (y) \neq +∞ \to +∞ = F (y)$
47	46	adantl	$⊢ ((((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \land y \in x) \land \neg F (y) \neq +∞) \to +∞ = F (y)$
48	2	ffund	$⊢ φ \to Fun F$
49	48	3ad2ant1	$⊢ (φ \land x \in (𝒫 X \cap Fin) \land y \in x) \to Fun F$
50	41	3impa	$⊢ (φ \land x \in (𝒫 X \cap Fin) \land y \in x) \to y \in X$
51	2	fdmd	$⊢ φ \to dom F = X$
52	51	eqcomd	$⊢ φ \to X = dom F$
53	52	3ad2ant1	$⊢ (φ \land x \in (𝒫 X \cap Fin) \land y \in x) \to X = dom F$
54	50 53	eleqtrd	$⊢ (φ \land x \in (𝒫 X \cap Fin) \land y \in x) \to y \in dom F$
55		fvelrn	$⊢ (Fun F \land y \in dom F) \to F (y) \in ran F$
56	49 54 55	syl2anc	$⊢ (φ \land x \in (𝒫 X \cap Fin) \land y \in x) \to F (y) \in ran F$
57	56	ad5ant134	$⊢ ((((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \land y \in x) \land \neg F (y) \neq +∞) \to F (y) \in ran F$
58	47 57	eqeltrd	$⊢ ((((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \land y \in x) \land \neg F (y) \neq +∞) \to +∞ \in ran F$
59	29	ad3antrrr	$⊢ ((((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \land y \in x) \land \neg F (y) \neq +∞) \to \neg +∞ \in ran F$
60	58 59	condan	$⊢ (((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \land y \in x) \to F (y) \neq +∞$
61		ge0xrre	$⊢ (F (y) \in [0, +∞] \land F (y) \neq +∞) \to F (y) \in ℝ$
62	43 60 61	syl2anc	$⊢ (((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \land y \in x) \to F (y) \in ℝ$
63	33 62	fsumrecl	$⊢ ((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \to \sum_{y \in x} F (y) \in ℝ$
64	63	ralrimiva	$⊢ (φ \land \neg +∞ \in ran F) \to \forall x \in (𝒫 X \cap Fin) \sum_{y \in x} F (y) \in ℝ$
65		eqid	$⊢ (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) = (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y))$
66	65	rnmptss	$⊢ \forall x \in (𝒫 X \cap Fin) \sum_{y \in x} F (y) \in ℝ \to ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \subseteq ℝ$
67	64 66	syl	$⊢ (φ \land \neg +∞ \in ran F) \to ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \subseteq ℝ$
68		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
69	68	a1i	$⊢ (φ \land \neg +∞ \in ran F) \to ℝ \subseteq ℝ^{*}$
70	67 69	sstrd	$⊢ (φ \land \neg +∞ \in ran F) \to ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \subseteq ℝ^{*}$
71		supxrcl	$⊢ ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \subseteq ℝ^{} \to sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ^{} <) \in ℝ^{*}$
72	70 71	syl	$⊢ (φ \land \neg +∞ \in ran F) \to sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ^{} <) \in ℝ^{}$
73	31 72	eqeltrd	$⊢ (φ \land \neg +∞ \in ran F) \to sum^(F) \in ℝ^{*}$
74	73	adantlr	$⊢ ((φ \land F \neq \emptyset) \land \neg +∞ \in ran F) \to sum^(F) \in ℝ^{*}$
75	52	adantr	$⊢ (φ \land F \neq \emptyset) \to X = dom F$
76		neneq	$⊢ F \neq \emptyset \to \neg F = \emptyset$
77	76	adantl	$⊢ (φ \land F \neq \emptyset) \to \neg F = \emptyset$
78		frel	$⊢ F : X ⟶ [0, +∞] \to Rel F$
79	2 78	syl	$⊢ φ \to Rel F$
80	79	adantr	$⊢ (φ \land F \neq \emptyset) \to Rel F$
81		reldm0	$⊢ Rel F \to (F = \emptyset \leftrightarrow dom F = \emptyset)$
82	80 81	syl	$⊢ (φ \land F \neq \emptyset) \to (F = \emptyset \leftrightarrow dom F = \emptyset)$
83	77 82	mtbid	$⊢ (φ \land F \neq \emptyset) \to \neg dom F = \emptyset$
84	83	neqned	$⊢ (φ \land F \neq \emptyset) \to dom F \neq \emptyset$
85	75 84	eqnetrd	$⊢ (φ \land F \neq \emptyset) \to X \neq \emptyset$
86		n0	$⊢ X \neq \emptyset \leftrightarrow \exists z z \in X$
87	85 86	sylib	$⊢ (φ \land F \neq \emptyset) \to \exists z z \in X$
88	87	adantr	$⊢ ((φ \land F \neq \emptyset) \land \neg +∞ \in ran F) \to \exists z z \in X$
89	23	a1i	$⊢ ((φ \land \neg +∞ \in ran F) \land z \in X) \to 0 \in ℝ^{*}$
90	2	ffvelrnda	$⊢ (φ \land z \in X) \to F (z) \in [0, +∞]$
91	90	adantlr	$⊢ ((φ \land \neg +∞ \in ran F) \land z \in X) \to F (z) \in [0, +∞]$
92		nne	$⊢ \neg F (z) \neq +∞ \leftrightarrow F (z) = +∞$
93	92	biimpi	$⊢ \neg F (z) \neq +∞ \to F (z) = +∞$
94	93	eqcomd	$⊢ \neg F (z) \neq +∞ \to +∞ = F (z)$
95	94	adantl	$⊢ (((φ \land \neg +∞ \in ran F) \land z \in X) \land \neg F (z) \neq +∞) \to +∞ = F (z)$
96	2	adantr	$⊢ (φ \land z \in X) \to F : X ⟶ [0, +∞]$
97	96	ffund	$⊢ (φ \land z \in X) \to Fun F$
98		simpr	$⊢ (φ \land z \in X) \to z \in X$
99	52	adantr	$⊢ (φ \land z \in X) \to X = dom F$
100	98 99	eleqtrd	$⊢ (φ \land z \in X) \to z \in dom F$
101		fvelrn	$⊢ (Fun F \land z \in dom F) \to F (z) \in ran F$
102	97 100 101	syl2anc	$⊢ (φ \land z \in X) \to F (z) \in ran F$
103	102	adantlr	$⊢ ((φ \land \neg +∞ \in ran F) \land z \in X) \to F (z) \in ran F$
104	103	adantr	$⊢ (((φ \land \neg +∞ \in ran F) \land z \in X) \land \neg F (z) \neq +∞) \to F (z) \in ran F$
105	95 104	eqeltrd	$⊢ (((φ \land \neg +∞ \in ran F) \land z \in X) \land \neg F (z) \neq +∞) \to +∞ \in ran F$
106	29	ad2antrr	$⊢ (((φ \land \neg +∞ \in ran F) \land z \in X) \land \neg F (z) \neq +∞) \to \neg +∞ \in ran F$
107	105 106	condan	$⊢ ((φ \land \neg +∞ \in ran F) \land z \in X) \to F (z) \neq +∞$
108		ge0xrre	$⊢ (F (z) \in [0, +∞] \land F (z) \neq +∞) \to F (z) \in ℝ$
109	91 107 108	syl2anc	$⊢ ((φ \land \neg +∞ \in ran F) \land z \in X) \to F (z) \in ℝ$
110	109	rexrd	$⊢ ((φ \land \neg +∞ \in ran F) \land z \in X) \to F (z) \in ℝ^{*}$
111	73	adantr	$⊢ ((φ \land \neg +∞ \in ran F) \land z \in X) \to sum^(F) \in ℝ^{*}$
112	23	a1i	$⊢ (φ \land z \in X) \to 0 \in ℝ^{*}$
113	25	a1i	$⊢ (φ \land z \in X) \to +∞ \in ℝ^{*}$
114		iccgelb	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land F (z) \in [0, +∞]) \to 0 \leq F (z)$
115	112 113 90 114	syl3anc	$⊢ (φ \land z \in X) \to 0 \leq F (z)$
116	115	adantlr	$⊢ ((φ \land \neg +∞ \in ran F) \land z \in X) \to 0 \leq F (z)$
117	70	adantr	$⊢ ((φ \land \neg +∞ \in ran F) \land z \in X) \to ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \subseteq ℝ^{*}$
118		snelpwi	$⊢ z \in X \to \{z\} \in 𝒫 X$
119		snfi	$⊢ \{z\} \in Fin$
120	119	a1i	$⊢ z \in X \to \{z\} \in Fin$
121	118 120	elind	$⊢ z \in X \to \{z\} \in (𝒫 X \cap Fin)$
122	121	adantl	$⊢ ((φ \land \neg +∞ \in ran F) \land z \in X) \to \{z\} \in (𝒫 X \cap Fin)$
123		simpr	$⊢ ((φ \land \neg +∞ \in ran F) \land z \in X) \to z \in X$
124	109	recnd	$⊢ ((φ \land \neg +∞ \in ran F) \land z \in X) \to F (z) \in ℂ$
125		fveq2	$⊢ y = z \to F (y) = F (z)$
126	125	sumsn	$⊢ (z \in X \land F (z) \in ℂ) \to \sum_{y \in \{z\}} F (y) = F (z)$
127	123 124 126	syl2anc	$⊢ ((φ \land \neg +∞ \in ran F) \land z \in X) \to \sum_{y \in \{z\}} F (y) = F (z)$
128	127	eqcomd	$⊢ ((φ \land \neg +∞ \in ran F) \land z \in X) \to F (z) = \sum_{y \in \{z\}} F (y)$
129		sumeq1	$⊢ x = \{z\} \to \sum_{y \in x} F (y) = \sum_{y \in \{z\}} F (y)$
130	129	rspceeqv	$⊢ (\{z\} \in (𝒫 X \cap Fin) \land F (z) = \sum_{y \in \{z\}} F (y)) \to \exists x \in (𝒫 X \cap Fin) F (z) = \sum_{y \in x} F (y)$
131	122 128 130	syl2anc	$⊢ ((φ \land \neg +∞ \in ran F) \land z \in X) \to \exists x \in (𝒫 X \cap Fin) F (z) = \sum_{y \in x} F (y)$
132	65	elrnmpt	$⊢ F (z) \in [0, +∞] \to (F (z) \in ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \leftrightarrow \exists x \in (𝒫 X \cap Fin) F (z) = \sum_{y \in x} F (y))$
133	91 132	syl	$⊢ ((φ \land \neg +∞ \in ran F) \land z \in X) \to (F (z) \in ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \leftrightarrow \exists x \in (𝒫 X \cap Fin) F (z) = \sum_{y \in x} F (y))$
134	131 133	mpbird	$⊢ ((φ \land \neg +∞ \in ran F) \land z \in X) \to F (z) \in ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y))$
135		supxrub	$⊢ (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \subseteq ℝ^{} \land F (z) \in ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y))) \to F (z) \leq sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ^{} <)$
136	117 134 135	syl2anc	$⊢ ((φ \land \neg +∞ \in ran F) \land z \in X) \to F (z) \leq sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ^{*} <)$
137	31	eqcomd	$⊢ (φ \land \neg +∞ \in ran F) \to sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ^{*} <) = sum^(F)$
138	137	adantr	$⊢ ((φ \land \neg +∞ \in ran F) \land z \in X) \to sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ^{*} <) = sum^(F)$
139	136 138	breqtrd	$⊢ ((φ \land \neg +∞ \in ran F) \land z \in X) \to F (z) \leq sum^(F)$
140	89 110 111 116 139	xrletrd	$⊢ ((φ \land \neg +∞ \in ran F) \land z \in X) \to 0 \leq sum^(F)$
141	140	ex	$⊢ (φ \land \neg +∞ \in ran F) \to (z \in X \to 0 \leq sum^(F))$
142	141	adantlr	$⊢ ((φ \land F \neq \emptyset) \land \neg +∞ \in ran F) \to (z \in X \to 0 \leq sum^(F))$
143	142	exlimdv	$⊢ ((φ \land F \neq \emptyset) \land \neg +∞ \in ran F) \to (\exists z z \in X \to 0 \leq sum^(F))$
144	88 143	mpd	$⊢ ((φ \land F \neq \emptyset) \land \neg +∞ \in ran F) \to 0 \leq sum^(F)$
145		pnfge	$⊢ sum^(F) \in ℝ^{*} \to sum^(F) \leq +∞$
146	73 145	syl	$⊢ (φ \land \neg +∞ \in ran F) \to sum^(F) \leq +∞$
147	146	adantlr	$⊢ ((φ \land F \neq \emptyset) \land \neg +∞ \in ran F) \to sum^(F) \leq +∞$
148	24 26 74 144 147	eliccxrd	$⊢ ((φ \land F \neq \emptyset) \land \neg +∞ \in ran F) \to sum^(F) \in [0, +∞]$
149	19 21 22 148	syl21anc	$⊢ ((φ \land \neg F = \emptyset) \land \neg +∞ \in ran F) \to sum^(F) \in [0, +∞]$
150	18 149	pm2.61dan	$⊢ (φ \land \neg F = \emptyset) \to sum^(F) \in [0, +∞]$
151	10 150	pm2.61dan	$⊢ φ \to sum^(F) \in [0, +∞]$

Metamath Proof Explorer

Theorem sge0cl

Proof