sge0split - Mathbox for Glauco Siliprandi

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

Theorem sge0split 38006

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 466	. . . 4 $/\$ Σ^{^}
3		sge0split.b	. . . . 5
4	3	adantr 466	. . . 4 $/\$ Σ^{^}
5		sge0split.u	. . . 4
6		sge0split.in0	. . . . 5
7	6	adantr 466	. . . 4 $/\$ Σ^{^}
8		sge0split.f	. . . . 5
9	8	adantr 466	. . . 4 $/\$ Σ^{^}
10		simpr 462	. . . 4 $/\$ Σ^{^} Σ^{^}
11	2, 4, 5, 7, 9, 10	sge0resplit 38003	. . 3 $/\$ Σ^{^} Σ^{^} Σ^{^} Σ^{^}
12		unexg 6598	. . . . . . . . 9 $/\$
13	1, 3, 12	syl2anc 665	. . . . . . . 8
14	5, 13	syl5eqel 2512	. . . . . . 7
15	14	adantr 466	. . . . . 6 $/\$ Σ^{^}
16	15, 9, 10	sge0ssre 37994	. . . . 5 $/\$ Σ^{^} Σ^{^}
17	15, 9, 10	sge0ssre 37994	. . . . 5 $/\$ Σ^{^} Σ^{^}
18		rexadd 11521	. . . . 5 Σ^{^} $/\$ Σ^{^} Σ^{^} Σ^{^} Σ^{^} Σ^{^}
19	16, 17, 18	syl2anc 665	. . . 4 $/\$ Σ^{^} Σ^{^} Σ^{^} Σ^{^} Σ^{^}
20	19	eqcomd 2428	. . 3 $/\$ Σ^{^} Σ^{^} Σ^{^} Σ^{^} Σ^{^}
21	11, 20	eqtrd 2461	. 2 $/\$ Σ^{^} Σ^{^} Σ^{^} Σ^{^}
22		simpl 458	. . 3 $/\$ Σ^{^}
23		simpr 462	. . . . 5 $/\$ Σ^{^} Σ^{^}
24	14, 8	sge0repnf 37983	. . . . . 6 Σ^{^} Σ^{^}
25	24	adantr 466	. . . . 5 $/\$ Σ^{^} Σ^{^} Σ^{^}
26	23, 25	mtbid 301	. . . 4 $/\$ Σ^{^} Σ^{^}
27	26	notnotrd 116	. . 3 $/\$ Σ^{^} Σ^{^}
28	14, 8	sge0xrcl 37982	. . . . 5 Σ^{^}
29	28	adantr 466	. . . 4 $/\$ Σ^{^} Σ^{^}
30		ssun1 3626	. . . . . . . . . 10
31	30, 5	sseqtr4i 3494	. . . . . . . . 9
32	31	a1i 11	. . . . . . . 8
33	8, 32	fssresd 5759	. . . . . . 7
34	1, 33	sge0xrcl 37982	. . . . . 6 Σ^{^}
35		iccssxr 11713	. . . . . . 7
36		ssun2 3627	. . . . . . . . . . 11
37	36, 5	sseqtr4i 3494	. . . . . . . . . 10
38	37	a1i 11	. . . . . . . . 9
39	8, 38	fssresd 5759	. . . . . . . 8
40	3, 39	sge0cl 37978	. . . . . . 7 Σ^{^}
41	35, 40	sseldi 3459	. . . . . 6 Σ^{^}
42	34, 41	xaddcld 11583	. . . . 5 Σ^{^} Σ^{^}
43	42	adantr 466	. . . 4 $/\$ Σ^{^} Σ^{^} Σ^{^}
44		pnfxr 11408	. . . . . . . . 9
45		eqid 2420	. . . . . . . . 9
46		xreqle 37364	. . . . . . . . 9 $/\$
47	44, 45, 46	mp2an 676	. . . . . . . 8
48	47	a1i 11	. . . . . . 7 $/\$
49	14	adantr 466	. . . . . . . . 9 $/\$
50	8	adantr 466	. . . . . . . . 9 $/\$
51		rnresss 37289	. . . . . . . . . . 11
52	51	sseli 3457	. . . . . . . . . 10
53	52	adantl 467	. . . . . . . . 9 $/\$
54	49, 50, 53	sge0pnfval 37970	. . . . . . . 8 $/\$ Σ^{^}
55		ge0nemnf2 37430	. . . . . . . . . . . . . 14 Σ^{^} Σ^{^}
56	40, 55	syl 17	. . . . . . . . . . . . 13 Σ^{^}
57		xaddpnf2 11516	. . . . . . . . . . . . 13 Σ^{^} $/\$ Σ^{^} Σ^{^}
58	41, 56, 57	syl2anc 665	. . . . . . . . . . . 12 Σ^{^}
59	58	eqcomd 2428	. . . . . . . . . . 11 Σ^{^}
60	59	adantr 466	. . . . . . . . . 10 $/\$ Σ^{^}
61	1	adantr 466	. . . . . . . . . . . 12 $/\$
62	33	adantr 466	. . . . . . . . . . . 12 $/\$
63		simpr 462	. . . . . . . . . . . 12 $/\$
64	61, 62, 63	sge0pnfval 37970	. . . . . . . . . . 11 $/\$ Σ^{^}
65	64	oveq1d 6312	. . . . . . . . . 10 $/\$ Σ^{^} Σ^{^} Σ^{^}
66	60, 54, 65	3eqtr4d 2471	. . . . . . . . 9 $/\$ Σ^{^} Σ^{^} Σ^{^}
67	66, 54	eqtr3d 2463	. . . . . . . 8 $/\$ Σ^{^} Σ^{^}
68	54, 67	breq12d 4430	. . . . . . 7 $/\$ Σ^{^} Σ^{^} Σ^{^}
69	48, 68	mpbird 235	. . . . . 6 $/\$ Σ^{^} Σ^{^} Σ^{^}
70	47	a1i 11	. . . . . . . . 9 $/\$
71	14	adantr 466	. . . . . . . . . . 11 $/\$
72	8	adantr 466	. . . . . . . . . . 11 $/\$
73		rnresss 37289	. . . . . . . . . . . . 13
74	73	sseli 3457	. . . . . . . . . . . 12
75	74	adantl 467	. . . . . . . . . . 11 $/\$
76	71, 72, 75	sge0pnfval 37970	. . . . . . . . . 10 $/\$ Σ^{^}
77	3	adantr 466	. . . . . . . . . . . . 13 $/\$
78	39	adantr 466	. . . . . . . . . . . . 13 $/\$
79		simpr 462	. . . . . . . . . . . . 13 $/\$
80	77, 78, 79	sge0pnfval 37970	. . . . . . . . . . . 12 $/\$ Σ^{^}
81	80	oveq2d 6313	. . . . . . . . . . 11 $/\$ Σ^{^} Σ^{^} Σ^{^}
82	1, 33	sge0cl 37978	. . . . . . . . . . . . . 14 Σ^{^}
83		ge0nemnf2 37430	. . . . . . . . . . . . . 14 Σ^{^} Σ^{^}
84	82, 83	syl 17	. . . . . . . . . . . . 13 Σ^{^}
85		xaddpnf1 11515	. . . . . . . . . . . . 13 Σ^{^} $/\$ Σ^{^} Σ^{^}
86	34, 84, 85	syl2anc 665	. . . . . . . . . . . 12 Σ^{^}
87	86	adantr 466	. . . . . . . . . . 11 $/\$ Σ^{^}
88	81, 87	eqtrd 2461	. . . . . . . . . 10 $/\$ Σ^{^} Σ^{^}
89	76, 88	breq12d 4430	. . . . . . . . 9 $/\$ Σ^{^} Σ^{^} Σ^{^}
90	70, 89	mpbird 235	. . . . . . . 8 $/\$ Σ^{^} Σ^{^} Σ^{^}
91	90	adantlr 719	. . . . . . 7 $/\$ $/\$ Σ^{^} Σ^{^} Σ^{^}
92		simpr 462	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
93		vex 3081	. . . . . . . . . . . . 13
94		eqid 2420	. . . . . . . . . . . . . 14
95	94	elrnmpt 5093	. . . . . . . . . . . . 13
96	93, 95	ax-mp 5	. . . . . . . . . . . 12
97	92, 96	sylib 199	. . . . . . . . . . 11 $/\$ $/\$ $/\$
98		simp3 1007	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
99		inss1 3679	. . . . . . . . . . . . . . . . . . . . . . . . 25
100		inss2 3680	. . . . . . . . . . . . . . . . . . . . . . . . 25
101	99, 100	sstri 3470	. . . . . . . . . . . . . . . . . . . . . . . 24
102		inss2 3680	. . . . . . . . . . . . . . . . . . . . . . . . 25
103		inss2 3680	. . . . . . . . . . . . . . . . . . . . . . . . 25
104	102, 103	sstri 3470	. . . . . . . . . . . . . . . . . . . . . . . 24
105	101, 104	ssini 3682	. . . . . . . . . . . . . . . . . . . . . . 23
106	105	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
107	106, 6	sseqtrd 3497	. . . . . . . . . . . . . . . . . . . . 21
108		ss0 3790	. . . . . . . . . . . . . . . . . . . . 21
109	107, 108	syl 17	. . . . . . . . . . . . . . . . . . . 20
110	109	ad3antrrr 734	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
111		indi 3716	. . . . . . . . . . . . . . . . . . . . . . 23
112	111	eqcomi 2433	. . . . . . . . . . . . . . . . . . . . . 22
113	112	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
114	5	eqcomi 2433	. . . . . . . . . . . . . . . . . . . . . . 23
115	114	ineq2i 3658	. . . . . . . . . . . . . . . . . . . . . 22
116	115	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
117		elinel1 3648	. . . . . . . . . . . . . . . . . . . . . . 23
118		elpwi 3985	. . . . . . . . . . . . . . . . . . . . . . 23
119	117, 118	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
120		df-ss 3447	. . . . . . . . . . . . . . . . . . . . . . 23
121	120	biimpi 197	. . . . . . . . . . . . . . . . . . . . . 22
122	119, 121	syl 17	. . . . . . . . . . . . . . . . . . . . 21
123	113, 116, 122	3eqtrrd 2466	. . . . . . . . . . . . . . . . . . . 20
124	123	adantl 467	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
125		elinel2 3649	. . . . . . . . . . . . . . . . . . . 20
126	125	adantl 467	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
127		rge0ssre 11734	. . . . . . . . . . . . . . . . . . . . 21
128	8	ad2antrr 730	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
129		pm4.56 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\/$
130	129	biimpi 197	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\/$
131		elun 3603	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\/$
132	130, 131	sylnibr 306	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
133	132	adantll 718	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
134		rnresun 37286	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
135	134	eqcomi 2433	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
136	135	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
137	114	reseq2i 5114	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
138	137	rneqi 5073	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
139	138	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
140		ffn 5738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
141		fnresdm 5695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
142	8, 140, 141	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
143	142	rneqd 5074	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
144	136, 139, 143	3eqtrd 2465	. . . . . . . . . . . . . . . . . . . . . . . . . 26
145	144	ad2antrr 730	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
146	133, 145	neleqtrd 2532	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
147	128, 146	fge0iccico 37967	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
148	147	ad2antrr 730	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
149	119	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
150		simpr 462	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
151	149, 150	sseldd 3462	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
152	151	adantll 718	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
153	148, 152	ffvelrnd 6030	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
154	127, 153	sseldi 3459	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
155	154	recnd 9665	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
156	110, 124, 126, 155	fsumsplit 13784	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
157		infi 7793	. . . . . . . . . . . . . . . . . . . . . . 23
158	125, 157	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
159	158	adantl 467	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
160		simpl 458	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
161		elinel1 3648	. . . . . . . . . . . . . . . . . . . . . . 23
162	161	adantl 467	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
163	160, 162, 154	syl2anc 665	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
164	159, 163	fsumrecl 13778	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
165		infi 7793	. . . . . . . . . . . . . . . . . . . . . . 23
166	125, 165	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
167	166	adantl 467	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
168		simpl 458	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
169		elinel1 3648	. . . . . . . . . . . . . . . . . . . . . . 23
170	169	adantl 467	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
171	168, 170, 154	syl2anc 665	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
172	167, 171	fsumrecl 13778	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
173		rexadd 11521	. . . . . . . . . . . . . . . . . . . 20 $/\$
174	164, 172, 173	syl2anc 665	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
175	174	eqcomd 2428	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
176	156, 175	eqtrd 2461	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
177		ressxr 9680	. . . . . . . . . . . . . . . . . . . 20
178	177, 164	sseldi 3459	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
179	177, 172	sseldi 3459	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
180	1	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
181	33	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
182		simpr 462	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
183	181, 182	fge0iccico 37967	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
184	180, 183	sge0reval 37969	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ Σ^{^}
185	184	eqcomd 2428	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ Σ^{^}
186	34	adantr 466	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ Σ^{^}
187	185, 186	eqeltrd 2508	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
188	187	adantr 466	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
189	3	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
190	39	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
191		simpr 462	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
192	190, 191	fge0iccico 37967	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
193	189, 192	sge0reval 37969	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ Σ^{^}
194	193	eqcomd 2428	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ Σ^{^}
195	41	adantr 466	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ Σ^{^}
196	194, 195	eqeltrd 2508	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
197	196	adantlr 719	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
198	188, 197	jca 534	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
199	198	adantr 466	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
200	178, 179, 199	jca31 536	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
201	180	adantr 466	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
202	181	adantr 466	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
203	182	adantr 466	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
204	202, 203	fge0iccico 37967	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
205	100	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
206	158	adantl 467	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
207	201, 204, 205, 206	fsumlesge0 37974	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ Σ^{^}
208	100	sseli 3457	. . . . . . . . . . . . . . . . . . . . . . . . 25
209		fvres 5887	. . . . . . . . . . . . . . . . . . . . . . . . 25
210	208, 209	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
211	210	adantl 467	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
212	211	sumeq2dv 13747	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
213	184	adantr 466	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ Σ^{^}
214	212, 213	breq12d 4430	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ Σ^{^}
215	207, 214	mpbid 213	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
216	215	adantlr 719	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
217	189	adantr 466	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
218	190	adantr 466	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
219	191	adantr 466	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
220	218, 219	fge0iccico 37967	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
221	103	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
222	166	adantl 467	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
223	217, 220, 221, 222	fsumlesge0 37974	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ Σ^{^}
224	103	sseli 3457	. . . . . . . . . . . . . . . . . . . . . . . . 25
225		fvres 5887	. . . . . . . . . . . . . . . . . . . . . . . . 25
226	224, 225	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
227	226	adantl 467	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
228	227	sumeq2dv 13747	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
229	193	adantr 466	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ Σ^{^}
230	228, 229	breq12d 4430	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ Σ^{^}
231	223, 230	mpbid 213	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
232	231	adantllr 723	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
233	216, 232	jca 534	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
234		xle2add 11541	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
235	200, 233, 234	sylc 62	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
236	176, 235	eqbrtrd 4438	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
237	236	3adant3 1025	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
238	98, 237	eqbrtrd 4438	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
239	238	3exp 1204	. . . . . . . . . . . . 13 $/\$ $/\$
240	239	rexlimdv 2913	. . . . . . . . . . . 12 $/\$ $/\$
241	240	adantr 466	. . . . . . . . . . 11 $/\$ $/\$ $/\$
242	97, 241	mpd 15	. . . . . . . . . 10 $/\$ $/\$ $/\$
243	242	ralrimiva 2837	. . . . . . . . 9 $/\$ $/\$
244	147	sge0rnre 37961	. . . . . . . . . . 11 $/\$ $/\$
245	177	a1i 11	. . . . . . . . . . 11 $/\$ $/\$
246	244, 245	sstrd 3471	. . . . . . . . . 10 $/\$ $/\$
247	188, 197	xaddcld 11583	. . . . . . . . . 10 $/\$ $/\$
248		supxrleub 11608	. . . . . . . . . 10 $/\$
249	246, 247, 248	syl2anc 665	. . . . . . . . 9 $/\$ $/\$
250	243, 249	mpbird 235	. . . . . . . 8 $/\$ $/\$
251	14	ad2antrr 730	. . . . . . . . 9 $/\$ $/\$
252	251, 147	sge0reval 37969	. . . . . . . 8 $/\$ $/\$ Σ^{^}
253	184	adantr 466	. . . . . . . . 9 $/\$ $/\$ Σ^{^}
254	193	adantlr 719	. . . . . . . . 9 $/\$ $/\$ Σ^{^}
255	253, 254	oveq12d 6315	. . . . . . . 8 $/\$ $/\$ Σ^{^} Σ^{^}
256	250, 252, 255	3brtr4d 4448	. . . . . . 7 $/\$ $/\$ Σ^{^} Σ^{^} Σ^{^}
257	91, 256	pm2.61dan 798	. . . . . 6 $/\$ Σ^{^} Σ^{^} Σ^{^}
258	69, 257	pm2.61dan 798	. . . . 5 Σ^{^} Σ^{^} Σ^{^}
259	258	adantr 466	. . . 4 $/\$ Σ^{^} Σ^{^} Σ^{^} Σ^{^}
260		pnfge 11428	. . . . . . 7 Σ^{^} Σ^{^} Σ^{^} Σ^{^}
261	42, 260	syl 17	. . . . . 6 Σ^{^} Σ^{^}
262	261	adantr 466	. . . . 5 $/\$ Σ^{^} Σ^{^} Σ^{^}
263		id 23	. . . . . . 7 Σ^{^} Σ^{^}
264	263	eqcomd 2428	. . . . . 6 Σ^{^} Σ^{^}
265	264	adantl 467	. . . . 5 $/\$ Σ^{^} Σ^{^}
266	262, 265	breqtrd 4442	. . . 4 $/\$ Σ^{^} Σ^{^} Σ^{^} Σ^{^}
267	29, 43, 259, 266	xrletrid 11448	. . 3 $/\$ Σ^{^} Σ^{^} Σ^{^} Σ^{^}
268	22, 27, 267	syl2anc 665	. 2 $/\$ Σ^{^} Σ^{^} Σ^{^} Σ^{^}
269	21, 268	pm2.61dan 798	1 Σ^{^} Σ^{^} Σ^{^}

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 187 $\/$ wo 369 $/\$ wa 370 $/\$ w3a 982

wceq 1437

wcel 1867

wne 2616

wral 2773

wrex 2774

cvv 3078

cun 3431

cin 3432

wss 3433

c0 3758

cpw 3976 class class class wbr 4417

cmpt 4476

crn 4847

cres 4848

wfn 5588

wf 5589

cfv 5593 (class class class)co 6297

cfn 7569

csup 7952

cr 9534

cc0 9535

caddc 9538

cpnf 9668

cmnf 9669

cxr 9670

clt 9671

cle 9672

cxad 11403

cico 11633

cicc 11634

csu 13730 Σ^{^}csumge0 37959

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1748 ax-6 1794 ax-7 1838 ax-8 1869 ax-9 1871 ax-10 1886 ax-11 1891 ax-12 1904 ax-13 2052 ax-ext 2398 ax-rep 4530 ax-sep 4540 ax-nul 4548 ax-pow 4595 ax-pr 4653 ax-un 6589 ax-inf2 8144 ax-cnex 9591 ax-resscn 9592 ax-1cn 9593 ax-icn 9594 ax-addcl 9595 ax-addrcl 9596 ax-mulcl 9597 ax-mulrcl 9598 ax-mulcom 9599 ax-addass 9600 ax-mulass 9601 ax-distr 9602 ax-i2m1 9603 ax-1ne0 9604 ax-1rid 9605 ax-rnegex 9606 ax-rrecex 9607 ax-cnre 9608 ax-pre-lttri 9609 ax-pre-lttrn 9610 ax-pre-ltadd 9611 ax-pre-mulgt0 9612 ax-pre-sup 9613

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-fal 1443 df-ex 1660 df-nf 1664 df-sb 1787 df-eu 2267 df-mo 2268 df-clab 2406 df-cleq 2412 df-clel 2415 df-nfc 2570 df-ne 2618 df-nel 2619 df-ral 2778 df-rex 2779 df-reu 2780 df-rmo 2781 df-rab 2782 df-v 3080 df-sbc 3297 df-csb 3393 df-dif 3436 df-un 3438 df-in 3440 df-ss 3447 df-pss 3449 df-nul 3759 df-if 3907 df-pw 3978 df-sn 3994 df-pr 3996 df-tp 3998 df-op 4000 df-uni 4214 df-int 4250 df-iun 4295 df-br 4418 df-opab 4477 df-mpt 4478 df-tr 4513 df-eprel 4757 df-id 4761 df-po 4767 df-so 4768 df-fr 4805 df-se 4806 df-we 4807 df-xp 4852 df-rel 4853 df-cnv 4854 df-co 4855 df-dm 4856 df-rn 4857 df-res 4858 df-ima 4859 df-pred 5391 df-ord 5437 df-on 5438 df-lim 5439 df-suc 5440 df-iota 5557 df-fun 5595 df-fn 5596 df-f 5597 df-f1 5598 df-fo 5599 df-f1o 5600 df-fv 5601 df-isom 5602 df-riota 6259 df-ov 6300 df-oprab 6301 df-mpt2 6302 df-om 6699 df-1st 6799 df-2nd 6800 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-1o 7182 df-oadd 7186 df-er 7363 df-en 7570 df-dom 7571 df-sdom 7572 df-fin 7573 df-sup 7954 df-oi 8023 df-card 8370 df-pnf 9673 df-mnf 9674 df-xr 9675 df-ltxr 9676 df-le 9677 df-sub 9858 df-neg 9859 df-div 10266 df-nn 10606 df-2 10664 df-3 10665 df-n0 10866 df-z 10934 df-uz 11156 df-rp 11299 df-xadd 11406 df-ico 11637 df-icc 11638 df-fz 11779 df-fzo 11910 df-seq 12207 df-exp 12266 df-hash 12509 df-cj 13141 df-re 13142 df-im 13143 df-sqrt 13277 df-abs 13278 df-clim 13530 df-sum 13731 df-sumge0 37960

This theorem is referenced by: sge0splitmpt 38008

W3C validator