Metamath Proof Explorer

Theorem sge0ltfirpmpt

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	sge0ltfirpmpt.xph	$⊢ Ⅎ x φ$
		sge0ltfirpmpt.a	$⊢ φ \to A \in V$
		sge0ltfirpmpt.b	$⊢ (φ \land x \in A) \to B \in [0, +∞]$
		sge0ltfirpmpt.rp	$⊢ φ \to Y \in ℝ^{+}$
		sge0ltfirpmpt.re	$⊢ φ \to sum^((x \in A ⟼ B)) \in ℝ$
	Assertion	sge0ltfirpmpt	$⊢ φ \to \exists y \in (𝒫 A \cap Fin) sum^((x \in A ⟼ B)) < sum^((x \in y ⟼ B)) + Y$

Proof

Step	Hyp	Ref	Expression
1		sge0ltfirpmpt.xph	$⊢ Ⅎ x φ$
2		sge0ltfirpmpt.a	$⊢ φ \to A \in V$
3		sge0ltfirpmpt.b	$⊢ (φ \land x \in A) \to B \in [0, +∞]$
4		sge0ltfirpmpt.rp	$⊢ φ \to Y \in ℝ^{+}$
5		sge0ltfirpmpt.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	$⊢ (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	oveq1d	$⊢ y \in (𝒫 A \cap Fin) \to sum^({(x \in A ⟼ B) ↾}_{y}) + Y = sum^((x \in y ⟼ B)) + Y$
14	13	adantr	$⊢ (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$
15	9 14	breqtrd	$⊢ (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$
16	15	ex	$⊢ 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)$
17	16	reximia	$⊢ \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$
18	17	a1i	$⊢ φ \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)$
19	8 18	mpd	$⊢ φ \to \exists y \in (𝒫 A \cap Fin) sum^((x \in A ⟼ B)) < sum^((x \in y ⟼ B)) + Y$