sge0ltfirp

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

	Ref	Expression
Hypotheses	sge0ltfirp.x	$⊢ φ \to X \in V$
	sge0ltfirp.f	$⊢ φ \to F : X ⟶ [0, +∞]$
	sge0ltfirp.y	$⊢ φ \to Y \in ℝ^{+}$
	sge0ltfirp.re	$⊢ φ \to sum^(F) \in ℝ$
Assertion	sge0ltfirp	$⊢ φ \to \exists x \in (𝒫 X \cap Fin) sum^(F) < sum^({F ↾}_{x}) + Y$

Proof

Step	Hyp	Ref	Expression
1		sge0ltfirp.x	$⊢ φ \to X \in V$
2		sge0ltfirp.f	$⊢ φ \to F : X ⟶ [0, +∞]$
3		sge0ltfirp.y	$⊢ φ \to Y \in ℝ^{+}$
4		sge0ltfirp.re	$⊢ φ \to sum^(F) \in ℝ$
5	1 2 4	sge0rern	$⊢ φ \to \neg +∞ \in ran F$
6	2 5	fge0iccico	$⊢ φ \to F : X ⟶ [0, +∞)$
7	6	sge0rnre	$⊢ φ \to ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \subseteq ℝ$
8		sge0rnn0	$⊢ ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \neq \emptyset$
9	8	a1i	$⊢ φ \to ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \neq \emptyset$
10	1 2 4	sge0rnbnd	$⊢ φ \to \exists z \in ℝ \forall w \in ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) w \leq z$
11	7 9 10 3	suprltrp	$⊢ φ \to \exists w \in 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)) ℝ <) - Y < w$
12		nfv	$⊢ Ⅎ w φ$
13		nfv	$⊢ Ⅎ w \exists x \in (𝒫 X \cap Fin) sum^(F) < sum^({F ↾}_{x}) + Y$
14		simp1	$⊢ (φ \land w \in ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \land sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y < w) \to φ$
15		vex	$⊢ w \in V$
16		eqid	$⊢ (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) = (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y))$
17	16	elrnmpt	$⊢ w \in V \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))$
18	15 17	ax-mp	$⊢ 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)$
19	18	biimpi	$⊢ 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)$
20	19	adantr	$⊢ (w \in ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \land sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y < w) \to \exists x \in (𝒫 X \cap Fin) w = \sum_{y \in x} F (y)$
21		nfmpt1	$⊢ \underline{Ⅎ} x (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y))$
22	21	nfrn	$⊢ \underline{Ⅎ} x ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y))$
23		nfcv	$⊢ \underline{Ⅎ} x ℝ$
24		nfcv	$⊢ \underline{Ⅎ} x <$
25	22 23 24	nfsup	$⊢ \underline{Ⅎ} x sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <)$
26		nfcv	$⊢ \underline{Ⅎ} x -$
27		nfcv	$⊢ \underline{Ⅎ} x Y$
28	25 26 27	nfov	$⊢ \underline{Ⅎ} x (sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y)$
29		nfcv	$⊢ \underline{Ⅎ} x w$
30	28 24 29	nfbr	$⊢ Ⅎ x sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y < w$
31		simpl	$⊢ (sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y < w \land w = \sum_{y \in x} F (y)) \to sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y < w$
32		simpr	$⊢ (sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y < w \land w = \sum_{y \in x} F (y)) \to w = \sum_{y \in x} F (y)$
33	31 32	breqtrd	$⊢ (sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y < w \land w = \sum_{y \in x} F (y)) \to sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y < \sum_{y \in x} F (y)$
34	33	ex	$⊢ sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y < w \to (w = \sum_{y \in x} F (y) \to sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y < \sum_{y \in x} F (y))$
35	34	a1d	$⊢ sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y < w \to (x \in (𝒫 X \cap Fin) \to (w = \sum_{y \in x} F (y) \to sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y < \sum_{y \in x} F (y)))$
36	30 35	reximdai	$⊢ sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y < w \to (\exists x \in (𝒫 X \cap Fin) w = \sum_{y \in x} F (y) \to \exists x \in (𝒫 X \cap Fin) sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y < \sum_{y \in x} F (y))$
37	36	adantl	$⊢ (w \in ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \land sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y < w) \to (\exists x \in (𝒫 X \cap Fin) w = \sum_{y \in x} F (y) \to \exists x \in (𝒫 X \cap Fin) sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y < \sum_{y \in x} F (y))$
38	20 37	mpd	$⊢ (w \in ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \land sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y < w) \to \exists x \in (𝒫 X \cap Fin) sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y < \sum_{y \in x} F (y)$
39	38	3adant1	$⊢ (φ \land w \in ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \land sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y < w) \to \exists x \in (𝒫 X \cap Fin) sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y < \sum_{y \in x} F (y)$
40		simpl	$⊢ ((φ \land x \in (𝒫 X \cap Fin)) \land sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y < \sum_{y \in x} F (y)) \to (φ \land x \in (𝒫 X \cap Fin))$
41	1 2 4	sge0supre	$⊢ φ \to sum^(F) = sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <)$
42	41	oveq1d	$⊢ φ \to sum^(F) - Y = sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y$
43	42	adantr	$⊢ (φ \land sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y < \sum_{y \in x} F (y)) \to sum^(F) - Y = sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y$
44		simpr	$⊢ (φ \land sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y < \sum_{y \in x} F (y)) \to sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y < \sum_{y \in x} F (y)$
45	43 44	eqbrtrd	$⊢ (φ \land sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y < \sum_{y \in x} F (y)) \to sum^(F) - Y < \sum_{y \in x} F (y)$
46	45	adantlr	$⊢ ((φ \land x \in (𝒫 X \cap Fin)) \land sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y < \sum_{y \in x} F (y)) \to sum^(F) - Y < \sum_{y \in x} F (y)$
47		simpr	$⊢ ((φ \land x \in (𝒫 X \cap Fin)) \land sum^(F) - Y < \sum_{y \in x} F (y)) \to sum^(F) - Y < \sum_{y \in x} F (y)$
48	4	adantr	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to sum^(F) \in ℝ$
49	3	rpred	$⊢ φ \to Y \in ℝ$
50	49	adantr	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to Y \in ℝ$
51		elinel2	$⊢ x \in (𝒫 X \cap Fin) \to x \in Fin$
52	51	adantl	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to x \in Fin$
53		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
54	6	adantr	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to F : X ⟶ [0, +∞)$
55	54	adantr	$⊢ ((φ \land x \in (𝒫 X \cap Fin)) \land y \in x) \to F : X ⟶ [0, +∞)$
56		elpwinss	$⊢ x \in (𝒫 X \cap Fin) \to x \subseteq X$
57	56	adantl	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to x \subseteq X$
58	57	sselda	$⊢ ((φ \land x \in (𝒫 X \cap Fin)) \land y \in x) \to y \in X$
59	55 58	ffvelcdmd	$⊢ ((φ \land x \in (𝒫 X \cap Fin)) \land y \in x) \to F (y) \in [0, +∞)$
60	53 59	sselid	$⊢ ((φ \land x \in (𝒫 X \cap Fin)) \land y \in x) \to F (y) \in ℝ$
61	52 60	fsumrecl	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to \sum_{y \in x} F (y) \in ℝ$
62	48 50 61	ltsubaddd	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to (sum^(F) - Y < \sum_{y \in x} F (y) \leftrightarrow sum^(F) < \sum_{y \in x} F (y) + Y)$
63	62	adantr	$⊢ ((φ \land x \in (𝒫 X \cap Fin)) \land sum^(F) - Y < \sum_{y \in x} F (y)) \to (sum^(F) - Y < \sum_{y \in x} F (y) \leftrightarrow sum^(F) < \sum_{y \in x} F (y) + Y)$
64	47 63	mpbid	$⊢ ((φ \land x \in (𝒫 X \cap Fin)) \land sum^(F) - Y < \sum_{y \in x} F (y)) \to sum^(F) < \sum_{y \in x} F (y) + Y$
65	54 57	fssresd	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to ({F ↾}_{x}) : x ⟶ [0, +∞)$
66	52 65	sge0fsum	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to sum^({F ↾}_{x}) = \sum_{y \in x} ({F ↾}_{x}) (y)$
67		fvres	$⊢ y \in x \to ({F ↾}_{x}) (y) = F (y)$
68	67	sumeq2i	$⊢ \sum_{y \in x} ({F ↾}_{x}) (y) = \sum_{y \in x} F (y)$
69	68	a1i	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to \sum_{y \in x} ({F ↾}_{x}) (y) = \sum_{y \in x} F (y)$
70	66 69	eqtr2d	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to \sum_{y \in x} F (y) = sum^({F ↾}_{x})$
71	70	oveq1d	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to \sum_{y \in x} F (y) + Y = sum^({F ↾}_{x}) + Y$
72	71	adantr	$⊢ ((φ \land x \in (𝒫 X \cap Fin)) \land sum^(F) - Y < \sum_{y \in x} F (y)) \to \sum_{y \in x} F (y) + Y = sum^({F ↾}_{x}) + Y$
73	64 72	breqtrd	$⊢ ((φ \land x \in (𝒫 X \cap Fin)) \land sum^(F) - Y < \sum_{y \in x} F (y)) \to sum^(F) < sum^({F ↾}_{x}) + Y$
74	40 46 73	syl2anc	$⊢ ((φ \land x \in (𝒫 X \cap Fin)) \land sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y < \sum_{y \in x} F (y)) \to sum^(F) < sum^({F ↾}_{x}) + Y$
75	74	ex	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to (sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y < \sum_{y \in x} F (y) \to sum^(F) < sum^({F ↾}_{x}) + Y)$
76	75	reximdva	$⊢ φ \to (\exists x \in (𝒫 X \cap Fin) sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y < \sum_{y \in x} F (y) \to \exists x \in (𝒫 X \cap Fin) sum^(F) < sum^({F ↾}_{x}) + Y)$
77	76	imp	$⊢ (φ \land \exists x \in (𝒫 X \cap Fin) sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y < \sum_{y \in x} F (y)) \to \exists x \in (𝒫 X \cap Fin) sum^(F) < sum^({F ↾}_{x}) + Y$
78	14 39 77	syl2anc	$⊢ (φ \land w \in ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \land sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y < w) \to \exists x \in (𝒫 X \cap Fin) sum^(F) < sum^({F ↾}_{x}) + Y$
79	78	3exp	$⊢ φ \to (w \in ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \to (sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y < w \to \exists x \in (𝒫 X \cap Fin) sum^(F) < sum^({F ↾}_{x}) + Y))$
80	12 13 79	rexlimd	$⊢ φ \to (\exists w \in 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)) ℝ <) - Y < w \to \exists x \in (𝒫 X \cap Fin) sum^(F) < sum^({F ↾}_{x}) + Y)$
81	11 80	mpd	$⊢ φ \to \exists x \in (𝒫 X \cap Fin) sum^(F) < sum^({F ↾}_{x}) + Y$

Metamath Proof Explorer

Theorem sge0ltfirp

Proof