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	bilani	$⊢ (φ \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$
49	2	3ad2ant1	$⊢ (φ \land x \in (𝒫 Z \cap Fin) \land y = \sum_{k \in x} B) \to M \in ℤ$
50	17	3ad2ant2	$⊢ (φ \land x \in (𝒫 Z \cap Fin) \land y = \sum_{k \in x} B) \to x \subseteq Z$
51	14	3adant3	$⊢ (φ \land x \in (𝒫 Z \cap Fin) \land y = \sum_{k \in x} B) \to x \in Fin$
52	49 3 50 51	uzfissfz	$⊢ (φ \land x \in (𝒫 Z \cap Fin) \land y = \sum_{k \in x} B) \to \exists n \in Z x \subseteq (M \dots n)$
53		nfv	$⊢ Ⅎ n (φ \land x \in (𝒫 Z \cap Fin) \land y = \sum_{k \in x} B)$
54		nfmpt1	$⊢ \underline{Ⅎ} n (n \in Z ⟼ \sum_{k = M}^{n} B)$
55	54	nfrn	$⊢ \underline{Ⅎ} n ran (n \in Z ⟼ \sum_{k = M}^{n} B)$
56		nfv	$⊢ Ⅎ n y \leq w$
57	55 56	nfrexw	$⊢ Ⅎ n \exists w \in ran (n \in Z ⟼ \sum_{k = M}^{n} B) y \leq w$
58		id	$⊢ n \in Z \to n \in Z$
59		sumex	$⊢ \sum_{k = M}^{n} B \in V$
60	59	a1i	$⊢ n \in Z \to \sum_{k = M}^{n} B \in V$
61	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)$
62	58 60 61	syl2anc	$⊢ n \in Z \to \sum_{k = M}^{n} B \in ran (n \in Z ⟼ \sum_{k = M}^{n} B)$
63	62	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)$
64		simplr	$⊢ ((φ \land y = \sum_{k \in x} B) \land x \subseteq (M \dots n)) \to y = \sum_{k \in x} B$
65		nfcv	$⊢ \underline{Ⅎ} k y$
66		nfcv	$⊢ \underline{Ⅎ} k x$
67	66	nfsum1	$⊢ \underline{Ⅎ} k \sum_{k \in x} B$
68	65 67	nfeq	$⊢ Ⅎ k y = \sum_{k \in x} B$
69	1 68	nfan	$⊢ Ⅎ k (φ \land y = \sum_{k \in x} B)$
70		nfv	$⊢ Ⅎ k x \subseteq (M \dots n)$
71	69 70	nfan	$⊢ Ⅎ k ((φ \land y = \sum_{k \in x} B) \land x \subseteq (M \dots n))$
72		fzfid	$⊢ ((φ \land y = \sum_{k \in x} B) \land x \subseteq (M \dots n)) \to (M \dots n) \in Fin$
73	38	ad4ant14	$⊢ (((φ \land y = \sum_{k \in x} B) \land x \subseteq (M \dots n)) \land k \in (M \dots n)) \to B \in ℝ$
74		simplll	$⊢ (((φ \land y = \sum_{k \in x} B) \land x \subseteq (M \dots n)) \land k \in (M \dots n)) \to φ$
75	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$
76		0xr	$⊢ 0 \in ℝ^{*}$
77	76	a1i	$⊢ (φ \land k \in Z) \to 0 \in ℝ^{*}$
78		pnfxr	$⊢ +∞ \in ℝ^{*}$
79	78	a1i	$⊢ (φ \land k \in Z) \to +∞ \in ℝ^{*}$
80		icogelb	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land B \in [0, +∞)) \to 0 \leq B$
81	77 79 4 80	syl3anc	$⊢ (φ \land k \in Z) \to 0 \leq B$
82	74 75 81	syl2anc	$⊢ (((φ \land y = \sum_{k \in x} B) \land x \subseteq (M \dots n)) \land k \in (M \dots n)) \to 0 \leq B$
83		simpr	$⊢ ((φ \land y = \sum_{k \in x} B) \land x \subseteq (M \dots n)) \to x \subseteq (M \dots n)$
84	71 72 73 82 83	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$
85	64 84	eqbrtrd	$⊢ ((φ \land y = \sum_{k \in x} B) \land x \subseteq (M \dots n)) \to y \leq \sum_{k = M}^{n} B$
86	85	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$
87		breq2	$⊢ w = \sum_{k = M}^{n} B \to (y \leq w \leftrightarrow y \leq \sum_{k = M}^{n} B)$
88	87	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$
89	63 86 88	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$
90	89	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))$
91	90	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))$
92	53 57 91	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)$
93	52 92	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$
94	93	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))$
95	94	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)$
96	95	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$
97	48 96	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$
98	26 42 97	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) ℝ^{} <)$
99	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)$
100	45 99	ax-mp	$⊢ y \in ran (n \in Z ⟼ \sum_{k = M}^{n} B) \leftrightarrow \exists n \in Z y = \sum_{k = M}^{n} B$
101	100	bilani	$⊢ (φ \land y \in ran (n \in Z ⟼ \sum_{k = M}^{n} B)) \to \exists n \in Z y = \sum_{k = M}^{n} B$
102	35	ssriv	$⊢ (M \dots n) \subseteq Z$
103		ovex	$⊢ (M \dots n) \in V$
104	103	elpw	$⊢ (M \dots n) \in 𝒫 Z \leftrightarrow (M \dots n) \subseteq Z$
105	102 104	mpbir	$⊢ (M \dots n) \in 𝒫 Z$
106		fzfi	$⊢ (M \dots n) \in Fin$
107	105 106	elini	$⊢ (M \dots n) \in (𝒫 Z \cap Fin)$
108	107	a1i	$⊢ y = \sum_{k = M}^{n} B \to (M \dots n) \in (𝒫 Z \cap Fin)$
109		id	$⊢ y = \sum_{k = M}^{n} B \to y = \sum_{k = M}^{n} B$
110		sumeq1	$⊢ x = (M \dots n) \to \sum_{k \in x} B = \sum_{k = M}^{n} B$
111	110	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$
112	108 109 111	syl2anc	$⊢ y = \sum_{k = M}^{n} B \to \exists x \in (𝒫 Z \cap Fin) y = \sum_{k \in x} B$
113	45	a1i	$⊢ y = \sum_{k = M}^{n} B \to y \in V$
114	10 112 113	elrnmptd	$⊢ y = \sum_{k = M}^{n} B \to y \in ran (x \in (𝒫 Z \cap Fin) ⟼ \sum_{k \in x} B)$
115	114	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)))$
116	115	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))$
117	116	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))$
118	101 117	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)$
119	118	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)$
120		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)$
121	119 120	sylibr	$⊢ φ \to ran (n \in Z ⟼ \sum_{k = M}^{n} B) \subseteq ran (x \in (𝒫 Z \cap Fin) ⟼ \sum_{k \in x} B)$
122		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) ℝ^{*} <)$
123	121 26 122	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) ℝ^{} <)$
124	28 44 98 123	xrletrid	$⊢ φ \to sup (ran (x \in (𝒫 Z \cap Fin) ⟼ \sum_{k \in x} B) ℝ^{} <) = sup (ran (n \in Z ⟼ \sum_{k = M}^{n} B) ℝ^{} <)$
125	8 124	eqtrd	$⊢ φ \to sum^((k \in Z ⟼ B)) = sup (ran (n \in Z ⟼ \sum_{k = M}^{n} B) ℝ^{*} <)$

Metamath Proof Explorer

Theorem sge0reuz

Proof