esumlub

Description: The extended sum is the lowest upper bound for the partial sums. (Contributed by Thierry Arnoux, 19-Oct-2017) (Proof shortened by AV, 12-Dec-2019)

	Ref	Expression
Hypotheses	esumlub.f	$⊢ Ⅎ k φ$
	esumlub.0	$⊢ φ \to A \in V$
	esumlub.1	$⊢ (φ \land k \in A) \to B \in [0, +∞]$
	esumlub.2	$⊢ φ \to X \in ℝ^{*}$
	esumlub.3	$⊢ φ \to X < \underset{k \in A}{\sum^{*}} B$
Assertion	esumlub	$⊢ φ \to \exists a \in (𝒫 A \cap Fin) X < \underset{k \in a}{\sum^{*}} B$

Proof

Step	Hyp	Ref	Expression
1		esumlub.f	$⊢ Ⅎ k φ$
2		esumlub.0	$⊢ φ \to A \in V$
3		esumlub.1	$⊢ (φ \land k \in A) \to B \in [0, +∞]$
4		esumlub.2	$⊢ φ \to X \in ℝ^{*}$
5		esumlub.3	$⊢ φ \to X < \underset{k \in A}{\sum^{*}} B$
6		nfcv	$⊢ \underline{Ⅎ} k A$
7		eqidd	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B = \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B$
8	1 6 2 3 7	esumval	$⊢ φ \to \underset{k \in A}{\sum^{}} B = sup (ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B) ℝ^{*} <)$
9	8	breq2d	$⊢ φ \to (X < \underset{k \in A}{\sum^{}} B \leftrightarrow X < sup (ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B) ℝ^{*} <))$
10		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
11		xrge0base	$⊢ [0, +∞] = {Base}_{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])}$
12		xrge0cmn	$⊢ ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞] \in CMnd$
13	12	a1i	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞] \in CMnd$
14		inss2	$⊢ 𝒫 A \cap Fin \subseteq Fin$
15		simpr	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to x \in (𝒫 A \cap Fin)$
16	14 15	sseldi	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to x \in Fin$
17		nfv	$⊢ Ⅎ k x \in (𝒫 A \cap Fin)$
18	1 17	nfan	$⊢ Ⅎ k (φ \land x \in (𝒫 A \cap Fin))$
19		simpll	$⊢ ((φ \land x \in (𝒫 A \cap Fin)) \land k \in x) \to φ$
20		inss1	$⊢ 𝒫 A \cap Fin \subseteq 𝒫 A$
21	20	sseli	$⊢ x \in (𝒫 A \cap Fin) \to x \in 𝒫 A$
22	21	ad2antlr	$⊢ ((φ \land x \in (𝒫 A \cap Fin)) \land k \in x) \to x \in 𝒫 A$
23	22	elpwid	$⊢ ((φ \land x \in (𝒫 A \cap Fin)) \land k \in x) \to x \subseteq A$
24		simpr	$⊢ ((φ \land x \in (𝒫 A \cap Fin)) \land k \in x) \to k \in x$
25	23 24	sseldd	$⊢ ((φ \land x \in (𝒫 A \cap Fin)) \land k \in x) \to k \in A$
26	19 25 3	syl2anc	$⊢ ((φ \land x \in (𝒫 A \cap Fin)) \land k \in x) \to B \in [0, +∞]$
27	26	ex	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to (k \in x \to B \in [0, +∞])$
28	18 27	ralrimi	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \forall k \in x B \in [0, +∞]$
29	11 13 16 28	gsummptcl	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \underset{k \in x}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} B \in [0, +∞]$
30	10 29	sseldi	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \in ℝ^{}$
31	30	ralrimiva	$⊢ φ \to \forall x \in (𝒫 A \cap Fin) \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \in ℝ^{}$
32		eqid	$⊢ (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B) = (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B)$
33	32	rnmptss	$⊢ \forall x \in (𝒫 A \cap Fin) \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \in ℝ^{} \to ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B) \subseteq ℝ^{}$
34	31 33	syl	$⊢ φ \to ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B) \subseteq ℝ^{}$
35		supxrlub	$⊢ (ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B) \subseteq ℝ^{} \land X \in ℝ^{}) \to (X < sup (ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B) ℝ^{} <) \leftrightarrow \exists y \in ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B) X < y)$
36	34 4 35	syl2anc	$⊢ φ \to (X < sup (ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B) ℝ^{} <) \leftrightarrow \exists y \in ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} B) X < y)$
37	9 36	bitrd	$⊢ φ \to (X < \underset{k \in A}{\sum^{}} B \leftrightarrow \exists y \in ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B) X < y)$
38	5 37	mpbid	$⊢ φ \to \exists y \in ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} B) X < y$
39		ovex	$⊢ \underset{k \in a}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} B \in V$
40	39	a1i	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to \underset{k \in a}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} B \in V$
41		mpteq1	$⊢ x = a \to (k \in x ⟼ B) = (k \in a ⟼ B)$
42	41	oveq2d	$⊢ x = a \to \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B = \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B$
43	42	cbvmptv	$⊢ (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B) = (a \in (𝒫 A \cap Fin) ⟼ \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B)$
44	43 39	elrnmpti	$⊢ y \in ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B) \leftrightarrow \exists a \in (𝒫 A \cap Fin) y = \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B$
45	44	a1i	$⊢ φ \to (y \in ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B) \leftrightarrow \exists a \in (𝒫 A \cap Fin) y = \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B)$
46		simpr	$⊢ (φ \land y = \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B) \to y = \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B$
47	46	breq2d	$⊢ (φ \land y = \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B) \to (X < y \leftrightarrow X < \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B)$
48	40 45 47	rexxfr2d	$⊢ φ \to (\exists y \in ran (x \in (𝒫 A \cap Fin) ⟼ \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B) X < y \leftrightarrow \exists a \in (𝒫 A \cap Fin) X < \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B)$
49	38 48	mpbid	$⊢ φ \to \exists a \in (𝒫 A \cap Fin) X < \underset{k \in a}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} B$
50		nfv	$⊢ Ⅎ k a \in (𝒫 A \cap Fin)$
51	1 50	nfan	$⊢ Ⅎ k (φ \land a \in (𝒫 A \cap Fin))$
52		simpr	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to a \in (𝒫 A \cap Fin)$
53	14 52	sseldi	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to a \in Fin$
54		simpll	$⊢ ((φ \land a \in (𝒫 A \cap Fin)) \land k \in a) \to φ$
55	20	sseli	$⊢ a \in (𝒫 A \cap Fin) \to a \in 𝒫 A$
56	55	ad2antlr	$⊢ ((φ \land a \in (𝒫 A \cap Fin)) \land k \in a) \to a \in 𝒫 A$
57	56	elpwid	$⊢ ((φ \land a \in (𝒫 A \cap Fin)) \land k \in a) \to a \subseteq A$
58		simpr	$⊢ ((φ \land a \in (𝒫 A \cap Fin)) \land k \in a) \to k \in a$
59	57 58	sseldd	$⊢ ((φ \land a \in (𝒫 A \cap Fin)) \land k \in a) \to k \in A$
60	54 59 3	syl2anc	$⊢ ((φ \land a \in (𝒫 A \cap Fin)) \land k \in a) \to B \in [0, +∞]$
61	51 53 60	gsumesum	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B = \underset{k \in a}{\sum^{}} B$
62	61	breq2d	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to (X < \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \leftrightarrow X < \underset{k \in a}{\sum^{}} B)$
63	62	biimpd	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to (X < \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \to X < \underset{k \in a}{\sum^{}} B)$
64	63	reximdva	$⊢ φ \to (\exists a \in (𝒫 A \cap Fin) X < \underset{k \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B \to \exists a \in (𝒫 A \cap Fin) X < \underset{k \in a}{\sum^{}} B)$
65	49 64	mpd	$⊢ φ \to \exists a \in (𝒫 A \cap Fin) X < \underset{k \in a}{\sum^{*}} B$

Metamath Proof Explorer

Theorem esumlub

Proof