sge0split - Mathbox for Glauco Siliprandi

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

Theorem sge0split 38365

Description: Split a sum of nonnegative extended reals into two parts. (Contributed by Glauco Siliprandi, 17-Aug-2020.)

**Hypotheses**
Ref	Expression
sge0split.a
sge0split.b
sge0split.u
sge0split.in0
sge0split.f

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

Proof of Theorem sge0split Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sge0split.a	. . . . 5
2	1	adantr 472	. . . 4 $/\$ Σ^{^}
3		sge0split.b	. . . . 5
4	3	adantr 472	. . . 4 $/\$ Σ^{^}
5		sge0split.u	. . . 4
6		sge0split.in0	. . . . 5
7	6	adantr 472	. . . 4 $/\$ Σ^{^}
8		sge0split.f	. . . . 5
9	8	adantr 472	. . . 4 $/\$ Σ^{^}
10		simpr 468	. . . 4 $/\$ Σ^{^} Σ^{^}
11	2, 4, 5, 7, 9, 10	sge0resplit 38362	. . 3 $/\$ Σ^{^} Σ^{^} Σ^{^} Σ^{^}
12		unexg 6611	. . . . . . . . 9 $/\$
13	1, 3, 12	syl2anc 673	. . . . . . . 8
14	5, 13	syl5eqel 2553	. . . . . . 7
15	14	adantr 472	. . . . . 6 $/\$ Σ^{^}
16	15, 9, 10	sge0ssre 38353	. . . . 5 $/\$ Σ^{^} Σ^{^}
17	15, 9, 10	sge0ssre 38353	. . . . 5 $/\$ Σ^{^} Σ^{^}
18		rexadd 11548	. . . . 5 Σ^{^} $/\$ Σ^{^} Σ^{^} Σ^{^} Σ^{^} Σ^{^}
19	16, 17, 18	syl2anc 673	. . . 4 $/\$ Σ^{^} Σ^{^} Σ^{^} Σ^{^} Σ^{^}
20	19	eqcomd 2477	. . 3 $/\$ Σ^{^} Σ^{^} Σ^{^} Σ^{^} Σ^{^}
21	11, 20	eqtrd 2505	. 2 $/\$ Σ^{^} Σ^{^} Σ^{^} Σ^{^}
22		simpl 464	. . 3 $/\$ Σ^{^}
23		simpr 468	. . . . 5 $/\$ Σ^{^} Σ^{^}
24	14, 8	sge0repnf 38342	. . . . . 6 Σ^{^} Σ^{^}
25	24	adantr 472	. . . . 5 $/\$ Σ^{^} Σ^{^} Σ^{^}
26	23, 25	mtbid 307	. . . 4 $/\$ Σ^{^} Σ^{^}
27	26	notnotrd 117	. . 3 $/\$ Σ^{^} Σ^{^}
28	14, 8	sge0xrcl 38341	. . . . 5 Σ^{^}
29	28	adantr 472	. . . 4 $/\$ Σ^{^} Σ^{^}
30		ssun1 3588	. . . . . . . . . 10
31	30, 5	sseqtr4i 3451	. . . . . . . . 9
32	31	a1i 11	. . . . . . . 8
33	8, 32	fssresd 5762	. . . . . . 7
34	1, 33	sge0xrcl 38341	. . . . . 6 Σ^{^}
35		iccssxr 11742	. . . . . . 7
36		ssun2 3589	. . . . . . . . . . 11
37	36, 5	sseqtr4i 3451	. . . . . . . . . 10
38	37	a1i 11	. . . . . . . . 9
39	8, 38	fssresd 5762	. . . . . . . 8
40	3, 39	sge0cl 38337	. . . . . . 7 Σ^{^}
41	35, 40	sseldi 3416	. . . . . 6 Σ^{^}
42	34, 41	xaddcld 11612	. . . . 5 Σ^{^} Σ^{^}
43	42	adantr 472	. . . 4 $/\$ Σ^{^} Σ^{^} Σ^{^}
44		pnfxr 11435	. . . . . . . . 9
45		eqid 2471	. . . . . . . . 9
46		xreqle 37628	. . . . . . . . 9 $/\$
47	44, 45, 46	mp2an 686	. . . . . . . 8
48	47	a1i 11	. . . . . . 7 $/\$
49	14	adantr 472	. . . . . . . . 9 $/\$
50	8	adantr 472	. . . . . . . . 9 $/\$
51		rnresss 37522	. . . . . . . . . . 11
52	51	sseli 3414	. . . . . . . . . 10
53	52	adantl 473	. . . . . . . . 9 $/\$
54	49, 50, 53	sge0pnfval 38329	. . . . . . . 8 $/\$ Σ^{^}
55		ge0nemnf2 37726	. . . . . . . . . . . . . 14 Σ^{^} Σ^{^}
56	40, 55	syl 17	. . . . . . . . . . . . 13 Σ^{^}
57		xaddpnf2 11543	. . . . . . . . . . . . 13 Σ^{^} $/\$ Σ^{^} Σ^{^}
58	41, 56, 57	syl2anc 673	. . . . . . . . . . . 12 Σ^{^}
59	58	eqcomd 2477	. . . . . . . . . . 11 Σ^{^}
60	59	adantr 472	. . . . . . . . . 10 $/\$ Σ^{^}
61	1	adantr 472	. . . . . . . . . . . 12 $/\$
62	33	adantr 472	. . . . . . . . . . . 12 $/\$
63		simpr 468	. . . . . . . . . . . 12 $/\$
64	61, 62, 63	sge0pnfval 38329	. . . . . . . . . . 11 $/\$ Σ^{^}
65	64	oveq1d 6323	. . . . . . . . . 10 $/\$ Σ^{^} Σ^{^} Σ^{^}
66	60, 54, 65	3eqtr4d 2515	. . . . . . . . 9 $/\$ Σ^{^} Σ^{^} Σ^{^}
67	66, 54	eqtr3d 2507	. . . . . . . 8 $/\$ Σ^{^} Σ^{^}
68	54, 67	breq12d 4408	. . . . . . 7 $/\$ Σ^{^} Σ^{^} Σ^{^}
69	48, 68	mpbird 240	. . . . . 6 $/\$ Σ^{^} Σ^{^} Σ^{^}
70	47	a1i 11	. . . . . . . . 9 $/\$
71	14	adantr 472	. . . . . . . . . . 11 $/\$
72	8	adantr 472	. . . . . . . . . . 11 $/\$
73		rnresss 37522	. . . . . . . . . . . . 13
74	73	sseli 3414	. . . . . . . . . . . 12
75	74	adantl 473	. . . . . . . . . . 11 $/\$
76	71, 72, 75	sge0pnfval 38329	. . . . . . . . . 10 $/\$ Σ^{^}
77	3	adantr 472	. . . . . . . . . . . . 13 $/\$
78	39	adantr 472	. . . . . . . . . . . . 13 $/\$
79		simpr 468	. . . . . . . . . . . . 13 $/\$
80	77, 78, 79	sge0pnfval 38329	. . . . . . . . . . . 12 $/\$ Σ^{^}
81	80	oveq2d 6324	. . . . . . . . . . 11 $/\$ Σ^{^} Σ^{^} Σ^{^}
82	1, 33	sge0cl 38337	. . . . . . . . . . . . . 14 Σ^{^}
83		ge0nemnf2 37726	. . . . . . . . . . . . . 14 Σ^{^} Σ^{^}
84	82, 83	syl 17	. . . . . . . . . . . . 13 Σ^{^}
85		xaddpnf1 11542	. . . . . . . . . . . . 13 Σ^{^} $/\$ Σ^{^} Σ^{^}
86	34, 84, 85	syl2anc 673	. . . . . . . . . . . 12 Σ^{^}
87	86	adantr 472	. . . . . . . . . . 11 $/\$ Σ^{^}
88	81, 87	eqtrd 2505	. . . . . . . . . 10 $/\$ Σ^{^} Σ^{^}
89	76, 88	breq12d 4408	. . . . . . . . 9 $/\$ Σ^{^} Σ^{^} Σ^{^}
90	70, 89	mpbird 240	. . . . . . . 8 $/\$ Σ^{^} Σ^{^} Σ^{^}
91	90	adantlr 729	. . . . . . 7 $/\$ $/\$ Σ^{^} Σ^{^} Σ^{^}
92		simpr 468	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
93		vex 3034	. . . . . . . . . . . . 13
94		eqid 2471	. . . . . . . . . . . . . 14
95	94	elrnmpt 5087	. . . . . . . . . . . . 13
96	93, 95	ax-mp 5	. . . . . . . . . . . 12
97	92, 96	sylib 201	. . . . . . . . . . 11 $/\$ $/\$ $/\$
98		simp3 1032	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
99		inss1 3643	. . . . . . . . . . . . . . . . . . . . . . . . 25
100		inss2 3644	. . . . . . . . . . . . . . . . . . . . . . . . 25
101	99, 100	sstri 3427	. . . . . . . . . . . . . . . . . . . . . . . 24
102		inss2 3644	. . . . . . . . . . . . . . . . . . . . . . . . 25
103		inss2 3644	. . . . . . . . . . . . . . . . . . . . . . . . 25
104	102, 103	sstri 3427	. . . . . . . . . . . . . . . . . . . . . . . 24
105	101, 104	ssini 3646	. . . . . . . . . . . . . . . . . . . . . . 23
106	105	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
107	106, 6	sseqtrd 3454	. . . . . . . . . . . . . . . . . . . . 21
108		ss0 3768	. . . . . . . . . . . . . . . . . . . . 21
109	107, 108	syl 17	. . . . . . . . . . . . . . . . . . . 20
110	109	ad3antrrr 744	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
111		indi 3680	. . . . . . . . . . . . . . . . . . . . . . 23
112	111	eqcomi 2480	. . . . . . . . . . . . . . . . . . . . . 22
113	112	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
114	5	eqcomi 2480	. . . . . . . . . . . . . . . . . . . . . . 23
115	114	ineq2i 3622	. . . . . . . . . . . . . . . . . . . . . 22
116	115	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
117		elinel1 3610	. . . . . . . . . . . . . . . . . . . . . . 23
118		elpwi 3951	. . . . . . . . . . . . . . . . . . . . . . 23
119	117, 118	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
120		df-ss 3404	. . . . . . . . . . . . . . . . . . . . . . 23
121	120	biimpi 199	. . . . . . . . . . . . . . . . . . . . . 22
122	119, 121	syl 17	. . . . . . . . . . . . . . . . . . . . 21
123	113, 116, 122	3eqtrrd 2510	. . . . . . . . . . . . . . . . . . . 20
124	123	adantl 473	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
125		elinel2 3611	. . . . . . . . . . . . . . . . . . . 20
126	125	adantl 473	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
127		rge0ssre 11766	. . . . . . . . . . . . . . . . . . . . 21
128	8	ad2antrr 740	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
129		pm4.56 503	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\/$
130	129	biimpi 199	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\/$
131		elun 3565	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\/$
132	130, 131	sylnibr 312	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
133	132	adantll 728	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
134		rnresun 37519	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
135	134	eqcomi 2480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
136	135	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
137	114	reseq2i 5108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
138	137	rneqi 5067	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
139	138	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
140		ffn 5739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
141		fnresdm 5695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
142	8, 140, 141	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
143	142	rneqd 5068	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
144	136, 139, 143	3eqtrd 2509	. . . . . . . . . . . . . . . . . . . . . . . . . 26
145	144	ad2antrr 740	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
146	133, 145	neleqtrd 2570	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
147	128, 146	fge0iccico 38326	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
148	147	ad2antrr 740	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
149	119	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
150		simpr 468	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
151	149, 150	sseldd 3419	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
152	151	adantll 728	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
153	148, 152	ffvelrnd 6038	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
154	127, 153	sseldi 3416	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
155	154	recnd 9687	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
156	110, 124, 126, 155	fsumsplit 13883	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
157		infi 7813	. . . . . . . . . . . . . . . . . . . . . . 23
158	125, 157	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
159	158	adantl 473	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
160		simpl 464	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
161		elinel1 3610	. . . . . . . . . . . . . . . . . . . . . . 23
162	161	adantl 473	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
163	160, 162, 154	syl2anc 673	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
164	159, 163	fsumrecl 13877	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
165		infi 7813	. . . . . . . . . . . . . . . . . . . . . . 23
166	125, 165	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
167	166	adantl 473	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
168		simpl 464	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
169		elinel1 3610	. . . . . . . . . . . . . . . . . . . . . . 23
170	169	adantl 473	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
171	168, 170, 154	syl2anc 673	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
172	167, 171	fsumrecl 13877	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
173		rexadd 11548	. . . . . . . . . . . . . . . . . . . 20 $/\$
174	164, 172, 173	syl2anc 673	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
175	174	eqcomd 2477	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
176	156, 175	eqtrd 2505	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
177		ressxr 9702	. . . . . . . . . . . . . . . . . . . 20
178	177, 164	sseldi 3416	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
179	177, 172	sseldi 3416	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
180	1	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
181	33	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
182		simpr 468	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
183	181, 182	fge0iccico 38326	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
184	180, 183	sge0reval 38328	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ Σ^{^}
185	184	eqcomd 2477	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ Σ^{^}
186	34	adantr 472	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ Σ^{^}
187	185, 186	eqeltrd 2549	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
188	187	adantr 472	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
189	3	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
190	39	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
191		simpr 468	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
192	190, 191	fge0iccico 38326	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
193	189, 192	sge0reval 38328	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ Σ^{^}
194	193	eqcomd 2477	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ Σ^{^}
195	41	adantr 472	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ Σ^{^}
196	194, 195	eqeltrd 2549	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
197	196	adantlr 729	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
198	188, 197	jca 541	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
199	198	adantr 472	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
200	178, 179, 199	jca31 543	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
201	180	adantr 472	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
202	181	adantr 472	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
203	182	adantr 472	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
204	202, 203	fge0iccico 38326	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
205	100	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
206	158	adantl 473	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
207	201, 204, 205, 206	fsumlesge0 38333	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ Σ^{^}
208	100	sseli 3414	. . . . . . . . . . . . . . . . . . . . . . . . 25
209		fvres 5893	. . . . . . . . . . . . . . . . . . . . . . . . 25
210	208, 209	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
211	210	adantl 473	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
212	211	sumeq2dv 13846	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
213	184	adantr 472	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ Σ^{^}
214	212, 213	breq12d 4408	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ Σ^{^}
215	207, 214	mpbid 215	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
216	215	adantlr 729	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
217	189	adantr 472	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
218	190	adantr 472	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
219	191	adantr 472	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
220	218, 219	fge0iccico 38326	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
221	103	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
222	166	adantl 473	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
223	217, 220, 221, 222	fsumlesge0 38333	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ Σ^{^}
224	103	sseli 3414	. . . . . . . . . . . . . . . . . . . . . . . . 25
225		fvres 5893	. . . . . . . . . . . . . . . . . . . . . . . . 25
226	224, 225	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
227	226	adantl 473	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
228	227	sumeq2dv 13846	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
229	193	adantr 472	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ Σ^{^}
230	228, 229	breq12d 4408	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ Σ^{^}
231	223, 230	mpbid 215	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
232	231	adantllr 733	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
233	216, 232	jca 541	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
234		xle2add 11570	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
235	200, 233, 234	sylc 61	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
236	176, 235	eqbrtrd 4416	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
237	236	3adant3 1050	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
238	98, 237	eqbrtrd 4416	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
239	238	3exp 1230	. . . . . . . . . . . . 13 $/\$ $/\$
240	239	rexlimdv 2870	. . . . . . . . . . . 12 $/\$ $/\$
241	240	adantr 472	. . . . . . . . . . 11 $/\$ $/\$ $/\$
242	97, 241	mpd 15	. . . . . . . . . 10 $/\$ $/\$ $/\$
243	242	ralrimiva 2809	. . . . . . . . 9 $/\$ $/\$
244	147	sge0rnre 38320	. . . . . . . . . . 11 $/\$ $/\$
245	177	a1i 11	. . . . . . . . . . 11 $/\$ $/\$
246	244, 245	sstrd 3428	. . . . . . . . . 10 $/\$ $/\$
247	188, 197	xaddcld 11612	. . . . . . . . . 10 $/\$ $/\$
248		supxrleub 11637	. . . . . . . . . 10 $/\$
249	246, 247, 248	syl2anc 673	. . . . . . . . 9 $/\$ $/\$
250	243, 249	mpbird 240	. . . . . . . 8 $/\$ $/\$
251	14	ad2antrr 740	. . . . . . . . 9 $/\$ $/\$
252	251, 147	sge0reval 38328	. . . . . . . 8 $/\$ $/\$ Σ^{^}
253	184	adantr 472	. . . . . . . . 9 $/\$ $/\$ Σ^{^}
254	193	adantlr 729	. . . . . . . . 9 $/\$ $/\$ Σ^{^}
255	253, 254	oveq12d 6326	. . . . . . . 8 $/\$ $/\$ Σ^{^} Σ^{^}
256	250, 252, 255	3brtr4d 4426	. . . . . . 7 $/\$ $/\$ Σ^{^} Σ^{^} Σ^{^}
257	91, 256	pm2.61dan 808	. . . . . 6 $/\$ Σ^{^} Σ^{^} Σ^{^}
258	69, 257	pm2.61dan 808	. . . . 5 Σ^{^} Σ^{^} Σ^{^}
259	258	adantr 472	. . . 4 $/\$ Σ^{^} Σ^{^} Σ^{^} Σ^{^}
260		pnfge 11455	. . . . . . 7 Σ^{^} Σ^{^} Σ^{^} Σ^{^}
261	42, 260	syl 17	. . . . . 6 Σ^{^} Σ^{^}
262	261	adantr 472	. . . . 5 $/\$ Σ^{^} Σ^{^} Σ^{^}
263		id 22	. . . . . . 7 Σ^{^} Σ^{^}
264	263	eqcomd 2477	. . . . . 6 Σ^{^} Σ^{^}
265	264	adantl 473	. . . . 5 $/\$ Σ^{^} Σ^{^}
266	262, 265	breqtrd 4420	. . . 4 $/\$ Σ^{^} Σ^{^} Σ^{^} Σ^{^}
267	29, 43, 259, 266	xrletrid 11475	. . 3 $/\$ Σ^{^} Σ^{^} Σ^{^} Σ^{^}
268	22, 27, 267	syl2anc 673	. 2 $/\$ Σ^{^} Σ^{^} Σ^{^} Σ^{^}
269	21, 268	pm2.61dan 808	1 Σ^{^} Σ^{^} Σ^{^}

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $\/$ wo 375 $/\$ wa 376 $/\$ w3a 1007

wceq 1452

wcel 1904

wne 2641

wral 2756

wrex 2757

cvv 3031

cun 3388

cin 3389

wss 3390

c0 3722

cpw 3942 class class class wbr 4395

cmpt 4454

crn 4840

cres 4841

wfn 5584

wf 5585

cfv 5589 (class class class)co 6308

cfn 7587

csup 7972

cr 9556

cc0 9557

caddc 9560

cpnf 9690

cmnf 9691

cxr 9692

clt 9693

cle 9694

cxad 11430

cico 11662

cicc 11663

csu 13829 Σ^{^}csumge0 38318

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-inf2 8164 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-pre-sup 9635

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-fal 1458 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-se 4799 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-isom 5598 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-om 6712 df-1st 6812 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-oadd 7204 df-er 7381 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-sup 7974 df-oi 8043 df-card 8391 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-div 10292 df-nn 10632 df-2 10690 df-3 10691 df-n0 10894 df-z 10962 df-uz 11183 df-rp 11326 df-xadd 11433 df-ico 11666 df-icc 11667 df-fz 11811 df-fzo 11943 df-seq 12252 df-exp 12311 df-hash 12554 df-cj 13239 df-re 13240 df-im 13241 df-sqrt 13375 df-abs 13376 df-clim 13629 df-sum 13830 df-sumge0 38319

This theorem is referenced by: sge0splitmpt 38367

W3C validator