sge0reuzb

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

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

Proof

Step	Hyp	Ref	Expression
1		sge0reuzb.k	$⊢ Ⅎ k φ$
2		sge0reuzb.p	$⊢ Ⅎ x φ$
3		sge0reuzb.m	$⊢ φ \to M \in ℤ$
4		sge0reuzb.z	$⊢ Z = ℤ_{\geq M}$
5		sge0reuzb.b	$⊢ (φ \land k \in Z) \to B \in [0, +∞)$
6		sge0reuzb.x	$⊢ φ \to \exists x \in ℝ \forall n \in Z \sum_{k = M}^{n} B \leq x$
7	1 3 4 5	sge0reuz	$⊢ φ \to sum^((k \in Z ⟼ B)) = sup (ran (n \in Z ⟼ \sum_{k = M}^{n} B) ℝ^{*} <)$
8		nfv	$⊢ Ⅎ n φ$
9		eqid	$⊢ (n \in Z ⟼ \sum_{k = M}^{n} B) = (n \in Z ⟼ \sum_{k = M}^{n} B)$
10		nfv	$⊢ Ⅎ k n \in Z$
11	1 10	nfan	$⊢ Ⅎ k (φ \land n \in Z)$
12		fzfid	$⊢ (φ \land n \in Z) \to (M \dots n) \in Fin$
13		elfzuz	$⊢ k \in (M \dots n) \to k \in ℤ_{\geq M}$
14	13 4	eleqtrrdi	$⊢ k \in (M \dots n) \to k \in Z$
15	14	adantl	$⊢ (φ \land k \in (M \dots n)) \to k \in Z$
16		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
17	16 5	sselid	$⊢ (φ \land k \in Z) \to B \in ℝ$
18	15 17	syldan	$⊢ (φ \land k \in (M \dots n)) \to B \in ℝ$
19	18	adantlr	$⊢ ((φ \land n \in Z) \land k \in (M \dots n)) \to B \in ℝ$
20	11 12 19	fsumreclf	$⊢ (φ \land n \in Z) \to \sum_{k = M}^{n} B \in ℝ$
21	8 9 20	rnmptssd	$⊢ φ \to ran (n \in Z ⟼ \sum_{k = M}^{n} B) \subseteq ℝ$
22		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
23	3 22	syl	$⊢ φ \to M \in ℤ_{\geq M}$
24	23 4	eleqtrrdi	$⊢ φ \to M \in Z$
25		eqidd	$⊢ φ \to \sum_{k = M}^{M} B = \sum_{k = M}^{M} B$
26		oveq2	$⊢ n = M \to (M \dots n) = (M \dots M)$
27	26	sumeq1d	$⊢ n = M \to \sum_{k = M}^{n} B = \sum_{k = M}^{M} B$
28	27	rspceeqv	$⊢ (M \in Z \land \sum_{k = M}^{M} B = \sum_{k = M}^{M} B) \to \exists n \in Z \sum_{k = M}^{M} B = \sum_{k = M}^{n} B$
29	24 25 28	syl2anc	$⊢ φ \to \exists n \in Z \sum_{k = M}^{M} B = \sum_{k = M}^{n} B$
30		sumex	$⊢ \sum_{k = M}^{M} B \in V$
31	30	a1i	$⊢ φ \to \sum_{k = M}^{M} B \in V$
32	9 29 31	elrnmptd	$⊢ φ \to \sum_{k = M}^{M} B \in ran (n \in Z ⟼ \sum_{k = M}^{n} B)$
33	32	ne0d	$⊢ φ \to ran (n \in Z ⟼ \sum_{k = M}^{n} B) \neq \emptyset$
34		vex	$⊢ y \in V$
35	9	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)$
36	34 35	ax-mp	$⊢ y \in ran (n \in Z ⟼ \sum_{k = M}^{n} B) \leftrightarrow \exists n \in Z y = \sum_{k = M}^{n} B$
37	36	bilani	$⊢ (((φ \land x \in ℝ) \land \forall n \in Z \sum_{k = M}^{n} B \leq x) \land y \in ran (n \in Z ⟼ \sum_{k = M}^{n} B)) \to \exists n \in Z y = \sum_{k = M}^{n} B$
38		nfv	$⊢ Ⅎ n (φ \land x \in ℝ)$
39		nfra1	$⊢ Ⅎ n \forall n \in Z \sum_{k = M}^{n} B \leq x$
40	38 39	nfan	$⊢ Ⅎ n ((φ \land x \in ℝ) \land \forall n \in Z \sum_{k = M}^{n} B \leq x)$
41		nfv	$⊢ Ⅎ n y \leq x$
42		rspa	$⊢ (\forall n \in Z \sum_{k = M}^{n} B \leq x \land n \in Z) \to \sum_{k = M}^{n} B \leq x$
43		simpr	$⊢ (\sum_{k = M}^{n} B \leq x \land y = \sum_{k = M}^{n} B) \to y = \sum_{k = M}^{n} B$
44		simpl	$⊢ (\sum_{k = M}^{n} B \leq x \land y = \sum_{k = M}^{n} B) \to \sum_{k = M}^{n} B \leq x$
45	43 44	eqbrtrd	$⊢ (\sum_{k = M}^{n} B \leq x \land y = \sum_{k = M}^{n} B) \to y \leq x$
46	45	ex	$⊢ \sum_{k = M}^{n} B \leq x \to (y = \sum_{k = M}^{n} B \to y \leq x)$
47	42 46	syl	$⊢ (\forall n \in Z \sum_{k = M}^{n} B \leq x \land n \in Z) \to (y = \sum_{k = M}^{n} B \to y \leq x)$
48	47	ex	$⊢ \forall n \in Z \sum_{k = M}^{n} B \leq x \to (n \in Z \to (y = \sum_{k = M}^{n} B \to y \leq x))$
49	48	adantl	$⊢ ((φ \land x \in ℝ) \land \forall n \in Z \sum_{k = M}^{n} B \leq x) \to (n \in Z \to (y = \sum_{k = M}^{n} B \to y \leq x))$
50	40 41 49	rexlimd	$⊢ ((φ \land x \in ℝ) \land \forall n \in Z \sum_{k = M}^{n} B \leq x) \to (\exists n \in Z y = \sum_{k = M}^{n} B \to y \leq x)$
51	50	adantr	$⊢ (((φ \land x \in ℝ) \land \forall n \in Z \sum_{k = M}^{n} B \leq x) \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 \leq x)$
52	37 51	mpd	$⊢ (((φ \land x \in ℝ) \land \forall n \in Z \sum_{k = M}^{n} B \leq x) \land y \in ran (n \in Z ⟼ \sum_{k = M}^{n} B)) \to y \leq x$
53	52	ralrimiva	$⊢ ((φ \land x \in ℝ) \land \forall n \in Z \sum_{k = M}^{n} B \leq x) \to \forall y \in ran (n \in Z ⟼ \sum_{k = M}^{n} B) y \leq x$
54	53	ex	$⊢ (φ \land x \in ℝ) \to (\forall n \in Z \sum_{k = M}^{n} B \leq x \to \forall y \in ran (n \in Z ⟼ \sum_{k = M}^{n} B) y \leq x)$
55	54	ex	$⊢ φ \to (x \in ℝ \to (\forall n \in Z \sum_{k = M}^{n} B \leq x \to \forall y \in ran (n \in Z ⟼ \sum_{k = M}^{n} B) y \leq x))$
56	2 55	reximdai	$⊢ φ \to (\exists x \in ℝ \forall n \in Z \sum_{k = M}^{n} B \leq x \to \exists x \in ℝ \forall y \in ran (n \in Z ⟼ \sum_{k = M}^{n} B) y \leq x)$
57	6 56	mpd	$⊢ φ \to \exists x \in ℝ \forall y \in ran (n \in Z ⟼ \sum_{k = M}^{n} B) y \leq x$
58		supxrre	$⊢ (ran (n \in Z ⟼ \sum_{k = M}^{n} B) \subseteq ℝ \land ran (n \in Z ⟼ \sum_{k = M}^{n} B) \neq \emptyset \land \exists x \in ℝ \forall y \in ran (n \in Z ⟼ \sum_{k = M}^{n} B) y \leq x) \to sup (ran (n \in Z ⟼ \sum_{k = M}^{n} B) ℝ^{*} <) = sup (ran (n \in Z ⟼ \sum_{k = M}^{n} B) ℝ <)$
59	21 33 57 58	syl3anc	$⊢ φ \to sup (ran (n \in Z ⟼ \sum_{k = M}^{n} B) ℝ^{*} <) = sup (ran (n \in Z ⟼ \sum_{k = M}^{n} B) ℝ <)$
60	7 59	eqtrd	$⊢ φ \to sum^((k \in Z ⟼ B)) = sup (ran (n \in Z ⟼ \sum_{k = M}^{n} B) ℝ <)$

Metamath Proof Explorer

Theorem sge0reuzb

Proof