itgspltprt - Mathbox for Glauco Siliprandi

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

Theorem itgspltprt 31620

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 10981	. . . . 5
3		itgspltprt.2	. . . . . 6
4		eluzelz 11103	. . . . . 6
5	3, 4	syl 16	. . . . 5
6	2, 5, 5	3jca 1176	. . . 4 $/\$ $/\$
7		eluzle 11106	. . . . 5
8	3, 7	syl 16	. . . 4
9		eluzelre 11104	. . . . . 6
10	3, 9	syl 16	. . . . 5
11	10	leidd 10131	. . . 4
12	6, 8, 11	jca32 535	. . 3 $/\$ $/\$ $/\$ $/\$
13		elfz2 11691	. . 3 $/\$ $/\$ $/\$ $/\$
14	12, 13	sylibr 212	. 2
15		fveq2 5872	. . . . . . 7
16	15	oveq2d 6311	. . . . . 6
17		itgeq1 22047	. . . . . 6
18	16, 17	syl 16	. . . . 5
19		oveq2 6303	. . . . . 6 ..^ ..^
20	19	sumeq1d 13503	. . . . 5 ..^ ..^
21	18, 20	eqeq12d 2489	. . . 4 ..^ ..^
22	21	imbi2d 316	. . 3 ..^ ..^
23		fveq2 5872	. . . . . . 7
24	23	oveq2d 6311	. . . . . 6
25		itgeq1 22047	. . . . . 6
26	24, 25	syl 16	. . . . 5
27		oveq2 6303	. . . . . 6 ..^ ..^
28	27	sumeq1d 13503	. . . . 5 ..^ ..^
29	26, 28	eqeq12d 2489	. . . 4 ..^ ..^
30	29	imbi2d 316	. . 3 ..^ ..^
31		fveq2 5872	. . . . . . 7
32	31	oveq2d 6311	. . . . . 6
33		itgeq1 22047	. . . . . 6
34	32, 33	syl 16	. . . . 5
35		oveq2 6303	. . . . . 6 ..^ ..^
36	35	sumeq1d 13503	. . . . 5 ..^ ..^
37	34, 36	eqeq12d 2489	. . . 4 ..^ ..^
38	37	imbi2d 316	. . 3 ..^ ..^
39		fveq2 5872	. . . . . . 7
40	39	oveq2d 6311	. . . . . 6
41		itgeq1 22047	. . . . . 6
42	40, 41	syl 16	. . . . 5
43		oveq2 6303	. . . . . 6 ..^ ..^
44	43	sumeq1d 13503	. . . . 5 ..^ ..^
45	42, 44	eqeq12d 2489	. . . 4 ..^ ..^
46	45	imbi2d 316	. . 3 ..^ ..^
47	1	adantl 466	. . . . . . . . 9 $/\$
48		fzval3 11865	. . . . . . . . 9 ..^
49	47, 48	syl 16	. . . . . . . 8 $/\$ ..^
50	49	eqcomd 2475	. . . . . . 7 $/\$ ..^
51	50	sumeq1d 13503	. . . . . 6 $/\$ ..^
52		simpl 457	. . . . . . . . . . . . 13 $/\$
53		itgspltprt.3	. . . . . . . . . . . . . . . . . . . 20
54	52, 53	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$
55	1	zred 10978	. . . . . . . . . . . . . . . . . . . . . . 23
56		1re 9607	. . . . . . . . . . . . . . . . . . . . . . . . . 26
57	56	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25
58	55, 57	readdcld 9635	. . . . . . . . . . . . . . . . . . . . . . . 24
59	55	ltp1d 10488	. . . . . . . . . . . . . . . . . . . . . . . 24
60	55, 58, 10, 59, 8	ltletrd 9753	. . . . . . . . . . . . . . . . . . . . . . 23
61	55, 10, 60	ltled 9744	. . . . . . . . . . . . . . . . . . . . . 22
62	1, 5	jca 532	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
63		eluz 11107	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
64	62, 63	syl 16	. . . . . . . . . . . . . . . . . . . . . 22
65	61, 64	mpbird 232	. . . . . . . . . . . . . . . . . . . . 21
66		eluzfz1 11705	. . . . . . . . . . . . . . . . . . . . 21
67	65, 66	syl 16	. . . . . . . . . . . . . . . . . . . 20
68	67	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$
69	54, 68	jca 532	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
70		ffvelrn 6030	. . . . . . . . . . . . . . . . . 18 $/\$
71	69, 70	syl 16	. . . . . . . . . . . . . . . . 17 $/\$
72	55	lep1d 10489	. . . . . . . . . . . . . . . . . . . . . 22
73	2, 72, 8	3jca 1176	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
74		elfz1 11689	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
75	62, 74	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
76	73, 75	mpbird 232	. . . . . . . . . . . . . . . . . . . 20
77	53, 76	jca 532	. . . . . . . . . . . . . . . . . . 19 $/\$
78		ffvelrn 6030	. . . . . . . . . . . . . . . . . . 19 $/\$
79	77, 78	syl 16	. . . . . . . . . . . . . . . . . 18
80	52, 79	syl 16	. . . . . . . . . . . . . . . . 17 $/\$
81		simpr 461	. . . . . . . . . . . . . . . . 17 $/\$
82	71, 80, 81	3jca 1176	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
83		eliccre 31427	. . . . . . . . . . . . . . . 16 $/\$ $/\$
84	82, 83	syl 16	. . . . . . . . . . . . . . 15 $/\$
85	53, 67, 70	syl2anc 661	. . . . . . . . . . . . . . . . . . 19
86	85	rexrd 9655	. . . . . . . . . . . . . . . . . 18
87	86	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$
88	80	rexrd 9655	. . . . . . . . . . . . . . . . 17 $/\$
89	87, 88, 81	3jca 1176	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
90		iccgelb 11593	. . . . . . . . . . . . . . . 16 $/\$ $/\$
91	89, 90	syl 16	. . . . . . . . . . . . . . 15 $/\$
92	5, 61, 11	3jca 1176	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
93		elfz1 11689	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
94	62, 93	syl 16	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
95	92, 94	mpbird 232	. . . . . . . . . . . . . . . . . . 19
96	53, 95	jca 532	. . . . . . . . . . . . . . . . . 18 $/\$
97		ffvelrn 6030	. . . . . . . . . . . . . . . . . 18 $/\$
98	96, 97	syl 16	. . . . . . . . . . . . . . . . 17
99	52, 98	syl 16	. . . . . . . . . . . . . . . 16 $/\$
100		iccleub 11592	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
101	89, 100	syl 16	. . . . . . . . . . . . . . . 16 $/\$
102	53	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$
103		elfzelz 11700	. . . . . . . . . . . . . . . . . . . . . . 23
104	103	adantl 466	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
105	55	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
106	104	zred 10978	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
107	58	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
108	59	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
109		elfzle1 11701	. . . . . . . . . . . . . . . . . . . . . . . . 25
110	109	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
111	105, 107, 106, 108, 110	ltletrd 9753	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
112	105, 106, 111	ltled 9744	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
113		elfzle2 11702	. . . . . . . . . . . . . . . . . . . . . . 23
114	113	adantl 466	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
115	104, 112, 114	3jca 1176	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
116	62	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
117		elfz1 11689	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
118	116, 117	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
119	115, 118	mpbird 232	. . . . . . . . . . . . . . . . . . . 20 $/\$
120	102, 119	jca 532	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
121		ffvelrn 6030	. . . . . . . . . . . . . . . . . . 19 $/\$
122	120, 121	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$
123	53	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 $/\$
124		elfzelz 11700	. . . . . . . . . . . . . . . . . . . . . . . 24
125	124	adantl 466	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
126	55	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
127	125	zred 10978	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
128	58	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
129	59	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
130		elfzle1 11701	. . . . . . . . . . . . . . . . . . . . . . . . . 26
131	130	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
132	126, 128, 127, 129, 131	ltletrd 9753	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
133	126, 127, 132	ltled 9744	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
134	10	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
135	56	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
136	134, 135	resubcld 9999	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
137		elfzle2 11702	. . . . . . . . . . . . . . . . . . . . . . . . . 26
138	137	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
139	134	ltm1d 10490	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
140	127, 136, 134, 138, 139	lelttrd 9751	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
141	127, 134, 140	ltled 9744	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
142	125, 133, 141	3jca 1176	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
143	62	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
144	143, 117	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
145	142, 144	mpbird 232	. . . . . . . . . . . . . . . . . . . . 21 $/\$
146	123, 145	jca 532	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
147	146, 121	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$
148	125	peano2zd 10981	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
149	127, 135	readdcld 9635	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
150	126, 127, 135, 132	ltadd1dd 10175	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
151	126, 128, 149, 129, 150	lttrd 9754	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
152	126, 149, 151	ltled 9744	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
153	5, 124	anim12ci 567	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
154		zltp1le 10924	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
155	153, 154	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
156	140, 155	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
157	148, 152, 156	3jca 1176	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
158		elfz1 11689	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
159	143, 158	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
160	157, 159	mpbird 232	. . . . . . . . . . . . . . . . . . . . 21 $/\$
161	123, 160	jca 532	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
162		ffvelrn 6030	. . . . . . . . . . . . . . . . . . . 20 $/\$
163	161, 162	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$
164		simpl 457	. . . . . . . . . . . . . . . . . . . . 21 $/\$
165	1, 124	anim12i 566	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
166		eluz 11107	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
167	165, 166	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
168	133, 167	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
169	164, 5	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
170	168, 169, 140	3jca 1176	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
171		elfzo2 11812	. . . . . . . . . . . . . . . . . . . . . 22 ..^ $/\$ $/\$
172	170, 171	sylibr 212	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^
173	164, 172	jca 532	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ ..^
174		itgspltprt.4	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^
175	173, 174	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$
176	147, 163, 175	ltled 9744	. . . . . . . . . . . . . . . . . 18 $/\$
177	3, 122, 176	monoord 12117	. . . . . . . . . . . . . . . . 17
178	52, 177	syl 16	. . . . . . . . . . . . . . . 16 $/\$
179	84, 80, 99, 101, 178	letrd 9750	. . . . . . . . . . . . . . 15 $/\$
180	84, 91, 179	3jca 1176	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
181	71, 99	jca 532	. . . . . . . . . . . . . . 15 $/\$ $/\$
182		elicc2 11601	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
183	181, 182	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
184	180, 183	mpbird 232	. . . . . . . . . . . . 13 $/\$
185	52, 184	jca 532	. . . . . . . . . . . 12 $/\$ $/\$
186		itgspltprt.5	. . . . . . . . . . . 12 $/\$
187	185, 186	syl 16	. . . . . . . . . . 11 $/\$
188		id 22	. . . . . . . . . . . . 13
189		fzolb 11814	. . . . . . . . . . . . . 14 ..^ $/\$ $/\$
190	1, 5, 60, 189	syl3anbrc 1180	. . . . . . . . . . . . 13 ..^
191	188, 190	jca 532	. . . . . . . . . . . 12 $/\$ ..^
192		eleq1 2539	. . . . . . . . . . . . . . 15 ..^ ..^
193	192	anbi2d 703	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ ..^
194		fveq2 5872	. . . . . . . . . . . . . . . . 17
195		oveq1 6302	. . . . . . . . . . . . . . . . . 18
196	195	fveq2d 5876	. . . . . . . . . . . . . . . . 17
197	194, 196	oveq12d 6313	. . . . . . . . . . . . . . . 16
198	197	mpteq1d 4534	. . . . . . . . . . . . . . 15
199	198	eleq1d 2536	. . . . . . . . . . . . . 14
200	193, 199	imbi12d 320	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ ..^
201		itgspltprt.6	. . . . . . . . . . . . . 14 $/\$ ..^
202	201	a1i 11	. . . . . . . . . . . . 13 $/\$ ..^
203	200, 202	vtoclga 3182	. . . . . . . . . . . 12 $/\$ ..^
204	1, 191, 203	sylc 60	. . . . . . . . . . 11
205	187, 204	itgcl 22058	. . . . . . . . . 10
206	205	idi 2	. . . . . . . . 9
207	1, 206	jca 532	. . . . . . . 8 $/\$
208		itgeq1 22047	. . . . . . . . . 10
209	197, 208	syl 16	. . . . . . . . 9
210	209	fsum1 13544	. . . . . . . 8 $/\$
211	207, 210	syl 16	. . . . . . 7
212	211	adantl 466	. . . . . 6 $/\$
213		eqidd 2468	. . . . . 6 $/\$
214	51, 212, 213	3eqtrd 2512	. . . . 5 $/\$ ..^
215	214	eqcomd 2475	. . . 4 $/\$ ..^
216	215	ex 434	. . 3 ..^
217		simp3 998	. . . . . 6 ..^ $/\$ ..^ $/\$
218		simp1 996	. . . . . 6 ..^ $/\$ ..^ $/\$ ..^
219		simp2 997	. . . . . . . 8 ..^ $/\$ ..^ $/\$ ..^
220	217, 219	jca 532	. . . . . . 7 ..^ $/\$ ..^ $/\$ $/\$ ..^
221		pm3.35 587	. . . . . . 7 $/\$ ..^ ..^
222	220, 221	syl 16	. . . . . 6 ..^ $/\$ ..^ $/\$ ..^
223	217, 218, 222	3jca 1176	. . . . 5 ..^ $/\$ ..^ $/\$ $/\$ ..^ $/\$ ..^
224	55	adantr 465	. . . . . . . . . . 11 $/\$ ..^
225		elfzoelz 11809	. . . . . . . . . . . . 13 ..^
226	225	zred 10978	. . . . . . . . . . . 12 ..^
227	226	adantl 466	. . . . . . . . . . 11 $/\$ ..^
228	58	adantr 465	. . . . . . . . . . . 12 $/\$ ..^
229	59	adantr 465	. . . . . . . . . . . 12 $/\$ ..^
230		elfzole1 11816	. . . . . . . . . . . . 13 ..^
231	230	adantl 466	. . . . . . . . . . . 12 $/\$ ..^
232	224, 228, 227, 229, 231	ltletrd 9753	. . . . . . . . . . 11 $/\$ ..^
233	224, 227, 232	ltled 9744	. . . . . . . . . 10 $/\$ ..^
234	1, 225	anim12i 566	. . . . . . . . . . 11 $/\$ ..^ $/\$
235		eluz 11107	. . . . . . . . . . 11 $/\$
236	234, 235	syl 16	. . . . . . . . . 10 $/\$ ..^
237	233, 236	mpbird 232	. . . . . . . . 9 $/\$ ..^
238	188	ad3antrrr 729	. . . . . . . . . . . 12 $/\$ ..^ $/\$ $/\$
239		eliccxr 31437	. . . . . . . . . . . . . . 15
240	239	adantl 466	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$
241	238, 85	syl 16	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$
242	238, 53	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$
243		elfzelz 11700	. . . . . . . . . . . . . . . . . . . . 21
244	243	adantl 466	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
245		elfzle1 11701	. . . . . . . . . . . . . . . . . . . . 21
246	245	adantl 466	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
247	244	zred 10978	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
248	10	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
249	227	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$
250		elfzle2 11702	. . . . . . . . . . . . . . . . . . . . . . 23
251	250	adantl 466	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$
252		elfzolt2 11817	. . . . . . . . . . . . . . . . . . . . . . 23 ..^
253	252	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$
254	247, 249, 248, 251, 253	lelttrd 9751	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
255	247, 248, 254	ltled 9744	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
256	244, 246, 255	3jca 1176	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$ $/\$
257	62	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$
258	257, 117	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$ $/\$
259	256, 258	mpbird 232	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
260	259	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$
261	242, 260	jca 532	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$ $/\$
262	261, 121	syl 16	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$
263	244	peano2zd 10981	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$
264	224	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$
265	263	zred 10978	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$
266	55	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
267	243	zred 10978	. . . . . . . . . . . . . . . . . . . . . . . . . 26
268	267	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
269	56	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
270	268, 269	readdcld 9635	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
271	245	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
272	268	ltp1d 10488	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
273	266, 268, 270, 271, 272	lelttrd 9751	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
274	273	adantlr 714	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$
275	264, 265, 274	ltled 9744	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$
276	5, 243	anim12ci 567	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
277	276	adantlr 714	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^ $/\$ $/\$
278	277, 154	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$
279	254, 278	mpbid 210	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$
280	263, 275, 279	3jca 1176	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$ $/\$ $/\$
281	257, 158	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$ $/\$ $/\$
282	280, 281	mpbird 232	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
283	282	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
284	242, 283	jca 532	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$ $/\$
285	284, 162	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$
286		simpr 461	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$
287	262, 285, 286	3jca 1176	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$ $/\$ $/\$
288		eliccre 31427	. . . . . . . . . . . . . . . 16 $/\$ $/\$
289	287, 288	syl 16	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$
290		elfzuz 11696	. . . . . . . . . . . . . . . . . 18
291	290	adantl 466	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
292	53	ad3antrrr 729	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
293		elfzelz 11700	. . . . . . . . . . . . . . . . . . . . . 22
294	293	adantl 466	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$ $/\$
295		elfzle1 11701	. . . . . . . . . . . . . . . . . . . . . 22
296	295	adantl 466	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$ $/\$
297	294	zred 10978	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$ $/\$
298	248	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$ $/\$
299	247	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$ $/\$
300		elfzle2 11702	. . . . . . . . . . . . . . . . . . . . . . . 24
301	300	adantl 466	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$ $/\$
302	254	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$ $/\$
303	297, 299, 298, 301, 302	lelttrd 9751	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$ $/\$
304	297, 298, 303	ltled 9744	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$ $/\$
305	294, 296, 304	3jca 1176	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$ $/\$ $/\$
306	257	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$ $/\$ $/\$
307		elfz1 11689	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
308	306, 307	syl 16	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$ $/\$ $/\$
309	305, 308	mpbird 232	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
310	292, 309	jca 532	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$ $/\$
311		ffvelrn 6030	. . . . . . . . . . . . . . . . . 18 $/\$
312	310, 311	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$
313	53	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$
314		elfzelz 11700	. . . . . . . . . . . . . . . . . . . . . . 23
315	314	adantl 466	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$ $/\$
316		elfzle1 11701	. . . . . . . . . . . . . . . . . . . . . . 23
317	316	adantl 466	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$ $/\$
318	315	zred 10978	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$ $/\$
319	248	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$ $/\$
320	247	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^ $/\$ $/\$
321	56	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ ..^ $/\$ $/\$
322	320, 321	resubcld 9999	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$ $/\$
323		elfzle2 11702	. . . . . . . . . . . . . . . . . . . . . . . . . 26
324	323	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$ $/\$
325	320	ltm1d 10490	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$ $/\$
326	318, 322, 320, 324, 325	lelttrd 9751	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^ $/\$ $/\$
327	254	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^ $/\$ $/\$
328	318, 320, 319, 326, 327	lttrd 9754	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$ $/\$
329	318, 319, 328	ltled 9744	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$ $/\$
330	315, 317, 329	3jca 1176	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$ $/\$ $/\$ $/\$
331	257	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$ $/\$ $/\$
332	331, 307	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$ $/\$ $/\$ $/\$
333	330, 332	mpbird 232	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$
334	313, 333	jca 532	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$ $/\$
335	334, 311	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
336	315	peano2zd 10981	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$ $/\$
337	264	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$ $/\$
338	318, 321	readdcld 9635	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$ $/\$
339		simplll 757	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$ $/\$
340		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$ $/\$
341	339, 340	jca 532	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^ $/\$ $/\$ $/\$
342	55	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
343	314	zred 10978	. . . . . . . . . . . . . . . . . . . . . . . . . 26
344	343	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
345	56	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
346	344, 345	readdcld 9635	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
347	316	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
348	344	ltp1d 10488	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
349	342, 344, 346, 347, 348	lelttrd 9751	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
350	341, 349	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$ $/\$
351	337, 338, 350	ltled 9744	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$ $/\$
352	244, 314	anim12ci 567	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ ..^ $/\$ $/\$ $/\$
353		zltp1le 10924	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
354	352, 353	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$ $/\$
355	326, 354	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^ $/\$ $/\$
356	338, 320, 319, 355, 327	lelttrd 9751	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$ $/\$
357	338, 319, 356	ltled 9744	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$ $/\$
358	336, 351, 357	3jca 1176	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$ $/\$ $/\$ $/\$
359		elfz1 11689	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
360	331, 359	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$ $/\$ $/\$ $/\$
361	358, 360	mpbird 232	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$
362	313, 361	jca 532	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$ $/\$
363		ffvelrn 6030	. . . . . . . . . . . . . . . . . . 19 $/\$
364	362, 363	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
365		elfzuz 11696	. . . . . . . . . . . . . . . . . . . . . . 23
366	365	adantl 466	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$ $/\$
367	339, 5	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$ $/\$
368	366, 367, 328	3jca 1176	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$ $/\$ $/\$ $/\$
369		elfzo2 11812	. . . . . . . . . . . . . . . . . . . . 21 ..^ $/\$ $/\$
370	368, 369	sylibr 212	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$ ..^
371	339, 370	jca 532	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$ $/\$ ..^
372		nfv 1683	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^
373		eleq1 2539	. . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^
374	373	anbi2d 703	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$ ..^
375		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . 22
376		oveq1 6302	. . . . . . . . . . . . . . . . . . . . . . 23
377	376	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . 22
378	375, 377	breq12d 4466	. . . . . . . . . . . . . . . . . . . . 21
379	374, 378	imbi12d 320	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ ..^
380	372, 379, 174	chvar 1982	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^
381	371, 380	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
382	335, 364, 381	ltled 9744	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$
383	291, 312, 382	monoord 12117	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
384	383	adantr 465	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$
385	262	rexrd 9655	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$
386	285	rexrd 9655	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$
387	385, 386, 286	3jca 1176	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$ $/\$ $/\$
388		iccgelb 11593	. . . . . . . . . . . . . . . 16 $/\$ $/\$
389	387, 388	syl 16	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$
390	241, 262, 289, 384, 389	letrd 9750	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$
391	238, 98	syl 16	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$
392		iccleub 11592	. . . . . . . . . . . . . . . 16 $/\$ $/\$
393	387, 392	syl 16	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$
394	257	simprd 463	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
395	263, 394	jca 532	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
396		eluz 11107	. . . . . . . . . . . . . . . . . . 19 $/\$
397	395, 396	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ <