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

Metamath Proof Explorer

Theorem sge0isum

Proof