sge0isum

Description: If a series of nonnegative reals is convergent, then it agrees with the generalized sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	sge0isum.m	$⊢ φ \to M \in ℤ$
	sge0isum.z	$⊢ Z = ℤ_{\geq M}$
	sge0isum.f	$⊢ φ \to F : Z ⟶ [0, +∞)$
	sge0isum.g	$⊢ G = seq M (+ F)$
	sge0isum.gcnv	$⊢ φ \to G ⇝ B$
Assertion	sge0isum	$⊢ φ \to sum^(F) = B$

Proof

Step	Hyp	Ref	Expression
1		sge0isum.m	$⊢ φ \to M \in ℤ$
2		sge0isum.z	$⊢ Z = ℤ_{\geq M}$
3		sge0isum.f	$⊢ φ \to F : Z ⟶ [0, +∞)$
4		sge0isum.g	$⊢ G = seq M (+ F)$
5		sge0isum.gcnv	$⊢ φ \to G ⇝ B$
6	2	fvexi	$⊢ Z \in V$
7	6	a1i	$⊢ φ \to Z \in V$
8		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
9	8	a1i	$⊢ φ \to [0, +∞) \subseteq [0, +∞]$
10	3 9	fssd	$⊢ φ \to F : Z ⟶ [0, +∞]$
11	7 10	sge0xrcl	$⊢ φ \to sum^(F) \in ℝ^{*}$
12		eqidd	$⊢ (φ \land k \in Z) \to F (k) = F (k)$
13		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
14	3	ffvelcdmda	$⊢ (φ \land k \in Z) \to F (k) \in [0, +∞)$
15	13 14	sselid	$⊢ (φ \land k \in Z) \to F (k) \in ℝ$
16		0xr	$⊢ 0 \in ℝ^{*}$
17	16	a1i	$⊢ (φ \land k \in Z) \to 0 \in ℝ^{*}$
18		pnfxr	$⊢ +∞ \in ℝ^{*}$
19	18	a1i	$⊢ (φ \land k \in Z) \to +∞ \in ℝ^{*}$
20		icogelb	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land F (k) \in [0, +∞)) \to 0 \leq F (k)$
21	17 19 14 20	syl3anc	$⊢ (φ \land k \in Z) \to 0 \leq F (k)$
22		seqex	$⊢ seq M (+ F) \in V$
23	4 22	eqeltri	$⊢ G \in V$
24	23	a1i	$⊢ φ \to G \in V$
25		climcl	$⊢ G ⇝ B \to B \in ℂ$
26	5 25	syl	$⊢ φ \to B \in ℂ$
27		breldmg	$⊢ (G \in V \land B \in ℂ \land G ⇝ B) \to G \in dom ⇝$
28	24 26 5 27	syl3anc	$⊢ φ \to G \in dom ⇝$
29	4	a1i	$⊢ (φ \land j \in Z) \to G = seq M (+ F)$
30	29	fveq1d	$⊢ (φ \land j \in Z) \to G (j) = seq M (+ F) (j)$
31	2	eleq2i	$⊢ j \in Z \leftrightarrow j \in ℤ_{\geq M}$
32	31	bilani	$⊢ (φ \land j \in Z) \to j \in ℤ_{\geq M}$
33		simpll	$⊢ ((φ \land j \in Z) \land k \in (M \dots j)) \to φ$
34		elfzuz	$⊢ k \in (M \dots j) \to k \in ℤ_{\geq M}$
35	34 2	eleqtrrdi	$⊢ k \in (M \dots j) \to k \in Z$
36	35	adantl	$⊢ ((φ \land j \in Z) \land k \in (M \dots j)) \to k \in Z$
37	33 36 15	syl2anc	$⊢ ((φ \land j \in Z) \land k \in (M \dots j)) \to F (k) \in ℝ$
38		readdcl	$⊢ (k \in ℝ \land i \in ℝ) \to k + i \in ℝ$
39	38	adantl	$⊢ ((φ \land j \in Z) \land (k \in ℝ \land i \in ℝ)) \to k + i \in ℝ$
40	32 37 39	seqcl	$⊢ (φ \land j \in Z) \to seq M (+ F) (j) \in ℝ$
41	30 40	eqeltrd	$⊢ (φ \land j \in Z) \to G (j) \in ℝ$
42	41	recnd	$⊢ (φ \land j \in Z) \to G (j) \in ℂ$
43	42	ralrimiva	$⊢ φ \to \forall j \in Z G (j) \in ℂ$
44	2	climbdd	$⊢ (M \in ℤ \land G \in dom ⇝ \land \forall j \in Z G (j) \in ℂ) \to \exists x \in ℝ \forall j \in Z \|G (j)\| \leq x$
45	1 28 43 44	syl3anc	$⊢ φ \to \exists x \in ℝ \forall j \in Z \|G (j)\| \leq x$
46	41	ad4ant13	$⊢ (((φ \land x \in ℝ) \land j \in Z) \land \|G (j)\| \leq x) \to G (j) \in ℝ$
47	42	ad4ant13	$⊢ (((φ \land x \in ℝ) \land j \in Z) \land \|G (j)\| \leq x) \to G (j) \in ℂ$
48	47	abscld	$⊢ (((φ \land x \in ℝ) \land j \in Z) \land \|G (j)\| \leq x) \to \|G (j)\| \in ℝ$
49		simpllr	$⊢ (((φ \land x \in ℝ) \land j \in Z) \land \|G (j)\| \leq x) \to x \in ℝ$
50	46	leabsd	$⊢ (((φ \land x \in ℝ) \land j \in Z) \land \|G (j)\| \leq x) \to G (j) \leq \|G (j)\|$
51		simpr	$⊢ (((φ \land x \in ℝ) \land j \in Z) \land \|G (j)\| \leq x) \to \|G (j)\| \leq x$
52	46 48 49 50 51	letrd	$⊢ (((φ \land x \in ℝ) \land j \in Z) \land \|G (j)\| \leq x) \to G (j) \leq x$
53	52	ex	$⊢ ((φ \land x \in ℝ) \land j \in Z) \to (\|G (j)\| \leq x \to G (j) \leq x)$
54	53	ralimdva	$⊢ (φ \land x \in ℝ) \to (\forall j \in Z \|G (j)\| \leq x \to \forall j \in Z G (j) \leq x)$
55	54	reximdva	$⊢ φ \to (\exists x \in ℝ \forall j \in Z \|G (j)\| \leq x \to \exists x \in ℝ \forall j \in Z G (j) \leq x)$
56	45 55	mpd	$⊢ φ \to \exists x \in ℝ \forall j \in Z G (j) \leq x$
57	2 4 1 12 15 21 56	isumsup2	$⊢ φ \to G ⇝ sup (ran G ℝ <)$
58	2 1 57 41	climrecl	$⊢ φ \to sup (ran G ℝ <) \in ℝ$
59	58	rexrd	$⊢ φ \to sup (ran G ℝ <) \in ℝ^{*}$
60	3	feqmptd	$⊢ φ \to F = (k \in Z ⟼ F (k))$
61	60	fveq2d	$⊢ φ \to sum^(F) = sum^((k \in Z ⟼ F (k)))$
62		mpteq1	$⊢ y = \emptyset \to (k \in y ⟼ F (k)) = (k \in \emptyset ⟼ F (k))$
63	62	fveq2d	$⊢ y = \emptyset \to sum^((k \in y ⟼ F (k))) = sum^((k \in \emptyset ⟼ F (k)))$
64		mpt0	$⊢ (k \in \emptyset ⟼ F (k)) = \emptyset$
65	64	fveq2i	$⊢ sum^((k \in \emptyset ⟼ F (k))) = sum^(\emptyset)$
66		sge00	$⊢ sum^(\emptyset) = 0$
67	65 66	eqtri	$⊢ sum^((k \in \emptyset ⟼ F (k))) = 0$
68	67	a1i	$⊢ y = \emptyset \to sum^((k \in \emptyset ⟼ F (k))) = 0$
69	63 68	eqtrd	$⊢ y = \emptyset \to sum^((k \in y ⟼ F (k))) = 0$
70	69	adantl	$⊢ ((φ \land y \in (𝒫 Z \cap Fin)) \land y = \emptyset) \to sum^((k \in y ⟼ F (k))) = 0$
71		0red	$⊢ φ \to 0 \in ℝ$
72	38	adantl	$⊢ (φ \land (k \in ℝ \land i \in ℝ)) \to k + i \in ℝ$
73	2 1 15 72	seqf	$⊢ φ \to seq M (+ F) : Z ⟶ ℝ$
74	4	a1i	$⊢ φ \to G = seq M (+ F)$
75	74	feq1d	$⊢ φ \to (G : Z ⟶ ℝ \leftrightarrow seq M (+ F) : Z ⟶ ℝ)$
76	73 75	mpbird	$⊢ φ \to G : Z ⟶ ℝ$
77	76	frnd	$⊢ φ \to ran G \subseteq ℝ$
78	76	ffund	$⊢ φ \to Fun G$
79		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
80	1 79	syl	$⊢ φ \to M \in ℤ_{\geq M}$
81	2	eqcomi	$⊢ ℤ_{\geq M} = Z$
82	80 81	eleqtrdi	$⊢ φ \to M \in Z$
83	76	fdmd	$⊢ φ \to dom G = Z$
84	83	eqcomd	$⊢ φ \to Z = dom G$
85	82 84	eleqtrd	$⊢ φ \to M \in dom G$
86		fvelrn	$⊢ (Fun G \land M \in dom G) \to G (M) \in ran G$
87	78 85 86	syl2anc	$⊢ φ \to G (M) \in ran G$
88	77 87	sseldd	$⊢ φ \to G (M) \in ℝ$
89	16	a1i	$⊢ φ \to 0 \in ℝ^{*}$
90	18	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
91	3 82	ffvelcdmd	$⊢ φ \to F (M) \in [0, +∞)$
92		icogelb	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land F (M) \in [0, +∞)) \to 0 \leq F (M)$
93	89 90 91 92	syl3anc	$⊢ φ \to 0 \leq F (M)$
94	4	fveq1i	$⊢ G (M) = seq M (+ F) (M)$
95	94	a1i	$⊢ φ \to G (M) = seq M (+ F) (M)$
96		seq1	$⊢ M \in ℤ \to seq M (+ F) (M) = F (M)$
97	1 96	syl	$⊢ φ \to seq M (+ F) (M) = F (M)$
98	95 97	eqtr2d	$⊢ φ \to F (M) = G (M)$
99	93 98	breqtrd	$⊢ φ \to 0 \leq G (M)$
100	87	ne0d	$⊢ φ \to ran G \neq \emptyset$
101		simpr	$⊢ (φ \land z \in ran G) \to z \in ran G$
102	76	ffnd	$⊢ φ \to G Fn Z$
103		fvelrnb	$⊢ G Fn Z \to (z \in ran G \leftrightarrow \exists j \in Z G (j) = z)$
104	102 103	syl	$⊢ φ \to (z \in ran G \leftrightarrow \exists j \in Z G (j) = z)$
105	104	adantr	$⊢ (φ \land z \in ran G) \to (z \in ran G \leftrightarrow \exists j \in Z G (j) = z)$
106	101 105	mpbid	$⊢ (φ \land z \in ran G) \to \exists j \in Z G (j) = z$
107	106	adantlr	$⊢ ((φ \land \forall j \in Z G (j) \leq x) \land z \in ran G) \to \exists j \in Z G (j) = z$
108		nfv	$⊢ Ⅎ j φ$
109		nfra1	$⊢ Ⅎ j \forall j \in Z G (j) \leq x$
110	108 109	nfan	$⊢ Ⅎ j (φ \land \forall j \in Z G (j) \leq x)$
111		nfv	$⊢ Ⅎ j z \in ran G$
112	110 111	nfan	$⊢ Ⅎ j ((φ \land \forall j \in Z G (j) \leq x) \land z \in ran G)$
113		nfv	$⊢ Ⅎ j z \leq x$
114		rspa	$⊢ (\forall j \in Z G (j) \leq x \land j \in Z) \to G (j) \leq x$
115	114	3adant3	$⊢ (\forall j \in Z G (j) \leq x \land j \in Z \land G (j) = z) \to G (j) \leq x$
116		simp3	$⊢ (\forall j \in Z G (j) \leq x \land j \in Z \land G (j) = z) \to G (j) = z$
117		id	$⊢ G (j) = z \to G (j) = z$
118	117	eqcomd	$⊢ G (j) = z \to z = G (j)$
119	118	adantl	$⊢ (G (j) \leq x \land G (j) = z) \to z = G (j)$
120		simpl	$⊢ (G (j) \leq x \land G (j) = z) \to G (j) \leq x$
121	119 120	eqbrtrd	$⊢ (G (j) \leq x \land G (j) = z) \to z \leq x$
122	115 116 121	syl2anc	$⊢ (\forall j \in Z G (j) \leq x \land j \in Z \land G (j) = z) \to z \leq x$
123	122	3exp	$⊢ \forall j \in Z G (j) \leq x \to (j \in Z \to (G (j) = z \to z \leq x))$
124	123	ad2antlr	$⊢ ((φ \land \forall j \in Z G (j) \leq x) \land z \in ran G) \to (j \in Z \to (G (j) = z \to z \leq x))$
125	112 113 124	rexlimd	$⊢ ((φ \land \forall j \in Z G (j) \leq x) \land z \in ran G) \to (\exists j \in Z G (j) = z \to z \leq x)$
126	107 125	mpd	$⊢ ((φ \land \forall j \in Z G (j) \leq x) \land z \in ran G) \to z \leq x$
127	126	ralrimiva	$⊢ (φ \land \forall j \in Z G (j) \leq x) \to \forall z \in ran G z \leq x$
128	127	ex	$⊢ φ \to (\forall j \in Z G (j) \leq x \to \forall z \in ran G z \leq x)$
129	128	reximdv	$⊢ φ \to (\exists x \in ℝ \forall j \in Z G (j) \leq x \to \exists x \in ℝ \forall z \in ran G z \leq x)$
130	56 129	mpd	$⊢ φ \to \exists x \in ℝ \forall z \in ran G z \leq x$
131		suprub	$⊢ ((ran G \subseteq ℝ \land ran G \neq \emptyset \land \exists x \in ℝ \forall z \in ran G z \leq x) \land G (M) \in ran G) \to G (M) \leq sup (ran G ℝ <)$
132	77 100 130 87 131	syl31anc	$⊢ φ \to G (M) \leq sup (ran G ℝ <)$
133	71 88 58 99 132	letrd	$⊢ φ \to 0 \leq sup (ran G ℝ <)$
134	133	ad2antrr	$⊢ ((φ \land y \in (𝒫 Z \cap Fin)) \land y = \emptyset) \to 0 \leq sup (ran G ℝ <)$
135	70 134	eqbrtrd	$⊢ ((φ \land y \in (𝒫 Z \cap Fin)) \land y = \emptyset) \to sum^((k \in y ⟼ F (k))) \leq sup (ran G ℝ <)$
136		simpr	$⊢ (φ \land y \in (𝒫 Z \cap Fin)) \to y \in (𝒫 Z \cap Fin)$
137		simpll	$⊢ ((φ \land y \in (𝒫 Z \cap Fin)) \land k \in y) \to φ$
138		elpwinss	$⊢ y \in (𝒫 Z \cap Fin) \to y \subseteq Z$
139	138	sselda	$⊢ (y \in (𝒫 Z \cap Fin) \land k \in y) \to k \in Z$
140	139	adantll	$⊢ ((φ \land y \in (𝒫 Z \cap Fin)) \land k \in y) \to k \in Z$
141	8 14	sselid	$⊢ (φ \land k \in Z) \to F (k) \in [0, +∞]$
142	137 140 141	syl2anc	$⊢ ((φ \land y \in (𝒫 Z \cap Fin)) \land k \in y) \to F (k) \in [0, +∞]$
143		eqid	$⊢ (k \in y ⟼ F (k)) = (k \in y ⟼ F (k))$
144	142 143	fmptd	$⊢ (φ \land y \in (𝒫 Z \cap Fin)) \to (k \in y ⟼ F (k)) : y ⟶ [0, +∞]$
145	136 144	sge0xrcl	$⊢ (φ \land y \in (𝒫 Z \cap Fin)) \to sum^((k \in y ⟼ F (k))) \in ℝ^{*}$
146	145	adantr	$⊢ ((φ \land y \in (𝒫 Z \cap Fin)) \land \neg y = \emptyset) \to sum^((k \in y ⟼ F (k))) \in ℝ^{*}$
147		fzfid	$⊢ (φ \land y \in (𝒫 Z \cap Fin)) \to (M \dots sup (y ℝ <)) \in Fin$
148		elfzuz	$⊢ k \in (M \dots sup (y ℝ <)) \to k \in ℤ_{\geq M}$
149	148 81	eleqtrdi	$⊢ k \in (M \dots sup (y ℝ <)) \to k \in Z$
150	149 141	sylan2	$⊢ (φ \land k \in (M \dots sup (y ℝ <))) \to F (k) \in [0, +∞]$
151		eqid	$⊢ (k \in (M \dots sup (y ℝ <)) ⟼ F (k)) = (k \in (M \dots sup (y ℝ <)) ⟼ F (k))$
152	150 151	fmptd	$⊢ φ \to (k \in (M \dots sup (y ℝ <)) ⟼ F (k)) : (M \dots sup (y ℝ <)) ⟶ [0, +∞]$
153	152	adantr	$⊢ (φ \land y \in (𝒫 Z \cap Fin)) \to (k \in (M \dots sup (y ℝ <)) ⟼ F (k)) : (M \dots sup (y ℝ <)) ⟶ [0, +∞]$
154	147 153	sge0xrcl	$⊢ (φ \land y \in (𝒫 Z \cap Fin)) \to sum^((k \in (M \dots sup (y ℝ <)) ⟼ F (k))) \in ℝ^{*}$
155	154	adantr	$⊢ ((φ \land y \in (𝒫 Z \cap Fin)) \land \neg y = \emptyset) \to sum^((k \in (M \dots sup (y ℝ <)) ⟼ F (k))) \in ℝ^{*}$
156	59	adantr	$⊢ (φ \land y \in (𝒫 Z \cap Fin)) \to sup (ran G ℝ <) \in ℝ^{*}$
157	156	adantr	$⊢ ((φ \land y \in (𝒫 Z \cap Fin)) \land \neg y = \emptyset) \to sup (ran G ℝ <) \in ℝ^{*}$
158		simpll	$⊢ ((φ \land y \in (𝒫 Z \cap Fin)) \land k \in (M \dots sup (y ℝ <))) \to φ$
159	149	adantl	$⊢ ((φ \land y \in (𝒫 Z \cap Fin)) \land k \in (M \dots sup (y ℝ <))) \to k \in Z$
160	158 159 141	syl2anc	$⊢ ((φ \land y \in (𝒫 Z \cap Fin)) \land k \in (M \dots sup (y ℝ <))) \to F (k) \in [0, +∞]$
161		elinel2	$⊢ y \in (𝒫 Z \cap Fin) \to y \in Fin$
162	2 138 161	ssuzfz	$⊢ y \in (𝒫 Z \cap Fin) \to y \subseteq (M \dots sup (y ℝ <))$
163	162	adantl	$⊢ (φ \land y \in (𝒫 Z \cap Fin)) \to y \subseteq (M \dots sup (y ℝ <))$
164	147 160 163	sge0lessmpt	$⊢ (φ \land y \in (𝒫 Z \cap Fin)) \to sum^((k \in y ⟼ F (k))) \leq sum^((k \in (M \dots sup (y ℝ <)) ⟼ F (k)))$
165	164	adantr	$⊢ ((φ \land y \in (𝒫 Z \cap Fin)) \land \neg y = \emptyset) \to sum^((k \in y ⟼ F (k))) \leq sum^((k \in (M \dots sup (y ℝ <)) ⟼ F (k)))$
166	77	adantr	$⊢ (φ \land y \in (𝒫 Z \cap Fin)) \to ran G \subseteq ℝ$
167	166	adantr	$⊢ ((φ \land y \in (𝒫 Z \cap Fin)) \land \neg y = \emptyset) \to ran G \subseteq ℝ$
168	100	adantr	$⊢ (φ \land y \in (𝒫 Z \cap Fin)) \to ran G \neq \emptyset$
169	168	adantr	$⊢ ((φ \land y \in (𝒫 Z \cap Fin)) \land \neg y = \emptyset) \to ran G \neq \emptyset$
170	130	adantr	$⊢ (φ \land y \in (𝒫 Z \cap Fin)) \to \exists x \in ℝ \forall z \in ran G z \leq x$
171	170	adantr	$⊢ ((φ \land y \in (𝒫 Z \cap Fin)) \land \neg y = \emptyset) \to \exists x \in ℝ \forall z \in ran G z \leq x$
172	158 159 14	syl2anc	$⊢ ((φ \land y \in (𝒫 Z \cap Fin)) \land k \in (M \dots sup (y ℝ <))) \to F (k) \in [0, +∞)$
173	147 172	sge0fsummpt	$⊢ (φ \land y \in (𝒫 Z \cap Fin)) \to sum^((k \in (M \dots sup (y ℝ <)) ⟼ F (k))) = \sum_{k = M}^{sup (y ℝ <)} F (k)$
174	173	adantr	$⊢ ((φ \land y \in (𝒫 Z \cap Fin)) \land \neg y = \emptyset) \to sum^((k \in (M \dots sup (y ℝ <)) ⟼ F (k))) = \sum_{k = M}^{sup (y ℝ <)} F (k)$
175		eqidd	$⊢ (((φ \land y \in (𝒫 Z \cap Fin)) \land \neg y = \emptyset) \land k \in (M \dots sup (y ℝ <))) \to F (k) = F (k)$
176	138 2	sseqtrdi	$⊢ y \in (𝒫 Z \cap Fin) \to y \subseteq ℤ_{\geq M}$
177	176	adantr	$⊢ (y \in (𝒫 Z \cap Fin) \land \neg y = \emptyset) \to y \subseteq ℤ_{\geq M}$
178		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
179	2 178	eqsstri	$⊢ Z \subseteq ℤ$
180	138 179	sstrdi	$⊢ y \in (𝒫 Z \cap Fin) \to y \subseteq ℤ$
181	180	adantr	$⊢ (y \in (𝒫 Z \cap Fin) \land \neg y = \emptyset) \to y \subseteq ℤ$
182		neqne	$⊢ \neg y = \emptyset \to y \neq \emptyset$
183	182	adantl	$⊢ (y \in (𝒫 Z \cap Fin) \land \neg y = \emptyset) \to y \neq \emptyset$
184	161	adantr	$⊢ (y \in (𝒫 Z \cap Fin) \land \neg y = \emptyset) \to y \in Fin$
185		suprfinzcl	$⊢ (y \subseteq ℤ \land y \neq \emptyset \land y \in Fin) \to sup (y ℝ <) \in y$
186	181 183 184 185	syl3anc	$⊢ (y \in (𝒫 Z \cap Fin) \land \neg y = \emptyset) \to sup (y ℝ <) \in y$
187	177 186	sseldd	$⊢ (y \in (𝒫 Z \cap Fin) \land \neg y = \emptyset) \to sup (y ℝ <) \in ℤ_{\geq M}$
188	187	adantll	$⊢ ((φ \land y \in (𝒫 Z \cap Fin)) \land \neg y = \emptyset) \to sup (y ℝ <) \in ℤ_{\geq M}$
189	15	recnd	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
190	158 159 189	syl2anc	$⊢ ((φ \land y \in (𝒫 Z \cap Fin)) \land k \in (M \dots sup (y ℝ <))) \to F (k) \in ℂ$
191	190	adantlr	$⊢ (((φ \land y \in (𝒫 Z \cap Fin)) \land \neg y = \emptyset) \land k \in (M \dots sup (y ℝ <))) \to F (k) \in ℂ$
192	175 188 191	fsumser	$⊢ ((φ \land y \in (𝒫 Z \cap Fin)) \land \neg y = \emptyset) \to \sum_{k = M}^{sup (y ℝ <)} F (k) = seq M (+ F) (sup (y ℝ <))$
193	4	eqcomi	$⊢ seq M (+ F) = G$
194	193	fveq1i	$⊢ seq M (+ F) (sup (y ℝ <)) = G (sup (y ℝ <))$
195	194	a1i	$⊢ ((φ \land y \in (𝒫 Z \cap Fin)) \land \neg y = \emptyset) \to seq M (+ F) (sup (y ℝ <)) = G (sup (y ℝ <))$
196	174 192 195	3eqtrd	$⊢ ((φ \land y \in (𝒫 Z \cap Fin)) \land \neg y = \emptyset) \to sum^((k \in (M \dots sup (y ℝ <)) ⟼ F (k))) = G (sup (y ℝ <))$
197	78	adantr	$⊢ (φ \land y \in (𝒫 Z \cap Fin)) \to Fun G$
198	197	adantr	$⊢ ((φ \land y \in (𝒫 Z \cap Fin)) \land \neg y = \emptyset) \to Fun G$
199	188 81	eleqtrdi	$⊢ ((φ \land y \in (𝒫 Z \cap Fin)) \land \neg y = \emptyset) \to sup (y ℝ <) \in Z$
200	84	ad2antrr	$⊢ ((φ \land y \in (𝒫 Z \cap Fin)) \land \neg y = \emptyset) \to Z = dom G$
201	199 200	eleqtrd	$⊢ ((φ \land y \in (𝒫 Z \cap Fin)) \land \neg y = \emptyset) \to sup (y ℝ <) \in dom G$
202		fvelrn	$⊢ (Fun G \land sup (y ℝ <) \in dom G) \to G (sup (y ℝ <)) \in ran G$
203	198 201 202	syl2anc	$⊢ ((φ \land y \in (𝒫 Z \cap Fin)) \land \neg y = \emptyset) \to G (sup (y ℝ <)) \in ran G$
204	196 203	eqeltrd	$⊢ ((φ \land y \in (𝒫 Z \cap Fin)) \land \neg y = \emptyset) \to sum^((k \in (M \dots sup (y ℝ <)) ⟼ F (k))) \in ran G$
205		suprub	$⊢ ((ran G \subseteq ℝ \land ran G \neq \emptyset \land \exists x \in ℝ \forall z \in ran G z \leq x) \land sum^((k \in (M \dots sup (y ℝ <)) ⟼ F (k))) \in ran G) \to sum^((k \in (M \dots sup (y ℝ <)) ⟼ F (k))) \leq sup (ran G ℝ <)$
206	167 169 171 204 205	syl31anc	$⊢ ((φ \land y \in (𝒫 Z \cap Fin)) \land \neg y = \emptyset) \to sum^((k \in (M \dots sup (y ℝ <)) ⟼ F (k))) \leq sup (ran G ℝ <)$
207	146 155 157 165 206	xrletrd	$⊢ ((φ \land y \in (𝒫 Z \cap Fin)) \land \neg y = \emptyset) \to sum^((k \in y ⟼ F (k))) \leq sup (ran G ℝ <)$
208	135 207	pm2.61dan	$⊢ (φ \land y \in (𝒫 Z \cap Fin)) \to sum^((k \in y ⟼ F (k))) \leq sup (ran G ℝ <)$
209	208	ralrimiva	$⊢ φ \to \forall y \in (𝒫 Z \cap Fin) sum^((k \in y ⟼ F (k))) \leq sup (ran G ℝ <)$
210		nfv	$⊢ Ⅎ k φ$
211	210 7 141 59	sge0lefimpt	$⊢ φ \to (sum^((k \in Z ⟼ F (k))) \leq sup (ran G ℝ <) \leftrightarrow \forall y \in (𝒫 Z \cap Fin) sum^((k \in y ⟼ F (k))) \leq sup (ran G ℝ <))$
212	209 211	mpbird	$⊢ φ \to sum^((k \in Z ⟼ F (k))) \leq sup (ran G ℝ <)$
213	61 212	eqbrtrd	$⊢ φ \to sum^(F) \leq sup (ran G ℝ <)$
214	35	ssriv	$⊢ (M \dots j) \subseteq Z$
215	214	a1i	$⊢ φ \to (M \dots j) \subseteq Z$
216	7 141 215	sge0lessmpt	$⊢ φ \to sum^((k \in (M \dots j) ⟼ F (k))) \leq sum^((k \in Z ⟼ F (k)))$
217	216	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)))$
218		fzfid	$⊢ φ \to (M \dots j) \in Fin$
219	35 14	sylan2	$⊢ (φ \land k \in (M \dots j)) \to F (k) \in [0, +∞)$
220	218 219	sge0fsummpt	$⊢ φ \to sum^((k \in (M \dots j) ⟼ F (k))) = \sum_{k = M}^{j} F (k)$
221	220	3ad2ant1	$⊢ (φ \land j \in Z \land G (j) = z) \to sum^((k \in (M \dots j) ⟼ F (k))) = \sum_{k = M}^{j} F (k)$
222	33 36 12	syl2anc	$⊢ ((φ \land j \in Z) \land k \in (M \dots j)) \to F (k) = F (k)$
223	33 36 189	syl2anc	$⊢ ((φ \land j \in Z) \land k \in (M \dots j)) \to F (k) \in ℂ$
224	222 32 223	fsumser	$⊢ (φ \land j \in Z) \to \sum_{k = M}^{j} F (k) = seq M (+ F) (j)$
225	224	3adant3	$⊢ (φ \land j \in Z \land G (j) = z) \to \sum_{k = M}^{j} F (k) = seq M (+ F) (j)$
226	221 225	eqtrd	$⊢ (φ \land j \in Z \land G (j) = z) \to sum^((k \in (M \dots j) ⟼ F (k))) = seq M (+ F) (j)$
227	193	fveq1i	$⊢ seq M (+ F) (j) = G (j)$
228	227	a1i	$⊢ (φ \land j \in Z \land G (j) = z) \to seq M (+ F) (j) = G (j)$
229		simp3	$⊢ (φ \land j \in Z \land G (j) = z) \to G (j) = z$
230	226 228 229	3eqtrrd	$⊢ (φ \land j \in Z \land G (j) = z) \to z = sum^((k \in (M \dots j) ⟼ F (k)))$
231	61	3ad2ant1	$⊢ (φ \land j \in Z \land G (j) = z) \to sum^(F) = sum^((k \in Z ⟼ F (k)))$
232	230 231	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))))$
233	217 232	mpbird	$⊢ (φ \land j \in Z \land G (j) = z) \to z \leq sum^(F)$
234	233	3exp	$⊢ φ \to (j \in Z \to (G (j) = z \to z \leq sum^(F)))$
235	234	adantr	$⊢ (φ \land z \in ran G) \to (j \in Z \to (G (j) = z \to z \leq sum^(F)))$
236	235	rexlimdv	$⊢ (φ \land z \in ran G) \to (\exists j \in Z G (j) = z \to z \leq sum^(F))$
237	106 236	mpd	$⊢ (φ \land z \in ran G) \to z \leq sum^(F)$
238	237	ralrimiva	$⊢ φ \to \forall z \in ran G z \leq sum^(F)$
239	7 10	sge0cl	$⊢ φ \to sum^(F) \in [0, +∞]$
240	58	ltpnfd	$⊢ φ \to sup (ran G ℝ <) < +∞$
241	11 59 90 213 240	xrlelttrd	$⊢ φ \to sum^(F) < +∞$
242	11 90 241	xrgtned	$⊢ φ \to +∞ \neq sum^(F)$
243	242	necomd	$⊢ φ \to sum^(F) \neq +∞$
244		ge0xrre	$⊢ (sum^(F) \in [0, +∞] \land sum^(F) \neq +∞) \to sum^(F) \in ℝ$
245	239 243 244	syl2anc	$⊢ φ \to sum^(F) \in ℝ$
246		suprleub	$⊢ ((ran G \subseteq ℝ \land ran G \neq \emptyset \land \exists x \in ℝ \forall z \in ran G z \leq x) \land sum^(F) \in ℝ) \to (sup (ran G ℝ <) \leq sum^(F) \leftrightarrow \forall z \in ran G z \leq sum^(F))$
247	77 100 130 245 246	syl31anc	$⊢ φ \to (sup (ran G ℝ <) \leq sum^(F) \leftrightarrow \forall z \in ran G z \leq sum^(F))$
248	238 247	mpbird	$⊢ φ \to sup (ran G ℝ <) \leq sum^(F)$
249	11 59 213 248	xrletrid	$⊢ φ \to sum^(F) = sup (ran G ℝ <)$
250		climuni	$⊢ (G ⇝ B \land G ⇝ sup (ran G ℝ <)) \to B = sup (ran G ℝ <)$
251	5 57 250	syl2anc	$⊢ φ \to B = sup (ran G ℝ <)$
252	249 251	eqtr4d	$⊢ φ \to sum^(F) = B$

Metamath Proof Explorer

Theorem sge0isum

Proof