sge0seq

Description: A series of nonnegative reals agrees with the generalized sum of nonnegative reals. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	sge0seq.m	$⊢ φ \to M \in ℤ$
	sge0seq.z	$⊢ Z = ℤ_{\geq M}$
	sge0seq.f	$⊢ φ \to F : Z ⟶ [0, +∞)$
	sge0seq.g	$⊢ G = seq M (+ F)$
Assertion	sge0seq	$⊢ φ \to sum^(F) = sup (ran G ℝ^{*} <)$

Proof

Step	Hyp	Ref	Expression
1		sge0seq.m	$⊢ φ \to M \in ℤ$
2		sge0seq.z	$⊢ Z = ℤ_{\geq M}$
3		sge0seq.f	$⊢ φ \to F : Z ⟶ [0, +∞)$
4		sge0seq.g	$⊢ G = seq M (+ F)$
5		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
6	3	ffvelcdmda	$⊢ (φ \land k \in Z) \to F (k) \in [0, +∞)$
7	5 6	sselid	$⊢ (φ \land k \in Z) \to F (k) \in ℝ$
8		readdcl	$⊢ (k \in ℝ \land i \in ℝ) \to k + i \in ℝ$
9	8	adantl	$⊢ (φ \land (k \in ℝ \land i \in ℝ)) \to k + i \in ℝ$
10	2 1 7 9	seqf	$⊢ φ \to seq M (+ F) : Z ⟶ ℝ$
11	4	a1i	$⊢ φ \to G = seq M (+ F)$
12	11	feq1d	$⊢ φ \to (G : Z ⟶ ℝ \leftrightarrow seq M (+ F) : Z ⟶ ℝ)$
13	10 12	mpbird	$⊢ φ \to G : Z ⟶ ℝ$
14	13	frnd	$⊢ φ \to ran G \subseteq ℝ$
15		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
16	15	a1i	$⊢ φ \to ℝ \subseteq ℝ^{*}$
17	14 16	sstrd	$⊢ φ \to ran G \subseteq ℝ^{*}$
18	2	fvexi	$⊢ Z \in V$
19	18	a1i	$⊢ φ \to Z \in V$
20		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
21	20	a1i	$⊢ φ \to [0, +∞) \subseteq [0, +∞]$
22	3 21	fssd	$⊢ φ \to F : Z ⟶ [0, +∞]$
23	19 22	sge0xrcl	$⊢ φ \to sum^(F) \in ℝ^{*}$
24		simpr	$⊢ (φ \land z \in ran G) \to z \in ran G$
25	13	ffnd	$⊢ φ \to G Fn Z$
26		fvelrnb	$⊢ G Fn Z \to (z \in ran G \leftrightarrow \exists j \in Z G (j) = z)$
27	25 26	syl	$⊢ φ \to (z \in ran G \leftrightarrow \exists j \in Z G (j) = z)$
28	27	adantr	$⊢ (φ \land z \in ran G) \to (z \in ran G \leftrightarrow \exists j \in Z G (j) = z)$
29	24 28	mpbid	$⊢ (φ \land z \in ran G) \to \exists j \in Z G (j) = z$
30	20 6	sselid	$⊢ (φ \land k \in Z) \to F (k) \in [0, +∞]$
31		elfzuz	$⊢ k \in (M \dots j) \to k \in ℤ_{\geq M}$
32	31 2	eleqtrrdi	$⊢ k \in (M \dots j) \to k \in Z$
33	32	ssriv	$⊢ (M \dots j) \subseteq Z$
34	33	a1i	$⊢ φ \to (M \dots j) \subseteq Z$
35	19 30 34	sge0lessmpt	$⊢ φ \to sum^((k \in (M \dots j) ⟼ F (k))) \leq sum^((k \in Z ⟼ F (k)))$
36	35	3ad2ant1	$⊢ (φ \land j \in Z \land G (j) = z) \to sum^((k \in (M \dots j) ⟼ F (k))) \leq sum^((k \in Z ⟼ F (k)))$
37		fzfid	$⊢ φ \to (M \dots j) \in Fin$
38	32 6	sylan2	$⊢ (φ \land k \in (M \dots j)) \to F (k) \in [0, +∞)$
39	37 38	sge0fsummpt	$⊢ φ \to sum^((k \in (M \dots j) ⟼ F (k))) = \sum_{k = M}^{j} F (k)$
40	39	3ad2ant1	$⊢ (φ \land j \in Z \land G (j) = z) \to sum^((k \in (M \dots j) ⟼ F (k))) = \sum_{k = M}^{j} F (k)$
41		simpll	$⊢ ((φ \land j \in Z) \land k \in (M \dots j)) \to φ$
42	32	adantl	$⊢ ((φ \land j \in Z) \land k \in (M \dots j)) \to k \in Z$
43		eqidd	$⊢ (φ \land k \in Z) \to F (k) = F (k)$
44	41 42 43	syl2anc	$⊢ ((φ \land j \in Z) \land k \in (M \dots j)) \to F (k) = F (k)$
45	2	eleq2i	$⊢ j \in Z \leftrightarrow j \in ℤ_{\geq M}$
46	45	bilani	$⊢ (φ \land j \in Z) \to j \in ℤ_{\geq M}$
47	7	recnd	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
48	41 42 47	syl2anc	$⊢ ((φ \land j \in Z) \land k \in (M \dots j)) \to F (k) \in ℂ$
49	44 46 48	fsumser	$⊢ (φ \land j \in Z) \to \sum_{k = M}^{j} F (k) = seq M (+ F) (j)$
50	49	3adant3	$⊢ (φ \land j \in Z \land G (j) = z) \to \sum_{k = M}^{j} F (k) = seq M (+ F) (j)$
51	40 50	eqtrd	$⊢ (φ \land j \in Z \land G (j) = z) \to sum^((k \in (M \dots j) ⟼ F (k))) = seq M (+ F) (j)$
52	4	eqcomi	$⊢ seq M (+ F) = G$
53	52	fveq1i	$⊢ seq M (+ F) (j) = G (j)$
54	53	a1i	$⊢ (φ \land j \in Z \land G (j) = z) \to seq M (+ F) (j) = G (j)$
55		simp3	$⊢ (φ \land j \in Z \land G (j) = z) \to G (j) = z$
56	51 54 55	3eqtrrd	$⊢ (φ \land j \in Z \land G (j) = z) \to z = sum^((k \in (M \dots j) ⟼ F (k)))$
57	3	feqmptd	$⊢ φ \to F = (k \in Z ⟼ F (k))$
58	57	fveq2d	$⊢ φ \to sum^(F) = sum^((k \in Z ⟼ F (k)))$
59	58	3ad2ant1	$⊢ (φ \land j \in Z \land G (j) = z) \to sum^(F) = sum^((k \in Z ⟼ F (k)))$
60	56 59	breq12d	$⊢ (φ \land j \in Z \land G (j) = z) \to (z \leq sum^(F) \leftrightarrow sum^((k \in (M \dots j) ⟼ F (k))) \leq sum^((k \in Z ⟼ F (k))))$
61	36 60	mpbird	$⊢ (φ \land j \in Z \land G (j) = z) \to z \leq sum^(F)$
62	61	3exp	$⊢ φ \to (j \in Z \to (G (j) = z \to z \leq sum^(F)))$
63	62	adantr	$⊢ (φ \land z \in ran G) \to (j \in Z \to (G (j) = z \to z \leq sum^(F)))$
64	63	rexlimdv	$⊢ (φ \land z \in ran G) \to (\exists j \in Z G (j) = z \to z \leq sum^(F))$
65	29 64	mpd	$⊢ (φ \land z \in ran G) \to z \leq sum^(F)$
66	65	ralrimiva	$⊢ φ \to \forall z \in ran G z \leq sum^(F)$
67		nfv	$⊢ Ⅎ k ((φ \land z \in ℝ) \land z < sum^(F))$
68	18	a1i	$⊢ ((φ \land z \in ℝ) \land z < sum^(F)) \to Z \in V$
69	6	ad4ant14	$⊢ (((φ \land z \in ℝ) \land z < sum^(F)) \land k \in Z) \to F (k) \in [0, +∞)$
70		simplr	$⊢ ((φ \land z \in ℝ) \land z < sum^(F)) \to z \in ℝ$
71		simpr	$⊢ (φ \land z < sum^(F)) \to z < sum^(F)$
72	58	adantr	$⊢ (φ \land z < sum^(F)) \to sum^(F) = sum^((k \in Z ⟼ F (k)))$
73	71 72	breqtrd	$⊢ (φ \land z < sum^(F)) \to z < sum^((k \in Z ⟼ F (k)))$
74	73	adantlr	$⊢ ((φ \land z \in ℝ) \land z < sum^(F)) \to z < sum^((k \in Z ⟼ F (k)))$
75	67 68 69 70 74	sge0gtfsumgt	$⊢ ((φ \land z \in ℝ) \land z < sum^(F)) \to \exists w \in (𝒫 Z \cap Fin) z < \sum_{k \in w} F (k)$
76	1	3ad2ant1	$⊢ (φ \land w \in (𝒫 Z \cap Fin) \land z < \sum_{k \in w} F (k)) \to M \in ℤ$
77		elpwinss	$⊢ w \in (𝒫 Z \cap Fin) \to w \subseteq Z$
78	77	3ad2ant2	$⊢ (φ \land w \in (𝒫 Z \cap Fin) \land z < \sum_{k \in w} F (k)) \to w \subseteq Z$
79		elinel2	$⊢ w \in (𝒫 Z \cap Fin) \to w \in Fin$
80	79	3ad2ant2	$⊢ (φ \land w \in (𝒫 Z \cap Fin) \land z < \sum_{k \in w} F (k)) \to w \in Fin$
81	76 2 78 80	uzfissfz	$⊢ (φ \land w \in (𝒫 Z \cap Fin) \land z < \sum_{k \in w} F (k)) \to \exists j \in Z w \subseteq (M \dots j)$
82	81	3adant1r	$⊢ ((φ \land z \in ℝ) \land w \in (𝒫 Z \cap Fin) \land z < \sum_{k \in w} F (k)) \to \exists j \in Z w \subseteq (M \dots j)$
83		simpl1r	$⊢ (((φ \land z \in ℝ) \land w \in (𝒫 Z \cap Fin) \land z < \sum_{k \in w} F (k)) \land w \subseteq (M \dots j)) \to z \in ℝ$
84	79	adantl	$⊢ (φ \land w \in (𝒫 Z \cap Fin)) \to w \in Fin$
85	57 7	fmpt3d	$⊢ φ \to F : Z ⟶ ℝ$
86	85	ad2antrr	$⊢ ((φ \land w \in (𝒫 Z \cap Fin)) \land k \in w) \to F : Z ⟶ ℝ$
87	77	sselda	$⊢ (w \in (𝒫 Z \cap Fin) \land k \in w) \to k \in Z$
88	87	adantll	$⊢ ((φ \land w \in (𝒫 Z \cap Fin)) \land k \in w) \to k \in Z$
89	86 88	ffvelcdmd	$⊢ ((φ \land w \in (𝒫 Z \cap Fin)) \land k \in w) \to F (k) \in ℝ$
90	84 89	fsumrecl	$⊢ (φ \land w \in (𝒫 Z \cap Fin)) \to \sum_{k \in w} F (k) \in ℝ$
91	90	ad4ant13	$⊢ (((φ \land z \in ℝ) \land w \in (𝒫 Z \cap Fin)) \land w \subseteq (M \dots j)) \to \sum_{k \in w} F (k) \in ℝ$
92	91	3adantl3	$⊢ (((φ \land z \in ℝ) \land w \in (𝒫 Z \cap Fin) \land z < \sum_{k \in w} F (k)) \land w \subseteq (M \dots j)) \to \sum_{k \in w} F (k) \in ℝ$
93	32 7	sylan2	$⊢ (φ \land k \in (M \dots j)) \to F (k) \in ℝ$
94	37 93	fsumrecl	$⊢ φ \to \sum_{k = M}^{j} F (k) \in ℝ$
95	94	ad3antrrr	$⊢ (((φ \land z \in ℝ) \land w \in (𝒫 Z \cap Fin)) \land w \subseteq (M \dots j)) \to \sum_{k = M}^{j} F (k) \in ℝ$
96	95	3adantl3	$⊢ (((φ \land z \in ℝ) \land w \in (𝒫 Z \cap Fin) \land z < \sum_{k \in w} F (k)) \land w \subseteq (M \dots j)) \to \sum_{k = M}^{j} F (k) \in ℝ$
97		simpl3	$⊢ (((φ \land z \in ℝ) \land w \in (𝒫 Z \cap Fin) \land z < \sum_{k \in w} F (k)) \land w \subseteq (M \dots j)) \to z < \sum_{k \in w} F (k)$
98	37	adantr	$⊢ (φ \land w \subseteq (M \dots j)) \to (M \dots j) \in Fin$
99	93	adantlr	$⊢ ((φ \land w \subseteq (M \dots j)) \land k \in (M \dots j)) \to F (k) \in ℝ$
100		0xr	$⊢ 0 \in ℝ^{*}$
101	100	a1i	$⊢ (φ \land k \in Z) \to 0 \in ℝ^{*}$
102		pnfxr	$⊢ +∞ \in ℝ^{*}$
103	102	a1i	$⊢ (φ \land k \in Z) \to +∞ \in ℝ^{*}$
104		icogelb	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land F (k) \in [0, +∞)) \to 0 \leq F (k)$
105	101 103 6 104	syl3anc	$⊢ (φ \land k \in Z) \to 0 \leq F (k)$
106	32 105	sylan2	$⊢ (φ \land k \in (M \dots j)) \to 0 \leq F (k)$
107	106	adantlr	$⊢ ((φ \land w \subseteq (M \dots j)) \land k \in (M \dots j)) \to 0 \leq F (k)$
108		simpr	$⊢ (φ \land w \subseteq (M \dots j)) \to w \subseteq (M \dots j)$
109	98 99 107 108	fsumless	$⊢ (φ \land w \subseteq (M \dots j)) \to \sum_{k \in w} F (k) \leq \sum_{k = M}^{j} F (k)$
110	109	adantlr	$⊢ ((φ \land z \in ℝ) \land w \subseteq (M \dots j)) \to \sum_{k \in w} F (k) \leq \sum_{k = M}^{j} F (k)$
111	110	3ad2antl1	$⊢ (((φ \land z \in ℝ) \land w \in (𝒫 Z \cap Fin) \land z < \sum_{k \in w} F (k)) \land w \subseteq (M \dots j)) \to \sum_{k \in w} F (k) \leq \sum_{k = M}^{j} F (k)$
112	83 92 96 97 111	ltletrd	$⊢ (((φ \land z \in ℝ) \land w \in (𝒫 Z \cap Fin) \land z < \sum_{k \in w} F (k)) \land w \subseteq (M \dots j)) \to z < \sum_{k = M}^{j} F (k)$
113	112	ex	$⊢ ((φ \land z \in ℝ) \land w \in (𝒫 Z \cap Fin) \land z < \sum_{k \in w} F (k)) \to (w \subseteq (M \dots j) \to z < \sum_{k = M}^{j} F (k))$
114	113	reximdv	$⊢ ((φ \land z \in ℝ) \land w \in (𝒫 Z \cap Fin) \land z < \sum_{k \in w} F (k)) \to (\exists j \in Z w \subseteq (M \dots j) \to \exists j \in Z z < \sum_{k = M}^{j} F (k))$
115	82 114	mpd	$⊢ ((φ \land z \in ℝ) \land w \in (𝒫 Z \cap Fin) \land z < \sum_{k \in w} F (k)) \to \exists j \in Z z < \sum_{k = M}^{j} F (k)$
116	115	3exp	$⊢ (φ \land z \in ℝ) \to (w \in (𝒫 Z \cap Fin) \to (z < \sum_{k \in w} F (k) \to \exists j \in Z z < \sum_{k = M}^{j} F (k)))$
117	116	adantr	$⊢ ((φ \land z \in ℝ) \land z < sum^(F)) \to (w \in (𝒫 Z \cap Fin) \to (z < \sum_{k \in w} F (k) \to \exists j \in Z z < \sum_{k = M}^{j} F (k)))$
118	117	rexlimdv	$⊢ ((φ \land z \in ℝ) \land z < sum^(F)) \to (\exists w \in (𝒫 Z \cap Fin) z < \sum_{k \in w} F (k) \to \exists j \in Z z < \sum_{k = M}^{j} F (k))$
119	75 118	mpd	$⊢ ((φ \land z \in ℝ) \land z < sum^(F)) \to \exists j \in Z z < \sum_{k = M}^{j} F (k)$
120	10	ffnd	$⊢ φ \to seq M (+ F) Fn Z$
121	120	adantr	$⊢ (φ \land j \in Z) \to seq M (+ F) Fn Z$
122	46 45	sylibr	$⊢ (φ \land j \in Z) \to j \in Z$
123		fnfvelrn	$⊢ (seq M (+ F) Fn Z \land j \in Z) \to seq M (+ F) (j) \in ran seq M (+ F)$
124	121 122 123	syl2anc	$⊢ (φ \land j \in Z) \to seq M (+ F) (j) \in ran seq M (+ F)$
125	4	a1i	$⊢ (φ \land j \in Z) \to G = seq M (+ F)$
126	125	rneqd	$⊢ (φ \land j \in Z) \to ran G = ran seq M (+ F)$
127	49 126	eleq12d	$⊢ (φ \land j \in Z) \to (\sum_{k = M}^{j} F (k) \in ran G \leftrightarrow seq M (+ F) (j) \in ran seq M (+ F))$
128	124 127	mpbird	$⊢ (φ \land j \in Z) \to \sum_{k = M}^{j} F (k) \in ran G$
129	128	adantlr	$⊢ ((φ \land z \in ℝ) \land j \in Z) \to \sum_{k = M}^{j} F (k) \in ran G$
130	129	3adant3	$⊢ ((φ \land z \in ℝ) \land j \in Z \land z < \sum_{k = M}^{j} F (k)) \to \sum_{k = M}^{j} F (k) \in ran G$
131		simp3	$⊢ ((φ \land z \in ℝ) \land j \in Z \land z < \sum_{k = M}^{j} F (k)) \to z < \sum_{k = M}^{j} F (k)$
132		breq2	$⊢ y = \sum_{k = M}^{j} F (k) \to (z < y \leftrightarrow z < \sum_{k = M}^{j} F (k))$
133	132	rspcev	$⊢ (\sum_{k = M}^{j} F (k) \in ran G \land z < \sum_{k = M}^{j} F (k)) \to \exists y \in ran G z < y$
134	130 131 133	syl2anc	$⊢ ((φ \land z \in ℝ) \land j \in Z \land z < \sum_{k = M}^{j} F (k)) \to \exists y \in ran G z < y$
135	134	3exp	$⊢ (φ \land z \in ℝ) \to (j \in Z \to (z < \sum_{k = M}^{j} F (k) \to \exists y \in ran G z < y))$
136	135	rexlimdv	$⊢ (φ \land z \in ℝ) \to (\exists j \in Z z < \sum_{k = M}^{j} F (k) \to \exists y \in ran G z < y)$
137	136	adantr	$⊢ ((φ \land z \in ℝ) \land z < sum^(F)) \to (\exists j \in Z z < \sum_{k = M}^{j} F (k) \to \exists y \in ran G z < y)$
138	119 137	mpd	$⊢ ((φ \land z \in ℝ) \land z < sum^(F)) \to \exists y \in ran G z < y$
139	138	ex	$⊢ (φ \land z \in ℝ) \to (z < sum^(F) \to \exists y \in ran G z < y)$
140	139	ralrimiva	$⊢ φ \to \forall z \in ℝ (z < sum^(F) \to \exists y \in ran G z < y)$
141		supxr2	$⊢ ((ran G \subseteq ℝ^{} \land sum^(F) \in ℝ^{}) \land (\forall z \in ran G z \leq sum^(F) \land \forall z \in ℝ (z < sum^(F) \to \exists y \in ran G z < y))) \to sup (ran G ℝ^{*} <) = sum^(F)$
142	17 23 66 140 141	syl22anc	$⊢ φ \to sup (ran G ℝ^{*} <) = sum^(F)$
143	142	eqcomd	$⊢ φ \to sum^(F) = sup (ran G ℝ^{*} <)$

Metamath Proof Explorer

Theorem sge0seq

Proof