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	biimpi	$⊢ y \in ran (n \in Z ⟼ \sum_{k = M}^{n} B) \to \exists n \in Z y = \sum_{k = M}^{n} B$
38	37	adantl	$⊢ (((φ \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$
39		nfv	$⊢ Ⅎ n (φ \land x \in ℝ)$
40		nfra1	$⊢ Ⅎ n \forall n \in Z \sum_{k = M}^{n} B \leq x$
41	39 40	nfan	$⊢ Ⅎ n ((φ \land x \in ℝ) \land \forall n \in Z \sum_{k = M}^{n} B \leq x)$
42		nfv	$⊢ Ⅎ n y \leq x$
43		rspa	$⊢ (\forall n \in Z \sum_{k = M}^{n} B \leq x \land n \in Z) \to \sum_{k = M}^{n} B \leq x$
44		simpr	$⊢ (\sum_{k = M}^{n} B \leq x \land y = \sum_{k = M}^{n} B) \to y = \sum_{k = M}^{n} B$
45		simpl	$⊢ (\sum_{k = M}^{n} B \leq x \land y = \sum_{k = M}^{n} B) \to \sum_{k = M}^{n} B \leq x$
46	44 45	eqbrtrd	$⊢ (\sum_{k = M}^{n} B \leq x \land y = \sum_{k = M}^{n} B) \to y \leq x$
47	46	ex	$⊢ \sum_{k = M}^{n} B \leq x \to (y = \sum_{k = M}^{n} B \to y \leq x)$
48	43 47	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)$
49	48	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))$
50	49	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))$
51	41 42 50	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)$
52	51	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)$
53	38 52	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$
54	53	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$
55	54	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)$
56	55	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))$
57	2 56	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)$
58	6 57	mpd	$⊢ φ \to \exists x \in ℝ \forall y \in ran (n \in Z ⟼ \sum_{k = M}^{n} B) y \leq x$
59		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) ℝ <)$
60	21 33 58 59	syl3anc	$⊢ φ \to sup (ran (n \in Z ⟼ \sum_{k = M}^{n} B) ℝ^{*} <) = sup (ran (n \in Z ⟼ \sum_{k = M}^{n} B) ℝ <)$
61	7 60	eqtrd	$⊢ φ \to sum^((k \in Z ⟼ B)) = sup (ran (n \in Z ⟼ \sum_{k = M}^{n} B) ℝ <)$

Metamath Proof Explorer

Theorem sge0reuzb

Proof