sge0lefi

Description: A sum of nonnegative extended reals is smaller than a given extended real if and only if every finite subsum is smaller than it. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0lefi.1	$⊢ φ \to X \in V$
	sge0lefi.2	$⊢ φ \to F : X ⟶ [0, +∞]$
	sge0lefi.3	$⊢ φ \to A \in ℝ^{*}$
Assertion	sge0lefi	$⊢ φ \to (sum^(F) \leq A \leftrightarrow \forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \leq A)$

Proof

Step	Hyp	Ref	Expression
1		sge0lefi.1	$⊢ φ \to X \in V$
2		sge0lefi.2	$⊢ φ \to F : X ⟶ [0, +∞]$
3		sge0lefi.3	$⊢ φ \to A \in ℝ^{*}$
4		simpr	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to x \in (𝒫 X \cap Fin)$
5	2	adantr	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to F : X ⟶ [0, +∞]$
6		elpwinss	$⊢ x \in (𝒫 X \cap Fin) \to x \subseteq X$
7	6	adantl	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to x \subseteq X$
8	5 7	fssresd	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to ({F ↾}_{x}) : x ⟶ [0, +∞]$
9	4 8	sge0xrcl	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to sum^({F ↾}_{x}) \in ℝ^{*}$
10	9	adantlr	$⊢ ((φ \land sum^(F) \leq A) \land x \in (𝒫 X \cap Fin)) \to sum^({F ↾}_{x}) \in ℝ^{*}$
11	1 2	sge0xrcl	$⊢ φ \to sum^(F) \in ℝ^{*}$
12	11	ad2antrr	$⊢ ((φ \land sum^(F) \leq A) \land x \in (𝒫 X \cap Fin)) \to sum^(F) \in ℝ^{*}$
13	3	ad2antrr	$⊢ ((φ \land sum^(F) \leq A) \land x \in (𝒫 X \cap Fin)) \to A \in ℝ^{*}$
14	1	adantr	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to X \in V$
15	14 5	sge0less	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to sum^({F ↾}_{x}) \leq sum^(F)$
16	15	adantlr	$⊢ ((φ \land sum^(F) \leq A) \land x \in (𝒫 X \cap Fin)) \to sum^({F ↾}_{x}) \leq sum^(F)$
17		simplr	$⊢ ((φ \land sum^(F) \leq A) \land x \in (𝒫 X \cap Fin)) \to sum^(F) \leq A$
18	10 12 13 16 17	xrletrd	$⊢ ((φ \land sum^(F) \leq A) \land x \in (𝒫 X \cap Fin)) \to sum^({F ↾}_{x}) \leq A$
19	18	ralrimiva	$⊢ (φ \land sum^(F) \leq A) \to \forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \leq A$
20	19	ex	$⊢ φ \to (sum^(F) \leq A \to \forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \leq A)$
21	1 2	sge0sup	$⊢ φ \to sum^(F) = sup (ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) ℝ^{*} <)$
22	21	adantr	$⊢ (φ \land \forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \leq A) \to sum^(F) = sup (ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) ℝ^{*} <)$
23		vex	$⊢ y \in V$
24		eqid	$⊢ (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) = (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x}))$
25	24	elrnmpt	$⊢ y \in V \to (y \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) \leftrightarrow \exists x \in (𝒫 X \cap Fin) y = sum^({F ↾}_{x}))$
26	23 25	ax-mp	$⊢ y \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) \leftrightarrow \exists x \in (𝒫 X \cap Fin) y = sum^({F ↾}_{x})$
27	26	bilani	$⊢ ((φ \land \forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \leq A) \land y \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x}))) \to \exists x \in (𝒫 X \cap Fin) y = sum^({F ↾}_{x})$
28		nfv	$⊢ Ⅎ x φ$
29		nfra1	$⊢ Ⅎ x \forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \leq A$
30	28 29	nfan	$⊢ Ⅎ x (φ \land \forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \leq A)$
31		nfcv	$⊢ \underline{Ⅎ} x y$
32		nfmpt1	$⊢ \underline{Ⅎ} x (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x}))$
33	32	nfrn	$⊢ \underline{Ⅎ} x ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x}))$
34	31 33	nfel	$⊢ Ⅎ x y \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x}))$
35	30 34	nfan	$⊢ Ⅎ x ((φ \land \forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \leq A) \land y \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})))$
36		nfv	$⊢ Ⅎ x y \leq A$
37		simp3	$⊢ (\forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \leq A \land x \in (𝒫 X \cap Fin) \land y = sum^({F ↾}_{x})) \to y = sum^({F ↾}_{x})$
38		rspa	$⊢ (\forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \leq A \land x \in (𝒫 X \cap Fin)) \to sum^({F ↾}_{x}) \leq A$
39	38	3adant3	$⊢ (\forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \leq A \land x \in (𝒫 X \cap Fin) \land y = sum^({F ↾}_{x})) \to sum^({F ↾}_{x}) \leq A$
40	37 39	eqbrtrd	$⊢ (\forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \leq A \land x \in (𝒫 X \cap Fin) \land y = sum^({F ↾}_{x})) \to y \leq A$
41	40	3adant1l	$⊢ ((φ \land \forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \leq A) \land x \in (𝒫 X \cap Fin) \land y = sum^({F ↾}_{x})) \to y \leq A$
42	41	3exp	$⊢ (φ \land \forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \leq A) \to (x \in (𝒫 X \cap Fin) \to (y = sum^({F ↾}_{x}) \to y \leq A))$
43	42	adantr	$⊢ ((φ \land \forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \leq A) \land y \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x}))) \to (x \in (𝒫 X \cap Fin) \to (y = sum^({F ↾}_{x}) \to y \leq A))$
44	35 36 43	rexlimd	$⊢ ((φ \land \forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \leq A) \land y \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x}))) \to (\exists x \in (𝒫 X \cap Fin) y = sum^({F ↾}_{x}) \to y \leq A)$
45	27 44	mpd	$⊢ ((φ \land \forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \leq A) \land y \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x}))) \to y \leq A$
46	45	ralrimiva	$⊢ (φ \land \forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \leq A) \to \forall y \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) y \leq A$
47	9	ralrimiva	$⊢ φ \to \forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \in ℝ^{*}$
48	24	rnmptss	$⊢ \forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \in ℝ^{} \to ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) \subseteq ℝ^{}$
49	47 48	syl	$⊢ φ \to ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) \subseteq ℝ^{*}$
50	49	adantr	$⊢ (φ \land \forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \leq A) \to ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) \subseteq ℝ^{*}$
51	3	adantr	$⊢ (φ \land \forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \leq A) \to A \in ℝ^{*}$
52		supxrleub	$⊢ (ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) \subseteq ℝ^{} \land A \in ℝ^{}) \to (sup (ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) ℝ^{*} <) \leq A \leftrightarrow \forall y \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) y \leq A)$
53	50 51 52	syl2anc	$⊢ (φ \land \forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \leq A) \to (sup (ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) ℝ^{*} <) \leq A \leftrightarrow \forall y \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) y \leq A)$
54	46 53	mpbird	$⊢ (φ \land \forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \leq A) \to sup (ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) ℝ^{*} <) \leq A$
55	22 54	eqbrtrd	$⊢ (φ \land \forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \leq A) \to sum^(F) \leq A$
56	55	ex	$⊢ φ \to (\forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \leq A \to sum^(F) \leq A)$
57	20 56	impbid	$⊢ φ \to (sum^(F) \leq A \leftrightarrow \forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \leq A)$

Metamath Proof Explorer

Theorem sge0lefi

Proof