itgspltprt - Mathbox for Glauco Siliprandi

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

Theorem itgspltprt 40195

Description: The

integral splits on a given partition

. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

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

**Assertion**
Ref	Expression
itgspltprt	..^

Distinct variable groups:

Allowed substitution hint:

(

)

Proof of Theorem itgspltprt Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		itgspltprt.1	. . . . . 6
2	1	peano2zd 11485	. . . . 5
3		itgspltprt.2	. . . . . 6
4		eluzelz 11697	. . . . . 6
5	3, 4	syl 17	. . . . 5
6	2, 5, 5	3jca 1242	. . . 4 $/\$ $/\$
7		eluzle 11700	. . . . 5
8	3, 7	syl 17	. . . 4
9		eluzelre 11698	. . . . . 6
10	3, 9	syl 17	. . . . 5
11	10	leidd 10594	. . . 4
12	6, 8, 11	jca32 558	. . 3 $/\$ $/\$ $/\$ $/\$
13		elfz2 12333	. . 3 $/\$ $/\$ $/\$ $/\$
14	12, 13	sylibr 224	. 2
15		fveq2 6191	. . . . . . 7
16	15	oveq2d 6666	. . . . . 6
17	16	itgeq1d 40172	. . . . 5
18		oveq2 6658	. . . . . 6 ..^ ..^
19	18	sumeq1d 14431	. . . . 5 ..^ ..^
20	17, 19	eqeq12d 2637	. . . 4 ..^ ..^
21	20	imbi2d 330	. . 3 ..^ ..^
22		fveq2 6191	. . . . . . 7
23	22	oveq2d 6666	. . . . . 6
24	23	itgeq1d 40172	. . . . 5
25		oveq2 6658	. . . . . 6 ..^ ..^
26	25	sumeq1d 14431	. . . . 5 ..^ ..^
27	24, 26	eqeq12d 2637	. . . 4 ..^ ..^
28	27	imbi2d 330	. . 3 ..^ ..^
29		fveq2 6191	. . . . . . 7
30	29	oveq2d 6666	. . . . . 6
31	30	itgeq1d 40172	. . . . 5
32		oveq2 6658	. . . . . 6 ..^ ..^
33	32	sumeq1d 14431	. . . . 5 ..^ ..^
34	31, 33	eqeq12d 2637	. . . 4 ..^ ..^
35	34	imbi2d 330	. . 3 ..^ ..^
36		fveq2 6191	. . . . . . 7
37	36	oveq2d 6666	. . . . . 6
38	37	itgeq1d 40172	. . . . 5
39		oveq2 6658	. . . . . 6 ..^ ..^
40	39	sumeq1d 14431	. . . . 5 ..^ ..^
41	38, 40	eqeq12d 2637	. . . 4 ..^ ..^
42	41	imbi2d 330	. . 3 ..^ ..^
43	1	adantl 482	. . . . . . . 8 $/\$
44		fzval3 12536	. . . . . . . 8 ..^
45	43, 44	syl 17	. . . . . . 7 $/\$ ..^
46	45	eqcomd 2628	. . . . . 6 $/\$ ..^
47	46	sumeq1d 14431	. . . . 5 $/\$ ..^
48		itgspltprt.3	. . . . . . . . . . . 12
49	48	adantr 481	. . . . . . . . . . 11 $/\$
50	1	zred 11482	. . . . . . . . . . . . . . 15
51		1red 10055	. . . . . . . . . . . . . . . . 17
52	50, 51	readdcld 10069	. . . . . . . . . . . . . . . 16
53	50	ltp1d 10954	. . . . . . . . . . . . . . . 16
54	50, 52, 10, 53, 8	ltletrd 10197	. . . . . . . . . . . . . . 15
55	50, 10, 54	ltled 10185	. . . . . . . . . . . . . 14
56		eluz 11701	. . . . . . . . . . . . . . 15 $/\$
57	1, 5, 56	syl2anc 693	. . . . . . . . . . . . . 14
58	55, 57	mpbird 247	. . . . . . . . . . . . 13
59		eluzfz1 12348	. . . . . . . . . . . . 13
60	58, 59	syl 17	. . . . . . . . . . . 12
61	60	adantr 481	. . . . . . . . . . 11 $/\$
62	49, 61	ffvelrnd 6360	. . . . . . . . . 10 $/\$
63		elfz1 12331	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
64	1, 5, 63	syl2anc 693	. . . . . . . . . . . . 13 $/\$ $/\$
65	5, 55, 11, 64	mpbir3and 1245	. . . . . . . . . . . 12
66	48, 65	ffvelrnd 6360	. . . . . . . . . . 11
67	66	adantr 481	. . . . . . . . . 10 $/\$
68	50	lep1d 10955	. . . . . . . . . . . . . 14
69		elfz1 12331	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
70	1, 5, 69	syl2anc 693	. . . . . . . . . . . . . 14 $/\$ $/\$
71	2, 68, 8, 70	mpbir3and 1245	. . . . . . . . . . . . 13
72	48, 71	ffvelrnd 6360	. . . . . . . . . . . 12
73	72	adantr 481	. . . . . . . . . . 11 $/\$
74		simpr 477	. . . . . . . . . . 11 $/\$
75		eliccre 39728	. . . . . . . . . . 11 $/\$ $/\$
76	62, 73, 74, 75	syl3anc 1326	. . . . . . . . . 10 $/\$
77	48, 60	ffvelrnd 6360	. . . . . . . . . . . . 13
78	77	rexrd 10089	. . . . . . . . . . . 12
79	78	adantr 481	. . . . . . . . . . 11 $/\$
80	73	rexrd 10089	. . . . . . . . . . 11 $/\$
81		iccgelb 12230	. . . . . . . . . . 11 $/\$ $/\$
82	79, 80, 74, 81	syl3anc 1326	. . . . . . . . . 10 $/\$
83		iccleub 12229	. . . . . . . . . . . 12 $/\$ $/\$
84	79, 80, 74, 83	syl3anc 1326	. . . . . . . . . . 11 $/\$
85	48	adantr 481	. . . . . . . . . . . . . 14 $/\$
86		elfzelz 12342	. . . . . . . . . . . . . . . 16
87	86	adantl 482	. . . . . . . . . . . . . . 15 $/\$
88	50	adantr 481	. . . . . . . . . . . . . . . 16 $/\$
89	87	zred 11482	. . . . . . . . . . . . . . . 16 $/\$
90	52	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$
91	53	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$
92		elfzle1 12344	. . . . . . . . . . . . . . . . . 18
93	92	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$
94	88, 90, 89, 91, 93	ltletrd 10197	. . . . . . . . . . . . . . . 16 $/\$
95	88, 89, 94	ltled 10185	. . . . . . . . . . . . . . 15 $/\$
96		elfzle2 12345	. . . . . . . . . . . . . . . 16
97	96	adantl 482	. . . . . . . . . . . . . . 15 $/\$
98	1, 5	jca 554	. . . . . . . . . . . . . . . . 17 $/\$
99	98	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ $/\$
100		elfz1 12331	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
101	99, 100	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
102	87, 95, 97, 101	mpbir3and 1245	. . . . . . . . . . . . . 14 $/\$
103	85, 102	ffvelrnd 6360	. . . . . . . . . . . . 13 $/\$
104	48	adantr 481	. . . . . . . . . . . . . . 15 $/\$
105		elfzelz 12342	. . . . . . . . . . . . . . . . 17
106	105	adantl 482	. . . . . . . . . . . . . . . 16 $/\$
107	50	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$
108	106	zred 11482	. . . . . . . . . . . . . . . . 17 $/\$
109	52	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$
110	53	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$
111		elfzle1 12344	. . . . . . . . . . . . . . . . . . 19
112	111	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$
113	107, 109, 108, 110, 112	ltletrd 10197	. . . . . . . . . . . . . . . . 17 $/\$
114	107, 108, 113	ltled 10185	. . . . . . . . . . . . . . . 16 $/\$
115	10	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$
116		1red 10055	. . . . . . . . . . . . . . . . . . 19 $/\$
117	115, 116	resubcld 10458	. . . . . . . . . . . . . . . . . 18 $/\$
118		elfzle2 12345	. . . . . . . . . . . . . . . . . . 19
119	118	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$
120	115	ltm1d 10956	. . . . . . . . . . . . . . . . . 18 $/\$
121	108, 117, 115, 119, 120	lelttrd 10195	. . . . . . . . . . . . . . . . 17 $/\$
122	108, 115, 121	ltled 10185	. . . . . . . . . . . . . . . 16 $/\$
123	98	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
124	123, 100	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
125	106, 114, 122, 124	mpbir3and 1245	. . . . . . . . . . . . . . 15 $/\$
126	104, 125	ffvelrnd 6360	. . . . . . . . . . . . . 14 $/\$
127	106	peano2zd 11485	. . . . . . . . . . . . . . . 16 $/\$
128	108, 116	readdcld 10069	. . . . . . . . . . . . . . . . 17 $/\$
129	107, 108, 116, 113	ltadd1dd 10638	. . . . . . . . . . . . . . . . . 18 $/\$
130	107, 109, 128, 110, 129	lttrd 10198	. . . . . . . . . . . . . . . . 17 $/\$
131	107, 128, 130	ltled 10185	. . . . . . . . . . . . . . . 16 $/\$
132		zltp1le 11427	. . . . . . . . . . . . . . . . . 18 $/\$
133	105, 5, 132	syl2anr 495	. . . . . . . . . . . . . . . . 17 $/\$
134	121, 133	mpbid 222	. . . . . . . . . . . . . . . 16 $/\$
135		elfz1 12331	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
136	123, 135	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
137	127, 131, 134, 136	mpbir3and 1245	. . . . . . . . . . . . . . 15 $/\$
138	104, 137	ffvelrnd 6360	. . . . . . . . . . . . . 14 $/\$
139		eluz 11701	. . . . . . . . . . . . . . . . . 18 $/\$
140	1, 105, 139	syl2an 494	. . . . . . . . . . . . . . . . 17 $/\$
141	114, 140	mpbird 247	. . . . . . . . . . . . . . . 16 $/\$
142	5	adantr 481	. . . . . . . . . . . . . . . 16 $/\$
143		elfzo2 12473	. . . . . . . . . . . . . . . 16 ..^ $/\$ $/\$
144	141, 142, 121, 143	syl3anbrc 1246	. . . . . . . . . . . . . . 15 $/\$ ..^
145		itgspltprt.4	. . . . . . . . . . . . . . 15 $/\$ ..^
146	144, 145	syldan 487	. . . . . . . . . . . . . 14 $/\$
147	126, 138, 146	ltled 10185	. . . . . . . . . . . . 13 $/\$
148	3, 103, 147	monoord 12831	. . . . . . . . . . . 12
149	148	adantr 481	. . . . . . . . . . 11 $/\$
150	76, 73, 67, 84, 149	letrd 10194	. . . . . . . . . 10 $/\$
151	62, 67, 76, 82, 150	eliccd 39726	. . . . . . . . 9 $/\$
152		itgspltprt.5	. . . . . . . . 9 $/\$
153	151, 152	syldan 487	. . . . . . . 8 $/\$
154		id 22	. . . . . . . . . 10
155		fzolb 12476	. . . . . . . . . . 11 ..^ $/\$ $/\$
156	1, 5, 54, 155	syl3anbrc 1246	. . . . . . . . . 10 ..^
157	154, 156	jca 554	. . . . . . . . 9 $/\$ ..^
158		eleq1 2689	. . . . . . . . . . . 12 ..^ ..^
159	158	anbi2d 740	. . . . . . . . . . 11 $/\$ ..^ $/\$ ..^
160		fveq2 6191	. . . . . . . . . . . . . 14
161		oveq1 6657	. . . . . . . . . . . . . . 15
162	161	fveq2d 6195	. . . . . . . . . . . . . 14
163	160, 162	oveq12d 6668	. . . . . . . . . . . . 13
164	163	mpteq1d 4738	. . . . . . . . . . . 12
165	164	eleq1d 2686	. . . . . . . . . . 11
166	159, 165	imbi12d 334	. . . . . . . . . 10 $/\$ ..^ $/\$ ..^
167		itgspltprt.6	. . . . . . . . . 10 $/\$ ..^
168	166, 167	vtoclg 3266	. . . . . . . . 9 $/\$ ..^
169	1, 157, 168	sylc 65	. . . . . . . 8
170	153, 169	itgcl 23550	. . . . . . 7
171	163	itgeq1d 40172	. . . . . . . 8
172	171	fsum1 14476	. . . . . . 7 $/\$
173	1, 170, 172	syl2anc 693	. . . . . 6
174	173	adantl 482	. . . . 5 $/\$
175	47, 174	eqtr2d 2657	. . . 4 $/\$ ..^
176	175	ex 450	. . 3 ..^
177		simp3 1063	. . . . 5 ..^ $/\$ ..^ $/\$
178		simp1 1061	. . . . 5 ..^ $/\$ ..^ $/\$ ..^
179		simp2 1062	. . . . . 6 ..^ $/\$ ..^ $/\$ ..^
180	177, 179	mpd 15	. . . . 5 ..^ $/\$ ..^ $/\$ ..^
181	50	adantr 481	. . . . . . . . . 10 $/\$ ..^
182		elfzoelz 12470	. . . . . . . . . . . 12 ..^
183	182	zred 11482	. . . . . . . . . . 11 ..^
184	183	adantl 482	. . . . . . . . . 10 $/\$ ..^
185	52	adantr 481	. . . . . . . . . . 11 $/\$ ..^
186	53	adantr 481	. . . . . . . . . . 11 $/\$ ..^
187		elfzole1 12478	. . . . . . . . . . . 12 ..^
188	187	adantl 482	. . . . . . . . . . 11 $/\$ ..^
189	181, 185, 184, 186, 188	ltletrd 10197	. . . . . . . . . 10 $/\$ ..^
190	181, 184, 189	ltled 10185	. . . . . . . . 9 $/\$ ..^
191		eluz 11701	. . . . . . . . . 10 $/\$
192	1, 182, 191	syl2an 494	. . . . . . . . 9 $/\$ ..^
193	190, 192	mpbird 247	. . . . . . . 8 $/\$ ..^
194		simplll 798	. . . . . . . . . 10 $/\$ ..^ $/\$ $/\$
195		eliccxr 39737	. . . . . . . . . . . 12
196	195	adantl 482	. . . . . . . . . . 11 $/\$ ..^ $/\$ $/\$
197	194, 77	syl 17	. . . . . . . . . . . 12 $/\$ ..^ $/\$ $/\$
198	194, 48	syl 17	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$
199		elfzelz 12342	. . . . . . . . . . . . . . . 16
200	199	adantl 482	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
201		elfzle1 12344	. . . . . . . . . . . . . . . 16
202	201	adantl 482	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
203	200	zred 11482	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
204	10	ad2antrr 762	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
205	184	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
206		elfzle2 12345	. . . . . . . . . . . . . . . . . 18
207	206	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
208		elfzolt2 12479	. . . . . . . . . . . . . . . . . 18 ..^
209	208	ad2antlr 763	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
210	203, 205, 204, 207, 209	lelttrd 10195	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
211	203, 204, 210	ltled 10185	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
212	98	ad2antrr 762	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$
213	212, 100	syl 17	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$ $/\$
214	200, 202, 211, 213	mpbir3and 1245	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
215	214	adantr 481	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$
216	198, 215	ffvelrnd 6360	. . . . . . . . . . . 12 $/\$ ..^ $/\$ $/\$
217	200	peano2zd 11485	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
218	50	ad2antrr 762	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
219	217	zred 11482	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
220	50	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$
221	199	zred 11482	. . . . . . . . . . . . . . . . . . . 20
222	221	adantl 482	. . . . . . . . . . . . . . . . . . 19 $/\$
223		1red 10055	. . . . . . . . . . . . . . . . . . . 20 $/\$
224	222, 223	readdcld 10069	. . . . . . . . . . . . . . . . . . 19 $/\$
225	201	adantl 482	. . . . . . . . . . . . . . . . . . 19 $/\$
226	222	ltp1d 10954	. . . . . . . . . . . . . . . . . . 19 $/\$
227	220, 222, 224, 225, 226	lelttrd 10195	. . . . . . . . . . . . . . . . . 18 $/\$
228	227	adantlr 751	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
229	218, 219, 228	ltled 10185	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
230	5, 199	anim12ci 591	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
231	230	adantlr 751	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
232	231, 132	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
233	210, 232	mpbid 222	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
234	212, 135	syl 17	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$ $/\$
235	217, 229, 233, 234	mpbir3and 1245	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
236	235	adantr 481	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$
237	198, 236	ffvelrnd 6360	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$
238		simpr 477	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$
239		eliccre 39728	. . . . . . . . . . . . 13 $/\$ $/\$
240	216, 237, 238, 239	syl3anc 1326	. . . . . . . . . . . 12 $/\$ ..^ $/\$ $/\$
241		elfzuz 12338	. . . . . . . . . . . . . . 15
242	241	adantl 482	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
243	48	ad3antrrr 766	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$
244		elfzelz 12342	. . . . . . . . . . . . . . . . 17
245	244	adantl 482	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$
246		elfzle1 12344	. . . . . . . . . . . . . . . . 17
247	246	adantl 482	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$
248	245	zred 11482	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$
249	204	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$
250	203	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
251		elfzle2 12345	. . . . . . . . . . . . . . . . . . 19
252	251	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
253	210	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
254	248, 250, 249, 252, 253	lelttrd 10195	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$
255	248, 249, 254	ltled 10185	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$
256	212	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$ $/\$
257		elfz1 12331	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
258	256, 257	syl 17	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$ $/\$ $/\$
259	245, 247, 255, 258	mpbir3and 1245	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$
260	243, 259	ffvelrnd 6360	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$
261	48	ad3antrrr 766	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$
262		elfzelz 12342	. . . . . . . . . . . . . . . . . 18
263	262	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$
264		elfzle1 12344	. . . . . . . . . . . . . . . . . 18
265	264	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$
266	263	zred 11482	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
267	204	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
268	203	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
269		1red 10055	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$ $/\$
270	268, 269	resubcld 10458	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$
271		elfzle2 12345	. . . . . . . . . . . . . . . . . . . . 21
272	271	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$
273	268	ltm1d 10956	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$
274	266, 270, 268, 272, 273	lelttrd 10195	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
275	210	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
276	266, 268, 267, 274, 275	lttrd 10198	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
277	266, 267, 276	ltled 10185	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$
278	212	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$ $/\$
279	278, 257	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$ $/\$ $/\$
280	263, 265, 277, 279	mpbir3and 1245	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$
281	261, 280	ffvelrnd 6360	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$
282	263	peano2zd 11485	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$
283	181	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
284	266, 269	readdcld 10069	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
285	50	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$
286	262	zred 11482	. . . . . . . . . . . . . . . . . . . . 21
287	286	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$
288		1red 10055	. . . . . . . . . . . . . . . . . . . . 21 $/\$
289	287, 288	readdcld 10069	. . . . . . . . . . . . . . . . . . . 20 $/\$
290	264	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$
291	287	ltp1d 10954	. . . . . . . . . . . . . . . . . . . 20 $/\$
292	285, 287, 289, 290, 291	lelttrd 10195	. . . . . . . . . . . . . . . . . . 19 $/\$
293	292	ad4ant14 1293	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
294	283, 284, 293	ltled 10185	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$
295		zltp1le 11427	. . . . . . . . . . . . . . . . . . . . 21 $/\$
296	262, 200, 295	syl2anr 495	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$
297	274, 296	mpbid 222	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
298	284, 268, 267, 297, 275	lelttrd 10195	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
299	284, 267, 298	ltled 10185	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$
300		elfz1 12331	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
301	278, 300	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$ $/\$ $/\$
302	282, 294, 299, 301	mpbir3and 1245	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$
303	261, 302	ffvelrnd 6360	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$
304		simplll 798	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$
305		elfzuz 12338	. . . . . . . . . . . . . . . . . 18
306	305	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$
307	304, 5	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$
308		elfzo2 12473	. . . . . . . . . . . . . . . . 17 ..^ $/\$ $/\$
309	306, 307, 276, 308	syl3anbrc 1246	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$ ..^
310		eleq1 2689	. . . . . . . . . . . . . . . . . . 19 ..^ ..^
311	310	anbi2d 740	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ ..^
312		fveq2 6191	. . . . . . . . . . . . . . . . . . 19
313		oveq1 6657	. . . . . . . . . . . . . . . . . . . 20
314	313	fveq2d 6195	. . . . . . . . . . . . . . . . . . 19
315	312, 314	breq12d 4666	. . . . . . . . . . . . . . . . . 18
316	311, 315	imbi12d 334	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ ..^
317	316, 145	chvarv 2263	. . . . . . . . . . . . . . . 16 $/\$ ..^
318	304, 309, 317	syl2anc 693	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$
319	281, 303, 318	ltled 10185	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$
320	242, 260, 319	monoord 12831	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
321	320	adantr 481	. . . . . . . . . . . 12 $/\$ ..^ $/\$ $/\$
322	216	rexrd 10089	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$
323	237	rexrd 10089	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$
324		iccgelb 12230	. . . . . . . . . . . . 13 $/\$ $/\$
325	322, 323, 238, 324	syl3anc 1326	. . . . . . . . . . . 12 $/\$ ..^ $/\$ $/\$
326	197, 216, 240, 321, 325	letrd 10194	. . . . . . . . . . 11 $/\$ ..^ $/\$ $/\$
327	194, 66	syl 17	. . . . . . . . . . . 12 $/\$ ..^ $/\$ $/\$
328		iccleub 12229	. . . . . . . . . . . . 13 $/\$ $/\$
329	322, 323, 238, 328	syl3anc 1326	. . . . . . . . . . . 12 $/\$ ..^ $/\$ $/\$
330	5	ad2antrr 762	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
331		eluz 11701	. . . . . . . . . . . . . . . 16 $/\$
332	217, 330, 331	syl2anc 693	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
333	233, 332	mpbird 247	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
334	333	adantr 481	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$
335	48	ad3antrrr 766	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$
336		elfzelz 12342	. . . . . . . . . . . . . . . . 17
337	336	adantl 482	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$
338		elfzel1 12341	. . . . . . . . . . . . . . . . . . . 20
339	338	zred 11482	. . . . . . . . . . . . . . . . . . 19
340	339	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$
341	336	zred 11482	. . . . . . . . . . . . . . . . . . 19
342	341	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$
343	221	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$
344		1red 10055	. . . . . . . . . . . . . . . . . . . 20 $/\$
345	343, 344	readdcld 10069	. . . . . . . . . . . . . . . . . . 19 $/\$
346	201	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$
347	343	ltp1d 10954	. . . . . . . . . . . . . . . . . . . 20 $/\$
348	340, 343, 345, 346, 347	lelttrd 10195	. . . . . . . . . . . . . . . . . . 19 $/\$
349		elfzle1 12344	. . . . . . . . . . . . . . . . . . . 20
350	349	adantl 482	. . . . . . . . . . . . . . . . . . 19 $/\$
351	340, 345, 342, 348, 350	ltletrd 10197	. . . . . . . . . . . . . . . . . 18 $/\$
352	340, 342, 351	ltled 10185	. . . . . . . . . . . . . . . . 17 $/\$
353	352	adantll 750	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$
354		elfzle2 12345	. . . . . . . . . . . . . . . . 17
355	354	adantl 482	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$
356	212	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$ $/\$
357	356, 257	syl 17	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$ $/\$ $/\$
358	337, 353, 355, 357	mpbir3and 1245	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$
359	335, 358	ffvelrnd 6360	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$
360	359	adantlr 751	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$ $/\$
361		simplll 798	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$
362		simplr 792	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$
363		simpr 477	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$
364	48	3ad2ant1 1082	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
365		elfzelz 12342	. . . . . . . . . . . . . . . . . . 19
366	365	3ad2ant3 1084	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
367	50	3ad2ant1 1082	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
368	366	zred 11482	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
369	224	3adant3 1081	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
370	227	3adant3 1081	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
371		elfzle1 12344	. . . . . . . . . . . . . . . . . . . . 21
372	371	3ad2ant3 1084	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
373	367, 369, 368, 370, 372	ltletrd 10197	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
374	367, 368, 373	ltled 10185	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
375	365	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$
376	375	zred 11482	. . . . . . . . . . . . . . . . . . . 20 $/\$
377	10	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$
378		1red 10055	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
379	377, 378	resubcld 10458	. . . . . . . . . . . . . . . . . . . . 21 $/\$
380		elfzle2 12345	. . . . . . . . . . . . . . . . . . . . . 22
381	380	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$
382	377	ltm1d 10956	. . . . . . . . . . . . . . . . . . . . 21 $/\$
383	376, 379, 377, 381, 382	lelttrd 10195	. . . . . . . . . . . . . . . . . . . 20 $/\$
384	376, 377, 383	ltled 10185	. . . . . . . . . . . . . . . . . . 19 $/\$
385	384	3adant2 1080	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
386	98	3ad2ant1 1082	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
387	386, 257	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
388	366, 374, 385, 387	mpbir3and 1245	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
389	364, 388	ffvelrnd 6360	. . . . . . . . . . . . . . . 16 $/\$ $/\$
390	366	peano2zd 11485	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
391	390	zred 11482	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
392	221	3ad2ant2 1083	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
393		1red 10055	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
394	226	3adant3 1081	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
395	392, 369, 368, 394, 372	ltletrd 10197	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
396	392, 368, 395	ltled 10185	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
397	392, 368, 393, 396	leadd1dd 10641	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
398	367, 369, 391, 370, 397	ltletrd 10197	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
399	367, 391, 398	ltled 10185	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
400		zltp1le 11427	. . . . . . . . . . . . . . . . . . . . 21 $/\$
401	365, 5, 400	syl2anr 495	. . . . . . . . . . . . . . . . . . . 20 $/\$
402	383, 401	mpbid 222	. . . . . . . . . . . . . . . . . . 19 $/\$
403	402	3adant2 1080	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
404	386, 300	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
405	390, 399, 403, 404	mpbir3and 1245	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
406	364, 405	ffvelrnd 6360	. . . . . . . . . . . . . . . 16 $/\$ $/\$
407		simp1 1061	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
408	1	3ad2ant1 1082	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
409		eluz 11701	. . . . . . . . . . . . . . . . . . . 20 $/\$
410	408, 366, 409	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
411	374, 410	mpbird 247	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
412	5	3ad2ant1 1082	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
413	383	3adant2 1080	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
414	411, 412, 413, 308	syl3anbrc 1246	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ..^
415	407, 414, 317	syl2anc 693	. . . . . . . . . . . . . . . 16 $/\$ $/\$
416	389, 406, 415	ltled 10185	. . . . . . . . . . . . . . 15 $/\$ $/\$
417	361, 362, 363, 416	syl3anc 1326	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$
418	417	adantlr 751	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$ $/\$
419	334, 360, 418	monoord 12831	. . . . . . . . . . . 12 $/\$ ..^ $/\$ $/\$
420	240, 237, 327, 329, 419	letrd 10194	. . . . . . . . . . 11 $/\$ ..^ $/\$ $/\$
421	66	rexrd 10089	. . . . . . . . . . . . . 14
422	78, 421	jca 554	. . . . . . . . . . . . 13 $/\$
423	194, 422	syl 17	. . . . . . . . . . . 12 $/\$ ..^ $/\$ $/\$ $/\$
424		elicc1 12219	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
425	423, 424	syl 17	. . . . . . . . . . 11 $/\$ ..^ $/\$ $/\$ $/\$ $/\$
426	196, 326, 420, 425	mpbir3and 1245	. . . . . . . . . 10 $/\$ ..^ $/\$ $/\$
427	194, 426, 152	syl2anc 693	. . . . . . . . 9 $/\$ ..^ $/\$ $/\$
428		simpll 790	. . . . . . . . . 10 $/\$ ..^ $/\$
429	242, 330, 210, 143	syl3anbrc 1246	. . . . . . . . . 10 $/\$ ..^ $/\$ ..^
430	428, 429, 167	syl2anc 693	. . . . . . . . 9 $/\$ ..^ $/\$
431	427, 430	itgcl 23550	. . . . . . . 8 $/\$ ..^ $/\$
432		fveq2 6191	. . . . . . . . . 10
433		oveq1 6657	. . . . . . . . . . 11
434	433	fveq2d 6195	. . . . . . . . . 10
435	432, 434	oveq12d 6668	. . . . . . . . 9
436	435	itgeq1d 40172	. . . . . . . 8
437	193, 431, 436	fzosump1 14481	. . . . . . 7 $/\$ ..^ ..^ ..^
438	437	3adant3 1081	. . . . . 6 $/\$ ..^ $/\$ ..^ ..^ ..^
439		oveq1 6657	. . . . . . . 8 ..^ ..^
440	439	eqcomd 2628	. . . . . . 7 ..^ ..^
441	440	3ad2ant3 1084	. . . . . 6 $/\$ ..^ $/\$ ..^ ..^
442	77	adantr 481	. . . . . . . . 9 $/\$ ..^
443	48	adantr 481	. . . . . . . . . 10 $/\$ ..^
444	182	adantl 482	. . . . . . . . . . . 12 $/\$ ..^
445	444	peano2zd 11485	. . . . . . . . . . 11 $/\$ ..^
446	445	zred 11482	. . . . . . . . . . . 12 $/\$ ..^
447	184	ltp1d 10954	. . . . . . . . . . . . 13 $/\$ ..^
448	181, 184, 446, 189, 447	lttrd 10198	. . . . . . . . . . . 12 $/\$ ..^
449	181, 446, 448	ltled 10185	. . . . . . . . . . 11 $/\$ ..^
450	208	adantl 482	. . . . . . . . . . . 12 $/\$ ..^
451		zltp1le 11427	. . . . . . . . . . . . 13 $/\$
452	182, 5, 451	syl2anr 495	. . . . . . . . . . . 12 $/\$ ..^
453	450, 452	mpbid 222	. . . . . . . . . . 11 $/\$ ..^
454	98	adantr 481	. . . . . . . . . . . 12 $/\$ ..^ $/\$
455		elfz1 12331	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
456	454, 455	syl 17	. . . . . . . . . . 11 $/\$ ..^ $/\$ $/\$
457	445, 449, 453, 456	mpbir3and 1245	. . . . . . . . . 10 $/\$ ..^
458	443, 457	ffvelrnd 6360	. . . . . . . . 9 $/\$ ..^
459	10	adantr 481	. . . . . . . . . . . . . 14 $/\$ ..^
460	184, 459, 450	ltled 10185	. . . . . . . . . . . . 13 $/\$ ..^
461		elfz1 12331	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
462	454, 461	syl 17	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$
463	444, 190, 460, 462	mpbir3and 1245	. . . . . . . . . . . 12 $/\$ ..^
464	443, 463	ffvelrnd 6360	. . . . . . . . . . 11 $/\$ ..^
465	464	rexrd 10089	. . . . . . . . . 10 $/\$ ..^
466	48	ad2antrr 762	. . . . . . . . . . . 12 $/\$ ..^ $/\$
467	466, 214	ffvelrnd 6360	. . . . . . . . . . 11 $/\$ ..^ $/\$
468	48	ad2antrr 762	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
469		elfzelz 12342	. . . . . . . . . . . . . . 15
470	469	adantl 482	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
471		elfzle1 12344	. . . . . . . . . . . . . . 15
472	471	adantl 482	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
473	470	zred 11482	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
474	10	ad2antrr 762	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
475	184	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
476		1red 10055	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
477	475, 476	resubcld 10458	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
478		elfzle2 12345	. . . . . . . . . . . . . . . . . 18
479	478	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
480	475	ltm1d 10956	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
481	473, 477, 475, 479, 480	lelttrd 10195	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
482	450	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
483	473, 475, 474, 481, 482	lttrd 10198	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
484	473, 474, 483	ltled 10185	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
485	98	ad2antrr 762	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$
486	485, 100	syl 17	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$ $/\$
487	470, 472, 484, 486	mpbir3and 1245	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
488	468, 487	ffvelrnd 6360	. . . . . . . . . . . 12 $/\$ ..^ $/\$
489	470	peano2zd 11485	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
490	50	ad2antrr 762	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
491	473, 476	readdcld 10069	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
492	473	ltp1d 10954	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
493	490, 473, 491, 472, 492	lelttrd 10195	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
494	490, 491, 493	ltled 10185	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
495		zltp1le 11427	. . . . . . . . . . . . . . . . . 18 $/\$
496	469, 444, 495	syl2anr 495	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
497	481, 496	mpbid 222	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
498	491, 475, 474, 497, 482	lelttrd 10195	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
499	491, 474, 498	ltled 10185	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
500	485, 135	syl 17	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$ $/\$
501	489, 494, 499, 500	mpbir3and 1245	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
502	468, 501	ffvelrnd 6360	. . . . . . . . . . . 12 $/\$ ..^ $/\$
503		simpll 790	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
504		elfzuz 12338	. . . . . . . . . . . . . . 15
505	504	adantl 482	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
506	5	ad2antrr 762	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
507	505, 506, 483, 143	syl3anbrc 1246	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ ..^
508	503, 507, 145	syl2anc 693	. . . . . . . . . . . 12 $/\$ ..^ $/\$
509	488, 502, 508	ltled 10185	. . . . . . . . . . 11 $/\$ ..^ $/\$
510	193, 467, 509	monoord 12831	. . . . . . . . . 10 $/\$ ..^
511	5	adantr 481	. . . . . . . . . . . . 13 $/\$ ..^
512		elfzo2 12473	. . . . . . . . . . . . 13 ..^ $/\$ $/\$
513	193, 511, 450, 512	syl3anbrc 1246	. . . . . . . . . . . 12 $/\$ ..^ ..^
514		eleq1 2689	. . . . . . . . . . . . . . 15 ..^ ..^
515	514	anbi2d 740	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ ..^
516	432, 434	breq12d 4666	. . . . . . . . . . . . . 14
517	515, 516	imbi12d 334	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ ..^
518	517, 145	chvarv 2263	. . . . . . . . . . . 12 $/\$ ..^
519	513, 518	syldan 487	. . . . . . . . . . 11 $/\$ ..^
520	464, 458, 519	ltled 10185	. . . . . . . . . 10 $/\$ ..^
521	78	adantr 481	. . . . . . . . . . 11 $/\$ ..^
522	458	rexrd 10089	. . . . . . . . . . 11 $/\$ ..^
523		elicc1 12219	. . . . . . . . . . 11 $/\$ $/\$ $/\$
524	521, 522, 523	syl2anc 693	. . . . . . . . . 10 $/\$ ..^ $/\$ $/\$
525	465, 510, 520, 524	mpbir3and 1245	. . . . . . . . 9 $/\$ ..^
526		simpll 790	. . . . . . . . . 10 $/\$ ..^ $/\$
527		eliccxr 39737	. . . . . . . . . . . 12
528	527	adantl 482	. . . . . . . . . . 11 $/\$ ..^ $/\$
529	78	ad2antrr 762	. . . . . . . . . . . 12 $/\$ ..^ $/\$
530	522	adantr 481	. . . . . . . . . . . 12 $/\$ ..^ $/\$
531		simpr 477	. . . . . . . . . . . 12 $/\$ ..^ $/\$
532		iccgelb 12230	. . . . . . . . . . . 12 $/\$ $/\$
533	529, 530, 531, 532	syl3anc 1326	. . . . . . . . . . 11 $/\$ ..^ $/\$
534	77	ad2antrr 762	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
535	458	adantr 481	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
536		eliccre 39728	. . . . . . . . . . . . 13 $/\$ $/\$
537	534, 535, 531, 536	syl3anc 1326	. . . . . . . . . . . 12 $/\$ ..^ $/\$
538	66	ad2antrr 762	. . . . . . . . . . . 12 $/\$ ..^ $/\$
539		iccleub 12229	. . . . . . . . . . . . 13 $/\$ $/\$
540	529, 530, 531, 539	syl3anc 1326	. . . . . . . . . . . 12 $/\$ ..^ $/\$
541		eluz2 11693	. . . . . . . . . . . . . . 15 $/\$ $/\$
542	445, 511, 453, 541	syl3anbrc 1246	. . . . . . . . . . . . . 14 $/\$ ..^
543	48	ad2antrr 762	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
544	1	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
545	5	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
546		elfzelz 12342	. . . . . . . . . . . . . . . . . . 19
547	546	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
548	544, 545, 547	3jca 1242	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$ $/\$
549	50	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
550	547	zred 11482	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
551	184	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
552	189	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
553	183	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ..^ $/\$
554		1red 10055	. . . . . . . . . . . . . . . . . . . . . 22 ..^ $/\$
555	553, 554	readdcld 10069	. . . . . . . . . . . . . . . . . . . . 21 ..^ $/\$
556	546	zred 11482	. . . . . . . . . . . . . . . . . . . . . 22
557	556	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 ..^ $/\$
558	553	ltp1d 10954	. . . . . . . . . . . . . . . . . . . . 21 ..^ $/\$
559		elfzle1 12344	. . . . . . . . . . . . . . . . . . . . . 22
560	559	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 ..^ $/\$
561	553, 555, 557, 558, 560	ltletrd 10197	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$
562	561	adantll 750	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
563	549, 551, 550, 552, 562	lttrd 10198	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
564	549, 550, 563	ltled 10185	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
565		elfzle2 12345	. . . . . . . . . . . . . . . . . 18
566	565	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
567	548, 564, 566	jca32 558	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$ $/\$ $/\$ $/\$
568		elfz2 12333	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
569	567, 568	sylibr 224	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
570	543, 569	ffvelrnd 6360	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
571	48	ad2antrr 762	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
572	1	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
573	5	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
574		elfzelz 12342	. . . . . . . . . . . . . . . . . . . 20
575	574	adantl 482	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
576	572, 573, 575	3jca 1242	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$ $/\$
577	50	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
578	575	zred 11482	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
579	184	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
580	189	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
581	183	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ..^ $/\$
582		1red 10055	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ $/\$
583	581, 582	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . 22 ..^ $/\$
584	574	zred 11482	. . . . . . . . . . . . . . . . . . . . . . 23
585	584	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ..^ $/\$
586	581	ltp1d 10954	. . . . . . . . . . . . . . . . . . . . . 22 ..^ $/\$
587		elfzle1 12344	. . . . . . . . . . . . . . . . . . . . . . 23
588	587	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ..^ $/\$
589	581, 583, 585, 586, 588	ltletrd 10197	. . . . . . . . . . . . . . . . . . . . 21 ..^ $/\$
590	589	adantll 750	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
591	577, 579, 578, 580, 590	lttrd 10198	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
592	577, 578, 591	ltled 10185	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
593	584	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$
594	10	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$
595		1red 10055	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
596	594, 595	resubcld 10458	. . . . . . . . . . . . . . . . . . . . 21 $/\$
597		elfzle2 12345	. . . . . . . . . . . . . . . . . . . . . 22
598	597	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$
599	594	ltm1d 10956	. . . . . . . . . . . . . . . . . . . . 21 $/\$
600	593, 596, 594, 598, 599	lelttrd 10195	. . . . . . . . . . . . . . . . . . . 20 $/\$
601	593, 594, 600	ltled 10185	. . . . . . . . . . . . . . . . . . 19 $/\$
602	601	adantlr 751	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
603	576, 592, 602	jca32 558	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$ $/\$ $/\$ $/\$
604	603, 568	sylibr 224	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
605	571, 604	ffvelrnd 6360	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
606	575	peano2zd 11485	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
607	572, 573, 606	3jca 1242	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$ $/\$
608	606	zred 11482	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
609	578	ltp1d 10954	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
610	579, 578, 608, 590, 609	lttrd 10198	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
611	577, 579, 608, 580, 610	lttrd 10198	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
612	577, 608, 611	ltled 10185	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
613	600	adantlr 751	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
614	574, 511, 132	syl2anr 495	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
615	613, 614	mpbid 222	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
616	607, 612, 615	jca32 558	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$ $/\$ $/\$ $/\$
617		elfz2 12333	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
618	616, 617	sylibr 224	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
619	571, 618	ffvelrnd 6360	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
620		simpll 790	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
621		eluz2 11693	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
622	572, 575, 592, 621	syl3anbrc 1246	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
623	622, 573, 613, 143	syl3anbrc 1246	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ ..^
624	620, 623, 145	syl2anc 693	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
625	605, 619, 624	ltled 10185	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
626	542, 570, 625	monoord 12831	. . . . . . . . . . . . 13 $/\$ ..^
627	626	adantr 481	. . . . . . . . . . . 12 $/\$ ..^ $/\$
628	537, 535, 538, 540, 627	letrd 10194	. . . . . . . . . . 11 $/\$ ..^ $/\$
629	422	ad2antrr 762	. . . . . . . . . . . 12 $/\$ ..^ $/\$ $/\$
630	629, 424	syl 17	. . . . . . . . . . 11 $/\$ ..^ $/\$ $/\$ $/\$
631	528, 533, 628, 630	mpbir3and 1245	. . . . . . . . . 10 $/\$ ..^ $/\$
632	526, 631, 152	syl2anc 693	. . . . . . . . 9 $/\$ ..^ $/\$
633		nfv 1843	. . . . . . . . . 10 $/\$ ..^
634	1	adantr 481	. . . . . . . . . 10 $/\$ ..^
635		elfzouz 12474	. . . . . . . . . . 11 ..^
636	635	adantl 482	. . . . . . . . . 10 $/\$ ..^
637		simpll 790	. . . . . . . . . . 11 $/\$ ..^ $/\$ ..^
638		elfzouz 12474	. . . . . . . . . . . . 13 ..^
639	638	adantl 482	. . . . . . . . . . . 12 $/\$ ..^ $/\$ ..^
640	5	ad2antrr 762	. . . . . . . . . . . 12 $/\$ ..^ $/\$ ..^
641		elfzoelz 12470	. . . . . . . . . . . . . . 15 ..^
642	641	zred 11482	. . . . . . . . . . . . . 14 ..^
643	642	adantl 482	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ ..^
644	184	adantr 481	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ ..^
645	10	ad2antrr 762	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ ..^
646		elfzolt2 12479	. . . . . . . . . . . . . 14 ..^
647	646	adantl 482	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ ..^
648	450	adantr 481	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ ..^
649	643, 644, 645, 647, 648	lttrd 10198	. . . . . . . . . . . 12 $/\$ ..^ $/\$ ..^
650	639, 640, 649, 143	syl3anbrc 1246	. . . . . . . . . . 11 $/\$ ..^ $/\$ ..^ ..^
651	637, 650, 145	syl2anc 693	. . . . . . . . . 10 $/\$ ..^ $/\$ ..^
652		simpll 790	. . . . . . . . . . 11 $/\$ ..^ $/\$
653	77	ad2antrr 762	. . . . . . . . . . . 12 $/\$ ..^ $/\$
654	66	ad2antrr 762	. . . . . . . . . . . 12 $/\$ ..^ $/\$
655	464	adantr 481	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
656		simpr 477	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
657		eliccre 39728	. . . . . . . . . . . . 13 $/\$ $/\$
658	653, 655, 656, 657	syl3anc 1326	. . . . . . . . . . . 12 $/\$ ..^ $/\$
659	78	ad2antrr 762	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
660	465	adantr 481	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
661		iccgelb 12230	. . . . . . . . . . . . 13 $/\$ $/\$
662	659, 660, 656, 661	syl3anc 1326	. . . . . . . . . . . 12 $/\$ ..^ $/\$
663		iccleub 12229	. . . . . . . . . . . . . 14 $/\$ $/\$
664	659, 660, 656, 663	syl3anc 1326	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
665		elfzouz2 12484	. . . . . . . . . . . . . . . 16 ..^
666	665	adantl 482	. . . . . . . . . . . . . . 15 $/\$ ..^
667	48	ad2antrr 762	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
668	1	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
669	5	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
670		elfzelz 12342	. . . . . . . . . . . . . . . . . . . 20
671	670	adantl 482	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
672	668, 669, 671	3jca 1242	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$ $/\$
673	50	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
674	671	zred 11482	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
675	184	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
676	189	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
677		elfzle1 12344	. . . . . . . . . . . . . . . . . . . . 21
678	677	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
679	673, 675, 674, 676, 678	ltletrd 10197	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
680	673, 674, 679	ltled 10185	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
681		elfzle2 12345	. . . . . . . . . . . . . . . . . . 19
682	681	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
683	672, 680, 682	jca32 558	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$ $/\$ $/\$ $/\$
684	683, 568	sylibr 224	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
685	667, 684	ffvelrnd 6360	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
686	48	ad2antrr 762	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
687	1	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
688	5	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
689		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . 21
690	689	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
691	687, 688, 690	3jca 1242	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$ $/\$
692	50	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
693	690	zred 11482	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
694	184	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
695	189	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
696		elfzle1 12344	. . . . . . . . . . . . . . . . . . . . . 22
697	696	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
698	692, 694, 693, 695, 697	ltletrd 10197	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
699	692, 693, 698	ltled 10185	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
700	689	zred 11482	. . . . . . . . . . . . . . . . . . . . . 22
701	700	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$
702	10	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$
703		1red 10055	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
704	702, 703	resubcld 10458	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
705		elfzle2 12345	. . . . . . . . . . . . . . . . . . . . . . 23
706	705	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
707	702	ltm1d 10956	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
708	701, 704, 702, 706, 707	lelttrd 10195	. . . . . . . . . . . . . . . . . . . . 21 $/\$
709	701, 702, 708	ltled 10185	. . . . . . . . . . . . . . . . . . . 20 $/\$
710	709	adantlr 751	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
711	691, 699, 710	jca32 558	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$ $/\$ $/\$ $/\$
712	711, 568	sylibr 224	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
713	686, 712	ffvelrnd 6360	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
714	690	peano2zd 11485	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
715	687, 688, 714	3jca 1242	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$ $/\$
716	714	zred 11482	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
717	693	ltp1d 10954	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
718	692, 693, 716, 699, 717	lelttrd 10195	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
719	692, 716, 718	ltled 10185	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
720	689, 5, 132	syl2anr 495	. . . . . . . . . . . . . . . . . . . . 21 $/\$
721	708, 720	mpbid 222	. . . . . . . . . . . . . . . . . . . 20 $/\$
722	721	adantlr 751	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
723	715, 719, 722	jca32 558	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$ $/\$ $/\$ $/\$
724	723, 617	sylibr 224	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
725	686, 724	ffvelrnd 6360	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
726		simpll 790	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
727	687, 690, 699, 621	syl3anbrc 1246	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
728	708	adantlr 751	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
729	727, 688, 728, 143	syl3anbrc 1246	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ ..^
730	726, 729, 145	syl2anc 693	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
731	713, 725, 730	ltled 10185	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
732	666, 685, 731	monoord 12831	. . . . . . . . . . . . . 14 $/\$ ..^
733	732	adantr 481	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
734	658, 655, 654, 664, 733	letrd 10194	. . . . . . . . . . . 12 $/\$ ..^ $/\$
735	653, 654, 658, 662, 734	eliccd 39726	. . . . . . . . . . 11 $/\$ ..^ $/\$
736	652, 735, 152	syl2anc 693	. . . . . . . . . 10 $/\$ ..^ $/\$
737	637, 650, 167	syl2anc 693	. . . . . . . . . 10 $/\$ ..^ $/\$ ..^
738	633, 634, 636, 467, 651, 736, 737	iblspltprt 40189	. . . . . . . . 9 $/\$ ..^
739	435	mpteq1d 4738	. . . . . . . . . . . . 13
740	739	eleq1d 2686	. . . . . . . . . . . 12
741	515, 740	imbi12d 334	. . . . . . . . . . 11 $/\$ ..^ $/\$ ..^
742	741, 167	chvarv 2263	. . . . . . . . . 10 $/\$ ..^
743	513, 742	syldan 487	. . . . . . . . 9 $/\$ ..^
744	442, 458, 525, 632, 738, 743	itgspliticc 23603	. . . . . . . 8 $/\$ ..^
745	744	eqcomd 2628	. . . . . . 7 $/\$ ..^
746	745	3adant3 1081	. . . . . 6 $/\$ ..^ $/\$ ..^
747	438, 441, 746	3eqtrrd 2661	. . . . 5 $/\$ ..^ $/\$ ..^ ..^
748	177, 178, 180, 747	syl3anc 1326	. . . 4 ..^ $/\$ ..^ $/\$ ..^
749	748	3exp 1264	. . 3 ..^ ..^ ..^
750	21, 28, 35, 42, 176, 749	fzind2 12586	. 2 ..^
751	14, 750	mpcom 38	1 ..^

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1483

wcel 1990 class class class wbr 4653

cmpt 4729

wf 5884

cfv 5888 (class class class)co 6650

cc 9934

cr 9935

c1 9937

caddc 9939

cxr 10073

clt 10074

cle 10075

cmin 10266

cz 11377

cuz 11687

cicc 12178

cfz 12326 ..^cfzo 12465

csu 14416

cibl 23386

citg 23387

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 ax-addf 10015

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-disj 4621 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-of 6897 df-ofr 6898 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fi 8317 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-cda 8990 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-4 11081 df-n0 11293 df-z 11378 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ioo 12179 df-ico 12181 df-icc 12182 df-fz 12327 df-fzo 12466 df-fl 12593 df-mod 12669 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-sum 14417 df-rest 16083 df-topgen 16104 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-top 20699 df-topon 20716 df-bases 20750 df-cmp 21190 df-ovol 23233 df-vol 23234 df-mbf 23388 df-itg1 23389 df-itg2 23390 df-ibl 23391 df-itg 23392

This theorem is referenced by: fourierdlem73 40396 fourierdlem81 40404 fourierdlem93 40416

W3C validator