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 38245

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 467	. . . 4 $/\$ Σ^{^}
3		sge0split.b	. . . . 5
4	3	adantr 467	. . . 4 $/\$ Σ^{^}
5		sge0split.u	. . . 4
6		sge0split.in0	. . . . 5
7	6	adantr 467	. . . 4 $/\$ Σ^{^}
8		sge0split.f	. . . . 5
9	8	adantr 467	. . . 4 $/\$ Σ^{^}
10		simpr 463	. . . 4 $/\$ Σ^{^} Σ^{^}
11	2, 4, 5, 7, 9, 10	sge0resplit 38242	. . 3 $/\$ Σ^{^} Σ^{^} Σ^{^} Σ^{^}
12		unexg 6589	. . . . . . . . 9 $/\$
13	1, 3, 12	syl2anc 666	. . . . . . . 8
14	5, 13	syl5eqel 2532	. . . . . . 7
15	14	adantr 467	. . . . . 6 $/\$ Σ^{^}
16	15, 9, 10	sge0ssre 38233	. . . . 5 $/\$ Σ^{^} Σ^{^}
17	15, 9, 10	sge0ssre 38233	. . . . 5 $/\$ Σ^{^} Σ^{^}
18		rexadd 11522	. . . . 5 Σ^{^} $/\$ Σ^{^} Σ^{^} Σ^{^} Σ^{^} Σ^{^}
19	16, 17, 18	syl2anc 666	. . . 4 $/\$ Σ^{^} Σ^{^} Σ^{^} Σ^{^} Σ^{^}
20	19	eqcomd 2456	. . 3 $/\$ Σ^{^} Σ^{^} Σ^{^} Σ^{^} Σ^{^}
21	11, 20	eqtrd 2484	. 2 $/\$ Σ^{^} Σ^{^} Σ^{^} Σ^{^}
22		simpl 459	. . 3 $/\$ Σ^{^}
23		simpr 463	. . . . 5 $/\$ Σ^{^} Σ^{^}
24	14, 8	sge0repnf 38222	. . . . . 6 Σ^{^} Σ^{^}
25	24	adantr 467	. . . . 5 $/\$ Σ^{^} Σ^{^} Σ^{^}
26	23, 25	mtbid 302	. . . 4 $/\$ Σ^{^} Σ^{^}
27	26	notnotrd 117	. . 3 $/\$ Σ^{^} Σ^{^}
28	14, 8	sge0xrcl 38221	. . . . 5 Σ^{^}
29	28	adantr 467	. . . 4 $/\$ Σ^{^} Σ^{^}
30		ssun1 3596	. . . . . . . . . 10
31	30, 5	sseqtr4i 3464	. . . . . . . . 9
32	31	a1i 11	. . . . . . . 8
33	8, 32	fssresd 5748	. . . . . . 7
34	1, 33	sge0xrcl 38221	. . . . . 6 Σ^{^}
35		iccssxr 11714	. . . . . . 7
36		ssun2 3597	. . . . . . . . . . 11
37	36, 5	sseqtr4i 3464	. . . . . . . . . 10
38	37	a1i 11	. . . . . . . . 9
39	8, 38	fssresd 5748	. . . . . . . 8
40	3, 39	sge0cl 38217	. . . . . . 7 Σ^{^}
41	35, 40	sseldi 3429	. . . . . 6 Σ^{^}
42	34, 41	xaddcld 11584	. . . . 5 Σ^{^} Σ^{^}
43	42	adantr 467	. . . 4 $/\$ Σ^{^} Σ^{^} Σ^{^}
44		pnfxr 11409	. . . . . . . . 9
45		eqid 2450	. . . . . . . . 9
46		xreqle 37534	. . . . . . . . 9 $/\$
47	44, 45, 46	mp2an 677	. . . . . . . 8
48	47	a1i 11	. . . . . . 7 $/\$
49	14	adantr 467	. . . . . . . . 9 $/\$
50	8	adantr 467	. . . . . . . . 9 $/\$
51		rnresss 37445	. . . . . . . . . . 11
52	51	sseli 3427	. . . . . . . . . 10
53	52	adantl 468	. . . . . . . . 9 $/\$
54	49, 50, 53	sge0pnfval 38209	. . . . . . . 8 $/\$ Σ^{^}
55		ge0nemnf2 37624	. . . . . . . . . . . . . 14 Σ^{^} Σ^{^}
56	40, 55	syl 17	. . . . . . . . . . . . 13 Σ^{^}
57		xaddpnf2 11517	. . . . . . . . . . . . 13 Σ^{^} $/\$ Σ^{^} Σ^{^}
58	41, 56, 57	syl2anc 666	. . . . . . . . . . . 12 Σ^{^}
59	58	eqcomd 2456	. . . . . . . . . . 11 Σ^{^}
60	59	adantr 467	. . . . . . . . . 10 $/\$ Σ^{^}
61	1	adantr 467	. . . . . . . . . . . 12 $/\$
62	33	adantr 467	. . . . . . . . . . . 12 $/\$
63		simpr 463	. . . . . . . . . . . 12 $/\$
64	61, 62, 63	sge0pnfval 38209	. . . . . . . . . . 11 $/\$ Σ^{^}
65	64	oveq1d 6303	. . . . . . . . . 10 $/\$ Σ^{^} Σ^{^} Σ^{^}
66	60, 54, 65	3eqtr4d 2494	. . . . . . . . 9 $/\$ Σ^{^} Σ^{^} Σ^{^}
67	66, 54	eqtr3d 2486	. . . . . . . 8 $/\$ Σ^{^} Σ^{^}
68	54, 67	breq12d 4414	. . . . . . 7 $/\$ Σ^{^} Σ^{^} Σ^{^}
69	48, 68	mpbird 236	. . . . . 6 $/\$ Σ^{^} Σ^{^} Σ^{^}
70	47	a1i 11	. . . . . . . . 9 $/\$
71	14	adantr 467	. . . . . . . . . . 11 $/\$
72	8	adantr 467	. . . . . . . . . . 11 $/\$
73		rnresss 37445	. . . . . . . . . . . . 13
74	73	sseli 3427	. . . . . . . . . . . 12
75	74	adantl 468	. . . . . . . . . . 11 $/\$
76	71, 72, 75	sge0pnfval 38209	. . . . . . . . . 10 $/\$ Σ^{^}
77	3	adantr 467	. . . . . . . . . . . . 13 $/\$
78	39	adantr 467	. . . . . . . . . . . . 13 $/\$
79		simpr 463	. . . . . . . . . . . . 13 $/\$
80	77, 78, 79	sge0pnfval 38209	. . . . . . . . . . . 12 $/\$ Σ^{^}
81	80	oveq2d 6304	. . . . . . . . . . 11 $/\$ Σ^{^} Σ^{^} Σ^{^}
82	1, 33	sge0cl 38217	. . . . . . . . . . . . . 14 Σ^{^}
83		ge0nemnf2 37624	. . . . . . . . . . . . . 14 Σ^{^} Σ^{^}
84	82, 83	syl 17	. . . . . . . . . . . . 13 Σ^{^}
85		xaddpnf1 11516	. . . . . . . . . . . . 13 Σ^{^} $/\$ Σ^{^} Σ^{^}
86	34, 84, 85	syl2anc 666	. . . . . . . . . . . 12 Σ^{^}
87	86	adantr 467	. . . . . . . . . . 11 $/\$ Σ^{^}
88	81, 87	eqtrd 2484	. . . . . . . . . 10 $/\$ Σ^{^} Σ^{^}
89	76, 88	breq12d 4414	. . . . . . . . 9 $/\$ Σ^{^} Σ^{^} Σ^{^}
90	70, 89	mpbird 236	. . . . . . . 8 $/\$ Σ^{^} Σ^{^} Σ^{^}
91	90	adantlr 720	. . . . . . 7 $/\$ $/\$ Σ^{^} Σ^{^} Σ^{^}
92		simpr 463	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
93		vex 3047	. . . . . . . . . . . . 13
94		eqid 2450	. . . . . . . . . . . . . 14
95	94	elrnmpt 5080	. . . . . . . . . . . . 13
96	93, 95	ax-mp 5	. . . . . . . . . . . 12
97	92, 96	sylib 200	. . . . . . . . . . 11 $/\$ $/\$ $/\$
98		simp3 1009	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
99		inss1 3651	. . . . . . . . . . . . . . . . . . . . . . . . 25
100		inss2 3652	. . . . . . . . . . . . . . . . . . . . . . . . 25
101	99, 100	sstri 3440	. . . . . . . . . . . . . . . . . . . . . . . 24
102		inss2 3652	. . . . . . . . . . . . . . . . . . . . . . . . 25
103		inss2 3652	. . . . . . . . . . . . . . . . . . . . . . . . 25
104	102, 103	sstri 3440	. . . . . . . . . . . . . . . . . . . . . . . 24
105	101, 104	ssini 3654	. . . . . . . . . . . . . . . . . . . . . . 23
106	105	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
107	106, 6	sseqtrd 3467	. . . . . . . . . . . . . . . . . . . . 21
108		ss0 3764	. . . . . . . . . . . . . . . . . . . . 21
109	107, 108	syl 17	. . . . . . . . . . . . . . . . . . . 20
110	109	ad3antrrr 735	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
111		indi 3688	. . . . . . . . . . . . . . . . . . . . . . 23
112	111	eqcomi 2459	. . . . . . . . . . . . . . . . . . . . . 22
113	112	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
114	5	eqcomi 2459	. . . . . . . . . . . . . . . . . . . . . . 23
115	114	ineq2i 3630	. . . . . . . . . . . . . . . . . . . . . 22
116	115	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
117		elinel1 3618	. . . . . . . . . . . . . . . . . . . . . . 23
118		elpwi 3959	. . . . . . . . . . . . . . . . . . . . . . 23
119	117, 118	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
120		df-ss 3417	. . . . . . . . . . . . . . . . . . . . . . 23
121	120	biimpi 198	. . . . . . . . . . . . . . . . . . . . . 22
122	119, 121	syl 17	. . . . . . . . . . . . . . . . . . . . 21
123	113, 116, 122	3eqtrrd 2489	. . . . . . . . . . . . . . . . . . . 20
124	123	adantl 468	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
125		elinel2 3619	. . . . . . . . . . . . . . . . . . . 20
126	125	adantl 468	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
127		rge0ssre 11737	. . . . . . . . . . . . . . . . . . . . 21
128	8	ad2antrr 731	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
129		pm4.56 498	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\/$
130	129	biimpi 198	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\/$
131		elun 3573	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\/$
132	130, 131	sylnibr 307	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
133	132	adantll 719	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
134		rnresun 37442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
135	134	eqcomi 2459	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
136	135	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
137	114	reseq2i 5101	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
138	137	rneqi 5060	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
139	138	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
140		ffn 5726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
141		fnresdm 5683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
142	8, 140, 141	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
143	142	rneqd 5061	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
144	136, 139, 143	3eqtrd 2488	. . . . . . . . . . . . . . . . . . . . . . . . . 26
145	144	ad2antrr 731	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
146	133, 145	neleqtrd 2549	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
147	128, 146	fge0iccico 38206	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
148	147	ad2antrr 731	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
149	119	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
150		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
151	149, 150	sseldd 3432	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
152	151	adantll 719	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
153	148, 152	ffvelrnd 6021	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
154	127, 153	sseldi 3429	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
155	154	recnd 9666	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
156	110, 124, 126, 155	fsumsplit 13799	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
157		infi 7792	. . . . . . . . . . . . . . . . . . . . . . 23
158	125, 157	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
159	158	adantl 468	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
160		simpl 459	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
161		elinel1 3618	. . . . . . . . . . . . . . . . . . . . . . 23
162	161	adantl 468	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
163	160, 162, 154	syl2anc 666	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
164	159, 163	fsumrecl 13793	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
165		infi 7792	. . . . . . . . . . . . . . . . . . . . . . 23
166	125, 165	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
167	166	adantl 468	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
168		simpl 459	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
169		elinel1 3618	. . . . . . . . . . . . . . . . . . . . . . 23
170	169	adantl 468	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
171	168, 170, 154	syl2anc 666	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
172	167, 171	fsumrecl 13793	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
173		rexadd 11522	. . . . . . . . . . . . . . . . . . . 20 $/\$
174	164, 172, 173	syl2anc 666	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
175	174	eqcomd 2456	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
176	156, 175	eqtrd 2484	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
177		ressxr 9681	. . . . . . . . . . . . . . . . . . . 20
178	177, 164	sseldi 3429	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
179	177, 172	sseldi 3429	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
180	1	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
181	33	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
182		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
183	181, 182	fge0iccico 38206	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
184	180, 183	sge0reval 38208	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ Σ^{^}
185	184	eqcomd 2456	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ Σ^{^}
186	34	adantr 467	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ Σ^{^}
187	185, 186	eqeltrd 2528	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
188	187	adantr 467	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
189	3	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
190	39	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
191		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
192	190, 191	fge0iccico 38206	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
193	189, 192	sge0reval 38208	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ Σ^{^}
194	193	eqcomd 2456	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ Σ^{^}
195	41	adantr 467	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ Σ^{^}
196	194, 195	eqeltrd 2528	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
197	196	adantlr 720	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
198	188, 197	jca 535	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
199	198	adantr 467	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
200	178, 179, 199	jca31 537	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
201	180	adantr 467	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
202	181	adantr 467	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
203	182	adantr 467	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
204	202, 203	fge0iccico 38206	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
205	100	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
206	158	adantl 468	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
207	201, 204, 205, 206	fsumlesge0 38213	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ Σ^{^}
208	100	sseli 3427	. . . . . . . . . . . . . . . . . . . . . . . . 25
209		fvres 5877	. . . . . . . . . . . . . . . . . . . . . . . . 25
210	208, 209	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
211	210	adantl 468	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
212	211	sumeq2dv 13762	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
213	184	adantr 467	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ Σ^{^}
214	212, 213	breq12d 4414	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ Σ^{^}
215	207, 214	mpbid 214	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
216	215	adantlr 720	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
217	189	adantr 467	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
218	190	adantr 467	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
219	191	adantr 467	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
220	218, 219	fge0iccico 38206	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
221	103	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
222	166	adantl 468	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
223	217, 220, 221, 222	fsumlesge0 38213	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ Σ^{^}
224	103	sseli 3427	. . . . . . . . . . . . . . . . . . . . . . . . 25
225		fvres 5877	. . . . . . . . . . . . . . . . . . . . . . . . 25
226	224, 225	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
227	226	adantl 468	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
228	227	sumeq2dv 13762	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
229	193	adantr 467	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ Σ^{^}
230	228, 229	breq12d 4414	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ Σ^{^}
231	223, 230	mpbid 214	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
232	231	adantllr 724	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
233	216, 232	jca 535	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
234		xle2add 11542	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
235	200, 233, 234	sylc 62	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
236	176, 235	eqbrtrd 4422	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
237	236	3adant3 1027	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
238	98, 237	eqbrtrd 4422	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
239	238	3exp 1206	. . . . . . . . . . . . 13 $/\$ $/\$
240	239	rexlimdv 2876	. . . . . . . . . . . 12 $/\$ $/\$
241	240	adantr 467	. . . . . . . . . . 11 $/\$ $/\$ $/\$
242	97, 241	mpd 15	. . . . . . . . . 10 $/\$ $/\$ $/\$
243	242	ralrimiva 2801	. . . . . . . . 9 $/\$ $/\$
244	147	sge0rnre 38200	. . . . . . . . . . 11 $/\$ $/\$
245	177	a1i 11	. . . . . . . . . . 11 $/\$ $/\$
246	244, 245	sstrd 3441	. . . . . . . . . 10 $/\$ $/\$
247	188, 197	xaddcld 11584	. . . . . . . . . 10 $/\$ $/\$
248		supxrleub 11609	. . . . . . . . . 10 $/\$
249	246, 247, 248	syl2anc 666	. . . . . . . . 9 $/\$ $/\$
250	243, 249	mpbird 236	. . . . . . . 8 $/\$ $/\$
251	14	ad2antrr 731	. . . . . . . . 9 $/\$ $/\$
252	251, 147	sge0reval 38208	. . . . . . . 8 $/\$ $/\$ Σ^{^}
253	184	adantr 467	. . . . . . . . 9 $/\$ $/\$ Σ^{^}
254	193	adantlr 720	. . . . . . . . 9 $/\$ $/\$ Σ^{^}
255	253, 254	oveq12d 6306	. . . . . . . 8 $/\$ $/\$ Σ^{^} Σ^{^}
256	250, 252, 255	3brtr4d 4432	. . . . . . 7 $/\$ $/\$ Σ^{^} Σ^{^} Σ^{^}
257	91, 256	pm2.61dan 799	. . . . . 6 $/\$ Σ^{^} Σ^{^} Σ^{^}
258	69, 257	pm2.61dan 799	. . . . 5 Σ^{^} Σ^{^} Σ^{^}
259	258	adantr 467	. . . 4 $/\$ Σ^{^} Σ^{^} Σ^{^} Σ^{^}
260		pnfge 11429	. . . . . . 7 Σ^{^} Σ^{^} Σ^{^} Σ^{^}
261	42, 260	syl 17	. . . . . 6 Σ^{^} Σ^{^}
262	261	adantr 467	. . . . 5 $/\$ Σ^{^} Σ^{^} Σ^{^}
263		id 22	. . . . . . 7 Σ^{^} Σ^{^}
264	263	eqcomd 2456	. . . . . 6 Σ^{^} Σ^{^}
265	264	adantl 468	. . . . 5 $/\$ Σ^{^} Σ^{^}
266	262, 265	breqtrd 4426	. . . 4 $/\$ Σ^{^} Σ^{^} Σ^{^} Σ^{^}
267	29, 43, 259, 266	xrletrid 11449	. . 3 $/\$ Σ^{^} Σ^{^} Σ^{^} Σ^{^}
268	22, 27, 267	syl2anc 666	. 2 $/\$ Σ^{^} Σ^{^} Σ^{^} Σ^{^}
269	21, 268	pm2.61dan 799	1 Σ^{^} Σ^{^} Σ^{^}

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $\/$ wo 370 $/\$ wa 371 $/\$ w3a 984

wceq 1443

wcel 1886

wne 2621

wral 2736

wrex 2737

cvv 3044

cun 3401

cin 3402

wss 3403

c0 3730

cpw 3950 class class class wbr 4401

cmpt 4460

crn 4834

cres 4835

wfn 5576

wf 5577

cfv 5581 (class class class)co 6288

cfn 7566

csup 7951

cr 9535

cc0 9536

caddc 9539

cpnf 9669

cmnf 9670

cxr 9671

clt 9672

cle 9673

cxad 11404

cico 11634

cicc 11635

csu 13745 Σ^{^}csumge0 38198

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-8 1888 ax-9 1895 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-rep 4514 ax-sep 4524 ax-nul 4533 ax-pow 4580 ax-pr 4638 ax-un 6580 ax-inf2 8143 ax-cnex 9592 ax-resscn 9593 ax-1cn 9594 ax-icn 9595 ax-addcl 9596 ax-addrcl 9597 ax-mulcl 9598 ax-mulrcl 9599 ax-mulcom 9600 ax-addass 9601 ax-mulass 9602 ax-distr 9603 ax-i2m1 9604 ax-1ne0 9605 ax-1rid 9606 ax-rnegex 9607 ax-rrecex 9608 ax-cnre 9609 ax-pre-lttri 9610 ax-pre-lttrn 9611 ax-pre-ltadd 9612 ax-pre-mulgt0 9613 ax-pre-sup 9614

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 985 df-3an 986 df-tru 1446 df-fal 1449 df-ex 1663 df-nf 1667 df-sb 1797 df-eu 2302 df-mo 2303 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-nel 2624 df-ral 2741 df-rex 2742 df-reu 2743 df-rmo 2744 df-rab 2745 df-v 3046 df-sbc 3267 df-csb 3363 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-pss 3419 df-nul 3731 df-if 3881 df-pw 3952 df-sn 3968 df-pr 3970 df-tp 3972 df-op 3974 df-uni 4198 df-int 4234 df-iun 4279 df-br 4402 df-opab 4461 df-mpt 4462 df-tr 4497 df-eprel 4744 df-id 4748 df-po 4754 df-so 4755 df-fr 4792 df-se 4793 df-we 4794 df-xp 4839 df-rel 4840 df-cnv 4841 df-co 4842 df-dm 4843 df-rn 4844 df-res 4845 df-ima 4846 df-pred 5379 df-ord 5425 df-on 5426 df-lim 5427 df-suc 5428 df-iota 5545 df-fun 5583 df-fn 5584 df-f 5585 df-f1 5586 df-fo 5587 df-f1o 5588 df-fv 5589 df-isom 5590 df-riota 6250 df-ov 6291 df-oprab 6292 df-mpt2 6293 df-om 6690 df-1st 6790 df-2nd 6791 df-wrecs 7025 df-recs 7087 df-rdg 7125 df-1o 7179 df-oadd 7183 df-er 7360 df-en 7567 df-dom 7568 df-sdom 7569 df-fin 7570 df-sup 7953 df-oi 8022 df-card 8370 df-pnf 9674 df-mnf 9675 df-xr 9676 df-ltxr 9677 df-le 9678 df-sub 9859 df-neg 9860 df-div 10267 df-nn 10607 df-2 10665 df-3 10666 df-n0 10867 df-z 10935 df-uz 11157 df-rp 11300 df-xadd 11407 df-ico 11638 df-icc 11639 df-fz 11782 df-fzo 11913 df-seq 12211 df-exp 12270 df-hash 12513 df-cj 13155 df-re 13156 df-im 13157 df-sqrt 13291 df-abs 13292 df-clim 13545 df-sum 13746 df-sumge0 38199

This theorem is referenced by: sge0splitmpt 38247

W3C validator