sge0gerp

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

	Ref	Expression
Hypotheses	sge0gerp.x	$⊢ φ \to X \in V$
	sge0gerp.f	$⊢ φ \to F : X ⟶ [0, +∞]$
	sge0gerp.a	$⊢ φ \to A \in ℝ^{*}$
	sge0gerp.z	$⊢ (φ \land x \in ℝ^{+}) \to \exists z \in (𝒫 X \cap Fin) A \leq sum^({F ↾}_{z}) +_{𝑒} x$
Assertion	sge0gerp	$⊢ φ \to A \leq sum^(F)$

Proof

Step	Hyp	Ref	Expression
1		sge0gerp.x	$⊢ φ \to X \in V$
2		sge0gerp.f	$⊢ φ \to F : X ⟶ [0, +∞]$
3		sge0gerp.a	$⊢ φ \to A \in ℝ^{*}$
4		sge0gerp.z	$⊢ (φ \land x \in ℝ^{+}) \to \exists z \in (𝒫 X \cap Fin) A \leq sum^({F ↾}_{z}) +_{𝑒} x$
5		nfv	$⊢ Ⅎ x φ$
6		simpr	$⊢ (φ \land z \in (𝒫 X \cap Fin)) \to z \in (𝒫 X \cap Fin)$
7	2	adantr	$⊢ (φ \land z \in (𝒫 X \cap Fin)) \to F : X ⟶ [0, +∞]$
8		elinel1	$⊢ z \in (𝒫 X \cap Fin) \to z \in 𝒫 X$
9		elpwi	$⊢ z \in 𝒫 X \to z \subseteq X$
10	8 9	syl	$⊢ z \in (𝒫 X \cap Fin) \to z \subseteq X$
11	10	adantl	$⊢ (φ \land z \in (𝒫 X \cap Fin)) \to z \subseteq X$
12	7 11	fssresd	$⊢ (φ \land z \in (𝒫 X \cap Fin)) \to ({F ↾}_{z}) : z ⟶ [0, +∞]$
13	6 12	sge0xrcl	$⊢ (φ \land z \in (𝒫 X \cap Fin)) \to sum^({F ↾}_{z}) \in ℝ^{*}$
14	13	ralrimiva	$⊢ φ \to \forall z \in (𝒫 X \cap Fin) sum^({F ↾}_{z}) \in ℝ^{*}$
15		eqid	$⊢ (z \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{z})) = (z \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{z}))$
16	15	rnmptss	$⊢ \forall z \in (𝒫 X \cap Fin) sum^({F ↾}_{z}) \in ℝ^{} \to ran (z \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{z})) \subseteq ℝ^{}$
17	14 16	syl	$⊢ φ \to ran (z \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{z})) \subseteq ℝ^{*}$
18		nfv	$⊢ Ⅎ z (φ \land x \in ℝ^{+})$
19		nfmpt1	$⊢ \underline{Ⅎ} z (z \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{z}))$
20	19	nfrn	$⊢ \underline{Ⅎ} z ran (z \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{z}))$
21		nfv	$⊢ Ⅎ z A \leq y +_{𝑒} x$
22	20 21	nfrexw	$⊢ Ⅎ z \exists y \in ran (z \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{z})) A \leq y +_{𝑒} x$
23		id	$⊢ z \in (𝒫 X \cap Fin) \to z \in (𝒫 X \cap Fin)$
24		fvexd	$⊢ z \in (𝒫 X \cap Fin) \to sum^({F ↾}_{z}) \in V$
25	15	elrnmpt1	$⊢ (z \in (𝒫 X \cap Fin) \land sum^({F ↾}_{z}) \in V) \to sum^({F ↾}_{z}) \in ran (z \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{z}))$
26	23 24 25	syl2anc	$⊢ z \in (𝒫 X \cap Fin) \to sum^({F ↾}_{z}) \in ran (z \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{z}))$
27	26	3ad2ant2	$⊢ ((φ \land x \in ℝ^{+}) \land z \in (𝒫 X \cap Fin) \land A \leq sum^({F ↾}_{z}) +_{𝑒} x) \to sum^({F ↾}_{z}) \in ran (z \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{z}))$
28		simp3	$⊢ ((φ \land x \in ℝ^{+}) \land z \in (𝒫 X \cap Fin) \land A \leq sum^({F ↾}_{z}) +_{𝑒} x) \to A \leq sum^({F ↾}_{z}) +_{𝑒} x$
29		nfv	$⊢ Ⅎ y A \leq sum^({F ↾}_{z}) +_{𝑒} x$
30		oveq1	$⊢ y = sum^({F ↾}_{z}) \to y +_{𝑒} x = sum^({F ↾}_{z}) +_{𝑒} x$
31	30	breq2d	$⊢ y = sum^({F ↾}_{z}) \to (A \leq y +_{𝑒} x \leftrightarrow A \leq sum^({F ↾}_{z}) +_{𝑒} x)$
32	29 31	rspce	$⊢ (sum^({F ↾}_{z}) \in ran (z \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{z})) \land A \leq sum^({F ↾}_{z}) +_{𝑒} x) \to \exists y \in ran (z \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{z})) A \leq y +_{𝑒} x$
33	27 28 32	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land z \in (𝒫 X \cap Fin) \land A \leq sum^({F ↾}_{z}) +_{𝑒} x) \to \exists y \in ran (z \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{z})) A \leq y +_{𝑒} x$
34	33	3exp	$⊢ (φ \land x \in ℝ^{+}) \to (z \in (𝒫 X \cap Fin) \to (A \leq sum^({F ↾}_{z}) +_{𝑒} x \to \exists y \in ran (z \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{z})) A \leq y +_{𝑒} x))$
35	18 22 34	rexlimd	$⊢ (φ \land x \in ℝ^{+}) \to (\exists z \in (𝒫 X \cap Fin) A \leq sum^({F ↾}_{z}) +_{𝑒} x \to \exists y \in ran (z \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{z})) A \leq y +_{𝑒} x)$
36	4 35	mpd	$⊢ (φ \land x \in ℝ^{+}) \to \exists y \in ran (z \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{z})) A \leq y +_{𝑒} x$
37	5 17 3 36	supxrge	$⊢ φ \to A \leq sup (ran (z \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{z})) ℝ^{*} <)$
38	1 2	sge0sup	$⊢ φ \to sum^(F) = sup (ran (z \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{z})) ℝ^{*} <)$
39	38	eqcomd	$⊢ φ \to sup (ran (z \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{z})) ℝ^{*} <) = sum^(F)$
40	37 39	breqtrd	$⊢ φ \to A \leq sum^(F)$

Metamath Proof Explorer

Theorem sge0gerp

Proof