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	ffvelrnda	$⊢ (φ \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	biimpi	$⊢ j \in Z \to j \in ℤ_{\geq M}$
47	46	adantl	$⊢ (φ \land j \in Z) \to j \in ℤ_{\geq M}$
48	7	recnd	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
49	41 42 48	syl2anc	$⊢ ((φ \land j \in Z) \land k \in (M \dots j)) \to F (k) \in ℂ$
50	44 47 49	fsumser	$⊢ (φ \land j \in Z) \to \sum_{k = M}^{j} F (k) = seq M (+ F) (j)$
51	50	3adant3	$⊢ (φ \land j \in Z \land G (j) = z) \to \sum_{k = M}^{j} F (k) = seq M (+ F) (j)$
52	40 51	eqtrd	$⊢ (φ \land j \in Z \land G (j) = z) \to sum^((k \in (M \dots j) ⟼ F (k))) = seq M (+ F) (j)$
53	4	eqcomi	$⊢ seq M (+ F) = G$
54	53	fveq1i	$⊢ seq M (+ F) (j) = G (j)$
55	54	a1i	$⊢ (φ \land j \in Z \land G (j) = z) \to seq M (+ F) (j) = G (j)$
56		simp3	$⊢ (φ \land j \in Z \land G (j) = z) \to G (j) = z$
57	52 55 56	3eqtrrd	$⊢ (φ \land j \in Z \land G (j) = z) \to z = sum^((k \in (M \dots j) ⟼ F (k)))$
58	3	feqmptd	$⊢ φ \to F = (k \in Z ⟼ F (k))$
59	58	fveq2d	$⊢ φ \to sum^(F) = sum^((k \in Z ⟼ F (k)))$
60	59	3ad2ant1	$⊢ (φ \land j \in Z \land G (j) = z) \to sum^(F) = sum^((k \in Z ⟼ F (k)))$
61	57 60	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))))$
62	36 61	mpbird	$⊢ (φ \land j \in Z \land G (j) = z) \to z \leq sum^(F)$
63	62	3exp	$⊢ φ \to (j \in Z \to (G (j) = z \to z \leq sum^(F)))$
64	63	adantr	$⊢ (φ \land z \in ran G) \to (j \in Z \to (G (j) = z \to z \leq sum^(F)))$
65	64	rexlimdv	$⊢ (φ \land z \in ran G) \to (\exists j \in Z G (j) = z \to z \leq sum^(F))$
66	29 65	mpd	$⊢ (φ \land z \in ran G) \to z \leq sum^(F)$
67	66	ralrimiva	$⊢ φ \to \forall z \in ran G z \leq sum^(F)$
68		nfv	$⊢ Ⅎ k ((φ \land z \in ℝ) \land z < sum^(F))$
69	18	a1i	$⊢ ((φ \land z \in ℝ) \land z < sum^(F)) \to Z \in V$
70	6	ad4ant14	$⊢ (((φ \land z \in ℝ) \land z < sum^(F)) \land k \in Z) \to F (k) \in [0, +∞)$
71		simplr	$⊢ ((φ \land z \in ℝ) \land z < sum^(F)) \to z \in ℝ$
72		simpr	$⊢ (φ \land z < sum^(F)) \to z < sum^(F)$
73	59	adantr	$⊢ (φ \land z < sum^(F)) \to sum^(F) = sum^((k \in Z ⟼ F (k)))$
74	72 73	breqtrd	$⊢ (φ \land z < sum^(F)) \to z < sum^((k \in Z ⟼ F (k)))$
75	74	adantlr	$⊢ ((φ \land z \in ℝ) \land z < sum^(F)) \to z < sum^((k \in Z ⟼ F (k)))$
76	68 69 70 71 75	sge0gtfsumgt	$⊢ ((φ \land z \in ℝ) \land z < sum^(F)) \to \exists w \in (𝒫 Z \cap Fin) z < \sum_{k \in w} F (k)$
77	1	3ad2ant1	$⊢ (φ \land w \in (𝒫 Z \cap Fin) \land z < \sum_{k \in w} F (k)) \to M \in ℤ$
78		elpwinss	$⊢ w \in (𝒫 Z \cap Fin) \to w \subseteq Z$
79	78	3ad2ant2	$⊢ (φ \land w \in (𝒫 Z \cap Fin) \land z < \sum_{k \in w} F (k)) \to w \subseteq Z$
80		elinel2	$⊢ w \in (𝒫 Z \cap Fin) \to w \in Fin$
81	80	3ad2ant2	$⊢ (φ \land w \in (𝒫 Z \cap Fin) \land z < \sum_{k \in w} F (k)) \to w \in Fin$
82	77 2 79 81	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)$
83	82	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)$
84		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 ℝ$
85	80	adantl	$⊢ (φ \land w \in (𝒫 Z \cap Fin)) \to w \in Fin$
86	58 7	fmpt3d	$⊢ φ \to F : Z ⟶ ℝ$
87	86	ad2antrr	$⊢ ((φ \land w \in (𝒫 Z \cap Fin)) \land k \in w) \to F : Z ⟶ ℝ$
88	78	sselda	$⊢ (w \in (𝒫 Z \cap Fin) \land k \in w) \to k \in Z$
89	88	adantll	$⊢ ((φ \land w \in (𝒫 Z \cap Fin)) \land k \in w) \to k \in Z$
90	87 89	ffvelrnd	$⊢ ((φ \land w \in (𝒫 Z \cap Fin)) \land k \in w) \to F (k) \in ℝ$
91	85 90	fsumrecl	$⊢ (φ \land w \in (𝒫 Z \cap Fin)) \to \sum_{k \in w} F (k) \in ℝ$
92	91	ad4ant13	$⊢ (((φ \land z \in ℝ) \land w \in (𝒫 Z \cap Fin)) \land w \subseteq (M \dots j)) \to \sum_{k \in w} F (k) \in ℝ$
93	92	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 ℝ$
94	32 7	sylan2	$⊢ (φ \land k \in (M \dots j)) \to F (k) \in ℝ$
95	37 94	fsumrecl	$⊢ φ \to \sum_{k = M}^{j} F (k) \in ℝ$
96	95	ad3antrrr	$⊢ (((φ \land z \in ℝ) \land w \in (𝒫 Z \cap Fin)) \land w \subseteq (M \dots j)) \to \sum_{k = M}^{j} F (k) \in ℝ$
97	96	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 ℝ$
98		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)$
99	37	adantr	$⊢ (φ \land w \subseteq (M \dots j)) \to (M \dots j) \in Fin$
100	94	adantlr	$⊢ ((φ \land w \subseteq (M \dots j)) \land k \in (M \dots j)) \to F (k) \in ℝ$
101		0xr	$⊢ 0 \in ℝ^{*}$
102	101	a1i	$⊢ (φ \land k \in Z) \to 0 \in ℝ^{*}$
103		pnfxr	$⊢ +∞ \in ℝ^{*}$
104	103	a1i	$⊢ (φ \land k \in Z) \to +∞ \in ℝ^{*}$
105		icogelb	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land F (k) \in [0, +∞)) \to 0 \leq F (k)$
106	102 104 6 105	syl3anc	$⊢ (φ \land k \in Z) \to 0 \leq F (k)$
107	32 106	sylan2	$⊢ (φ \land k \in (M \dots j)) \to 0 \leq F (k)$
108	107	adantlr	$⊢ ((φ \land w \subseteq (M \dots j)) \land k \in (M \dots j)) \to 0 \leq F (k)$
109		simpr	$⊢ (φ \land w \subseteq (M \dots j)) \to w \subseteq (M \dots j)$
110	99 100 108 109	fsumless	$⊢ (φ \land w \subseteq (M \dots j)) \to \sum_{k \in w} F (k) \leq \sum_{k = M}^{j} F (k)$
111	110	adantlr	$⊢ ((φ \land z \in ℝ) \land w \subseteq (M \dots j)) \to \sum_{k \in w} F (k) \leq \sum_{k = M}^{j} F (k)$
112	111	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)$
113	84 93 97 98 112	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)$
114	113	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))$
115	114	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))$
116	83 115	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)$
117	116	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)))$
118	117	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)))$
119	118	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))$
120	76 119	mpd	$⊢ ((φ \land z \in ℝ) \land z < sum^(F)) \to \exists j \in Z z < \sum_{k = M}^{j} F (k)$
121	10	ffnd	$⊢ φ \to seq M (+ F) Fn Z$
122	121	adantr	$⊢ (φ \land j \in Z) \to seq M (+ F) Fn Z$
123	47 45	sylibr	$⊢ (φ \land j \in Z) \to j \in Z$
124		fnfvelrn	$⊢ (seq M (+ F) Fn Z \land j \in Z) \to seq M (+ F) (j) \in ran seq M (+ F)$
125	122 123 124	syl2anc	$⊢ (φ \land j \in Z) \to seq M (+ F) (j) \in ran seq M (+ F)$
126	4	a1i	$⊢ (φ \land j \in Z) \to G = seq M (+ F)$
127	126	rneqd	$⊢ (φ \land j \in Z) \to ran G = ran seq M (+ F)$
128	50 127	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))$
129	125 128	mpbird	$⊢ (φ \land j \in Z) \to \sum_{k = M}^{j} F (k) \in ran G$
130	129	adantlr	$⊢ ((φ \land z \in ℝ) \land j \in Z) \to \sum_{k = M}^{j} F (k) \in ran G$
131	130	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$
132		simp3	$⊢ ((φ \land z \in ℝ) \land j \in Z \land z < \sum_{k = M}^{j} F (k)) \to z < \sum_{k = M}^{j} F (k)$
133		breq2	$⊢ y = \sum_{k = M}^{j} F (k) \to (z < y \leftrightarrow z < \sum_{k = M}^{j} F (k))$
134	133	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$
135	131 132 134	syl2anc	$⊢ ((φ \land z \in ℝ) \land j \in Z \land z < \sum_{k = M}^{j} F (k)) \to \exists y \in ran G z < y$
136	135	3exp	$⊢ (φ \land z \in ℝ) \to (j \in Z \to (z < \sum_{k = M}^{j} F (k) \to \exists y \in ran G z < y))$
137	136	rexlimdv	$⊢ (φ \land z \in ℝ) \to (\exists j \in Z z < \sum_{k = M}^{j} F (k) \to \exists y \in ran G z < y)$
138	137	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)$
139	120 138	mpd	$⊢ ((φ \land z \in ℝ) \land z < sum^(F)) \to \exists y \in ran G z < y$
140	139	ex	$⊢ (φ \land z \in ℝ) \to (z < sum^(F) \to \exists y \in ran G z < y)$
141	140	ralrimiva	$⊢ φ \to \forall z \in ℝ (z < sum^(F) \to \exists y \in ran G z < y)$
142		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)$
143	17 23 67 141 142	syl22anc	$⊢ φ \to sup (ran G ℝ^{*} <) = sum^(F)$
144	143	eqcomd	$⊢ φ \to sum^(F) = sup (ran G ℝ^{*} <)$

Metamath Proof Explorer

Theorem sge0seq

Proof