sge0supre

Description: 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 , but here we can use sup with respect to RR instead of RR* . (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0supre.x	$⊢ φ \to X \in V$
	sge0supre.f	$⊢ φ \to F : X ⟶ [0, +∞]$
	sge0supre.re	$⊢ φ \to sum^(F) \in ℝ$
Assertion	sge0supre	$⊢ φ \to sum^(F) = sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <)$

Proof

Step	Hyp	Ref	Expression
1		sge0supre.x	$⊢ φ \to X \in V$
2		sge0supre.f	$⊢ φ \to F : X ⟶ [0, +∞]$
3		sge0supre.re	$⊢ φ \to sum^(F) \in ℝ$
4	1	adantr	$⊢ (φ \land +∞ \in ran F) \to X \in V$
5	2	adantr	$⊢ (φ \land +∞ \in ran F) \to F : X ⟶ [0, +∞]$
6		simpr	$⊢ (φ \land +∞ \in ran F) \to +∞ \in ran F$
7	4 5 6	sge0pnfval	$⊢ (φ \land +∞ \in ran F) \to sum^(F) = +∞$
8	1 2	sge0repnf	$⊢ φ \to (sum^(F) \in ℝ \leftrightarrow \neg sum^(F) = +∞)$
9	3 8	mpbid	$⊢ φ \to \neg sum^(F) = +∞$
10	9	adantr	$⊢ (φ \land +∞ \in ran F) \to \neg sum^(F) = +∞$
11	7 10	pm2.65da	$⊢ φ \to \neg +∞ \in ran F$
12	2 11	fge0iccico	$⊢ φ \to F : X ⟶ [0, +∞)$
13	1 12	sge0reval	$⊢ φ \to sum^(F) = sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ^{*} <)$
14	12	sge0rnre	$⊢ φ \to ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \subseteq ℝ$
15		sge0rnn0	$⊢ ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \neq \emptyset$
16	15	a1i	$⊢ φ \to ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \neq \emptyset$
17		simpr	$⊢ (φ \land w \in ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y))) \to w \in ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y))$
18		eqid	$⊢ (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) = (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y))$
19	18	elrnmpt	$⊢ w \in ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \to (w \in ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \leftrightarrow \exists x \in (𝒫 X \cap Fin) w = \sum_{y \in x} F (y))$
20	19	adantl	$⊢ (φ \land w \in ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y))) \to (w \in ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \leftrightarrow \exists x \in (𝒫 X \cap Fin) w = \sum_{y \in x} F (y))$
21	17 20	mpbid	$⊢ (φ \land w \in ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y))) \to \exists x \in (𝒫 X \cap Fin) w = \sum_{y \in x} F (y)$
22		simp3	$⊢ (φ \land x \in (𝒫 X \cap Fin) \land w = \sum_{y \in x} F (y)) \to w = \sum_{y \in x} F (y)$
23		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
24	23	a1i	$⊢ φ \to ℝ \subseteq ℝ^{*}$
25	14 24	sstrd	$⊢ φ \to ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \subseteq ℝ^{*}$
26	25	adantr	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \subseteq ℝ^{*}$
27		id	$⊢ x \in (𝒫 X \cap Fin) \to x \in (𝒫 X \cap Fin)$
28		sumex	$⊢ \sum_{y \in x} F (y) \in V$
29	28	a1i	$⊢ x \in (𝒫 X \cap Fin) \to \sum_{y \in x} F (y) \in V$
30	18	elrnmpt1	$⊢ (x \in (𝒫 X \cap Fin) \land \sum_{y \in x} F (y) \in V) \to \sum_{y \in x} F (y) \in ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y))$
31	27 29 30	syl2anc	$⊢ x \in (𝒫 X \cap Fin) \to \sum_{y \in x} F (y) \in ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y))$
32	31	adantl	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to \sum_{y \in x} F (y) \in ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y))$
33		supxrub	$⊢ (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \subseteq ℝ^{} \land \sum_{y \in x} F (y) \in ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y))) \to \sum_{y \in x} F (y) \leq sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ^{} <)$
34	26 32 33	syl2anc	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to \sum_{y \in x} F (y) \leq sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ^{*} <)$
35	13	eqcomd	$⊢ φ \to sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ^{*} <) = sum^(F)$
36	35	adantr	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ^{*} <) = sum^(F)$
37	34 36	breqtrd	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to \sum_{y \in x} F (y) \leq sum^(F)$
38	37	3adant3	$⊢ (φ \land x \in (𝒫 X \cap Fin) \land w = \sum_{y \in x} F (y)) \to \sum_{y \in x} F (y) \leq sum^(F)$
39	22 38	eqbrtrd	$⊢ (φ \land x \in (𝒫 X \cap Fin) \land w = \sum_{y \in x} F (y)) \to w \leq sum^(F)$
40	39	3exp	$⊢ φ \to (x \in (𝒫 X \cap Fin) \to (w = \sum_{y \in x} F (y) \to w \leq sum^(F)))$
41	40	rexlimdv	$⊢ φ \to (\exists x \in (𝒫 X \cap Fin) w = \sum_{y \in x} F (y) \to w \leq sum^(F))$
42	41	adantr	$⊢ (φ \land w \in ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y))) \to (\exists x \in (𝒫 X \cap Fin) w = \sum_{y \in x} F (y) \to w \leq sum^(F))$
43	21 42	mpd	$⊢ (φ \land w \in ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y))) \to w \leq sum^(F)$
44	43	ralrimiva	$⊢ φ \to \forall w \in ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) w \leq sum^(F)$
45		brralrspcev	$⊢ (sum^(F) \in ℝ \land \forall w \in ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) w \leq sum^(F)) \to \exists z \in ℝ \forall w \in ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) w \leq z$
46	3 44 45	syl2anc	$⊢ φ \to \exists z \in ℝ \forall w \in ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) w \leq z$
47		supxrre	$⊢ (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \subseteq ℝ \land ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \neq \emptyset \land \exists z \in ℝ \forall w \in ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) w \leq z) \to sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ^{*} <) = sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <)$
48	14 16 46 47	syl3anc	$⊢ φ \to sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ^{*} <) = sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <)$
49	13 48	eqtrd	$⊢ φ \to sum^(F) = sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <)$

Metamath Proof Explorer

Theorem sge0supre

Proof