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	biimpi	$⊢ y \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) \to \exists x \in (𝒫 X \cap Fin) y = sum^({F ↾}_{x})$
28	27	adantl	$⊢ ((φ \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})$
29		nfv	$⊢ Ⅎ x φ$
30		nfra1	$⊢ Ⅎ x \forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \leq A$
31	29 30	nfan	$⊢ Ⅎ x (φ \land \forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \leq A)$
32		nfcv	$⊢ \underline{Ⅎ} x y$
33		nfmpt1	$⊢ \underline{Ⅎ} x (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x}))$
34	33	nfrn	$⊢ \underline{Ⅎ} x ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x}))$
35	32 34	nfel	$⊢ Ⅎ x y \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x}))$
36	31 35	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})))$
37		nfv	$⊢ Ⅎ x y \leq A$
38		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})$
39		rspa	$⊢ (\forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \leq A \land x \in (𝒫 X \cap Fin)) \to sum^({F ↾}_{x}) \leq A$
40	39	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$
41	38 40	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$
42	41	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$
43	42	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))$
44	43	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))$
45	36 37 44	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)$
46	28 45	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$
47	46	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$
48	9	ralrimiva	$⊢ φ \to \forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \in ℝ^{*}$
49	24	rnmptss	$⊢ \forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \in ℝ^{} \to ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) \subseteq ℝ^{}$
50	48 49	syl	$⊢ φ \to ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) \subseteq ℝ^{*}$
51	50	adantr	$⊢ (φ \land \forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \leq A) \to ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) \subseteq ℝ^{*}$
52	3	adantr	$⊢ (φ \land \forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \leq A) \to A \in ℝ^{*}$
53		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)$
54	51 52 53	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)$
55	47 54	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$
56	22 55	eqbrtrd	$⊢ (φ \land \forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \leq A) \to sum^(F) \leq A$
57	56	ex	$⊢ φ \to (\forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \leq A \to sum^(F) \leq A)$
58	20 57	impbid	$⊢ φ \to (sum^(F) \leq A \leftrightarrow \forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \leq A)$

Metamath Proof Explorer

Theorem sge0lefi

Proof