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	birani	$⊢ (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)$
20		nfmpt1	$⊢ \underline{Ⅎ} x (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y))$
21	20	nfrn	$⊢ \underline{Ⅎ} x ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y))$
22		nfcv	$⊢ \underline{Ⅎ} x ℝ$
23		nfcv	$⊢ \underline{Ⅎ} x <$
24	21 22 23	nfsup	$⊢ \underline{Ⅎ} x sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <)$
25		nfcv	$⊢ \underline{Ⅎ} x -$
26		nfcv	$⊢ \underline{Ⅎ} x Y$
27	24 25 26	nfov	$⊢ \underline{Ⅎ} x (sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y)$
28		nfcv	$⊢ \underline{Ⅎ} x w$
29	27 23 28	nfbr	$⊢ Ⅎ x sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y < w$
30		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$
31		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)$
32	30 31	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)$
33	32	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))$
34	33	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)))$
35	29 34	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))$
36	35	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))$
37	19 36	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)$
38	37	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)$
39		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))$
40	1 2 4	sge0supre	$⊢ φ \to sum^(F) = sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <)$
41	40	oveq1d	$⊢ φ \to sum^(F) - Y = sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ <) - Y$
42	41	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$
43		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)$
44	42 43	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)$
45	44	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)$
46		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)$
47	4	adantr	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to sum^(F) \in ℝ$
48	3	rpred	$⊢ φ \to Y \in ℝ$
49	48	adantr	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to Y \in ℝ$
50		elinel2	$⊢ x \in (𝒫 X \cap Fin) \to x \in Fin$
51	50	adantl	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to x \in Fin$
52		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
53	6	adantr	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to F : X ⟶ [0, +∞)$
54	53	adantr	$⊢ ((φ \land x \in (𝒫 X \cap Fin)) \land y \in x) \to F : X ⟶ [0, +∞)$
55		elpwinss	$⊢ x \in (𝒫 X \cap Fin) \to x \subseteq X$
56	55	adantl	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to x \subseteq X$
57	56	sselda	$⊢ ((φ \land x \in (𝒫 X \cap Fin)) \land y \in x) \to y \in X$
58	54 57	ffvelcdmd	$⊢ ((φ \land x \in (𝒫 X \cap Fin)) \land y \in x) \to F (y) \in [0, +∞)$
59	52 58	sselid	$⊢ ((φ \land x \in (𝒫 X \cap Fin)) \land y \in x) \to F (y) \in ℝ$
60	51 59	fsumrecl	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to \sum_{y \in x} F (y) \in ℝ$
61	47 49 60	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)$
62	61	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)$
63	46 62	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$
64	53 56	fssresd	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to ({F ↾}_{x}) : x ⟶ [0, +∞)$
65	51 64	sge0fsum	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to sum^({F ↾}_{x}) = \sum_{y \in x} ({F ↾}_{x}) (y)$
66		fvres	$⊢ y \in x \to ({F ↾}_{x}) (y) = F (y)$
67	66	sumeq2i	$⊢ \sum_{y \in x} ({F ↾}_{x}) (y) = \sum_{y \in x} F (y)$
68	67	a1i	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to \sum_{y \in x} ({F ↾}_{x}) (y) = \sum_{y \in x} F (y)$
69	65 68	eqtr2d	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to \sum_{y \in x} F (y) = sum^({F ↾}_{x})$
70	69	oveq1d	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to \sum_{y \in x} F (y) + Y = sum^({F ↾}_{x}) + Y$
71	70	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$
72	63 71	breqtrd	$⊢ ((φ \land x \in (𝒫 X \cap Fin)) \land sum^(F) - Y < \sum_{y \in x} F (y)) \to sum^(F) < sum^({F ↾}_{x}) + Y$
73	39 45 72	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$
74	73	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)$
75	74	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)$
76	75	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$
77	14 38 76	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$
78	77	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))$
79	12 13 78	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)$
80	11 79	mpd	$⊢ φ \to \exists x \in (𝒫 X \cap Fin) sum^(F) < sum^({F ↾}_{x}) + Y$

Metamath Proof Explorer

Theorem sge0ltfirp

Proof