sge0ltfirpmpt2

Description: If the extended sum of nonnegative reals is not +oo , then it can be approximated from below by finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0ltfirpmpt2.xph	$⊢ Ⅎ x φ$
	sge0ltfirpmpt2.a	$⊢ φ \to A \in V$
	sge0ltfirpmpt2.b	$⊢ (φ \land x \in A) \to B \in [0, +∞]$
	sge0ltfirpmpt2.rp	$⊢ φ \to Y \in ℝ^{+}$
	sge0ltfirpmpt2.re	$⊢ φ \to sum^((x \in A ⟼ B)) \in ℝ$
Assertion	sge0ltfirpmpt2	$⊢ φ \to \exists y \in (𝒫 A \cap Fin) sum^((x \in A ⟼ B)) < \sum_{x \in y} B + Y$

Proof

Step	Hyp	Ref	Expression
1		sge0ltfirpmpt2.xph	$⊢ Ⅎ x φ$
2		sge0ltfirpmpt2.a	$⊢ φ \to A \in V$
3		sge0ltfirpmpt2.b	$⊢ (φ \land x \in A) \to B \in [0, +∞]$
4		sge0ltfirpmpt2.rp	$⊢ φ \to Y \in ℝ^{+}$
5		sge0ltfirpmpt2.re	$⊢ φ \to sum^((x \in A ⟼ B)) \in ℝ$
6		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
7	1 3 6	fmptdf	$⊢ φ \to (x \in A ⟼ B) : A ⟶ [0, +∞]$
8	2 7 4 5	sge0ltfirp	$⊢ φ \to \exists y \in (𝒫 A \cap Fin) sum^((x \in A ⟼ B)) < sum^({(x \in A ⟼ B) ↾}_{y}) + Y$
9		simpr	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land sum^((x \in A ⟼ B)) < sum^({(x \in A ⟼ B) ↾}_{y}) + Y) \to sum^((x \in A ⟼ B)) < sum^({(x \in A ⟼ B) ↾}_{y}) + Y$
10		elpwinss	$⊢ y \in (𝒫 A \cap Fin) \to y \subseteq A$
11	10	resmptd	$⊢ y \in (𝒫 A \cap Fin) \to {(x \in A ⟼ B) ↾}_{y} = (x \in y ⟼ B)$
12	11	fveq2d	$⊢ y \in (𝒫 A \cap Fin) \to sum^({(x \in A ⟼ B) ↾}_{y}) = sum^((x \in y ⟼ B))$
13	12	adantl	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to sum^({(x \in A ⟼ B) ↾}_{y}) = sum^((x \in y ⟼ B))$
14		elinel2	$⊢ y \in (𝒫 A \cap Fin) \to y \in Fin$
15	14	adantl	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to y \in Fin$
16		nfv	$⊢ Ⅎ x y \in (𝒫 A \cap Fin)$
17	1 16	nfan	$⊢ Ⅎ x (φ \land y \in (𝒫 A \cap Fin))$
18		simpll	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land x \in y) \to φ$
19	10	sselda	$⊢ (y \in (𝒫 A \cap Fin) \land x \in y) \to x \in A$
20	19	adantll	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land x \in y) \to x \in A$
21	1 2 3 5	sge0rernmpt	$⊢ (φ \land x \in A) \to B \in [0, +∞)$
22	18 20 21	syl2anc	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land x \in y) \to B \in [0, +∞)$
23		eqid	$⊢ (x \in y ⟼ B) = (x \in y ⟼ B)$
24	17 22 23	fmptdf	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to (x \in y ⟼ B) : y ⟶ [0, +∞)$
25	15 24	sge0fsum	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to sum^((x \in y ⟼ B)) = \sum_{k \in y} (x \in y ⟼ B) (k)$
26		simpr	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land k \in y) \to k \in y$
27		simpll	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land k \in y) \to φ$
28	10	sselda	$⊢ (y \in (𝒫 A \cap Fin) \land k \in y) \to k \in A$
29	28	adantll	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land k \in y) \to k \in A$
30		nfv	$⊢ Ⅎ x k \in A$
31	1 30	nfan	$⊢ Ⅎ x (φ \land k \in A)$
32		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ k / x ⦌ B$
33	32	nfel1	$⊢ Ⅎ x ⦋ k / x ⦌ B \in [0, +∞)$
34	31 33	nfim	$⊢ Ⅎ x ((φ \land k \in A) \to ⦋ k / x ⦌ B \in [0, +∞))$
35		eleq1w	$⊢ x = k \to (x \in A \leftrightarrow k \in A)$
36	35	anbi2d	$⊢ x = k \to ((φ \land x \in A) \leftrightarrow (φ \land k \in A))$
37		csbeq1a	$⊢ x = k \to B = ⦋ k / x ⦌ B$
38	37	eleq1d	$⊢ x = k \to (B \in [0, +∞) \leftrightarrow ⦋ k / x ⦌ B \in [0, +∞))$
39	36 38	imbi12d	$⊢ x = k \to (((φ \land x \in A) \to B \in [0, +∞)) \leftrightarrow ((φ \land k \in A) \to ⦋ k / x ⦌ B \in [0, +∞)))$
40	34 39 21	chvarfv	$⊢ (φ \land k \in A) \to ⦋ k / x ⦌ B \in [0, +∞)$
41	27 29 40	syl2anc	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land k \in y) \to ⦋ k / x ⦌ B \in [0, +∞)$
42		nfcv	$⊢ \underline{Ⅎ} k B$
43	42 32 37	cbvmpt	$⊢ (x \in y ⟼ B) = (k \in y ⟼ ⦋ k / x ⦌ B)$
44	43	fvmpt2	$⊢ (k \in y \land ⦋ k / x ⦌ B \in [0, +∞)) \to (x \in y ⟼ B) (k) = ⦋ k / x ⦌ B$
45	26 41 44	syl2anc	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land k \in y) \to (x \in y ⟼ B) (k) = ⦋ k / x ⦌ B$
46	45	sumeq2dv	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to \sum_{k \in y} (x \in y ⟼ B) (k) = \sum_{k \in y} ⦋ k / x ⦌ B$
47		eqcom	$⊢ x = k \leftrightarrow k = x$
48	47	imbi1i	$⊢ (x = k \to B = ⦋ k / x ⦌ B) \leftrightarrow (k = x \to B = ⦋ k / x ⦌ B)$
49		eqcom	$⊢ B = ⦋ k / x ⦌ B \leftrightarrow ⦋ k / x ⦌ B = B$
50	49	imbi2i	$⊢ (k = x \to B = ⦋ k / x ⦌ B) \leftrightarrow (k = x \to ⦋ k / x ⦌ B = B)$
51	48 50	bitri	$⊢ (x = k \to B = ⦋ k / x ⦌ B) \leftrightarrow (k = x \to ⦋ k / x ⦌ B = B)$
52	37 51	mpbi	$⊢ k = x \to ⦋ k / x ⦌ B = B$
53		nfcv	$⊢ \underline{Ⅎ} x y$
54		nfcv	$⊢ \underline{Ⅎ} k y$
55	52 53 54 32 42	cbvsum	$⊢ \sum_{k \in y} ⦋ k / x ⦌ B = \sum_{x \in y} B$
56	55	a1i	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to \sum_{k \in y} ⦋ k / x ⦌ B = \sum_{x \in y} B$
57	46 56	eqtrd	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to \sum_{k \in y} (x \in y ⟼ B) (k) = \sum_{x \in y} B$
58	13 25 57	3eqtrd	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to sum^({(x \in A ⟼ B) ↾}_{y}) = \sum_{x \in y} B$
59	58	oveq1d	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to sum^({(x \in A ⟼ B) ↾}_{y}) + Y = \sum_{x \in y} B + Y$
60	59	adantr	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land sum^((x \in A ⟼ B)) < sum^({(x \in A ⟼ B) ↾}_{y}) + Y) \to sum^({(x \in A ⟼ B) ↾}_{y}) + Y = \sum_{x \in y} B + Y$
61	9 60	breqtrd	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land sum^((x \in A ⟼ B)) < sum^({(x \in A ⟼ B) ↾}_{y}) + Y) \to sum^((x \in A ⟼ B)) < \sum_{x \in y} B + Y$
62	61	ex	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to (sum^((x \in A ⟼ B)) < sum^({(x \in A ⟼ B) ↾}_{y}) + Y \to sum^((x \in A ⟼ B)) < \sum_{x \in y} B + Y)$
63	62	reximdva	$⊢ φ \to (\exists y \in (𝒫 A \cap Fin) sum^((x \in A ⟼ B)) < sum^({(x \in A ⟼ B) ↾}_{y}) + Y \to \exists y \in (𝒫 A \cap Fin) sum^((x \in A ⟼ B)) < \sum_{x \in y} B + Y)$
64	8 63	mpd	$⊢ φ \to \exists y \in (𝒫 A \cap Fin) sum^((x \in A ⟼ B)) < \sum_{x \in y} B + Y$

Metamath Proof Explorer

Theorem sge0ltfirpmpt2

Proof