sge0isum - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > sge0isum		Structured version Visualization version Unicode version

Theorem sge0isum 40644

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.)

**Hypotheses**
Ref	Expression
sge0isum.m
sge0isum.z
sge0isum.f
sge0isum.g
sge0isum.gcnv

**Assertion**
Ref	Expression
sge0isum	Σ^{^}

Proof of Theorem sge0isum Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sge0isum.z	. . . . . 6
2		fvex 6201	. . . . . 6
3	1, 2	eqeltri 2697	. . . . 5
4	3	a1i 11	. . . 4
5		sge0isum.f	. . . . 5
6		icossicc 12260	. . . . . 6
7	6	a1i 11	. . . . 5
8	5, 7	fssd 6057	. . . 4
9	4, 8	sge0xrcl 40602	. . 3 Σ^{^}
10		sge0isum.m	. . . . 5
11		sge0isum.g	. . . . . 6
12		eqidd 2623	. . . . . 6 $/\$
13		rge0ssre 12280	. . . . . . 7
14	5	ffvelrnda 6359	. . . . . . 7 $/\$
15	13, 14	sseldi 3601	. . . . . 6 $/\$
16		0xr 10086	. . . . . . . 8
17	16	a1i 11	. . . . . . 7 $/\$
18		pnfxr 10092	. . . . . . . 8
19	18	a1i 11	. . . . . . 7 $/\$
20		icogelb 12225	. . . . . . 7 $/\$ $/\$
21	17, 19, 14, 20	syl3anc 1326	. . . . . 6 $/\$
22		seqex 12803	. . . . . . . . . . 11
23	11, 22	eqeltri 2697	. . . . . . . . . 10
24	23	a1i 11	. . . . . . . . 9
25		sge0isum.gcnv	. . . . . . . . . 10
26		climcl 14230	. . . . . . . . . 10
27	25, 26	syl 17	. . . . . . . . 9
28		breldmg 5330	. . . . . . . . 9 $/\$ $/\$
29	24, 27, 25, 28	syl3anc 1326	. . . . . . . 8
30	11	a1i 11	. . . . . . . . . . . 12 $/\$
31	30	fveq1d 6193	. . . . . . . . . . 11 $/\$
32	1	eleq2i 2693	. . . . . . . . . . . . . 14
33	32	biimpi 206	. . . . . . . . . . . . 13
34	33	adantl 482	. . . . . . . . . . . 12 $/\$
35		simpll 790	. . . . . . . . . . . . 13 $/\$ $/\$
36		elfzuz 12338	. . . . . . . . . . . . . . 15
37	36, 1	syl6eleqr 2712	. . . . . . . . . . . . . 14
38	37	adantl 482	. . . . . . . . . . . . 13 $/\$ $/\$
39	35, 38, 15	syl2anc 693	. . . . . . . . . . . 12 $/\$ $/\$
40		readdcl 10019	. . . . . . . . . . . . 13 $/\$
41	40	adantl 482	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
42	34, 39, 41	seqcl 12821	. . . . . . . . . . 11 $/\$
43	31, 42	eqeltrd 2701	. . . . . . . . . 10 $/\$
44	43	recnd 10068	. . . . . . . . 9 $/\$
45	44	ralrimiva 2966	. . . . . . . 8
46	1	climbdd 14402	. . . . . . . 8 $/\$ $/\$
47	10, 29, 45, 46	syl3anc 1326	. . . . . . 7
48	43	ad4ant13 1292	. . . . . . . . . . 11 $/\$ $/\$ $/\$
49	44	ad4ant13 1292	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
50	49	abscld 14175	. . . . . . . . . . 11 $/\$ $/\$ $/\$
51		simpllr 799	. . . . . . . . . . 11 $/\$ $/\$ $/\$
52	48	leabsd 14153	. . . . . . . . . . 11 $/\$ $/\$ $/\$
53		simpr 477	. . . . . . . . . . 11 $/\$ $/\$ $/\$
54	48, 50, 51, 52, 53	letrd 10194	. . . . . . . . . 10 $/\$ $/\$ $/\$
55	54	ex 450	. . . . . . . . 9 $/\$ $/\$
56	55	ralimdva 2962	. . . . . . . 8 $/\$
57	56	reximdva 3017	. . . . . . 7
58	47, 57	mpd 15	. . . . . 6
59	1, 11, 10, 12, 15, 21, 58	isumsup2 14578	. . . . 5
60	1, 10, 59, 43	climrecl 14314	. . . 4
61	60	rexrd 10089	. . 3
62	5	feqmptd 6249	. . . . 5
63	62	fveq2d 6195	. . . 4 Σ^{^} Σ^{^}
64		mpteq1 4737	. . . . . . . . . . 11
65	64	fveq2d 6195	. . . . . . . . . 10 Σ^{^} Σ^{^}
66		mpt0 6021	. . . . . . . . . . . . 13
67	66	fveq2i 6194	. . . . . . . . . . . 12 Σ^{^} Σ^{^}
68		sge00 40593	. . . . . . . . . . . 12 Σ^{^}
69	67, 68	eqtri 2644	. . . . . . . . . . 11 Σ^{^}
70	69	a1i 11	. . . . . . . . . 10 Σ^{^}
71	65, 70	eqtrd 2656	. . . . . . . . 9 Σ^{^}
72	71	adantl 482	. . . . . . . 8 $/\$ $/\$ Σ^{^}
73		0red 10041	. . . . . . . . . 10
74	40	adantl 482	. . . . . . . . . . . . . 14 $/\$ $/\$
75	1, 10, 15, 74	seqf 12822	. . . . . . . . . . . . 13
76	11	a1i 11	. . . . . . . . . . . . . 14
77	76	feq1d 6030	. . . . . . . . . . . . 13
78	75, 77	mpbird 247	. . . . . . . . . . . 12
79		frn 6053	. . . . . . . . . . . 12
80	78, 79	syl 17	. . . . . . . . . . 11
81		ffun 6048	. . . . . . . . . . . . 13
82	78, 81	syl 17	. . . . . . . . . . . 12
83		uzid 11702	. . . . . . . . . . . . . . 15
84	10, 83	syl 17	. . . . . . . . . . . . . 14
85	1	eqcomi 2631	. . . . . . . . . . . . . 14
86	84, 85	syl6eleq 2711	. . . . . . . . . . . . 13
87		fdm 6051	. . . . . . . . . . . . . . 15
88	78, 87	syl 17	. . . . . . . . . . . . . 14
89	88	eqcomd 2628	. . . . . . . . . . . . 13
90	86, 89	eleqtrd 2703	. . . . . . . . . . . 12
91		fvelrn 6352	. . . . . . . . . . . 12 $/\$
92	82, 90, 91	syl2anc 693	. . . . . . . . . . 11
93	80, 92	sseldd 3604	. . . . . . . . . 10
94	16	a1i 11	. . . . . . . . . . . 12
95	18	a1i 11	. . . . . . . . . . . 12
96	5, 86	ffvelrnd 6360	. . . . . . . . . . . 12
97		icogelb 12225	. . . . . . . . . . . 12 $/\$ $/\$
98	94, 95, 96, 97	syl3anc 1326	. . . . . . . . . . 11
99	11	fveq1i 6192	. . . . . . . . . . . . 13
100	99	a1i 11	. . . . . . . . . . . 12
101		seq1 12814	. . . . . . . . . . . . 13
102	10, 101	syl 17	. . . . . . . . . . . 12
103	100, 102	eqtr2d 2657	. . . . . . . . . . 11
104	98, 103	breqtrd 4679	. . . . . . . . . 10
105		ne0i 3921	. . . . . . . . . . . 12
106	92, 105	syl 17	. . . . . . . . . . 11
107		simpr 477	. . . . . . . . . . . . . . . . . 18 $/\$
108		ffn 6045	. . . . . . . . . . . . . . . . . . . . 21
109	78, 108	syl 17	. . . . . . . . . . . . . . . . . . . 20
110		fvelrnb 6243	. . . . . . . . . . . . . . . . . . . 20
111	109, 110	syl 17	. . . . . . . . . . . . . . . . . . 19
112	111	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$
113	107, 112	mpbid 222	. . . . . . . . . . . . . . . . 17 $/\$
114	113	adantlr 751	. . . . . . . . . . . . . . . 16 $/\$ $/\$
115		nfv 1843	. . . . . . . . . . . . . . . . . . 19
116		nfra1 2941	. . . . . . . . . . . . . . . . . . 19
117	115, 116	nfan 1828	. . . . . . . . . . . . . . . . . 18 $/\$
118		nfv 1843	. . . . . . . . . . . . . . . . . 18
119	117, 118	nfan 1828	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
120		nfv 1843	. . . . . . . . . . . . . . . . 17
121		rspa 2930	. . . . . . . . . . . . . . . . . . . . 21 $/\$
122	121	3adant3 1081	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
123		simp3 1063	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
124		id 22	. . . . . . . . . . . . . . . . . . . . . . 23
125	124	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . 22
126	125	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$
127		simpl 473	. . . . . . . . . . . . . . . . . . . . 21 $/\$
128	126, 127	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . . 20 $/\$
129	122, 123, 128	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
130	129	3exp 1264	. . . . . . . . . . . . . . . . . 18
131	130	ad2antlr 763	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
132	119, 120, 131	rexlimd 3026	. . . . . . . . . . . . . . . 16 $/\$ $/\$
133	114, 132	mpd 15	. . . . . . . . . . . . . . 15 $/\$ $/\$
134	133	ralrimiva 2966	. . . . . . . . . . . . . 14 $/\$
135	134	ex 450	. . . . . . . . . . . . 13
136	135	reximdv 3016	. . . . . . . . . . . 12
137	58, 136	mpd 15	. . . . . . . . . . 11
138		suprub 10984	. . . . . . . . . . 11 $/\$ $/\$ $/\$
139	80, 106, 137, 92, 138	syl31anc 1329	. . . . . . . . . 10
140	73, 93, 60, 104, 139	letrd 10194	. . . . . . . . 9
141	140	ad2antrr 762	. . . . . . . 8 $/\$ $/\$
142	72, 141	eqbrtrd 4675	. . . . . . 7 $/\$ $/\$ Σ^{^}
143		simpr 477	. . . . . . . . . 10 $/\$
144		simpll 790	. . . . . . . . . . . 12 $/\$ $/\$
145		elpwinss 39216	. . . . . . . . . . . . . 14
146	145	sselda 3603	. . . . . . . . . . . . 13 $/\$
147	146	adantll 750	. . . . . . . . . . . 12 $/\$ $/\$
148	6, 14	sseldi 3601	. . . . . . . . . . . 12 $/\$
149	144, 147, 148	syl2anc 693	. . . . . . . . . . 11 $/\$ $/\$
150		eqid 2622	. . . . . . . . . . 11
151	149, 150	fmptd 6385	. . . . . . . . . 10 $/\$
152	143, 151	sge0xrcl 40602	. . . . . . . . 9 $/\$ Σ^{^}
153	152	adantr 481	. . . . . . . 8 $/\$ $/\$ Σ^{^}
154		fzfid 12772	. . . . . . . . . 10 $/\$
155		elfzuz 12338	. . . . . . . . . . . . . 14
156	155, 85	syl6eleq 2711	. . . . . . . . . . . . 13
157	156, 148	sylan2 491	. . . . . . . . . . . 12 $/\$
158		eqid 2622	. . . . . . . . . . . 12
159	157, 158	fmptd 6385	. . . . . . . . . . 11
160	159	adantr 481	. . . . . . . . . 10 $/\$
161	154, 160	sge0xrcl 40602	. . . . . . . . 9 $/\$ Σ^{^}
162	161	adantr 481	. . . . . . . 8 $/\$ $/\$ Σ^{^}
163	61	adantr 481	. . . . . . . . 9 $/\$
164	163	adantr 481	. . . . . . . 8 $/\$ $/\$
165		simpll 790	. . . . . . . . . . 11 $/\$ $/\$
166	156	adantl 482	. . . . . . . . . . 11 $/\$ $/\$
167	165, 166, 148	syl2anc 693	. . . . . . . . . 10 $/\$ $/\$
168		elinel2 3800	. . . . . . . . . . . 12
169	1, 145, 168	ssuzfz 39565	. . . . . . . . . . 11
170	169	adantl 482	. . . . . . . . . 10 $/\$
171	154, 167, 170	sge0lessmpt 40616	. . . . . . . . 9 $/\$ Σ^{^} Σ^{^}
172	171	adantr 481	. . . . . . . 8 $/\$ $/\$ Σ^{^} Σ^{^}
173	80	adantr 481	. . . . . . . . . 10 $/\$
174	173	adantr 481	. . . . . . . . 9 $/\$ $/\$
175	106	adantr 481	. . . . . . . . . 10 $/\$
176	175	adantr 481	. . . . . . . . 9 $/\$ $/\$
177	137	adantr 481	. . . . . . . . . 10 $/\$
178	177	adantr 481	. . . . . . . . 9 $/\$ $/\$
179	165, 166, 14	syl2anc 693	. . . . . . . . . . . . 13 $/\$ $/\$
180	154, 179	sge0fsummpt 40607	. . . . . . . . . . . 12 $/\$ Σ^{^}
181	180	adantr 481	. . . . . . . . . . 11 $/\$ $/\$ Σ^{^}
182		eqidd 2623	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
183	145, 1	syl6sseq 3651	. . . . . . . . . . . . . . 15
184	183	adantr 481	. . . . . . . . . . . . . 14 $/\$
185		uzssz 11707	. . . . . . . . . . . . . . . . . 18
186	1, 185	eqsstri 3635	. . . . . . . . . . . . . . . . 17
187	145, 186	syl6ss 3615	. . . . . . . . . . . . . . . 16
188	187	adantr 481	. . . . . . . . . . . . . . 15 $/\$
189		neqne 2802	. . . . . . . . . . . . . . . 16
190	189	adantl 482	. . . . . . . . . . . . . . 15 $/\$
191	168	adantr 481	. . . . . . . . . . . . . . 15 $/\$
192		suprfinzcl 11492	. . . . . . . . . . . . . . 15 $/\$ $/\$
193	188, 190, 191, 192	syl3anc 1326	. . . . . . . . . . . . . 14 $/\$
194	184, 193	sseldd 3604	. . . . . . . . . . . . 13 $/\$
195	194	adantll 750	. . . . . . . . . . . 12 $/\$ $/\$
196	15	recnd 10068	. . . . . . . . . . . . . 14 $/\$
197	165, 166, 196	syl2anc 693	. . . . . . . . . . . . 13 $/\$ $/\$
198	197	adantlr 751	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
199	182, 195, 198	fsumser 14461	. . . . . . . . . . 11 $/\$ $/\$
200	11	eqcomi 2631	. . . . . . . . . . . . 13
201	200	fveq1i 6192	. . . . . . . . . . . 12
202	201	a1i 11	. . . . . . . . . . 11 $/\$ $/\$
203	181, 199, 202	3eqtrd 2660	. . . . . . . . . 10 $/\$ $/\$ Σ^{^}
204	82	adantr 481	. . . . . . . . . . . 12 $/\$
205	204	adantr 481	. . . . . . . . . . 11 $/\$ $/\$
206	195, 85	syl6eleq 2711	. . . . . . . . . . . 12 $/\$ $/\$
207	89	ad2antrr 762	. . . . . . . . . . . 12 $/\$ $/\$
208	206, 207	eleqtrd 2703	. . . . . . . . . . 11 $/\$ $/\$
209		fvelrn 6352	. . . . . . . . . . 11 $/\$
210	205, 208, 209	syl2anc 693	. . . . . . . . . 10 $/\$ $/\$
211	203, 210	eqeltrd 2701	. . . . . . . . 9 $/\$ $/\$ Σ^{^}
212		suprub 10984	. . . . . . . . 9 $/\$ $/\$ $/\$ Σ^{^} Σ^{^}
213	174, 176, 178, 211, 212	syl31anc 1329	. . . . . . . 8 $/\$ $/\$ Σ^{^}
214	153, 162, 164, 172, 213	xrletrd 11993	. . . . . . 7 $/\$ $/\$ Σ^{^}
215	142, 214	pm2.61dan 832	. . . . . 6 $/\$ Σ^{^}
216	215	ralrimiva 2966	. . . . 5 Σ^{^}
217		nfv 1843	. . . . . 6
218	217, 4, 148, 61	sge0lefimpt 40640	. . . . 5 Σ^{^} Σ^{^}
219	216, 218	mpbird 247	. . . 4 Σ^{^}
220	63, 219	eqbrtrd 4675	. . 3 Σ^{^}
221	37	ssriv 3607	. . . . . . . . . . . . 13
222	221	a1i 11	. . . . . . . . . . . 12
223	4, 148, 222	sge0lessmpt 40616	. . . . . . . . . . 11 Σ^{^} Σ^{^}
224	223	3ad2ant1 1082	. . . . . . . . . 10 $/\$ $/\$ Σ^{^} Σ^{^}
225		fzfid 12772	. . . . . . . . . . . . . . 15
226	37, 14	sylan2 491	. . . . . . . . . . . . . . 15 $/\$
227	225, 226	sge0fsummpt 40607	. . . . . . . . . . . . . 14 Σ^{^}
228	227	3ad2ant1 1082	. . . . . . . . . . . . 13 $/\$ $/\$ Σ^{^}
229	35, 38, 12	syl2anc 693	. . . . . . . . . . . . . . 15 $/\$ $/\$
230	35, 38, 196	syl2anc 693	. . . . . . . . . . . . . . 15 $/\$ $/\$
231	229, 34, 230	fsumser 14461	. . . . . . . . . . . . . 14 $/\$
232	231	3adant3 1081	. . . . . . . . . . . . 13 $/\$ $/\$
233	228, 232	eqtrd 2656	. . . . . . . . . . . 12 $/\$ $/\$ Σ^{^}
234	200	fveq1i 6192	. . . . . . . . . . . . 13
235	234	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$
236		simp3 1063	. . . . . . . . . . . 12 $/\$ $/\$
237	233, 235, 236	3eqtrrd 2661	. . . . . . . . . . 11 $/\$ $/\$ Σ^{^}
238	63	3ad2ant1 1082	. . . . . . . . . . 11 $/\$ $/\$ Σ^{^} Σ^{^}
239	237, 238	breq12d 4666	. . . . . . . . . 10 $/\$ $/\$ Σ^{^} Σ^{^} Σ^{^}
240	224, 239	mpbird 247	. . . . . . . . 9 $/\$ $/\$ Σ^{^}
241	240	3exp 1264	. . . . . . . 8 Σ^{^}
242	241	adantr 481	. . . . . . 7 $/\$ Σ^{^}
243	242	rexlimdv 3030	. . . . . 6 $/\$ Σ^{^}
244	113, 243	mpd 15	. . . . 5 $/\$ Σ^{^}
245	244	ralrimiva 2966	. . . 4 Σ^{^}
246	4, 8	sge0cl 40598	. . . . . 6 Σ^{^}
247	60	ltpnfd 11955	. . . . . . . . 9
248	9, 61, 95, 220, 247	xrlelttrd 11991	. . . . . . . 8 Σ^{^}
249	9, 95, 248	xrgtned 39538	. . . . . . 7 Σ^{^}
250	249	necomd 2849	. . . . . 6 Σ^{^}
251		ge0xrre 39758	. . . . . 6 Σ^{^} $/\$ Σ^{^} Σ^{^}
252	246, 250, 251	syl2anc 693	. . . . 5 Σ^{^}
253		suprleub 10989	. . . . 5 $/\$ $/\$ $/\$ Σ^{^} Σ^{^} Σ^{^}
254	80, 106, 137, 252, 253	syl31anc 1329	. . . 4 Σ^{^} Σ^{^}
255	245, 254	mpbird 247	. . 3 Σ^{^}
256	9, 61, 220, 255	xrletrid 11986	. 2 Σ^{^}
257		climuni 14283	. . 3 $/\$
258	25, 59, 257	syl2anc 693	. 2
259	256, 258	eqtr4d 2659	1 Σ^{^}

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $/\$ wa 384 $/\$ w3a 1037

wceq 1483

wcel 1990

wne 2794

wral 2912

wrex 2913

cvv 3200

cin 3573

wss 3574

c0 3915

cpw 4158 class class class wbr 4653

cmpt 4729

cdm 5114

crn 5115

wfun 5882

wfn 5883

wf 5884

cfv 5888 (class class class)co 6650

cfn 7955

csup 8346

cc 9934

cr 9935

cc0 9936

caddc 9939

cpnf 10071

cxr 10073

clt 10074

cle 10075

cz 11377

cuz 11687

cico 12177

cicc 12178

cfz 12326

cseq 12801

cabs 13974

cli 14215

csu 14416 Σ^{^}csumge0 40579

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-pm 7860 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-n0 11293 df-z 11378 df-uz 11688 df-rp 11833 df-ico 12181 df-icc 12182 df-fz 12327 df-fzo 12466 df-fl 12593 df-seq 12802 df-exp 12861 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-clim 14219 df-rlim 14220 df-sum 14417 df-sumge0 40580

This theorem is referenced by: sge0isummpt 40647

W3C validator