iblspltprt - Mathbox for Glauco Siliprandi

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

Theorem iblspltprt 31933

Description: If a function is integrable on any interval of a partition, then it is integrable on the whole interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
iblspltprt.1
iblspltprt.2
iblspltprt.3
iblspltprt.4	$/\$
iblspltprt.5	$/\$ ..^
iblspltprt.6	$/\$
iblspltprt.7	$/\$ ..^

**Assertion**
Ref	Expression
iblspltprt

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

Proof of Theorem iblspltprt Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		iblspltprt.3	. . . 4
2		eluzelz 11115	. . . 4
3	1, 2	syl 16	. . 3
4		eluzle 11118	. . . 4
5	1, 4	syl 16	. . 3
6	3	zred 10990	. . . 4
7	6	leidd 10140	. . 3
8		iblspltprt.2	. . . . 5
9	8	peano2zd 10993	. . . 4
10		elfz1 11702	. . . 4 $/\$ $/\$ $/\$
11	9, 3, 10	syl2anc 661	. . 3 $/\$ $/\$
12	3, 5, 7, 11	mpbir3and 1179	. 2
13		fveq2 5872	. . . . . . 7
14	13	oveq2d 6312	. . . . . 6
15	14	mpteq1d 4538	. . . . 5
16	15	eleq1d 2526	. . . 4
17	16	imbi2d 316	. . 3
18		fveq2 5872	. . . . . . 7
19	18	oveq2d 6312	. . . . . 6
20	19	mpteq1d 4538	. . . . 5
21	20	eleq1d 2526	. . . 4
22	21	imbi2d 316	. . 3
23		fveq2 5872	. . . . . . 7
24	23	oveq2d 6312	. . . . . 6
25	24	mpteq1d 4538	. . . . 5
26	25	eleq1d 2526	. . . 4
27	26	imbi2d 316	. . 3
28		fveq2 5872	. . . . . . 7
29	28	oveq2d 6312	. . . . . 6
30	29	mpteq1d 4538	. . . . 5
31	30	eleq1d 2526	. . . 4
32	31	imbi2d 316	. . 3
33		uzid 11120	. . . . . . 7
34	8, 33	syl 16	. . . . . 6
35	8	zred 10990	. . . . . . 7
36		1red 9628	. . . . . . . 8
37	35, 36	readdcld 9640	. . . . . . 7
38	35	ltp1d 10496	. . . . . . 7
39	35, 37, 6, 38, 5	ltletrd 9759	. . . . . 6
40		elfzo2 11828	. . . . . 6 ..^ $/\$ $/\$
41	34, 3, 39, 40	syl3anbrc 1180	. . . . 5 ..^
42		fveq2 5872	. . . . . . . . . 10
43		oveq1 6303	. . . . . . . . . . 11
44	43	fveq2d 5876	. . . . . . . . . 10
45	42, 44	oveq12d 6314	. . . . . . . . 9
46	45	mpteq1d 4538	. . . . . . . 8
47	46	eleq1d 2526	. . . . . . 7
48	47	imbi2d 316	. . . . . 6
49		iblspltprt.7	. . . . . . 7 $/\$ ..^
50	49	expcom 435	. . . . . 6 ..^
51	48, 50	vtoclga 3173	. . . . 5 ..^
52	41, 51	mpcom 36	. . . 4
53	52	a1i 11	. . 3
54		nfv 1708	. . . . . 6 ..^
55		iblspltprt.1	. . . . . . 7
56		nfmpt1 4546	. . . . . . . 8
57	56	nfel1 2635	. . . . . . 7
58	55, 57	nfim 1921	. . . . . 6
59	54, 58, 55	nf3an 1931	. . . . 5 ..^ $/\$ $/\$
60		simp3 998	. . . . . 6 ..^ $/\$ $/\$
61		simp1 996	. . . . . 6 ..^ $/\$ $/\$ ..^
62	35	leidd 10140	. . . . . . . . . . . . 13
63	35, 6, 39	ltled 9750	. . . . . . . . . . . . 13
64		elfz1 11702	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
65	8, 3, 64	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$
66	8, 62, 63, 65	mpbir3and 1179	. . . . . . . . . . . 12
67	66	ancli 551	. . . . . . . . . . . 12 $/\$
68		eleq1 2529	. . . . . . . . . . . . . . 15
69	68	anbi2d 703	. . . . . . . . . . . . . 14 $/\$ $/\$
70	42	eleq1d 2526	. . . . . . . . . . . . . 14
71	69, 70	imbi12d 320	. . . . . . . . . . . . 13 $/\$ $/\$
72		iblspltprt.4	. . . . . . . . . . . . 13 $/\$
73	71, 72	vtoclg 3167	. . . . . . . . . . . 12 $/\$
74	66, 67, 73	sylc 60	. . . . . . . . . . 11
75	74	adantr 465	. . . . . . . . . 10 $/\$ ..^
76	75	rexrd 9660	. . . . . . . . 9 $/\$ ..^
77		simpl 457	. . . . . . . . . . 11 $/\$ ..^
78		elfzoelz 11825	. . . . . . . . . . . . 13 ..^
79	78	adantl 466	. . . . . . . . . . . 12 $/\$ ..^
80	35	adantr 465	. . . . . . . . . . . . 13 $/\$ ..^
81	79	zred 10990	. . . . . . . . . . . . 13 $/\$ ..^
82	37	adantr 465	. . . . . . . . . . . . . 14 $/\$ ..^
83	38	adantr 465	. . . . . . . . . . . . . 14 $/\$ ..^
84		elfzole1 11833	. . . . . . . . . . . . . . 15 ..^
85	84	adantl 466	. . . . . . . . . . . . . 14 $/\$ ..^
86	80, 82, 81, 83, 85	ltletrd 9759	. . . . . . . . . . . . 13 $/\$ ..^
87	80, 81, 86	ltled 9750	. . . . . . . . . . . 12 $/\$ ..^
88	6	adantr 465	. . . . . . . . . . . . 13 $/\$ ..^
89		elfzolt2 11834	. . . . . . . . . . . . . 14 ..^
90	89	adantl 466	. . . . . . . . . . . . 13 $/\$ ..^
91	81, 88, 90	ltled 9750	. . . . . . . . . . . 12 $/\$ ..^
92	8, 3	jca 532	. . . . . . . . . . . . . 14 $/\$
93	92	adantr 465	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
94		elfz1 11702	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
95	93, 94	syl 16	. . . . . . . . . . . 12 $/\$ ..^ $/\$ $/\$
96	79, 87, 91, 95	mpbir3and 1179	. . . . . . . . . . 11 $/\$ ..^
97		eleq1 2529	. . . . . . . . . . . . . 14
98	97	anbi2d 703	. . . . . . . . . . . . 13 $/\$ $/\$
99		fveq2 5872	. . . . . . . . . . . . . 14
100	99	eleq1d 2526	. . . . . . . . . . . . 13
101	98, 100	imbi12d 320	. . . . . . . . . . . 12 $/\$ $/\$
102	101, 72	chvarv 2015	. . . . . . . . . . 11 $/\$
103	77, 96, 102	syl2anc 661	. . . . . . . . . 10 $/\$ ..^
104	103	rexrd 9660	. . . . . . . . 9 $/\$ ..^
105	79	peano2zd 10993	. . . . . . . . . . . 12 $/\$ ..^
106	105	zred 10990	. . . . . . . . . . . . 13 $/\$ ..^
107		1red 9628	. . . . . . . . . . . . . . 15 $/\$ ..^
108	80, 81, 107, 86	ltadd1dd 10184	. . . . . . . . . . . . . 14 $/\$ ..^
109	80, 82, 106, 83, 108	lttrd 9760	. . . . . . . . . . . . 13 $/\$ ..^
110	80, 106, 109	ltled 9750	. . . . . . . . . . . 12 $/\$ ..^
111		zltp1le 10934	. . . . . . . . . . . . . 14 $/\$
112	78, 3, 111	syl2anr 478	. . . . . . . . . . . . 13 $/\$ ..^
113	90, 112	mpbid 210	. . . . . . . . . . . 12 $/\$ ..^
114		elfz1 11702	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
115	93, 114	syl 16	. . . . . . . . . . . 12 $/\$ ..^ $/\$ $/\$
116	105, 110, 113, 115	mpbir3and 1179	. . . . . . . . . . 11 $/\$ ..^
117	77, 116	jca 532	. . . . . . . . . . 11 $/\$ ..^ $/\$
118		eleq1 2529	. . . . . . . . . . . . . 14
119	118	anbi2d 703	. . . . . . . . . . . . 13 $/\$ $/\$
120		fveq2 5872	. . . . . . . . . . . . . 14
121	120	eleq1d 2526	. . . . . . . . . . . . 13
122	119, 121	imbi12d 320	. . . . . . . . . . . 12 $/\$ $/\$
123	122, 72	vtoclg 3167	. . . . . . . . . . 11 $/\$
124	116, 117, 123	sylc 60	. . . . . . . . . 10 $/\$ ..^
125	124	rexrd 9660	. . . . . . . . 9 $/\$ ..^
126		eluz 11119	. . . . . . . . . . . 12 $/\$
127	8, 78, 126	syl2an 477	. . . . . . . . . . 11 $/\$ ..^
128	87, 127	mpbird 232	. . . . . . . . . 10 $/\$ ..^
129		simpll 753	. . . . . . . . . . 11 $/\$ ..^ $/\$
130		elfzelz 11713	. . . . . . . . . . . . 13
131	130	adantl 466	. . . . . . . . . . . 12 $/\$ ..^ $/\$
132		elfzle1 11714	. . . . . . . . . . . . 13
133	132	adantl 466	. . . . . . . . . . . 12 $/\$ ..^ $/\$
134	131	zred 10990	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
135	129, 6	syl 16	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
136	81	adantr 465	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
137		elfzle2 11715	. . . . . . . . . . . . . . 15
138	137	adantl 466	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
139	90	adantr 465	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
140	134, 136, 135, 138, 139	lelttrd 9757	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
141	134, 135, 140	ltled 9750	. . . . . . . . . . . 12 $/\$ ..^ $/\$
142		elfz1 11702	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
143	129, 92, 142	3syl 20	. . . . . . . . . . . 12 $/\$ ..^ $/\$ $/\$ $/\$
144	131, 133, 141, 143	mpbir3and 1179	. . . . . . . . . . 11 $/\$ ..^ $/\$
145	129, 144, 72	syl2anc 661	. . . . . . . . . 10 $/\$ ..^ $/\$
146		simpll 753	. . . . . . . . . . . 12 $/\$ ..^ $/\$
147		elfzelz 11713	. . . . . . . . . . . . . 14
148	147	adantl 466	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
149		elfzle1 11714	. . . . . . . . . . . . . 14
150	149	adantl 466	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
151	148	zred 10990	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
152	146, 6	syl 16	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
153	81	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
154		1red 9628	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
155	153, 154	resubcld 10008	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
156		elfzle2 11715	. . . . . . . . . . . . . . . 16
157	156	adantl 466	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
158	78	zred 10990	. . . . . . . . . . . . . . . . . 18 ..^
159		1red 9628	. . . . . . . . . . . . . . . . . 18 ..^
160	158, 159	resubcld 10008	. . . . . . . . . . . . . . . . 17 ..^
161		elfzoel2 11824	. . . . . . . . . . . . . . . . . 18 ..^
162	161	zred 10990	. . . . . . . . . . . . . . . . 17 ..^
163	158	ltm1d 10498	. . . . . . . . . . . . . . . . 17 ..^
164	160, 158, 162, 163, 89	lttrd 9760	. . . . . . . . . . . . . . . 16 ..^
165	164	ad2antlr 726	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
166	151, 155, 152, 157, 165	lelttrd 9757	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
167	151, 152, 166	ltled 9750	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
168	146, 92, 142	3syl 20	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$ $/\$
169	148, 150, 167, 168	mpbir3and 1179	. . . . . . . . . . . 12 $/\$ ..^ $/\$
170	146, 169, 72	syl2anc 661	. . . . . . . . . . 11 $/\$ ..^ $/\$
171	148	peano2zd 10993	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
172		elfzel1 11712	. . . . . . . . . . . . . . . 16
173	172	zred 10990	. . . . . . . . . . . . . . 15
174	147	zred 10990	. . . . . . . . . . . . . . . 16
175		1red 9628	. . . . . . . . . . . . . . . 16
176	174, 175	readdcld 9640	. . . . . . . . . . . . . . 15
177	174	ltp1d 10496	. . . . . . . . . . . . . . . 16
178	173, 174, 176, 149, 177	lelttrd 9757	. . . . . . . . . . . . . . 15
179	173, 176, 178	ltled 9750	. . . . . . . . . . . . . 14
180	179	adantl 466	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
181	146, 1, 2	3syl 20	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
182		zltp1le 10934	. . . . . . . . . . . . . . 15 $/\$
183	148, 181, 182	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
184	166, 183	mpbid 210	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
185		elfz1 11702	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
186	146, 92, 185	3syl 20	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$ $/\$
187	171, 180, 184, 186	mpbir3and 1179	. . . . . . . . . . . 12 $/\$ ..^ $/\$
188	146, 187	jca 532	. . . . . . . . . . . 12 $/\$ ..^ $/\$ $/\$
189		eleq1 2529	. . . . . . . . . . . . . . 15
190	189	anbi2d 703	. . . . . . . . . . . . . 14 $/\$ $/\$
191		fveq2 5872	. . . . . . . . . . . . . . 15
192	191	eleq1d 2526	. . . . . . . . . . . . . 14
193	190, 192	imbi12d 320	. . . . . . . . . . . . 13 $/\$ $/\$
194	193, 102	vtoclg 3167	. . . . . . . . . . . 12 $/\$
195	187, 188, 194	sylc 60	. . . . . . . . . . 11 $/\$ ..^ $/\$
196		elfzuz 11709	. . . . . . . . . . . . . 14
197	196	adantl 466	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
198		elfzo2 11828	. . . . . . . . . . . . 13 ..^ $/\$ $/\$
199	197, 181, 166, 198	syl3anbrc 1180	. . . . . . . . . . . 12 $/\$ ..^ $/\$ ..^
200		iblspltprt.5	. . . . . . . . . . . 12 $/\$ ..^
201	146, 199, 200	syl2anc 661	. . . . . . . . . . 11 $/\$ ..^ $/\$
202	170, 195, 201	ltled 9750	. . . . . . . . . 10 $/\$ ..^ $/\$
203	128, 145, 202	monoord 12139	. . . . . . . . 9 $/\$ ..^
204	161	adantl 466	. . . . . . . . . . . 12 $/\$ ..^
205		elfzo2 11828	. . . . . . . . . . . 12 ..^ $/\$ $/\$
206	128, 204, 90, 205	syl3anbrc 1180	. . . . . . . . . . 11 $/\$ ..^ ..^
207		eleq1 2529	. . . . . . . . . . . . . 14 ..^ ..^
208	207	anbi2d 703	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ ..^
209		oveq1 6303	. . . . . . . . . . . . . . 15
210	209	fveq2d 5876	. . . . . . . . . . . . . 14
211	99, 210	breq12d 4469	. . . . . . . . . . . . 13
212	208, 211	imbi12d 320	. . . . . . . . . . . 12 $/\$ ..^ $/\$ ..^
213	212, 200	chvarv 2015	. . . . . . . . . . 11 $/\$ ..^
214	77, 206, 213	syl2anc 661	. . . . . . . . . 10 $/\$ ..^
215	103, 124, 214	ltled 9750	. . . . . . . . 9 $/\$ ..^
216		iccintsng 31724	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
217	76, 104, 125, 203, 215, 216	syl32anc 1236	. . . . . . . 8 $/\$ ..^
218	217	fveq2d 5876	. . . . . . 7 $/\$ ..^
219		ovolsn 22031	. . . . . . . 8
220	103, 219	syl 16	. . . . . . 7 $/\$ ..^
221	218, 220	eqtrd 2498	. . . . . 6 $/\$ ..^
222	60, 61, 221	syl2anc 661	. . . . 5 ..^ $/\$ $/\$
223	75, 124, 103, 203, 215	eliccd 31699	. . . . . . . 8 $/\$ ..^
224	75, 124, 223	3jca 1176	. . . . . . 7 $/\$ ..^ $/\$ $/\$
225	60, 61, 224	syl2anc 661	. . . . . 6 ..^ $/\$ $/\$ $/\$ $/\$
226		iccsplit 11678	. . . . . 6 $/\$ $/\$
227	225, 226	syl 16	. . . . 5 ..^ $/\$ $/\$
228		simpl3 1001	. . . . . 6 ..^ $/\$ $/\$ $/\$
229		simpl1 999	. . . . . 6 ..^ $/\$ $/\$ $/\$ ..^
230		simpr 461	. . . . . 6 ..^ $/\$ $/\$ $/\$
231		simp1 996	. . . . . . 7 $/\$ ..^ $/\$
232		eliccxr 31711	. . . . . . . . 9
233	232	3ad2ant3 1019	. . . . . . . 8 $/\$ ..^ $/\$
234	74	rexrd 9660	. . . . . . . . . 10
235	234	3ad2ant1 1017	. . . . . . . . 9 $/\$ ..^ $/\$
236	125	3adant3 1016	. . . . . . . . 9 $/\$ ..^ $/\$
237		simp3 998	. . . . . . . . 9 $/\$ ..^ $/\$
238		iccgelb 11606	. . . . . . . . 9 $/\$ $/\$
239	235, 236, 237, 238	syl3anc 1228	. . . . . . . 8 $/\$ ..^ $/\$
240	75, 124	jca 532	. . . . . . . . . . 11 $/\$ ..^ $/\$
241	240	3adant3 1016	. . . . . . . . . 10 $/\$ ..^ $/\$ $/\$
242		iccssre 11631	. . . . . . . . . . 11 $/\$
243	242	sseld 3498	. . . . . . . . . 10 $/\$
244	241, 237, 243	sylc 60	. . . . . . . . 9 $/\$ ..^ $/\$
245	124	3adant3 1016	. . . . . . . . 9 $/\$ ..^ $/\$
246		elfz1 11702	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
247	8, 3, 246	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$
248	3, 63, 7, 247	mpbir3and 1179	. . . . . . . . . . . 12
249	248	ancli 551	. . . . . . . . . . 11 $/\$
250		eleq1 2529	. . . . . . . . . . . . . 14
251	250	anbi2d 703	. . . . . . . . . . . . 13 $/\$ $/\$
252		fveq2 5872	. . . . . . . . . . . . . 14
253	252	eleq1d 2526	. . . . . . . . . . . . 13
254	251, 253	imbi12d 320	. . . . . . . . . . . 12 $/\$ $/\$
255	254, 72	vtoclg 3167	. . . . . . . . . . 11 $/\$
256	3, 249, 255	sylc 60	. . . . . . . . . 10
257	256	3ad2ant1 1017	. . . . . . . . 9 $/\$ ..^ $/\$
258		elicc1 11598	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
259	235, 236, 258	syl2anc 661	. . . . . . . . . . 11 $/\$ ..^ $/\$ $/\$ $/\$
260	237, 259	mpbid 210	. . . . . . . . . 10 $/\$ ..^ $/\$ $/\$ $/\$
261	260	simp3d 1010	. . . . . . . . 9 $/\$ ..^ $/\$
262		elfzop1le2 31639	. . . . . . . . . . . . 13 ..^
263	78	peano2zd 10993	. . . . . . . . . . . . . 14 ..^
264		eluz 11119	. . . . . . . . . . . . . 14 $/\$
265	263, 161, 264	syl2anc 661	. . . . . . . . . . . . 13 ..^
266	262, 265	mpbird 232	. . . . . . . . . . . 12 ..^
267	266	adantl 466	. . . . . . . . . . 11 $/\$ ..^
268		simpll 753	. . . . . . . . . . . 12 $/\$ ..^ $/\$
269		elfzelz 11713	. . . . . . . . . . . . . 14
270	269	adantl 466	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
271	268, 35	syl 16	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
272	270	zred 10990	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
273	81	adantr 465	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
274	86	adantr 465	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
275	158	adantr 465	. . . . . . . . . . . . . . . . 17 ..^ $/\$
276		1red 9628	. . . . . . . . . . . . . . . . . 18 ..^ $/\$
277	275, 276	readdcld 9640	. . . . . . . . . . . . . . . . 17 ..^ $/\$
278	269	zred 10990	. . . . . . . . . . . . . . . . . 18
279	278	adantl 466	. . . . . . . . . . . . . . . . 17 ..^ $/\$
280	275	ltp1d 10496	. . . . . . . . . . . . . . . . 17 ..^ $/\$
281		elfzle1 11714	. . . . . . . . . . . . . . . . . 18
282	281	adantl 466	. . . . . . . . . . . . . . . . 17 ..^ $/\$
283	275, 277, 279, 280, 282	ltletrd 9759	. . . . . . . . . . . . . . . 16 ..^ $/\$
284	283	adantll 713	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
285	271, 273, 272, 274, 284	lttrd 9760	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
286	271, 272, 285	ltled 9750	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
287		elfzle2 11715	. . . . . . . . . . . . . 14
288	287	adantl 466	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
289	268, 92, 142	3syl 20	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$ $/\$
290	270, 286, 288, 289	mpbir3and 1179	. . . . . . . . . . . 12 $/\$ ..^ $/\$
291	268, 290, 72	syl2anc 661	. . . . . . . . . . 11 $/\$ ..^ $/\$
292		simpll 753	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
293		elfzelz 11713	. . . . . . . . . . . . . . 15
294	293	adantl 466	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
295	292, 35	syl 16	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
296	294	zred 10990	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
297	81	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
298	86	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
299	158	adantr 465	. . . . . . . . . . . . . . . . . 18 ..^ $/\$
300		1red 9628	. . . . . . . . . . . . . . . . . . 19 ..^ $/\$
301	299, 300	readdcld 9640	. . . . . . . . . . . . . . . . . 18 ..^ $/\$
302	293	zred 10990	. . . . . . . . . . . . . . . . . . 19
303	302	adantl 466	. . . . . . . . . . . . . . . . . 18 ..^ $/\$
304	299	ltp1d 10496	. . . . . . . . . . . . . . . . . 18 ..^ $/\$
305		elfzle1 11714	. . . . . . . . . . . . . . . . . . 19
306	305	adantl 466	. . . . . . . . . . . . . . . . . 18 ..^ $/\$
307	299, 301, 303, 304, 306	ltletrd 9759	. . . . . . . . . . . . . . . . 17 ..^ $/\$
308	307	adantll 713	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
309	295, 297, 296, 298, 308	lttrd 9760	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
310	295, 296, 309	ltled 9750	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
311	302	adantl 466	. . . . . . . . . . . . . . . 16 $/\$
312	6	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
313		1red 9628	. . . . . . . . . . . . . . . . . 18 $/\$
314	312, 313	resubcld 10008	. . . . . . . . . . . . . . . . 17 $/\$
315		elfzle2 11715	. . . . . . . . . . . . . . . . . 18
316	315	adantl 466	. . . . . . . . . . . . . . . . 17 $/\$
317	312	ltm1d 10498	. . . . . . . . . . . . . . . . 17 $/\$
318	311, 314, 312, 316, 317	lelttrd 9757	. . . . . . . . . . . . . . . 16 $/\$
319	311, 312, 318	ltled 9750	. . . . . . . . . . . . . . 15 $/\$
320	319	adantlr 714	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
321	292, 92, 142	3syl 20	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$ $/\$
322	294, 310, 320, 321	mpbir3and 1179	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
323	292, 322, 72	syl2anc 661	. . . . . . . . . . . 12 $/\$ ..^ $/\$
324	294	peano2zd 10993	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
325	324	zred 10990	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
326	303, 300	readdcld 9640	. . . . . . . . . . . . . . . . . 18 ..^ $/\$
327	299, 303, 307	ltled 9750	. . . . . . . . . . . . . . . . . . 19 ..^ $/\$
328	299, 303, 300, 327	leadd1dd 10187	. . . . . . . . . . . . . . . . . 18 ..^ $/\$
329	299, 301, 326, 304, 328	ltletrd 9759	. . . . . . . . . . . . . . . . 17 ..^ $/\$
330	329	adantll 713	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
331	295, 297, 325, 298, 330	lttrd 9760	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
332	295, 325, 331	ltled 9750	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
333	293, 3, 182	syl2anr 478	. . . . . . . . . . . . . . . 16 $/\$
334	318, 333	mpbid 210	. . . . . . . . . . . . . . 15 $/\$
335	334	adantlr 714	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
336	292, 92, 185	3syl 20	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$ $/\$
337	324, 332, 335, 336	mpbir3and 1179	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
338	292, 337	jca 532	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$
339	337, 338, 194	sylc 60	. . . . . . . . . . . 12 $/\$ ..^ $/\$
340	292, 8	syl 16	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
341		eluz 11119	. . . . . . . . . . . . . . . 16 $/\$
342	340, 294, 341	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
343	310, 342	mpbird 232	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
344	292, 1, 2	3syl 20	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
345	318	adantlr 714	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
346	343, 344, 345, 198	syl3anbrc 1180	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ ..^
347	292, 346, 200	syl2anc 661	. . . . . . . . . . . 12 $/\$ ..^ $/\$
348	323, 339, 347	ltled 9750	. . . . . . . . . . 11 $/\$ ..^ $/\$
349	267, 291, 348	monoord 12139	. . . . . . . . . 10 $/\$ ..^
350	349	3adant3 1016	. . . . . . . . 9 $/\$ ..^ $/\$
351	244, 245, 257, 261, 350	letrd 9756	. . . . . . . 8 $/\$ ..^ $/\$
352	257	rexrd 9660	. . . . . . . . 9 $/\$ ..^ $/\$
353		elicc1 11598	. . . . . . . . 9 $/\$ $/\$ $/\$
354	235, 352, 353	syl2anc 661	. . . . . . . 8 $/\$ ..^ $/\$ $/\$ $/\$
355	233, 239, 351, 354	mpbir3and 1179	. . . . . . 7 $/\$ ..^ $/\$
356		iblspltprt.6	. . . . . . 7 $/\$
357	231, 355, 356	syl2anc 661	. . . . . 6 $/\$ ..^ $/\$
358	228, 229, 230, 357	syl3anc 1228	. . . . 5 ..^ $/\$ $/\$ $/\$
359		simp2 997	. . . . . 6 ..^ $/\$ $/\$
360	60, 359	mpd 15	. . . . 5 ..^ $/\$ $/\$
361	60, 61	jca 532	. . . . . 6 ..^ $/\$ $/\$ $/\$ ..^
362	77, 206	jca 532	. . . . . 6 $/\$ ..^ $/\$ ..^
363	99, 210	oveq12d 6314	. . . . . . . . . 10
364	363	mpteq1d 4538	. . . . . . . . 9
365	364	eleq1d 2526	. . . . . . . 8
366	208, 365	imbi12d 320	. . . . . . 7 $/\$ ..^ $/\$ ..^
367	366, 49	chvarv 2015	. . . . . 6 $/\$ ..^
368	361, 362, 367	3syl 20	. . . . 5 ..^ $/\$ $/\$
369	59, 222, 227, 358, 360, 368	iblsplitf 31930	. . . 4 ..^ $/\$ $/\$
370	369	3exp 1195	. . 3 ..^
371	17, 22, 27, 32, 53, 370	fzind2 11926	. 2
372	12, 371	mpcom 36	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 973

wceq 1395

wnf 1617

wcel 1819

cun 3469

cin 3470

csn 4032 class class class wbr 4456

cmpt 4515

cfv 5594 (class class class)co 6296

cc 9507

cr 9508

cc0 9509

c1 9510

caddc 9512

cxr 9644

clt 9645

cle 9646

cmin 9824

cz 10885

cuz 11106

cicc 11557

cfz 11697 ..^cfzo 11820

covol 21999

cibl 22151

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-rep 4568 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-inf2 8075 ax-cnex 9565 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585 ax-pre-mulgt0 9586 ax-pre-sup 9587 ax-addf 9588

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-fal 1401 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-int 4289 df-iun 4334 df-disj 4428 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-se 4848 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-isom 5603 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-of 6539 df-ofr 6540 df-om 6700 df-1st 6799 df-2nd 6800 df-recs 7060 df-rdg 7094 df-1o 7148 df-2o 7149 df-oadd 7152 df-er 7329 df-map 7440 df-pm 7441 df-en 7536 df-dom 7537 df-sdom 7538 df-fin 7539 df-fi 7889 df-sup 7919 df-oi 7953 df-card 8337 df-cda 8565 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-sub 9826 df-neg 9827 df-div 10228 df-nn 10557 df-2 10615 df-3 10616 df-n0 10817 df-z 10886 df-uz 11107 df-q 11208 df-rp 11246 df-xneg 11343 df-xadd 11344 df-xmul 11345 df-ioo 11558 df-ico 11560 df-icc 11561 df-fz 11698 df-fzo 11821 df-fl 11931 df-seq 12110 df-exp 12169 df-hash 12408 df-cj 12943 df-re 12944 df-im 12945 df-sqrt 13079 df-abs 13080 df-clim 13322 df-sum 13520 df-rest 14839 df-topgen 14860 df-psmet 18537 df-xmet 18538 df-met 18539 df-bl 18540 df-mopn 18541 df-top 19525 df-bases 19527 df-topon 19528 df-cmp 20013 df-ovol 22001 df-vol 22002 df-mbf 22153 df-itg1 22154 df-itg2 22155 df-ibl 22156

This theorem is referenced by: itgspltprt 31939 fourierdlem69 32119

W3C validator