ovolicc2lem4OLD - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ovolicc2lem4OLD		Structured version Unicode version

Theorem ovolicc2lem4OLD 22460

Description: Lemma for ovolicc2 22463. (Contributed by Mario Carneiro, 14-Jun-2014.) Obsolete version of ovolicc2lem4 22461 as of 17-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.)

**Hypotheses**
Ref	Expression
ovolicc.1
ovolicc.2
ovolicc.3
ovolicc2.4
ovolicc2.5
ovolicc2.6
ovolicc2.7
ovolicc2.8
ovolicc2.9	$/\$
ovolicc2.10
ovolicc2.11
ovolicc2.12	$/\$
ovolicc2.13
ovolicc2.14
ovolicc2.15
ovolicc2.16
ovolicc2lem4OLD.17

**Assertion**
Ref	Expression
ovolicc2lem4OLD

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

Proof of Theorem ovolicc2lem4OLD Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		arch 10867	. . . . 5
2	1	ad2antlr 731	. . . 4 $/\$ $/\$
3		df-ima 4863	. . . . . . . . . . . . . . . 16
4		ovolicc2.8	. . . . . . . . . . . . . . . . . . 19
5		nnuz 11195	. . . . . . . . . . . . . . . . . . . . 21
6		ovolicc2.15	. . . . . . . . . . . . . . . . . . . . 21
7		1zzd 10969	. . . . . . . . . . . . . . . . . . . . 21
8		ovolicc2.14	. . . . . . . . . . . . . . . . . . . . 21
9		ovolicc2.11	. . . . . . . . . . . . . . . . . . . . 21
10	5, 6, 7, 8, 9	algrf 14520	. . . . . . . . . . . . . . . . . . . 20
11		ovolicc2.10	. . . . . . . . . . . . . . . . . . . . 21
12		ssrab2 3546	. . . . . . . . . . . . . . . . . . . . 21
13	11, 12	eqsstri 3494	. . . . . . . . . . . . . . . . . . . 20
14		fss 5751	. . . . . . . . . . . . . . . . . . . 20 $/\$
15	10, 13, 14	sylancl 666	. . . . . . . . . . . . . . . . . . 19
16		fco 5753	. . . . . . . . . . . . . . . . . . 19 $/\$
17	4, 15, 16	syl2anc 665	. . . . . . . . . . . . . . . . . 18
18		elfznn 11829	. . . . . . . . . . . . . . . . . . 19
19	18	ssriv 3468	. . . . . . . . . . . . . . . . . 18
20		fssres 5763	. . . . . . . . . . . . . . . . . 18 $/\$
21	17, 19, 20	sylancl 666	. . . . . . . . . . . . . . . . 17
22		frn 5749	. . . . . . . . . . . . . . . . 17
23	21, 22	syl 17	. . . . . . . . . . . . . . . 16
24	3, 23	syl5eqss 3508	. . . . . . . . . . . . . . 15
25		nnssre 10614	. . . . . . . . . . . . . . 15
26	24, 25	syl6ss 3476	. . . . . . . . . . . . . 14
27	26	ad3antrrr 734	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
28		simpr 462	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
29	27, 28	sseldd 3465	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
30		simpllr 767	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
31		nnre 10617	. . . . . . . . . . . . 13
32	31	ad2antlr 731	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
33		lelttr 9725	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
34	29, 30, 32, 33	syl3anc 1264	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
35	34	ancomsd 455	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
36	35	expdimp 438	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
37	36	an32s 811	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
38	37	ralimdva 2833	. . . . . . 7 $/\$ $/\$ $/\$
39	38	impancom 441	. . . . . 6 $/\$ $/\$ $/\$
40	39	an32s 811	. . . . 5 $/\$ $/\$ $/\$
41	40	reximdva 2900	. . . 4 $/\$ $/\$
42	2, 41	mpd 15	. . 3 $/\$ $/\$
43		fzfid 12186	. . . . 5
44		fvres 5892	. . . . . . . . . . . . . . 15
45	44	adantl 467	. . . . . . . . . . . . . 14 $/\$
46		fvco3 5955	. . . . . . . . . . . . . . 15 $/\$
47	10, 18, 46	syl2an 479	. . . . . . . . . . . . . 14 $/\$
48	45, 47	eqtrd 2463	. . . . . . . . . . . . 13 $/\$
49	48	adantrr 721	. . . . . . . . . . . 12 $/\$ $/\$
50		fvres 5892	. . . . . . . . . . . . . 14
51	50	ad2antll 733	. . . . . . . . . . . . 13 $/\$ $/\$
52		elfznn 11829	. . . . . . . . . . . . . . 15
53	52	adantl 467	. . . . . . . . . . . . . 14 $/\$
54		fvco3 5955	. . . . . . . . . . . . . 14 $/\$
55	10, 53, 54	syl2an 479	. . . . . . . . . . . . 13 $/\$ $/\$
56	51, 55	eqtrd 2463	. . . . . . . . . . . 12 $/\$ $/\$
57	49, 56	eqeq12d 2444	. . . . . . . . . . 11 $/\$ $/\$
58		fveq2 5878	. . . . . . . . . . . . 13
59	58	fveq2d 5882	. . . . . . . . . . . 12
60	19	a1i 11	. . . . . . . . . . . . . . . . 17
61		elfznn 11829	. . . . . . . . . . . . . . . . . . . . 21
62	61	ad2antlr 731	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
63	62	nnred 10625	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
64		ovolicc2.16	. . . . . . . . . . . . . . . . . . . . . . 23
65		ssrab2 3546	. . . . . . . . . . . . . . . . . . . . . . 23
66	64, 65	eqsstri 3494	. . . . . . . . . . . . . . . . . . . . . 22
67	66, 25	sstri 3473	. . . . . . . . . . . . . . . . . . . . 21
68		ovolicc2lem4OLD.17	. . . . . . . . . . . . . . . . . . . . . 22
69	66, 5	sseqtri 3496	. . . . . . . . . . . . . . . . . . . . . . 23
70		1z 10968	. . . . . . . . . . . . . . . . . . . . . . . . 25
71	5	uzinf 12179	. . . . . . . . . . . . . . . . . . . . . . . . 25
72	70, 71	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24
73		ovolicc2.6	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
74		elin 3649	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
75	73, 74	sylib 199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
76	75	simprd 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
77		ssfi 7795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
78	76, 13, 77	sylancl 666	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
79	78	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
80	10	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
81		fveq2 5878	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
82	81	fveq2d 5882	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
83	82	fveq2d 5882	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
84		simpll 758	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
85		simprl 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
86		ral0 3902	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
87		simplr 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$
88	87	raleqdv 3031	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$
89	86, 88	mpbiri 236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
90	89	ralrimivw 2840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
91		rabid2 3006	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
92	90, 91	sylibr 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
93	85, 92	eleqtrd 2512	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
94		simprr 764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
95	94, 92	eleqtrd 2512	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
96		ovolicc.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
97		ovolicc.2	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
98		ovolicc.3	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
99		ovolicc2.4	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
100		ovolicc2.5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
101		ovolicc2.7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
102		ovolicc2.9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
103		ovolicc2.12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
104		ovolicc2.13	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
105	96, 97, 98, 99, 100, 73, 101, 4, 102, 11, 9, 103, 104, 8, 6, 64	ovolicc2lem3 22459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
106	84, 93, 95, 105	syl12anc 1262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
107	83, 106	syl5ibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
108	107	ralrimivva 2846	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
109		dff13 6171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
110	80, 108, 109	sylanbrc 668	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
111		f1domg 7593	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
112	79, 110, 111	sylc 62	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
113		domfi 7796	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
114	79, 112, 113	syl2anc 665	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
115	114	ex 435	. . . . . . . . . . . . . . . . . . . . . . . . 25
116	115	necon3bd 2636	. . . . . . . . . . . . . . . . . . . . . . . 24
117	72, 116	mpi 21	. . . . . . . . . . . . . . . . . . . . . . 23
118		infmssuzclOLD 11248	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
119	69, 117, 118	sylancr 667	. . . . . . . . . . . . . . . . . . . . . 22
120	68, 119	syl5eqel 2514	. . . . . . . . . . . . . . . . . . . . 21
121	67, 120	sseldi 3462	. . . . . . . . . . . . . . . . . . . 20
122	121	ad2antrr 730	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
123	67	sseli 3460	. . . . . . . . . . . . . . . . . . . 20
124	123	adantl 467	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
125		elfzle2 11804	. . . . . . . . . . . . . . . . . . . 20
126	125	ad2antlr 731	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
127		infmssuzleOLD 11247	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
128	69, 127	mpan 674	. . . . . . . . . . . . . . . . . . . . 21
129	68, 128	syl5eqbr 4454	. . . . . . . . . . . . . . . . . . . 20
130	129	adantl 467	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
131	63, 122, 124, 126, 130	letrd 9793	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
132	131	ralrimiva 2839	. . . . . . . . . . . . . . . . 17 $/\$
133	60, 132	ssrabdv 3540	. . . . . . . . . . . . . . . 16
134	133	adantr 466	. . . . . . . . . . . . . . 15 $/\$ $/\$
135		simprl 762	. . . . . . . . . . . . . . 15 $/\$ $/\$
136	134, 135	sseldd 3465	. . . . . . . . . . . . . 14 $/\$ $/\$
137		simprr 764	. . . . . . . . . . . . . . 15 $/\$ $/\$
138	134, 137	sseldd 3465	. . . . . . . . . . . . . 14 $/\$ $/\$
139	136, 138	jca 534	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
140	139, 105	syldan 472	. . . . . . . . . . . 12 $/\$ $/\$
141	59, 140	syl5ibr 224	. . . . . . . . . . 11 $/\$ $/\$
142	57, 141	sylbid 218	. . . . . . . . . 10 $/\$ $/\$
143	142	ralrimivva 2846	. . . . . . . . 9
144		dff13 6171	. . . . . . . . 9 $/\$
145	21, 143, 144	sylanbrc 668	. . . . . . . 8
146		f1f1orn 5839	. . . . . . . 8
147	145, 146	syl 17	. . . . . . 7
148		f1oeq3 5821	. . . . . . . 8
149	3, 148	ax-mp 5	. . . . . . 7
150	147, 149	sylibr 215	. . . . . 6
151		f1ofo 5835	. . . . . 6
152	150, 151	syl 17	. . . . 5
153		fofi 7863	. . . . 5 $/\$
154	43, 152, 153	syl2anc 665	. . . 4
155		fimaxre2 10553	. . . 4 $/\$
156	26, 154, 155	syl2anc 665	. . 3
157	42, 156	r19.29a 2970	. 2
158	97, 96	resubcld 10048	. . . . 5
159	158	rexrd 9691	. . . 4
160	159	adantr 466	. . 3 $/\$ $/\$
161		fzfid 12186	. . . . . 6
162		elfznn 11829	. . . . . . . . 9
163		eqid 2422	. . . . . . . . . . . 12
164	163	ovolfsf 22411	. . . . . . . . . . 11
165	100, 164	syl 17	. . . . . . . . . 10
166	165	ffvelrnda 6034	. . . . . . . . 9 $/\$
167	162, 166	sylan2 476	. . . . . . . 8 $/\$
168		elrege0 11739	. . . . . . . 8 $/\$
169	167, 168	sylib 199	. . . . . . 7 $/\$ $/\$
170	169	simpld 460	. . . . . 6 $/\$
171	161, 170	fsumrecl 13788	. . . . 5
172	171	adantr 466	. . . 4 $/\$ $/\$
173	172	rexrd 9691	. . 3 $/\$ $/\$
174	163, 99	ovolsf 22412	. . . . . . . . 9
175	100, 174	syl 17	. . . . . . . 8
176		frn 5749	. . . . . . . 8
177	175, 176	syl 17	. . . . . . 7
178		rge0ssre 11741	. . . . . . 7
179	177, 178	syl6ss 3476	. . . . . 6
180		ressxr 9685	. . . . . 6
181	179, 180	syl6ss 3476	. . . . 5
182		supxrcl 11601	. . . . 5
183	181, 182	syl 17	. . . 4
184	183	adantr 466	. . 3 $/\$ $/\$
185	158	adantr 466	. . . 4 $/\$ $/\$
186	24	sselda 3464	. . . . . . 7 $/\$
187	178, 166	sseldi 3462	. . . . . . 7 $/\$
188	186, 187	syldan 472	. . . . . 6 $/\$
189	154, 188	fsumrecl 13788	. . . . 5
190	189	adantr 466	. . . 4 $/\$ $/\$
191		inss2 3683	. . . . . . . . . . 11
192		fss 5751	. . . . . . . . . . 11 $/\$
193	100, 191, 192	sylancl 666	. . . . . . . . . 10
194	66, 120	sseldi 3462	. . . . . . . . . . . 12
195	15, 194	ffvelrnd 6035	. . . . . . . . . . 11
196	4, 195	ffvelrnd 6035	. . . . . . . . . 10
197	193, 196	ffvelrnd 6035	. . . . . . . . 9
198		xp2nd 6835	. . . . . . . . 9
199	197, 198	syl 17	. . . . . . . 8
200	13, 8	sseldi 3462	. . . . . . . . . . 11
201	4, 200	ffvelrnd 6035	. . . . . . . . . 10
202	193, 201	ffvelrnd 6035	. . . . . . . . 9
203		xp1st 6834	. . . . . . . . 9
204	202, 203	syl 17	. . . . . . . 8
205	199, 204	resubcld 10048	. . . . . . 7
206		fveq2 5878	. . . . . . . . . 10
207	187	recnd 9670	. . . . . . . . . . 11 $/\$
208	186, 207	syldan 472	. . . . . . . . . 10 $/\$
209	206, 43, 150, 48, 208	fsumf1o 13777	. . . . . . . . 9
210	100	adantr 466	. . . . . . . . . . 11 $/\$
211	4	adantr 466	. . . . . . . . . . . 12 $/\$
212		ffvelrn 6032	. . . . . . . . . . . . 13 $/\$
213	15, 18, 212	syl2an 479	. . . . . . . . . . . 12 $/\$
214	211, 213	ffvelrnd 6035	. . . . . . . . . . 11 $/\$
215	163	ovolfsval 22410	. . . . . . . . . . 11 $/\$
216	210, 214, 215	syl2anc 665	. . . . . . . . . 10 $/\$
217	216	sumeq2dv 13757	. . . . . . . . 9
218	193	adantr 466	. . . . . . . . . . . . . . 15 $/\$
219	4	adantr 466	. . . . . . . . . . . . . . . 16 $/\$
220	15	ffvelrnda 6034	. . . . . . . . . . . . . . . 16 $/\$
221	219, 220	ffvelrnd 6035	. . . . . . . . . . . . . . 15 $/\$
222	218, 221	ffvelrnd 6035	. . . . . . . . . . . . . 14 $/\$
223		xp2nd 6835	. . . . . . . . . . . . . 14
224	222, 223	syl 17	. . . . . . . . . . . . 13 $/\$
225	18, 224	sylan2 476	. . . . . . . . . . . 12 $/\$
226	225	recnd 9670	. . . . . . . . . . 11 $/\$
227	193	adantr 466	. . . . . . . . . . . . . 14 $/\$
228	227, 214	ffvelrnd 6035	. . . . . . . . . . . . 13 $/\$
229		xp1st 6834	. . . . . . . . . . . . 13
230	228, 229	syl 17	. . . . . . . . . . . 12 $/\$
231	230	recnd 9670	. . . . . . . . . . 11 $/\$
232	43, 226, 231	fsumsub 13837	. . . . . . . . . 10
233	69, 120	sseldi 3462	. . . . . . . . . . . . 13
234		fveq2 5878	. . . . . . . . . . . . . . . 16
235	234	fveq2d 5882	. . . . . . . . . . . . . . 15
236	235	fveq2d 5882	. . . . . . . . . . . . . 14
237	236	fveq2d 5882	. . . . . . . . . . . . 13
238	233, 226, 237	fsumm1 13800	. . . . . . . . . . . 12
239		fzfid 12186	. . . . . . . . . . . . . . 15
240		elfznn 11829	. . . . . . . . . . . . . . . 16
241	240, 224	sylan2 476	. . . . . . . . . . . . . . 15 $/\$
242	239, 241	fsumrecl 13788	. . . . . . . . . . . . . 14
243	242	recnd 9670	. . . . . . . . . . . . 13
244	199	recnd 9670	. . . . . . . . . . . . 13
245	243, 244	addcomd 9836	. . . . . . . . . . . 12
246	238, 245	eqtrd 2463	. . . . . . . . . . 11
247		fveq2 5878	. . . . . . . . . . . . . . . 16
248	247	fveq2d 5882	. . . . . . . . . . . . . . 15
249	248	fveq2d 5882	. . . . . . . . . . . . . 14
250	249	fveq2d 5882	. . . . . . . . . . . . 13
251	233, 231, 250	fsum1p 13802	. . . . . . . . . . . 12
252	5, 6, 7, 8	algr0 14519	. . . . . . . . . . . . . . . 16
253	252	fveq2d 5882	. . . . . . . . . . . . . . 15
254	253	fveq2d 5882	. . . . . . . . . . . . . 14
255	254	fveq2d 5882	. . . . . . . . . . . . 13
256	7	peano2zd 11044	. . . . . . . . . . . . . . 15
257	194	nnzd 11040	. . . . . . . . . . . . . . 15
258		fzp1ss 11848	. . . . . . . . . . . . . . . . . 18
259	70, 258	mp1i 13	. . . . . . . . . . . . . . . . 17
260	259	sselda 3464	. . . . . . . . . . . . . . . 16 $/\$
261	260, 231	syldan 472	. . . . . . . . . . . . . . 15 $/\$
262		fveq2 5878	. . . . . . . . . . . . . . . . . 18
263	262	fveq2d 5882	. . . . . . . . . . . . . . . . 17
264	263	fveq2d 5882	. . . . . . . . . . . . . . . 16
265	264	fveq2d 5882	. . . . . . . . . . . . . . 15
266	7, 256, 257, 261, 265	fsumshftm 13830	. . . . . . . . . . . . . 14
267		ax-1cn 9598	. . . . . . . . . . . . . . . . . 18
268	267, 267	pncan3oi 9892	. . . . . . . . . . . . . . . . 17
269	268	oveq1i 6312	. . . . . . . . . . . . . . . 16
270	269	sumeq1i 13752	. . . . . . . . . . . . . . 15
271		oveq1 6309	. . . . . . . . . . . . . . . . . . . 20
272	271	fveq2d 5882	. . . . . . . . . . . . . . . . . . 19
273	272	fveq2d 5882	. . . . . . . . . . . . . . . . . 18
274	273	fveq2d 5882	. . . . . . . . . . . . . . . . 17
275	274	fveq2d 5882	. . . . . . . . . . . . . . . 16
276	275	cbvsumv 13750	. . . . . . . . . . . . . . 15
277	270, 276	eqtri 2451	. . . . . . . . . . . . . 14
278	266, 277	syl6eq 2479	. . . . . . . . . . . . 13
279	255, 278	oveq12d 6320	. . . . . . . . . . . 12
280	251, 279	eqtrd 2463	. . . . . . . . . . 11
281	246, 280	oveq12d 6320	. . . . . . . . . 10
282	204	recnd 9670	. . . . . . . . . . 11
283		peano2nn 10622	. . . . . . . . . . . . . . . . . 18
284		ffvelrn 6032	. . . . . . . . . . . . . . . . . 18 $/\$
285	15, 283, 284	syl2an 479	. . . . . . . . . . . . . . . . 17 $/\$
286	219, 285	ffvelrnd 6035	. . . . . . . . . . . . . . . 16 $/\$
287	218, 286	ffvelrnd 6035	. . . . . . . . . . . . . . 15 $/\$
288		xp1st 6834	. . . . . . . . . . . . . . 15
289	287, 288	syl 17	. . . . . . . . . . . . . 14 $/\$
290	240, 289	sylan2 476	. . . . . . . . . . . . 13 $/\$
291	239, 290	fsumrecl 13788	. . . . . . . . . . . 12
292	291	recnd 9670	. . . . . . . . . . 11
293	244, 243, 282, 292	addsub4d 10034	. . . . . . . . . 10
294	232, 281, 293	3eqtrd 2467	. . . . . . . . 9
295	209, 217, 294	3eqtrd 2467	. . . . . . . 8
296	295, 189	eqeltrrd 2511	. . . . . . 7
297		fveq2 5878	. . . . . . . . . . . . . . 15
298	297	eleq2d 2492	. . . . . . . . . . . . . 14
299	298, 64	elrab2 3231	. . . . . . . . . . . . 13 $/\$
300	120, 299	sylib 199	. . . . . . . . . . . 12 $/\$
301	300	simprd 464	. . . . . . . . . . 11
302	96, 97, 98, 99, 100, 73, 101, 4, 102	ovolicc2lem1 22457	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
303	195, 302	mpdan 672	. . . . . . . . . . 11 $/\$ $/\$
304	301, 303	mpbid 213	. . . . . . . . . 10 $/\$ $/\$
305	304	simp3d 1019	. . . . . . . . 9
306	96, 97, 98, 99, 100, 73, 101, 4, 102	ovolicc2lem1 22457	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
307	200, 306	mpdan 672	. . . . . . . . . . 11 $/\$ $/\$
308	104, 307	mpbid 213	. . . . . . . . . 10 $/\$ $/\$
309	308	simp2d 1018	. . . . . . . . 9
310	97, 204, 199, 96, 305, 309	lt2subd 10238	. . . . . . . 8
311	158, 205, 310	ltled 9784	. . . . . . 7
312	240	adantl 467	. . . . . . . . . . . . . . . . . 18 $/\$
313		simpr 462	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
314	257	adantr 466	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
315		elfzm11 11866	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
316	70, 314, 315	sylancr 667	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
317	313, 316	mpbid 213	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
318	317	simp3d 1019	. . . . . . . . . . . . . . . . . . . 20 $/\$
319	312	nnred 10625	. . . . . . . . . . . . . . . . . . . . 21 $/\$
320	121	adantr 466	. . . . . . . . . . . . . . . . . . . . 21 $/\$
321	319, 320	ltnled 9783	. . . . . . . . . . . . . . . . . . . 20 $/\$
322	318, 321	mpbid 213	. . . . . . . . . . . . . . . . . . 19 $/\$
323		infmssuzleOLD 11247	. . . . . . . . . . . . . . . . . . . . 21 $/\$
324	69, 323	mpan 674	. . . . . . . . . . . . . . . . . . . 20
325	68, 324	syl5eqbr 4454	. . . . . . . . . . . . . . . . . . 19
326	322, 325	nsyl 124	. . . . . . . . . . . . . . . . . 18 $/\$
327	312, 326	jca 534	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
328	96, 97, 98, 99, 100, 73, 101, 4, 102, 11, 9, 103, 104, 8, 6, 64	ovolicc2lem2 22458	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
329	327, 328	syldan 472	. . . . . . . . . . . . . . . 16 $/\$
330	329	iftrued 3917	. . . . . . . . . . . . . . 15 $/\$
331		ffvelrn 6032	. . . . . . . . . . . . . . . . 17 $/\$
332	10, 240, 331	syl2an 479	. . . . . . . . . . . . . . . 16 $/\$
333	103	ralrimiva 2839	. . . . . . . . . . . . . . . . 17
334	333	adantr 466	. . . . . . . . . . . . . . . 16 $/\$
335		fveq2 5878	. . . . . . . . . . . . . . . . . . . . . 22
336	335	fveq2d 5882	. . . . . . . . . . . . . . . . . . . . 21
337	336	fveq2d 5882	. . . . . . . . . . . . . . . . . . . 20
338	337	breq1d 4430	. . . . . . . . . . . . . . . . . . 19
339	338, 337	ifbieq1d 3932	. . . . . . . . . . . . . . . . . 18
340		fveq2 5878	. . . . . . . . . . . . . . . . . 18
341	339, 340	eleq12d 2504	. . . . . . . . . . . . . . . . 17
342	341	rspcv 3178	. . . . . . . . . . . . . . . 16
343	332, 334, 342	sylc 62	. . . . . . . . . . . . . . 15 $/\$
344	330, 343	eqeltrrd 2511	. . . . . . . . . . . . . 14 $/\$
345	5, 6, 7, 8, 9	algrp1 14521	. . . . . . . . . . . . . . 15 $/\$
346	240, 345	sylan2 476	. . . . . . . . . . . . . 14 $/\$
347	344, 346	eleqtrrd 2513	. . . . . . . . . . . . 13 $/\$
348	240, 285	sylan2 476	. . . . . . . . . . . . . 14 $/\$
349	96, 97, 98, 99, 100, 73, 101, 4, 102	ovolicc2lem1 22457	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
350	348, 349	syldan 472	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
351	347, 350	mpbid 213	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
352	351	simp2d 1018	. . . . . . . . . . 11 $/\$
353	290, 241, 352	ltled 9784	. . . . . . . . . 10 $/\$
354	239, 290, 241, 353	fsumle 13847	. . . . . . . . 9
355	242, 291	subge0d 10204	. . . . . . . . 9
356	354, 355	mpbird 235	. . . . . . . 8
357	242, 291	resubcld 10048	. . . . . . . . 9
358	205, 357	addge01d 10202	. . . . . . . 8
359	356, 358	mpbid 213	. . . . . . 7
360	158, 205, 296, 311, 359	letrd 9793	. . . . . 6
361	360, 295	breqtrrd 4447	. . . . 5
362	361	adantr 466	. . . 4 $/\$ $/\$
363		fzfid 12186	. . . . 5 $/\$ $/\$
364	170	adantlr 719	. . . . 5 $/\$ $/\$ $/\$
365	169	simprd 464	. . . . . 6 $/\$
366	365	adantlr 719	. . . . 5 $/\$ $/\$ $/\$
367	24	adantr 466	. . . . . . . . . . . 12 $/\$
368	367	sselda 3464	. . . . . . . . . . 11 $/\$ $/\$
369	368	nnred 10625	. . . . . . . . . 10 $/\$ $/\$
370	31	ad2antlr 731	. . . . . . . . . 10 $/\$ $/\$
371		ltle 9723	. . . . . . . . . 10 $/\$
372	369, 370, 371	syl2anc 665	. . . . . . . . 9 $/\$ $/\$
373	368, 5	syl6eleq 2520	. . . . . . . . . 10 $/\$ $/\$
374		nnz 10960	. . . . . . . . . . 11
375	374	ad2antlr 731	. . . . . . . . . 10 $/\$ $/\$
376		elfz5 11793	. . . . . . . . . 10 $/\$
377	373, 375, 376	syl2anc 665	. . . . . . . . 9 $/\$ $/\$
378	372, 377	sylibrd 237	. . . . . . . 8 $/\$ $/\$
379	378	ralimdva 2833	. . . . . . 7 $/\$
380	379	impr 623	. . . . . 6 $/\$ $/\$
381		dfss3 3454	. . . . . 6
382	380, 381	sylibr 215	. . . . 5 $/\$ $/\$
383	363, 364, 366, 382	fsumless 13844	. . . 4 $/\$ $/\$
384	185, 190, 172, 362, 383	letrd 9793	. . 3 $/\$ $/\$
385		eqidd 2423	. . . . . 6 $/\$ $/\$ $/\$
386		simprl 762	. . . . . . 7 $/\$ $/\$
387	386, 5	syl6eleq 2520	. . . . . 6 $/\$ $/\$
388	364	recnd 9670	. . . . . 6 $/\$ $/\$ $/\$
389	385, 387, 388	fsumser 13784	. . . . 5 $/\$ $/\$
390	99	fveq1i 5879	. . . . 5
391	389, 390	syl6eqr 2481	. . . 4 $/\$ $/\$
392	181	adantr 466	. . . . 5 $/\$ $/\$
393		ffn 5743	. . . . . . . 8
394	175, 393	syl 17	. . . . . . 7
395	394	adantr 466	. . . . . 6 $/\$ $/\$
396		fnfvelrn 6031	. . . . . 6 $/\$
397	395, 386, 396	syl2anc 665	. . . . 5 $/\$ $/\$
398		supxrub 11611	. . . . 5 $/\$
399	392, 397, 398	syl2anc 665	. . . 4 $/\$ $/\$
400	391, 399	eqbrtrd 4441	. . 3 $/\$ $/\$
401	160, 173, 184, 384, 400	xrletrd 11460	. 2 $/\$ $/\$
402	157, 401	rexlimddv 2921	1