sge0reuz

Description: Value of the generalized sum of nonnegative reals, when the domain is a set of upper integers. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	sge0reuz.k	$⊢ Ⅎ k φ$
	sge0reuz.m	$⊢ φ \to M \in ℤ$
	sge0reuz.z	$⊢ Z = ℤ_{\geq M}$
	sge0reuz.b	$⊢ (φ \land k \in Z) \to B \in [0, +∞)$
Assertion	sge0reuz	$⊢ φ \to sum^((k \in Z ⟼ B)) = sup (ran (n \in Z ⟼ \sum_{k = M}^{n} B) ℝ^{*} <)$

Proof

Step	Hyp	Ref	Expression
1		sge0reuz.k	$⊢ Ⅎ k φ$
2		sge0reuz.m	$⊢ φ \to M \in ℤ$
3		sge0reuz.z	$⊢ Z = ℤ_{\geq M}$
4		sge0reuz.b	$⊢ (φ \land k \in Z) \to B \in [0, +∞)$
5	3	a1i	$⊢ φ \to Z = ℤ_{\geq M}$
6		fvex	$⊢ ℤ_{\geq M} \in V$
7	5 6	eqeltrdi	$⊢ φ \to Z \in V$
8	1 7 4	sge0revalmpt	$⊢ φ \to sum^((k \in Z ⟼ B)) = sup (ran (x \in (𝒫 Z \cap Fin) ⟼ \sum_{k \in x} B) ℝ^{*} <)$
9		nfv	$⊢ Ⅎ x φ$
10		eqid	$⊢ (x \in (𝒫 Z \cap Fin) ⟼ \sum_{k \in x} B) = (x \in (𝒫 Z \cap Fin) ⟼ \sum_{k \in x} B)$
11		nfv	$⊢ Ⅎ k x \in (𝒫 Z \cap Fin)$
12	1 11	nfan	$⊢ Ⅎ k (φ \land x \in (𝒫 Z \cap Fin))$
13		elinel2	$⊢ x \in (𝒫 Z \cap Fin) \to x \in Fin$
14	13	adantl	$⊢ (φ \land x \in (𝒫 Z \cap Fin)) \to x \in Fin$
15		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
16		simpll	$⊢ ((φ \land x \in (𝒫 Z \cap Fin)) \land k \in x) \to φ$
17		elpwinss	$⊢ x \in (𝒫 Z \cap Fin) \to x \subseteq Z$
18	17	adantr	$⊢ (x \in (𝒫 Z \cap Fin) \land k \in x) \to x \subseteq Z$
19		simpr	$⊢ (x \in (𝒫 Z \cap Fin) \land k \in x) \to k \in x$
20	18 19	sseldd	$⊢ (x \in (𝒫 Z \cap Fin) \land k \in x) \to k \in Z$
21	20	adantll	$⊢ ((φ \land x \in (𝒫 Z \cap Fin)) \land k \in x) \to k \in Z$
22	16 21 4	syl2anc	$⊢ ((φ \land x \in (𝒫 Z \cap Fin)) \land k \in x) \to B \in [0, +∞)$
23	15 22	sselid	$⊢ ((φ \land x \in (𝒫 Z \cap Fin)) \land k \in x) \to B \in ℝ$
24	12 14 23	fsumreclf	$⊢ (φ \land x \in (𝒫 Z \cap Fin)) \to \sum_{k \in x} B \in ℝ$
25	24	rexrd	$⊢ (φ \land x \in (𝒫 Z \cap Fin)) \to \sum_{k \in x} B \in ℝ^{*}$
26	9 10 25	rnmptssd	$⊢ φ \to ran (x \in (𝒫 Z \cap Fin) ⟼ \sum_{k \in x} B) \subseteq ℝ^{*}$
27		supxrcl	$⊢ ran (x \in (𝒫 Z \cap Fin) ⟼ \sum_{k \in x} B) \subseteq ℝ^{} \to sup (ran (x \in (𝒫 Z \cap Fin) ⟼ \sum_{k \in x} B) ℝ^{} <) \in ℝ^{*}$
28	26 27	syl	$⊢ φ \to sup (ran (x \in (𝒫 Z \cap Fin) ⟼ \sum_{k \in x} B) ℝ^{} <) \in ℝ^{}$
29		nfv	$⊢ Ⅎ n φ$
30		eqid	$⊢ (n \in Z ⟼ \sum_{k = M}^{n} B) = (n \in Z ⟼ \sum_{k = M}^{n} B)$
31		nfv	$⊢ Ⅎ k n \in Z$
32	1 31	nfan	$⊢ Ⅎ k (φ \land n \in Z)$
33		fzfid	$⊢ (φ \land n \in Z) \to (M \dots n) \in Fin$
34		elfzuz	$⊢ k \in (M \dots n) \to k \in ℤ_{\geq M}$
35	34 3	eleqtrrdi	$⊢ k \in (M \dots n) \to k \in Z$
36	35	adantl	$⊢ (φ \land k \in (M \dots n)) \to k \in Z$
37	15 4	sselid	$⊢ (φ \land k \in Z) \to B \in ℝ$
38	36 37	syldan	$⊢ (φ \land k \in (M \dots n)) \to B \in ℝ$
39	38	adantlr	$⊢ ((φ \land n \in Z) \land k \in (M \dots n)) \to B \in ℝ$
40	32 33 39	fsumreclf	$⊢ (φ \land n \in Z) \to \sum_{k = M}^{n} B \in ℝ$
41	40	rexrd	$⊢ (φ \land n \in Z) \to \sum_{k = M}^{n} B \in ℝ^{*}$
42	29 30 41	rnmptssd	$⊢ φ \to ran (n \in Z ⟼ \sum_{k = M}^{n} B) \subseteq ℝ^{*}$
43		supxrcl	$⊢ ran (n \in Z ⟼ \sum_{k = M}^{n} B) \subseteq ℝ^{} \to sup (ran (n \in Z ⟼ \sum_{k = M}^{n} B) ℝ^{} <) \in ℝ^{*}$
44	42 43	syl	$⊢ φ \to sup (ran (n \in Z ⟼ \sum_{k = M}^{n} B) ℝ^{} <) \in ℝ^{}$
45		vex	$⊢ y \in V$
46	10	elrnmpt	$⊢ y \in V \to (y \in ran (x \in (𝒫 Z \cap Fin) ⟼ \sum_{k \in x} B) \leftrightarrow \exists x \in (𝒫 Z \cap Fin) y = \sum_{k \in x} B)$
47	45 46	ax-mp	$⊢ y \in ran (x \in (𝒫 Z \cap Fin) ⟼ \sum_{k \in x} B) \leftrightarrow \exists x \in (𝒫 Z \cap Fin) y = \sum_{k \in x} B$
48	47	biimpi	$⊢ y \in ran (x \in (𝒫 Z \cap Fin) ⟼ \sum_{k \in x} B) \to \exists x \in (𝒫 Z \cap Fin) y = \sum_{k \in x} B$
49	48	adantl	$⊢ (φ \land y \in ran (x \in (𝒫 Z \cap Fin) ⟼ \sum_{k \in x} B)) \to \exists x \in (𝒫 Z \cap Fin) y = \sum_{k \in x} B$
50	2	3ad2ant1	$⊢ (φ \land x \in (𝒫 Z \cap Fin) \land y = \sum_{k \in x} B) \to M \in ℤ$
51	17	3ad2ant2	$⊢ (φ \land x \in (𝒫 Z \cap Fin) \land y = \sum_{k \in x} B) \to x \subseteq Z$
52	14	3adant3	$⊢ (φ \land x \in (𝒫 Z \cap Fin) \land y = \sum_{k \in x} B) \to x \in Fin$
53	50 3 51 52	uzfissfz	$⊢ (φ \land x \in (𝒫 Z \cap Fin) \land y = \sum_{k \in x} B) \to \exists n \in Z x \subseteq (M \dots n)$
54		nfv	$⊢ Ⅎ n (φ \land x \in (𝒫 Z \cap Fin) \land y = \sum_{k \in x} B)$
55		nfmpt1	$⊢ \underline{Ⅎ} n (n \in Z ⟼ \sum_{k = M}^{n} B)$
56	55	nfrn	$⊢ \underline{Ⅎ} n ran (n \in Z ⟼ \sum_{k = M}^{n} B)$
57		nfv	$⊢ Ⅎ n y \leq w$
58	56 57	nfrexw	$⊢ Ⅎ n \exists w \in ran (n \in Z ⟼ \sum_{k = M}^{n} B) y \leq w$
59		id	$⊢ n \in Z \to n \in Z$
60		sumex	$⊢ \sum_{k = M}^{n} B \in V$
61	60	a1i	$⊢ n \in Z \to \sum_{k = M}^{n} B \in V$
62	30	elrnmpt1	$⊢ (n \in Z \land \sum_{k = M}^{n} B \in V) \to \sum_{k = M}^{n} B \in ran (n \in Z ⟼ \sum_{k = M}^{n} B)$
63	59 61 62	syl2anc	$⊢ n \in Z \to \sum_{k = M}^{n} B \in ran (n \in Z ⟼ \sum_{k = M}^{n} B)$
64	63	3ad2ant2	$⊢ ((φ \land y = \sum_{k \in x} B) \land n \in Z \land x \subseteq (M \dots n)) \to \sum_{k = M}^{n} B \in ran (n \in Z ⟼ \sum_{k = M}^{n} B)$
65		simplr	$⊢ ((φ \land y = \sum_{k \in x} B) \land x \subseteq (M \dots n)) \to y = \sum_{k \in x} B$
66		nfcv	$⊢ \underline{Ⅎ} k y$
67		nfcv	$⊢ \underline{Ⅎ} k x$
68	67	nfsum1	$⊢ \underline{Ⅎ} k \sum_{k \in x} B$
69	66 68	nfeq	$⊢ Ⅎ k y = \sum_{k \in x} B$
70	1 69	nfan	$⊢ Ⅎ k (φ \land y = \sum_{k \in x} B)$
71		nfv	$⊢ Ⅎ k x \subseteq (M \dots n)$
72	70 71	nfan	$⊢ Ⅎ k ((φ \land y = \sum_{k \in x} B) \land x \subseteq (M \dots n))$
73		fzfid	$⊢ ((φ \land y = \sum_{k \in x} B) \land x \subseteq (M \dots n)) \to (M \dots n) \in Fin$
74	38	ad4ant14	$⊢ (((φ \land y = \sum_{k \in x} B) \land x \subseteq (M \dots n)) \land k \in (M \dots n)) \to B \in ℝ$
75		simplll	$⊢ (((φ \land y = \sum_{k \in x} B) \land x \subseteq (M \dots n)) \land k \in (M \dots n)) \to φ$
76	35	adantl	$⊢ (((φ \land y = \sum_{k \in x} B) \land x \subseteq (M \dots n)) \land k \in (M \dots n)) \to k \in Z$
77		0xr	$⊢ 0 \in ℝ^{*}$
78	77	a1i	$⊢ (φ \land k \in Z) \to 0 \in ℝ^{*}$
79		pnfxr	$⊢ +∞ \in ℝ^{*}$
80	79	a1i	$⊢ (φ \land k \in Z) \to +∞ \in ℝ^{*}$
81		icogelb	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land B \in [0, +∞)) \to 0 \leq B$
82	78 80 4 81	syl3anc	$⊢ (φ \land k \in Z) \to 0 \leq B$
83	75 76 82	syl2anc	$⊢ (((φ \land y = \sum_{k \in x} B) \land x \subseteq (M \dots n)) \land k \in (M \dots n)) \to 0 \leq B$
84		simpr	$⊢ ((φ \land y = \sum_{k \in x} B) \land x \subseteq (M \dots n)) \to x \subseteq (M \dots n)$
85	72 73 74 83 84	fsumlessf	$⊢ ((φ \land y = \sum_{k \in x} B) \land x \subseteq (M \dots n)) \to \sum_{k \in x} B \leq \sum_{k = M}^{n} B$
86	65 85	eqbrtrd	$⊢ ((φ \land y = \sum_{k \in x} B) \land x \subseteq (M \dots n)) \to y \leq \sum_{k = M}^{n} B$
87	86	3adant2	$⊢ ((φ \land y = \sum_{k \in x} B) \land n \in Z \land x \subseteq (M \dots n)) \to y \leq \sum_{k = M}^{n} B$
88		breq2	$⊢ w = \sum_{k = M}^{n} B \to (y \leq w \leftrightarrow y \leq \sum_{k = M}^{n} B)$
89	88	rspcev	$⊢ (\sum_{k = M}^{n} B \in ran (n \in Z ⟼ \sum_{k = M}^{n} B) \land y \leq \sum_{k = M}^{n} B) \to \exists w \in ran (n \in Z ⟼ \sum_{k = M}^{n} B) y \leq w$
90	64 87 89	syl2anc	$⊢ ((φ \land y = \sum_{k \in x} B) \land n \in Z \land x \subseteq (M \dots n)) \to \exists w \in ran (n \in Z ⟼ \sum_{k = M}^{n} B) y \leq w$
91	90	3exp	$⊢ (φ \land y = \sum_{k \in x} B) \to (n \in Z \to (x \subseteq (M \dots n) \to \exists w \in ran (n \in Z ⟼ \sum_{k = M}^{n} B) y \leq w))$
92	91	3adant2	$⊢ (φ \land x \in (𝒫 Z \cap Fin) \land y = \sum_{k \in x} B) \to (n \in Z \to (x \subseteq (M \dots n) \to \exists w \in ran (n \in Z ⟼ \sum_{k = M}^{n} B) y \leq w))$
93	54 58 92	rexlimd	$⊢ (φ \land x \in (𝒫 Z \cap Fin) \land y = \sum_{k \in x} B) \to (\exists n \in Z x \subseteq (M \dots n) \to \exists w \in ran (n \in Z ⟼ \sum_{k = M}^{n} B) y \leq w)$
94	53 93	mpd	$⊢ (φ \land x \in (𝒫 Z \cap Fin) \land y = \sum_{k \in x} B) \to \exists w \in ran (n \in Z ⟼ \sum_{k = M}^{n} B) y \leq w$
95	94	3exp	$⊢ φ \to (x \in (𝒫 Z \cap Fin) \to (y = \sum_{k \in x} B \to \exists w \in ran (n \in Z ⟼ \sum_{k = M}^{n} B) y \leq w))$
96	95	rexlimdv	$⊢ φ \to (\exists x \in (𝒫 Z \cap Fin) y = \sum_{k \in x} B \to \exists w \in ran (n \in Z ⟼ \sum_{k = M}^{n} B) y \leq w)$
97	96	imp	$⊢ (φ \land \exists x \in (𝒫 Z \cap Fin) y = \sum_{k \in x} B) \to \exists w \in ran (n \in Z ⟼ \sum_{k = M}^{n} B) y \leq w$
98	49 97	syldan	$⊢ (φ \land y \in ran (x \in (𝒫 Z \cap Fin) ⟼ \sum_{k \in x} B)) \to \exists w \in ran (n \in Z ⟼ \sum_{k = M}^{n} B) y \leq w$
99	26 42 98	suplesup2	$⊢ φ \to sup (ran (x \in (𝒫 Z \cap Fin) ⟼ \sum_{k \in x} B) ℝ^{} <) \leq sup (ran (n \in Z ⟼ \sum_{k = M}^{n} B) ℝ^{} <)$
100	30	elrnmpt	$⊢ y \in V \to (y \in ran (n \in Z ⟼ \sum_{k = M}^{n} B) \leftrightarrow \exists n \in Z y = \sum_{k = M}^{n} B)$
101	45 100	ax-mp	$⊢ y \in ran (n \in Z ⟼ \sum_{k = M}^{n} B) \leftrightarrow \exists n \in Z y = \sum_{k = M}^{n} B$
102	101	biimpi	$⊢ y \in ran (n \in Z ⟼ \sum_{k = M}^{n} B) \to \exists n \in Z y = \sum_{k = M}^{n} B$
103	102	adantl	$⊢ (φ \land y \in ran (n \in Z ⟼ \sum_{k = M}^{n} B)) \to \exists n \in Z y = \sum_{k = M}^{n} B$
104	35	ssriv	$⊢ (M \dots n) \subseteq Z$
105		ovex	$⊢ (M \dots n) \in V$
106	105	elpw	$⊢ (M \dots n) \in 𝒫 Z \leftrightarrow (M \dots n) \subseteq Z$
107	104 106	mpbir	$⊢ (M \dots n) \in 𝒫 Z$
108		fzfi	$⊢ (M \dots n) \in Fin$
109	107 108	elini	$⊢ (M \dots n) \in (𝒫 Z \cap Fin)$
110	109	a1i	$⊢ y = \sum_{k = M}^{n} B \to (M \dots n) \in (𝒫 Z \cap Fin)$
111		id	$⊢ y = \sum_{k = M}^{n} B \to y = \sum_{k = M}^{n} B$
112		sumeq1	$⊢ x = (M \dots n) \to \sum_{k \in x} B = \sum_{k = M}^{n} B$
113	112	rspceeqv	$⊢ ((M \dots n) \in (𝒫 Z \cap Fin) \land y = \sum_{k = M}^{n} B) \to \exists x \in (𝒫 Z \cap Fin) y = \sum_{k \in x} B$
114	110 111 113	syl2anc	$⊢ y = \sum_{k = M}^{n} B \to \exists x \in (𝒫 Z \cap Fin) y = \sum_{k \in x} B$
115	45	a1i	$⊢ y = \sum_{k = M}^{n} B \to y \in V$
116	10 114 115	elrnmptd	$⊢ y = \sum_{k = M}^{n} B \to y \in ran (x \in (𝒫 Z \cap Fin) ⟼ \sum_{k \in x} B)$
117	116	2a1i	$⊢ φ \to (n \in Z \to (y = \sum_{k = M}^{n} B \to y \in ran (x \in (𝒫 Z \cap Fin) ⟼ \sum_{k \in x} B)))$
118	117	rexlimdv	$⊢ φ \to (\exists n \in Z y = \sum_{k = M}^{n} B \to y \in ran (x \in (𝒫 Z \cap Fin) ⟼ \sum_{k \in x} B))$
119	118	adantr	$⊢ (φ \land y \in ran (n \in Z ⟼ \sum_{k = M}^{n} B)) \to (\exists n \in Z y = \sum_{k = M}^{n} B \to y \in ran (x \in (𝒫 Z \cap Fin) ⟼ \sum_{k \in x} B))$
120	103 119	mpd	$⊢ (φ \land y \in ran (n \in Z ⟼ \sum_{k = M}^{n} B)) \to y \in ran (x \in (𝒫 Z \cap Fin) ⟼ \sum_{k \in x} B)$
121	120	ralrimiva	$⊢ φ \to \forall y \in ran (n \in Z ⟼ \sum_{k = M}^{n} B) y \in ran (x \in (𝒫 Z \cap Fin) ⟼ \sum_{k \in x} B)$
122		dfss3	$⊢ ran (n \in Z ⟼ \sum_{k = M}^{n} B) \subseteq ran (x \in (𝒫 Z \cap Fin) ⟼ \sum_{k \in x} B) \leftrightarrow \forall y \in ran (n \in Z ⟼ \sum_{k = M}^{n} B) y \in ran (x \in (𝒫 Z \cap Fin) ⟼ \sum_{k \in x} B)$
123	121 122	sylibr	$⊢ φ \to ran (n \in Z ⟼ \sum_{k = M}^{n} B) \subseteq ran (x \in (𝒫 Z \cap Fin) ⟼ \sum_{k \in x} B)$
124		supxrss	$⊢ (ran (n \in Z ⟼ \sum_{k = M}^{n} B) \subseteq ran (x \in (𝒫 Z \cap Fin) ⟼ \sum_{k \in x} B) \land ran (x \in (𝒫 Z \cap Fin) ⟼ \sum_{k \in x} B) \subseteq ℝ^{}) \to sup (ran (n \in Z ⟼ \sum_{k = M}^{n} B) ℝ^{} <) \leq sup (ran (x \in (𝒫 Z \cap Fin) ⟼ \sum_{k \in x} B) ℝ^{*} <)$
125	123 26 124	syl2anc	$⊢ φ \to sup (ran (n \in Z ⟼ \sum_{k = M}^{n} B) ℝ^{} <) \leq sup (ran (x \in (𝒫 Z \cap Fin) ⟼ \sum_{k \in x} B) ℝ^{} <)$
126	28 44 99 125	xrletrid	$⊢ φ \to sup (ran (x \in (𝒫 Z \cap Fin) ⟼ \sum_{k \in x} B) ℝ^{} <) = sup (ran (n \in Z ⟼ \sum_{k = M}^{n} B) ℝ^{} <)$
127	8 126	eqtrd	$⊢ φ \to sum^((k \in Z ⟼ B)) = sup (ran (n \in Z ⟼ \sum_{k = M}^{n} B) ℝ^{*} <)$

Metamath Proof Explorer

Theorem sge0reuz

Proof